Jason (jcreed) wrote,
Jason
jcreed

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.
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 3 comments