Jason (jcreed) wrote,

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:


Γ |- 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


λ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)

    Something that's bugged me for a long time is this: How many paths, starting at the origin, taking N steps either up, down, left or right, end up at…

  • (no subject)

    Still sad that SAC seems to end up being as complicated as it is. Surely there's some deeper duality between…

  • (no subject)

    I had already been meaning to dig into JaneSt's "Incremental" library, which bills itself as a practical implementation (in ocaml) of the ideas in…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded