Computation and Deduction 2009/20090401

This is Literate Twelf Code: here Status: %% ABORT %% Output: here.

Code from class, April 1.

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/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.

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

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

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 _ (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)))
     _.

%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
	_
	DofN)
     <- ({x} {dx:of x A}
	   sr (DofM x dx) (Dreduce x) (DofN x dx : of (N x) B)).

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