I think that maybe the type of linear lambda terms whose grammar is augmented with a term constructor of domain type x "is" the solution of the differential equation

Λlin = Λlin2 + Λ'lin + x

It doesn't seem to have a nice closed form. However, I can compute its Taylor coefficients! Not at all sure what that gets me.
```In[10]:= c = Array[0&,30]

Out[10]= {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,

>    0, 0, 0, 0, 0, 0, 0, 0}

In[11]:= Do[c[[x + 1]] = If[x == 0, 1, (c[[x]] - If[x == 2,1,0] - Sum[c[[i + 1]] * c[[x - i]], {i,0,x-1}]) / x],{x,0,29}]

In[12]:= Array[#!&,30] * c

Out[12]= {1, 0, -3, 4, -5, -30, 175, -600, -585, 19550, -140965, 349980,

>    3553355, -56853510, 365024775, 129889360, -33436442945, 415006625430,

>    -2006636383085, -21634372362300, 591392458678035, -6117377621205070,

>    5173447106557055, 984697205650139640, -18568584471358701625,

>    140968537139160162510, 1428362332773821249355, -62459127723700470787220,

>    923992442083031620141915, -2504836086812441855308950}

```
Tags:
• #### (no subject)

Playing around with the agda javascript backend, now. Like, my ears are popping from the sudden change of type-theory-pressure.

• #### (no subject)

Trying to understand in general what kind of diagrammatic interactions between degree-three nodes actually read sensibly in the lambda calculus:

• #### (no subject)

Not sure this is the simplest possible inverse (or even that it is correct) but it makes for a fun diagram:

• Post a new comment

#### Error

Anonymous comments are disabled in this journal

default userpic