POPL Tutorial/Nat

Nats

%sort nat %.
%term zero nat %.
%term succ %pi nat %-> nat %.

Add

%sort add {_ nat} {_ nat} {_ nat} %.
%term add/z add zero N N %.
%term add/s %pi (add (succ M) N (succ O)) %<- (add M N O) %.
%mode add %in %in %out %.
%worlds () (add _ _ _) %.
%total M (add M _ _) %.

Exercise: Mult

%sort mult {_ nat} {_ nat} {_ nat} %.
%term mult/z mult zero N zero %.
%term mult/s %pi (mult (succ M) N O') %<- (mult M N O) %<- (add N O O') %.
%mode mult %in %in %out %.
%worlds () (mult _ _ _) %.
%total M (mult M _ _) %.

Right-hand Identity

%sort rhzero {M nat} {_ add M zero M} %.
%mode rhzero %in %out %.
%term _ rhzero zero add/z %.
%term _ %pi (rhzero (succ M) (add/s D)) %<- (rhzero M (%the (add M zero M) D)) %.
%worlds () (rhzero _ _) %.
%total M (rhzero M _) %.

Right-hand succ

%sort rhsucc {_ add M N O} {_ add M (succ N) (succ O)} %.
%mode rhsucc %in %out %.
%term _ rhsucc (%the (add zero M M) add/z) (%the (add zero (succ M) (succ M)) add/z) %.
%term _
  %pi (rhsucc (%the (add (succ M) N (succ O)) (add/s (%the (add M N O) D1))) (add/s D2))
  %<- (rhsucc D1 (%the (add M (succ N) (succ O)) D2)) %.
%worlds () (rhsucc _ _) %.
%total M (rhsucc M _) %.

Exercise: put it all together

%sort commute {_ add M N O} {_ add N M O} %.
%mode commute %in %out %.
%term _ %pi (commute (%the (add zero M M) add/z) D) %<- (rhzero M D) %.
%term _
  %pi (commute (add/s (%the (add M N O) D)) D'')
  %<- (commute D (%the (add N M O) D'))
  %<- (rhsucc D' (%the (add N (succ M) (succ O)) D'')) %.
%worlds () (commute _ _) %.
%total D (commute D _) %.