Jason (jcreed) wrote,

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: math

  • (no subject)

    I think I got around the need for corecursion by just using One More Linear Token: defining ◇A = ∃x.z(x) ⊗ □!(z(x) ⊸ ∀a.q(a) ⊸ ∃b.q(b) ⊗ □!(ℓ(a) ⊸…

  • (no subject)

    Thought some more about what happens when you take positive props P ::= ↓G | P ⊕ P | 0 negative props N ::= ↑G | N & N | ⊤ games G ::= {N|P}…

  • (no subject)

    Dang. Stuff from yesterday led down a path that made me think I had a very tidy answer to the age-old question of "read-only…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded