# Computation and Deduction 2009/20090408

 This is Literate TwelfCode: hereStatus: %% OK %% Output: here.

Code from class, April 8.

```tp : type.  %name tp A.

tensor : tp -> tp -> tp.
1 : tp.
with : tp -> tp -> tp.
top : tp.
plus : tp -> tp -> tp.
0 : tp.
lolli : tp -> tp -> tp.
! : tp -> tp.

exp : type.  %name exp M x.

tens : exp -> exp -> exp.
lett : exp -> (exp -> exp -> exp) -> exp.
pair : exp -> exp -> exp.
pi1  : exp -> exp.
pi2  : exp -> exp.
star : exp.
lets : exp -> exp -> exp.
unit : exp.
in1  : exp -> exp.
in2  : exp -> exp.
case : exp -> (exp -> exp) -> (exp -> exp) -> exp.
abort : exp -> exp.
lam : tp -> (exp -> exp) -> exp.
app : exp -> exp -> exp.
bang : exp -> exp.
letb : exp -> (exp -> exp) -> exp.

linear : (exp -> exp) -> type.
of : exp -> tp -> type.

linear/var : linear ([x] x).

linear/tens1 : linear ([x] tens (M x) N)
<- linear ([x] M x).

linear/tens2 : linear ([x] tens M (N x))
<- linear ([x] N x).

of/tens : of (tens M N) (tensor A B)
<- of M A
<- of N B.

linear/lett1 : linear ([z] lett (M z) ([x] [y] N x y))
<- linear ([x] M x).

linear/lett2 : linear ([z] lett M ([x] [y] N z x y))
<- ({x} {y} linear ([z] N z x y)).

of/lett : of (lett M ([x] [y] N x y)) C
<- of M (tensor A B)
<- ({x:exp} of x A -> {y:exp} of y B -> of (N x y) C)
<- ({y:exp} linear ([x] N x y))
<- ({x:exp} linear ([y] N x y)).

linear/pair : linear ([x] pair (M x) (N x))
<- linear ([x] M x)
<- linear ([x] N x).

of/pair : of (pair M N) (with A B)
<- of M A
<- of N B.

linear/pi1 : linear ([x] pi1 (M x))
<- linear ([x] M x).

linear/pi2 : linear ([x] pi2 (M x))
<- linear ([x] M x).

of/pi1 : of (pi1 M) A
<- of M (with A B).

of/pi2 : of (pi1 M) B
<- of M (with A B).

of/star : of star 1.

linear/lets1 : linear ([x] lets (M x) N)
<- linear ([x] M x).

linear/lets2 : linear ([x] lets M (N x))
<- linear ([x] N x).

of/lets : of (lets M N) C
<- of M 1
<- of N C.

linear/unit : linear ([x] unit).

of/unit : of unit top.

linear/in1 : linear ([x] in1 (M x))
<- linear ([x] M x).

linear/in2 : linear ([x] in2 (M x))
<- linear ([x] M x).

of/in1 : of (in1 M) (plus A B)
<- of M A.

of/in2 : of (in2 M) (plus A B)
<- of M B.

linear/case1 : linear ([z] case (M z) ([x] N x) ([x] O x))
<- linear ([z] M z).

linear/case2 : linear ([z] case M ([x] N z x) ([x] O z x))
<- ({x:exp} linear ([z] N z x))
<- ({x:exp} linear ([z] O z x)).

of/case : of (case M ([x] N x) ([x] O x)) C
<- of M (plus A B)
<- ({x} of x A -> of (N x) C)
<- ({x} of x B -> of (O x)C)
<- linear ([x] N x)
<- linear ([x] O x).

linear/abort1 : linear ([x] abort (M x))
<- linear ([x] M x).

linear/abort2 : linear ([x] abort M).

of/abort : of (abort M) C
<- of M O.

linear/lam : linear ([x] (lam A ([y] (M x y))))
<- {y:exp} linear ([x] M x y).

of/lam : of (lam A ([x] M x)) (lolli A B)
<- ({x} (of x A) -> of (M x) B)
<- linear ([x] M x).

linear/app1 : linear ([x] (app (M x) N))
<- linear ([x] M x).

linear/app2 : linear ([x] (app M (N x)))
<- linear ([x] N x).

of/app : of (app M N) B
<- of M (lolli A B)
<- of N A.

of/bang : of (bang M) (! A)
<- of M A.

linear/letb1 : linear ([x] (letb (M x) ([y] (N y))))
<- linear ([x] M x).

linear/letb2 : linear ([x] (letb M ([y] N x y)))
<- ({y} linear ([x] N x y)).

of/letb : of (letb M ([x] N x)) C
<- of M (! A)
<- ({x} (of x A) -> of (N x) C).

reduce : exp -> exp -> type.

reduce/lam : reduce (lam A ([x] M x)) (lam A ([x] N x))
<- ({x} reduce (M x) (N x)).

reduce/app1 : reduce (app M N) (app M' N)
<- reduce M M'.

reduce/app2 : reduce (app M N) (app M N')
<- reduce N N'.

reduce/beta : reduce (app (lam A ([x] M x)) N) (M N).

%block block : block {x:exp}.
%block bind : some {A:tp} block {x:exp} {d : of x A}.

exp-eq : exp -> exp -> type.
exp-eq/i : exp-eq M M.

exp-compat: {M : exp -> exp} exp-eq N N' -> exp-eq (M N) (M N') -> type.
%mode exp-compat +I +I1 -O.

- : exp-compat M _ exp-eq/i.

%worlds (block) (exp-compat _ _ _).
%total {} (exp-compat _ _ _).

lam-compat: ({x:exp} exp-eq (N x) (N' x)) -> exp-eq (lam A N) (lam A N') -> type.
%mode +{N:exp -> exp} +{N':exp -> exp} +{A:tp} +{D1:{x:exp} exp-eq (N x) (N' x)}
-{D2:exp-eq (lam A ([x:exp] N x)) (lam A ([x:exp] N' x))} (lam-compat D1 D2).

-: lam-compat ([x] exp-eq/i) exp-eq/i.

%worlds (block) (lam-compat _ _).
%total {} (lam-compat _ _).

linear-resp: ({x:exp} exp-eq (M x) (N x) ) -> linear M -> linear N -> type.
%mode linear-resp +I +I2 -O.

-: linear-resp _ D D.

%worlds (block) (linear-resp _ _ _).
%total {} (linear-resp _ _ _).

reduce-closed : ({x:exp} reduce M (N x)) -> ({x:exp} exp-eq N' (N x) ) -> type.
%mode reduce-closed +D -D'.

-: reduce-closed ([x] reduce/app1 (Dreduce x : reduce M1 (N1 x)) ) Deq'
<- reduce-closed Dreduce (Deq : {x} exp-eq N1' (N1 x))
<- ({x} exp-compat ([y] app y M2) (Deq x) (Deq' x : exp-eq (app N1' M2) (app (N1 x) M2))).

-: reduce-closed ([x] reduce/app2 (Dreduce x :reduce M2 (N2 x))) Deq'
<- reduce-closed Dreduce (Deq : {x} exp-eq N2' (N2 x))
<- ({x} exp-compat ([y] app M1 y) (Deq x) (Deq' x : exp-eq (app M1 N2') (app M1 (N2 x)))).

-: reduce-closed ([x] reduce/lam (Dreduce x : {y} reduce (M y) (N x y))) Deq'
<- ({y} reduce-closed ([x] Dreduce x y) ([x] Deq x y: exp-eq (N' y) (N x y)))
<- ({x} lam-compat ([y] Deq x y) (Deq' x : exp-eq (lam A ([y] (N' y))) (lam A ([y] (N x y))))).

-: reduce-closed ([x] reduce/beta : reduce (app (lam A ([y] M y)) N) (M N)) ([x] exp-eq/i).

%worlds (block) (reduce-closed _ _).
%total D (reduce-closed D _).

linear-compose: linear ([x] M x) -> linear ([y] N y) -> linear ([y] M (N y)) -> type.
%mode linear-compose +I +I1 -O.

-: linear-compose linear/var D D.

-: linear-compose linear/unit _ linear/unit.

-: linear-compose (linear/app1 (D1 :linear ([x] M1 x)) ) (D2:linear ([y] N y))
(linear/app1 D)
<- linear-compose D1 D2 (D: linear ([y] M1 (N y))).

-: linear-compose (linear/app2 (D1 :linear ([x] M1 x)) ) (D2 : linear ([y] N y))
(linear/app2 D)
<- linear-compose D1 D2 D.
-: linear-compose (linear/tens1 (D1 : linear ([x] M1 x)))
(D2 : linear ([y] N y))
(linear/tens1 D)
<- linear-compose D1 D2 D.
-: linear-compose (linear/tens2 (D1 : linear ([x] M1 x)))
(D2 : linear ([y] N y))
(linear/tens2 D)
<- linear-compose D1 D2 D.
-: linear-compose (linear/lett1 (D1 : linear ([x] M1 x)))
(D2 : linear ([y] N y))
(linear/lett1 D)
<- linear-compose D1 D2 D.
-: linear-compose (linear/lett2 (D1 : {x} {y} linear ([z] M1 x y z)))
(D2 : linear ([k] N k))
(linear/lett2 D )
<- ({x} {y} linear-compose (D1 x y) D2 (D x y)).

-: linear-compose (linear/pair (X1 : linear ([x] M1 x)) (X2 : linear ([y] M2 y)))
D1
(linear/pair A B)
<- linear-compose X1 D1 A
<- linear-compose X2 D1 B.
-: linear-compose (linear/pi1 (D1 : linear ([x] M1 x)))
D2
(linear/pi1 D)
<- linear-compose D1 D2 D.
-: linear-compose (linear/pi2 (D1 : linear ([x] M1 x)))
D2
(linear/pi2 D)
<- linear-compose D1 D2 D.
-: linear-compose (linear/lets1 (D1 : linear ([x] M1 x)))
D2
(linear/lets1 D)
<- linear-compose D1 D2 D.
-: linear-compose (linear/lets2 (D1 : linear ([x] M1 x)))
D2
(linear/lets2 D)
<- linear-compose D1 D2 D.
-: linear-compose (linear/in1 (D1 : linear ([x] M1 x)))
D2
(linear/in1 D)
<- linear-compose D1 D2 D.
-: linear-compose (linear/in2 (D1 : linear ([x] M1 x)))
D2
(linear/in2 D)
<- linear-compose D1 D2 D.
-: linear-compose (linear/case1 (D1 : linear ([x] M1 x)))
D2
(linear/case1 D)
<- linear-compose D1 D2 D.

-: linear-compose (linear/case2 ([x] D1 x) ([x] D2 x)) D3 (linear/case2 D4 D5)
<- ({x} linear-compose (D1 x) D3 (D4 x))
<- ({x} linear-compose (D2 x) D3 (D5 x)).

-: linear-compose (linear/abort1 (D1 : linear ([x] M1 x)))
D2
(linear/abort1 D)
<- linear-compose D1 D2 D.

-: linear-compose (linear/abort2) _ linear/abort2.

-: linear-compose (linear/lam ([y] X1 y)) X2 (linear/lam D)
<- ({x} linear-compose (X1 x) X2 (D x)).

-: linear-compose (linear/letb1 (D1 : linear ([x] M1 x)))
D2
(linear/letb1 D)
<- linear-compose D1 D2 D.
-: linear-compose (linear/letb2 ([y] X1 y)) X2 (linear/letb2 D)
<- ({x} linear-compose (X1 x) X2 (D x)).

%worlds (block) (linear-compose _ _ _).
%total (R) (linear-compose R _ _).

srl : ({x} (of x A) -> of (M x) B) -> linear ([x] M x) -> ({x} reduce (M x) (M' x)) -> linear ([x] M' x) -> type.
%mode srl +D1 +D2 +D3 -D4.

- : srl
([x] [d:of x A] of/lam (DDD x) (Dof x d : {y} of y B -> of (M x y) C))
(linear/lam (Dlinear : {y} linear ([x] M x y)))
([x] reduce/lam (Dreduce x : {y} reduce (M x y) (N x y)))
(linear/lam ([y] Dlinear' y))
<- ({y} {dy:of y B} srl ([x] [dx:of x A] Dof x dx y dy) (Dlinear y) ([x] Dreduce x y)
(Dlinear' y : linear ([x] N x y))).

- : srl
([x] [d:of x A] of/app _ (Dof x d : of (M x) (lolli B C)))
(linear/app1 (Dlinear : linear ([x] M x)))
([x] reduce/app1 (Dreduce x : reduce (M x) (M' x)))
(linear/app1 Dlinear')
<- srl Dof Dlinear Dreduce (Dlinear' : linear ([x] M' x)).

- : srl
_
(linear/app2 (Dlinear : linear ([x] N x)))
([x] reduce/app1 (Dreduce x : reduce M (M' x)))
Dlinear'
<- reduce-closed Dreduce (Deq: {x} exp-eq  M'' (M' x)  )
<- ({x} exp-compat ([z] app z (N x)) (Deq x) (Deq' x : exp-eq (app M'' (N x) ) (app (M' x) (N x))))
<- linear-resp Deq' (linear/app2 Dlinear) (Dlinear' : linear ([x] app (M' x) (N x))).

- : srl
_
(linear/app1 (linear/lam (Dlinear:{y} linear ([x] M x y))))
([x] reduce/beta)
(Dlinear _).

-: srl
([x][d:of x A] of/app _ (of/lam (Dlinear' x : linear ([y] M y)) _ ))
(linear/app2 (Dlinear : linear ([x] N x) ))
([x] reduce/beta)
Dlinear''
<- linear-compose (Dlinear' unit) Dlinear (Dlinear'' : linear ([x] M (N x))).

-: srl
([x] [d : of x A] of/app (Dof x d : of (N x) B) _)
(linear/app2 (Dlinear : linear ([x] N x)))
([x] reduce/app2 (Dreduce x : reduce (N x) (N' x)))
(linear/app2 Dlinear')
<- srl Dof Dlinear Dreduce (Dlinear' : linear ([x] N' x)).

-: srl
_
(linear/app1 (Dlinear : linear ([x] M x)))
([x] reduce/app2 (Dreduce x : reduce N (N' x)))
Dlinear'
<- reduce-closed Dreduce (Deq : {x} exp-eq N'' (N' x))
<- ({x} exp-compat ([z] app (M x) z) (Deq x) (Deq' x : exp-eq (app (M x) N'') (app (M x) (N' x))))
<- linear-resp Deq' (linear/app1 Dlinear) (Dlinear' : linear ([x] app (M x) (N' x))).

%worlds (bind) (srl _ _ _ _).
%total D (srl _ _ D _).

sr : of M A -> reduce M M' -> of M' A -> type.
%mode sr +D1 +D2 -D3.

- : sr
(of/app (DofN : of N A) (DofM : of M (lolli A B)))
(reduce/app1 (Dreduce : reduce M M'))
(of/app DofN DofM')
<- sr DofM Dreduce (DofM' : of M' (lolli A B)).

- : sr
(of/app (DofN : of N A) (DofM : of M (lolli A B)))
(reduce/app2 (Dreduce : reduce N N'))
(of/app DofN' DofM)
<- sr DofN Dreduce (DofN' : of N' A).

- : sr
(of/app (DofN : of N A) (of/lam _ (DofM : {x} (of x A) -> of (M x) B)))
reduce/beta
(DofM N DofN).

- : sr
(of/lam
(Dlinear : linear ([x] M x))
(DofM : {x} (of x A) -> of (M x) B))
(reduce/lam (Dreduce : {x} reduce (M x) (N x)))
(of/lam
Dlinear'
DofN)
<- ({x} {dx:of x A}
sr (DofM x dx) (Dreduce x) (DofN x dx : of (N x) B))
<- srl DofM Dlinear Dreduce (Dlinear': linear ([x] N x)).

%worlds (bind) (sr _ _ _).
%total D1 (sr _ D1 _).```