POPL Tutorial/Session 4 Starter

Session 4: Type Preservation Starter

Syntax

%sort tp %.
%name tp %.
%term nat tp %.
%term arr %pi tp %-> tp %-> tp %.
%sort exp %.
%name exp %.
%term z exp %.
%term fun %pi tp %-> tp %-> (%pi exp %-> exp %-> exp) %-> exp %.
%term app %pi exp %-> exp %-> exp %.

TASK 1:

Add constants for successor and ifz:

Static Semantics

%sort of {_ exp} {_ tp} %.
%name of %.
%term of/z of z nat %.
%term of/fun
  %pi (of (fun T1 T2 ([f] [x] E f x)) (arr T1 T2))
  %<- ({f} %pi (of f (arr T1 T2)) %-> ({x} %pi (of x T1) %-> (of (E f x) T2))) %.
%term of/app %pi (of (app E1 E2) T') %<- (of E1 (arr T T')) %<- (of E2 T) %.

TASK 2:

Add two new typing rules for successor and ifz

Dynamic Semantics

%sort value {_ exp} %.
%name value %.
%term value/z value z %.

Task 3a: Add a value rule for successor

%term value/fun value (fun _ _ _) %.
%sort step {_ exp} {_ exp} %.
%name step %.
%term step/app/fun %pi (step (app E1 E2) (app E1' E2)) %<- (step E1 E1') %.
%term step/app/arg %pi (step (app E1 E2) (app E1 E2')) %<- (value E1) %<- (step E2 E2') %.
%term step/app/beta-v
  %pi (step (app (fun T1 T2 ([f] [x] E1 f x)) E2) (E1 (fun T1 T2 ([f] [x] E1 f x)) E2))
  %<- (value E2) %.

TASK 3:

Add four more operational semantics rules for successor and ifz.

Preservation

%sort preservation {_ of E T} {_ step E E'} {_ of E' T} %.
%mode preservation %in %in %out %.
%term _
  %pi (preservation (of/app (%the (of E2 T) DofE2) (%the (of E1 (arr T T')) DofE1)) (%the (step (app E1 E2) (app E1' E2)) (step/app/fun (%the (step E1 E1') Dstep))) (of/app DofE2 DofE1'))
  %<- (preservation DofE1 Dstep (%the (of E1' (arr T T')) DofE1')) %.
%term _
  %pi (preservation (of/app (%the (of E2 T) DofE2) (%the (of E1 (arr T T')) DofE1)) (%the (step (app E1 E2) (app E1 E2')) (step/app/arg (%the (step E2 E2') Dstep) _)) (of/app DofE2' DofE1))
  %<- (preservation DofE2 Dstep (%the (of E2' T) DofE2')) %.
%term _ preservation (of/app (%the (of E2 T1) DofE2) (%the (of (fun T1 T2 ([f] [x] E1 f x)) (arr T1 T2)) (of/fun (%the ({f} %pi (of f (arr T1 T2)) %-> ({x} %pi (of x T1) %-> (of (E1 f x) T2))) DofE1)))) (%the (step (app (fun T1 T2 ([f] [x] E1 f x)) E2) (E1 (fun T1 T2 ([f] [x] E1 f x)) E2)) (step/app/beta-v _)) (DofE1 (fun T1 T2 ([f] [x] E1 f x)) (of/fun DofE1) E2 DofE2) %.

TASK 4: Finish the proof!

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