gistfile1.txt

Left rules are funky: they don't apply to the connective variable as an argument,
instead they introduce syntax that has the variable as an index. You get a kind
of continuation syntax rather than an applicative syntax.





----------------- ID
G, x : A => x : A


let x = M in x  ~>  M




----------- 1R
G => <> : 1

no 1L




no 0R

-------------------------- 0L
G, x : 0 => abort[x]() : C




G => M : A   G => N : B
----------------------- *R
   G => <M,N> : A*B

G, p : A*B, x : A, y : B => M : C
--------------------------------- *L
G, p : A*B => split[p](x,y.M) : C


let p = <M,N> in split[p](x,y.P)  ~>  let x = M, y = N, p = <M,N> in P





   G => M : A
----------------- +R1
G => inl(M) : A+B

   G => N : B
----------------- +R2
G => inr(N) : A+B

G, d : A+B, x : A => M : C   G, d : A+B, y : B => N : C
------------------------------------------------------- +L
          G, d : A+B => case[d](x.M ; y.N)


let d = inl(M) in case[d](x.P ; y.Q)  ~>  let x = M, d = inl(M) in P
let d = inr(N) in case[d](x.P ; y.Q)  ~>  let y = N, d = inr(N) in Q




G, x : A => M : B
------------------ ->R
G => \x.M : A -> B

G, f : A -> B => M : A         G, f : A -> B, y : B => N : C
------------------------------------------------------------ ->L
          G, f : A -> B => app[f](M ; y.N) : C


let f = \x.M in app[f](N ; y.P)  ~>  let y = (let x = N in M), f = \x.M in P





let x = M in N  ~>  N   (when x does not occur in N)





--   (\x.x) M

     let f = \x.x in app[f](M ; y.y)
~>   let y = (let x = M in x), f = \x.x in y
~>   let y = (let x = M in x) in y
~>   let x = M in x
~>   M



--   (\p. fst(p)) <M,N>

     let f = \p. fst[p](x.x) in app[f](<M,N> ; x'.x')
~>   let x' = (let p = <M,N> in fst[p](x.x)), f = \p. fst[p](x.x) in x'
~>   let x' = (let p = <M,N> in fst[p](x.x)) in x'
~>   let p = <M,N>, x' = (let p = <M,N> in fst[p](x.x)) in fst[p](x.x)
~>   let p = <M,N> in fst[p](x.x)
~>   let x = M, p = <M,N> in x
~>   let x = M in x
~>   M



Some sugar:

FST(P)                =   let p = P in fst[p](x.x)
SND(P)                =   let p = P in snd[p](y.y)
CASE(D ; x.M ; y.N)   =   let d = D in case[d](x.M ; y.N)
APP(M ; N)            =   let f = M in app[f](N ; z.z)