I think I've explained λ and application in Parigot's λμ-calculus in terms of more basic things. I really can't come up with sensible names for these new proof term constructors, but:

```if

Γ |- M : A => B false    Γ, x : A false |- N : B true
----------------------------------------------------------
Γ |- send M := (x.N) : C

Γ |- N : A true    Γ, x : B false |- M : .
----------------------------------------------------------
Γ |- apply x = N in M : A => B false

Γ, x : A false |- M : .
-----------------------------
Γ |- μx.M : A true

Γ |- M : A true     Γ |- N : A false
-----------------------------
Γ |- M <--A-- N : C

then

λx.M is really μz.(send z := (x.M))
M N is really μz.(M <--(A=>B)-- (apply w = N in w <--B-- z))

the ordinary β-reduction of λ against application is then imitated by one η and two β
reductions of μ against <----, one β of send against apply.
```

Man, is it 2 already? I'm just β-reducing the night away.
• #### (no subject)

A paper on describing circuits in an agda DSL: http://www.staff.science.uu.nl/~swier004/publications/2015-types-draft.pdf

• #### (no subject)

Going more carefully now through this little tutorial on fpga programming with the iCEstick. It's in spanish, which makes it slightly more…

• #### (no subject)

Some further progress cleaning up the https://xkcd.com/1360/ -esque augean stables that is my hard drive. Tomato chicken I made a couple days ago…

• #### Error

Anonymous comments are disabled in this journal

default userpic