Computation and Deduction 2009/20090330

From The Twelf Project

Code from class, March 30.

tp : type.

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.

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 (pi2 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 0.

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:exp} linear ([x] N x y)).

of/letb : of (letb M ([x] N x)) C
	   <- of M (! A)
	   <- ({x:exp} (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).

srl : ({x} (of x A) -> of (M x) B) -> linear ([x] M x) -> ({x} reduce (M x) (M' x)) -> linear ([x] M' x) -> type.


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

%block bind : some {A:tp} block {x:exp} {dx : of x A}.
%worlds (bind) (sr _ _ _).
%total D1 (sr _ D1 _).