Computation and Deduction 2009/20090204

From The Twelf Project
Jump to: navigation, search
This is Literate Twelf
Code: here
Status: %% ABORT %%
Output: here.

Code from class, February 4

tp : type.  %name tp T.

num : tp.
arr : tp -> tp -> tp.

%worlds () (tp).

term : type.  %name term E.

z : term.
s : term -> term.
ifz : term -> term -> (term -> term) -> term.
lam : tp -> (term -> term) -> term.
app : term -> term -> term.

%block var : block {x:term}.
%worlds (var) (term).

of : term -> tp -> type.

of/z : of z num.

of/s : of (s N) num
        <- of N num.

of/ifz : of (ifz E E0 ([x] E1 x)) T
          <- of E num
          <- of E0 T
          <- ({x} of x num -> of (E1 x) T).

of/lam : of (lam T ([x] E x)) (arr T T')
          <- ({x} of x T -> of (E x) T').

of/app : of (app E1 E2) T'
          <- of E1 (arr T T')
          <- of E2 T.

%block stupid : some {x:term} {t:tp} block {d:of x t}.
%block bind : some {T:tp} block {x:term} {d : of x T}.
%worlds (bind) (of _ _).

value : term -> type.

value/z : value z.

value/s : value (s E)
           <- value E.

value/lam : value (lam T E).

%worlds () (value _).



step : term -> term -> type.

step/s : step (s E) (s E')
          <- step E E'.

step/ifz/arg : step (ifz E E0 ([x] E1 x)) (ifz E' E0 E1)
                <- step E E'.

step/ifz/z : step (ifz z E0 E1) E0.

step/ifz/s : step (ifz (s E) E0 ([x] E1 x)) (E1 E)
              <- value E.

step/app/fn : step (app E1 E2) (app E1' E2)
	       <- step E1 E1'.

step/app/arg : step (app E1 E2) (app E1 E2')
		<- value E1
		<- step E2 E2'.

step/app/beta : step (app (lam T ([x] E1 x)) E2) (E1 E2)
		 <- value E2.

%worlds () (step _ _).


unstuck : term -> type.
unstuck/val : unstuck E
	       <- value E.

unstuck/step : unstuck E
		<- step E E'.

progress-s : unstuck E -> unstuck (s E) -> type.
%mode progress-s +X1 -X2.

- : progress-s (unstuck/val (D : value E)) (unstuck/val (value/s D)).

- : progress-s (unstuck/step (D : step E E')) (unstuck/step (step/s D)).

%worlds () (progress-s _ _).
%total {} (progress-s _ _).

progress-ifz : of E num -> unstuck E -> {E0:term} {E1:term -> term} unstuck (ifz E E0 E1) -> type.
%mode progress-ifz +D1 +D2 +E0 +E1 -D3.

- : progress-ifz _ (unstuck/step (D : step E E')) E0 E1 (unstuck/step (step/ifz/arg D)).

- : progress-ifz 
     (Dof : of z num)
     (unstuck/val (value/z))
     E0 E1
     (unstuck/step step/ifz/z).

- : progress-ifz
     (Dof : of (s E) num)
     (unstuck/val (value/s (Dval : value E)))
     E0 E1
     (unstuck/step (step/ifz/s Dval)).

%worlds () (progress-ifz _ _ _ _ _).
%total {} (progress-ifz _ _ _ _ _).

progress : of E T -> unstuck E -> type.
%mode progress +D -D'.

- : progress of/z (unstuck/val value/z).

- : progress (of/s (D : of E num)) D''
     <- progress D (D' : unstuck E)
     <- progress-s D' (D'' : unstuck (s E)).

- : progress 
     (of/ifz
	(D1 : {x} of x num -> of (E1 x) T)
	(D0 : of E0 T)
	(D : of E num))
     D''
     <- progress D (D' : unstuck E)
     <- progress-ifz D  D' E0 E1 (D'' : unstuck (ifz E E0 E1)).

%worlds () (progress _ _).
%total D (progress D _).