POPL Tutorial/Session 4 Live

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

Please fill feedback form

Syntax

%% Types:

tp : type.  %name tp T.
nat : tp.
arr : tp -> tp -> tp.

%% Terms:

exp : type.  %name exp E.

%% variables represented by LF variables

z : exp.

fun : tp -> tp -> (exp -> exp -> exp) -> exp.
app : exp -> exp -> exp.

%% TASK 1 Answer:

s : exp -> exp.
ifz : exp -> exp -> (exp -> exp) -> exp.
%% not: ifz : exp -> exp -> exp -> exp.

Typing

%% Note: not total!  Not all terms are well-typed
%% Don't need mode, worlds right now.
of : exp -> tp -> type.

%% represent variables as LF variables

of/z : of z nat.

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

%% really: 
%% of E2 T -> of E1 (arr T T') -> of/app : of (app E1 E2) T'

%% not eta-long:
%% of/fun' : of (fun T1 T2 E) _.

%% eta-long:
of/fun : of (fun T1 T2 ([f] [x] E f x)) (arr T1 T2)
	  <- ({f : exp} of f (arr T1 T2) 
		-> {x : exp} of x T1 
		-> of (E f x) T2).

% of/fun : of (fun T1 T2 ([f] [x] E f x)) (arr T1 T2)
% 	  %% make assumptions in a different order
% 	  <- ({f : exp} {x : exp}
% 		-> of f (arr T1 T2) -> of x T1 
% 		-> of (E f x) T2).

%% Task: give typing rules for
%% s, ifz

e : nat

---

s e : nat

e : nat e0 : T x exp , x : nat |- e1 : T

---

ifz(e,e0,x.e1) : T

of/s : of (s E) nat
	<- of E nat.

of/ifz : of (ifz E E0 ([x] Es x)) T
	  <- of E nat
	  <- of E0 T
	  <- ({x : exp} of x nat
		-> of (Es x) T).

Operational semantics

%% Which expressions are values?
%% Use a predicate

value : exp -> type.
%mode value +E.

value/z : value z.
value/s : value (s E)
	   <- value E.
%% value/fun : value (fun T1 T2 ([f] [x] E f x)).
value/fun : value (fun _ _ _).

%% Small-step evaluation

step : exp -> exp -> type.
%mode step +E -E'.

step/app/fun : 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 
		    (fun T1 T2 ([f] [x] E1 f x))
		    E2)
	      %% substitution = LF function application
		 (E1 (fun T1 T2 ([f] [x] E1 f x)) E2)
		 <- value E2.


%% Task 3:
%% (s E) takes a step if E takes a step

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


%% when E takes a step then
%% ifz E _ _ takes a step

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

%% (ifz z E0 Es) steps to E0

step/ifz/z : step
	      (ifz z E0 ([x] Es x))
	      E0.

%% (ifz (s E) _ x.Es) steps to [E/x]Es
%% when E is a value

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

Proof of type preservation

If e : T and step e e' then e' : T.

(eval relates expressions to answers)

Type preservation relates derivations of judgements to other derivations

Relate: e : T and step e e' to e' : T

Key idea: define total relations

%% Type family:

pres : of E T 
	-> step E E'
	-> of E' T
	-> type.
%mode pres +Dof +Dstep -Dof'.

%% gives cases

- : pres 
     ((of/app 
	 (DofE2 : of E2 T2)
	 (DofE1 : of E1 (arr T2 T1)))
	: of (app E1 E2) T1)
     (step/app/fun 
	(Dstep : step E1 E1') 
	: step (app E1 E2) (app E1' E2))
     (of/app DofE2 DofE1')
     <- pres DofE1 Dstep (DofE1' : of E1' (arr T2 T1)).

- : pres
     ((of/app 
	 (DofE2 : of E2 T2)
	 (DofE1 : of E1 (arr T2 T1)))
	: of (app E1 E2) T1)
     (step/app/arg 
	(Dstep : step E2 E2')
	(Dval : value E1)
	: step (app E1 E2) (app E1 E2'))
     (of/app DofE2' DofE1)
     <- pres DofE2 Dstep (DofE2' : of E2' T2).

- : pres 
     ((of/app 
	 (DofE2 : of E2 T2)
	 ((of/fun 
	     (DofE1 : {f} of f (arr T2 T1)
		       -> {x} of x T2
		       -> of (E1 f x) T1))  
	    : of (fun T2 T1 ([f] [x] E1 f x)) (arr T2 T1)))
	: of (app (fun T2 T1 ([f] [x] E1 f x)) E2) T1)
     (step/app/beta
	(Dval : value E2)
	: step (app (fun T2 T1 ([f] [x] E1 f x)) E2)
	   (E1 (fun T2 T1 ([f] [x] E1 f x)) E2))
     (DofE1 (fun T2 T1 ([f] [x] E1 f x)) (of/fun DofE1) E2 DofE2).

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