POPL Tutorial/New language

Arithmetic Primitives

%sort nat %.
%term z nat %.
%term s %pi nat %-> nat %.
%sort add {_ nat} {_ nat} {_ nat} %.
%mode add %in %in %out %.
%term add/z add z N N %.
%term add/s %pi (add (s M) N (s P)) %<- (add M N P) %.
%worlds () (add _ _ _) %.
%total M (add M _ _) %.
%sort mult {_ nat} {_ nat} {_ nat} %.
%mode mult %in %in %out %.
%term mult/z mult z N z %.
%term mult/s %pi (mult (s M) N Q) %<- (mult M N P) %<- (add P N Q) %.
%worlds () (mult _ _ _) %.
%total M (mult M _ _) %.

Language Syntax

%sort tp %.
%term num tp %.
%term arrow %pi tp %-> tp %-> tp %.
%term prod %pi tp %-> tp %-> tp %.
%sort exp %.
%term numeral %pi nat %-> exp %.
%term plus %pi exp %-> exp %-> exp %.
%term times %pi exp %-> exp %-> exp %.
%term lam %pi tp %-> (%pi exp %-> exp) %-> exp %.
%term app %pi exp %-> exp %-> exp %.
%term pair %pi exp %-> exp %-> exp %.
%term split %pi exp %-> (%pi exp %-> exp %-> exp) %-> exp %.

Dynamic Semantics

%sort value {_ exp} %.
%sort step {_ exp} {_ exp} %.
%%% argh, too many rules!
%term value/numeral value (numeral N) %.
%term value/lam value (lam T ([x] E x)) %.
%term value/pair %pi (value (pair E1 E2)) %<- (value E1) %<- (value E2) %.
%term step/plus/1 %pi (step (plus E1 E2) (plus E1' E2)) %<- (step E1 E1') %.
%term step/plus/2 %pi (step (plus V1 E2) (plus V1 E2')) %<- (value V1) %<- (step E2 E2') %.
%term step/plus/add %pi (step (plus (numeral N1) (numeral N2)) (numeral N3)) %<- (add N1 N2 N3) %.
%term step/times/1 %pi (step (times E1 E2) (times E1' E2)) %<- (step E1 E1') %.
%term step/times/2 %pi (step (times V1 E2) (times V1 E2')) %<- (value V1) %<- (step E2 E2') %.
%term step/times/mult %pi (step (times (numeral N1) (numeral N2)) (numeral N3)) %<- (mult N1 N2 N3) %.
%term step/app/fun %pi (step (app E1 E2) (app E1' E2)) %<- (step E1 E1') %.
%term step/app/arg %pi (step (app V1 E2) (app V1 E2')) %<- (value V1) %<- (step E2 E2') %.
%term step/app/beta %pi (step (app (lam T ([x] E x)) V) (E V)) %<- (value V) %.
%term step/pair/1 %pi (step (pair E1 E2) (pair E1' E2)) %<- (step E1 E1') %.
%term step/pair/2 %pi (step (pair V1 E2) (pair V1 E2')) %<- (value V1) %<- (step E2 E2') %.
%term step/split/arg
  %pi (step (split E1 ([x] [y] E2 x y)) (split E1' ([x] [y] E2 x y)))
  %<- (step E1 E1') %.
%term step/split/pair
  %pi (step (split (pair V1 V2) ([x] [y] E x y)) (E V1 V2))
  %<- (value V1)
  %<- (value V2) %.
%worlds () (value _) %.
%worlds () (step _ _) %.

Static Semantics

%sort of {_ exp} {_ tp} %.
%term of/numeral of (numeral N) num %.
%term of/plus %pi (of (plus E1 E2) num) %<- (of E1 num) %<- (of E2 num) %.
%term of/times %pi (of (times E1 E2) num) %<- (of E1 num) %<- (of E2 num) %.
%term of/lam
  %pi (of (lam T1 ([x] E x)) (arrow T1 T2))
  %<- ({x} %pi (of x T1) %-> (of (E x) T2)) %.
%term of/app %pi (of (app E1 E2) T) %<- (of E1 (arrow T2 T)) %<- (of E2 T2) %.
%term of/pair %pi (of (pair E1 E2) (prod T1 T2)) %<- (of E1 T1) %<- (of E2 T2) %.
%term of/split
  %pi (of (split E ([x] [y] Ebody x y)) T)
  %<- (of E (prod T1 T2))
  %<- ({x} %pi (of x T1) %-> ({y} %pi (of y T2) %-> (of (Ebody x y) T))) %.
%block tbind [T tp] {x exp} {dx of x T}%.
%worlds (tbind) (of _ _) %.

Progress

%sort notstuck {_ exp} %.
%term notstuck/value %pi (notstuck E) %<- (value E) %.
%term notstuck/step %pi (notstuck E) %<- (step E E') %.
%sort progress-app {_ of E1 (arrow T1 T2)} {_ notstuck E1} {_ notstuck E2} {_ notstuck (app E1 E2)} %.
%mode progress-app %in %in %in %out %.
%term _ progress-app Dof (notstuck/step Dstep) Dns2 (notstuck/step (step/app/fun Dstep)) %.
%term _ progress-app Dof (notstuck/value Dval) (notstuck/step Dstep) (notstuck/step (step/app/arg Dstep Dval)) %.
%term _ progress-app (of/lam Dof') (notstuck/value value/lam) (notstuck/value Dval2) (notstuck/step (step/app/beta Dval2)) %.
%worlds () (progress-app _ _ _ _) %.
%total {} (progress-app _ _ _ _) %.
%sort progress-pair {_ notstuck E1} {_ notstuck E2} {_ notstuck (pair E1 E2)} %.
%mode progress-pair %in %in %out %.
%term _ progress-pair (notstuck/step Dstep) Dns2 (notstuck/step (step/pair/1 Dstep)) %.
%term _ progress-pair (notstuck/value Dval1) (notstuck/step Dstep2) (notstuck/step (step/pair/2 Dstep2 Dval1)) %.
%term _ progress-pair (notstuck/value Dval1) (notstuck/value Dval2) (notstuck/value (value/pair Dval2 Dval1)) %.
%worlds () (progress-pair _ _ _) %.
%total {} (progress-pair _ _ _) %.
%sort progress-split {_ of E1 (prod T1 T2)} {_ notstuck E1} {Ebody} {_ notstuck (split E1 Ebody)} %.
%mode progress-split %in %in %in %out %.
%term _ progress-split Dof (notstuck/step Dstep) Ebody (notstuck/step (step/split/arg Dstep)) %.
%term _ progress-split (of/pair Dof2 Dof1) (notstuck/value (value/pair Dval2 Dval1)) Ebody (notstuck/step (step/split/pair Dval2 Dval1)) %.
%worlds () (progress-split _ _ _ _) %.
%total {} (progress-split _ _ _ _) %.
%sort can-add {N1} {N2} {_ add N1 N2 N3} %.
%mode can-add %in %in %out %.
%term _ can-add z N add/z %.
%term _ %pi (can-add (s N1) N2 (add/s Dadd)) %<- (can-add N1 N2 Dadd) %.
%worlds () (can-add _ _ _) %.
%total (D1) (can-add D1 _ _) %.
%sort progress-plus {_ of E1 num} {_ of E2 num} {_ notstuck E1} {_ notstuck E2} {_ notstuck (plus E1 E2)} %.
%mode progress-plus %in %in %in %in %out %.
%term _ progress-plus Dof1 Dof2 (notstuck/step Dstep) Dns2 (notstuck/step (step/plus/1 Dstep)) %.
%term _ progress-plus Dof1 Dof2 (notstuck/value Dval1) (notstuck/step Dstep2) (notstuck/step (step/plus/2 Dstep2 Dval1)) %.
%term _
  %pi (progress-plus of/numeral of/numeral (notstuck/value value/numeral) (notstuck/value value/numeral) (notstuck/step (step/plus/add Dadd)))
  %<- (can-add N1 N2 (%the (add N1 N2 N3) Dadd)) %.
%worlds () (progress-plus _ _ _ _ _) %.
%total {} (progress-plus _ _ _ _ _) %.
%sort can-mult {N1} {N2} {_ mult N1 N2 N3} %.
%mode can-mult %in %in %out %.
%term _ can-mult z N mult/z %.
%term _
  %pi (can-mult (s N1) N2 (mult/s Dadd Dmult))
  %<- (can-mult N1 N2 (%the (mult N1 N2 N3) Dmult))
  %<- (can-add N3 N2 Dadd) %.
%worlds () (can-mult _ _ _) %.
%total (D1) (can-mult D1 _ _) %.
%sort progress-times {_ of E1 num} {_ of E2 num} {_ notstuck E1} {_ notstuck E2} {_ notstuck (times E1 E2)} %.
%mode progress-times %in %in %in %in %out %.
%term _ progress-times Dof1 Dof2 (notstuck/step Dstep) Dns2 (notstuck/step (step/times/1 Dstep)) %.
%term _ progress-times Dof1 Dof2 (notstuck/value Dval1) (notstuck/step Dstep2) (notstuck/step (step/times/2 Dstep2 Dval1)) %.
%term _
  %pi (progress-times of/numeral of/numeral (notstuck/value value/numeral) (notstuck/value value/numeral) (notstuck/step (step/times/mult Dmult)))
  %<- (can-mult N1 N2 (%the (mult N1 N2 N3) Dmult)) %.
%worlds () (progress-times _ _ _ _ _) %.
%total {} (progress-times _ _ _ _ _) %.
%sort progress {_ of E T} {_ notstuck E} %.
%mode progress %in %out %.
%term _ progress of/numeral (notstuck/value value/numeral) %.
%term _
  %pi (progress (of/plus Dof2 Dof1) Dns3)
  %<- (progress Dof1 Dns1)
  %<- (progress Dof2 Dns2)
  %<- (progress-plus Dof1 Dof2 Dns1 Dns2 Dns3) %.
%term _
  %pi (progress (of/times Dof2 Dof1) Dns3)
  %<- (progress Dof1 Dns1)
  %<- (progress Dof2 Dns2)
  %<- (progress-times Dof1 Dof2 Dns1 Dns2 Dns3) %.
%term _ progress (of/lam Dof1) (notstuck/value value/lam) %.
%term _
  %pi (progress (of/app Dof2 Dof1) Dns3)
  %<- (progress Dof1 Dns1)
  %<- (progress Dof2 Dns2)
  %<- (progress-app Dof1 Dns1 Dns2 Dns3) %.
%term _
  %pi (progress (of/pair Dof2 Dof1) Dns3)
  %<- (progress Dof1 Dns1)
  %<- (progress Dof2 Dns2)
  %<- (progress-pair Dns1 Dns2 Dns3) %.
%term _
  %pi (progress (of/split (%the ({x} %pi (of x T1) %-> ({y} %pi (of y T2) %-> (of (Ebody x y) T))) Dbody) Dof1) Dns2)
  %<- (progress Dof1 Dns1)
  %<- (progress-split Dof1 Dns1 Ebody Dns2) %.
%worlds () (progress _ _) %.
%total (D1) (progress D1 _) %.

Preservation

%sort preservation {_ of E1 T1} {_ step E1 E2} {_ of E2 T1} %.
%mode preservation %in %in %out %.
%term _
  %pi (preservation (of/plus Dof2 Dof1) (step/plus/1 Dstep1) (of/plus Dof2 Dof1'))
  %<- (preservation Dof1 Dstep1 Dof1') %.
%term _
  %pi (preservation (of/plus Dof2 Dof1) (step/plus/2 Dstep2 Dval1) (of/plus Dof2' Dof1))
  %<- (preservation Dof2 Dstep2 Dof2') %.
%term _ preservation (of/plus Dof2 Dof1) (step/plus/add Dadd) of/numeral %.
%term _
  %pi (preservation (of/times Dof2 Dof1) (step/times/1 Dstep1) (of/times Dof2 Dof1'))
  %<- (preservation Dof1 Dstep1 Dof1') %.
%term _
  %pi (preservation (of/times Dof2 Dof1) (step/times/2 Dstep2 Dval1) (of/times Dof2' Dof1))
  %<- (preservation Dof2 Dstep2 Dof2') %.
%term _ preservation (of/times Dof2 Dof1) (step/times/mult Dmult) of/numeral %.
%term _
  %pi (preservation (of/pair Dof2 Dof1) (step/pair/1 Dstep1) (of/pair Dof2 Dof1'))
  %<- (preservation Dof1 Dstep1 Dof1') %.
%term _
  %pi (preservation (of/pair Dof2 Dof1) (step/pair/2 Dstep2 Dval) (of/pair Dof2' Dof1))
  %<- (preservation Dof2 Dstep2 Dof2') %.
%term _
  %pi (preservation (of/split Dbody Dof1) (step/split/arg Dstep1) (of/split Dbody Dof1'))
  %<- (preservation Dof1 Dstep1 Dof1') %.
%term _ preservation (of/split Dbody (of/pair Dof2 Dof1)) (step/split/pair Dval2 Dval1) (Dbody E1 Dof1 E2 Dof2) %.
%term _
  %pi (preservation (of/app Dof2 Dof1) (step/app/fun Dstep1) (of/app Dof2 Dof1'))
  %<- (preservation Dof1 Dstep1 Dof1') %.
%term _
  %pi (preservation (of/app Dof2 Dof1) (step/app/arg Dstep2 Dval) (of/app Dof2' Dof1))
  %<- (preservation Dof2 Dstep2 Dof2') %.
%term _ preservation (of/app Dof2 (of/lam Dbody)) (step/app/beta Dval1) (Dbody E2 Dof2) %.
%worlds () (preservation _ _ _) %.
%total (D1) (preservation _ D1 _) %.