And for anyone that followed that last post, consider the following:

α list = 1 + α + α2 + ...

right? So morally

α list = 1 / (1 - α)

by "solving the geometric series". However, unless I did my algebra wrong, it seems that setting f(x) = 1 / (1 - x) has the property that

f(f(f(x))) = x

which, at one in the morning, seems mysterious and significant to me. This function does a three-card monte among the intervals (1, ∞), (-&infin,0), and (0,1).

So is there any interesting connection at all between the types α and α list list list? It seems to me there cannot be a natural (either in the informal or categorical sense) isomorphism, but who knows.

A cute trick that actually works involves solving for an immediate fixed point of the function f. You get

x = 1 / (1 - x)
(1 - x) x = 1
x = 1 + x2

the characteristic type equation of binary trees, et voila, indeed the type of binary trees is elegantly isomorphic to the type of lists of binary trees. Witness LISP's representation of trees with cons cells! I'm nearly certain I've seen this before, but it's fun to work through it again and find it for myself.

Oh! I just had a realization. The paper revealed that eX was multisets (aka "bags") over the type X, and I just realized that cosh X and sinh X ought to be multisets over X with, respectively, an even and odd number of elements.
Tags:
• #### (no subject)

Didn't sleep well. Long day of work. Dinner with akiva at hanamichi.

• #### (no subject)

K was going to do a thing for her dad's birthday, but scheduling kept slipping and slipping so I guess we're going to try doing it tomorrow instead.

• #### (no subject)

Had a pleasant lunch with paul and gabe back from working-at-facebook times. Discussed the important issues of the day, by which I mean video games…

• #### Error

Anonymous comments are disabled in this journal

default userpic