POPL Tutorial/Combinators (karl)

Lambda Terms

%sort exp %.
%name exp %.
%term lam %pi (%pi exp %-> exp) %-> exp %.
%term app %pi exp %-> exp %-> exp %.

Reduction

%sort reduce {_ exp} {_ exp} %.
%term reduce/refl reduce E E %.
%term reduce/trans %pi (reduce E1 E3) %<- (reduce E1 E2) %<- (reduce E2 E3) %.
%term reduce/lam %pi (reduce (lam ([x] E x)) (lam ([x] E' x))) %<- ({x} reduce (E x) (E' x)) %.
%term reduce/app %pi (reduce (app E1 E2) (app E1' E2')) %<- (reduce E1 E1') %<- (reduce E2 E2') %.
%term reduce/beta reduce (app (lam ([x] E1 x)) E2) (E1 E2) %.

Combinators

%define s exp lam ([a] lam ([b] lam ([x] app (app a x) (app b x)))) %.
%define k exp lam ([x] lam ([y] x)) %.
%define i exp lam ([x] x) %.

Bracket Abstraction

%sort abstract {_ %pi exp %-> exp} {_ exp} %.
%mode abstract %in %out %.
%term abstract/var abstract ([x] x) i %.
%term abstract/closed abstract ([x] E) (app k E) %.
%term abstract/app
  %pi (abstract ([x] app (E1 x) (E2 x)) (app (app s E1') E2'))
  %<- (abstract E1 E1')
  %<- (abstract E2 E2') %.
%sort translate {_ exp} {_ exp} %.
%mode translate %in %out %.
%term translate/lam
  %pi (translate (lam ([x] E x)) E'')
  %<- ({x exp} %pi (translate x x) %-> (translate (E x) (E' x)))
  %<- (abstract ([x] E' x) E'') %.
%term translate/app
  %pi (translate (app E1 E2) (app E1' E2'))
  %<- (translate E1 E1')
  %<- (translate E2 E2') %.

Soundness

%sort abstract-sound {_ abstract ([x] E x) E'} {_ reduce E' (lam ([x] E x))} %.
%mode abstract-sound %in %out %.
%block abstract-sound-block {x exp}%.
%term _ abstract-sound (%the (abstract ([x] x) i) abstract/var) (%the (reduce i (lam ([x] x))) reduce/refl) %.
%term _ abstract-sound (%the (abstract ([x] E) (app k E)) abstract/closed) (%the (reduce (app k E) (lam ([x] E))) reduce/beta) %.
%term _
  %pi (abstract-sound (abstract/app (%the (abstract ([x] E2 x) E2') Dabstract2) (%the (abstract ([x] E1 x) E1') Dabstract1)) (reduce/trans (reduce/lam ([x] reduce/app reduce/beta reduce/beta)) (reduce/trans reduce/beta (reduce/app Dreduce2 (reduce/trans reduce/beta (reduce/app Dreduce1 reduce/refl))))))
  %<- (abstract-sound Dabstract1 (%the (reduce E1' (lam ([x] E1 x))) Dreduce1))
  %<- (abstract-sound Dabstract2 (%the (reduce E2' (lam ([x] E2 x))) Dreduce2)) %.
%worlds (abstract-sound-block) (abstract-sound _ _) %.
%total D (abstract-sound D _) %.
%sort translate-sound {_ translate E E'} {_ reduce E' E} %.
%mode translate-sound %in %out %.
%block translate-sound-block {x exp} {d_translate translate x x} {_ translate-sound d_translate reduce/refl}%.
%term _
  %pi (translate-sound (%the (translate (lam ([x] E x)) E'') (translate/lam (%the (abstract ([x] E' x) E'') Dabstract) (%the ({x exp} %pi (translate x x) %-> (translate (E x) (E' x))) Dtranslate))) (reduce/trans (reduce/lam ([x] Dreduce1 x)) Dreduce2))
  %<- ({x} {d_translate translate x x}
  %pi (translate-sound d_translate reduce/refl)
  %-> (translate-sound (Dtranslate x d_translate) (%the (reduce (E' x) (E x)) (Dreduce1 x))))
  %<- (abstract-sound Dabstract (%the (reduce E'' (lam ([x] E' x))) Dreduce2)) %.
%term _
  %pi (translate-sound (%the (translate (app E1 E2) (app E1' E2')) (translate/app (%the (translate E2 E2') Dtranslate2) (%the (translate E1 E1') Dtranslate1))) (reduce/app Dreduce2 Dreduce1))
  %<- (translate-sound Dtranslate1 (%the (reduce E1' E1) Dreduce1))
  %<- (translate-sound Dtranslate2 (%the (reduce E2' E2) Dreduce2)) %.
%worlds (translate-sound-block) (translate-sound _ _) %.
%total D (translate-sound D _) %.

Completeness

%sort clean {_ exp} %.
%term clean/s clean s %.
%term clean/k clean k %.
%term clean/i clean i %.
%term clean/app %pi (clean (app E1 E2)) %<- (clean E1) %<- (clean E2) %.
%sort abstract-clean {_ {x} %pi (clean x) %-> (clean (E x))} {_ abstract ([x] E x) E'} {_ clean E'} %.
%mode abstract-clean %in %in %out %.
%block abstract-clean-block {x exp} {d_clean clean x}%.
%term _ abstract-clean _ (%the (abstract ([x] x) i) abstract/var) clean/i %.
%term _ abstract-clean (%the ({x} %pi (clean x) %-> (clean E)) Dclean) abstract/closed (clean/app (%the (clean E) (Dclean i clean/i)) clean/k) %.
%term _
  %pi (abstract-clean ([x] [d_clean clean x] clean/app (%the (clean (E2 x)) (Dclean2 x d_clean)) (%the (clean (E1 x)) (Dclean1 x d_clean))) (abstract/app (%the (abstract ([x] E2 x) E2') Dabstract2) (%the (abstract ([x] E1 x) E1') Dabstract1)) (%the (clean (app (app s E1') E2')) (clean/app Dclean2' (clean/app Dclean1' clean/s))))
  %<- (abstract-clean Dclean1 Dabstract1 (%the (clean E1') Dclean1'))
  %<- (abstract-clean Dclean2 Dabstract2 (%the (clean E2') Dclean2')) %.
%worlds (abstract-clean-block) (abstract-clean _ _ _) %.
%total D (abstract-clean _ D _) %.
%sort translate-clean {_ translate E E'} {_ clean E'} %.
%mode translate-clean %in %out %.
%block translate-clean-block {x exp} {d_translate translate x x} {d_clean clean x} {_ translate-clean d_translate d_clean}%.
%term _
  %pi (translate-clean (%the (translate (lam ([x] E x)) E'') (translate/lam (%the (abstract ([x] E' x) E'') Dabstract) (%the ({x exp} %pi (translate x x) %-> (translate (E x) (E' x))) Dtranslate))) Dclean')
  %<- ({x} {d_translate translate x x} {d_clean clean x}
  %pi (translate-clean d_translate d_clean)
  %-> (translate-clean (Dtranslate x d_translate) (%the (clean (E' x)) (Dclean x d_clean))))
  %<- (abstract-clean Dclean Dabstract (%the (clean E'') Dclean')) %.
%term _
  %pi (translate-clean (%the (translate (app E1 E2) (app E1' E2')) (translate/app (%the (translate E2 E2') Dtranslate2) (%the (translate E1 E1') Dtranslate1))) (%the (clean (app E1' E2')) (clean/app Dclean2 Dclean1)))
  %<- (translate-clean Dtranslate1 (%the (clean E1') Dclean1))
  %<- (translate-clean Dtranslate2 (%the (clean E2') Dclean2)) %.
%worlds (translate-clean-block) (translate-clean _ _) %.
%total D (translate-clean D _) %.
%sort can-abstract {_ {x} %pi (clean x) %-> (clean (E x))} {_ abstract ([x] E x) E'} %.
%mode can-abstract %in %out %.
%block can-abstract-block {x exp} {d_clean clean x}%.
%term _ can-abstract ([x] [d clean x] d) abstract/var %.
%term _ can-abstract (%the ({x} %pi (clean x) %-> (clean E)) _) abstract/closed %.
%term _
  %pi (can-abstract ([x] [d_clean clean x] clean/app (%the (clean (E2 x)) (Dclean2 x d_clean)) (%the (clean (E1 x)) (Dclean1 x d_clean))) (abstract/app Dabstract2 Dabstract1))
  %<- (can-abstract Dclean1 (%the (abstract ([x] E1 x) E1') Dabstract1))
  %<- (can-abstract Dclean2 (%the (abstract ([x] E2 x) E2') Dabstract2)) %.
%worlds (can-abstract-block) (can-abstract _ _) %.
%total D (can-abstract D _) %.
%sort can-translate {E exp} {_ translate E E'} %.
%mode can-translate %in %out %.
%block can-translate-block {x exp} {d_translate translate x x} {d_clean clean x} {_ translate-clean d_translate d_clean} {_ can-translate x d_translate}%.
%term _
  %pi (can-translate (lam ([x] E x)) (%the (translate (lam ([x] E x)) E'') (translate/lam Dabstract Dtranslate)))
  %<- ({x} {d_translate translate x x} {d_clean clean x}
  %pi (translate-clean d_translate d_clean)
  %-> (can-translate x d_translate)
  %-> (can-translate (E x) (%the (translate (E x) (E' x)) (Dtranslate x d_translate))))
  %<- ({x} {d_translate translate x x} {d_clean clean x}
  %pi (translate-clean d_translate d_clean)
  %-> (translate-clean (Dtranslate x d_translate) (%the (clean (E' x)) (Dclean x d_clean))))
  %<- (can-abstract Dclean (%the (abstract ([x] E' x) E'') Dabstract)) %.
%term _
  %pi (can-translate (app E1 E2) (%the (translate (app E1 E2) (app E1' E2')) (translate/app Dtranslate2 Dtranslate1)))
  %<- (can-translate E1 (%the (translate E1 E1') Dtranslate1))
  %<- (can-translate E2 (%the (translate E2 E2') Dtranslate2)) %.
%worlds (can-translate-block) (can-translate _ _) %.
%total E (can-translate E _) %.