POPL Tutorial/Basics Answer

Natural numbers

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

Addition

%sort add {_ nat} {_ nat} {_ nat} %.
%term add/z add zero N N %.
%term add/s %pi (add (succ M) N (succ P)) %<- (add M N P) %.

Example derivations

%define 1 nat succ zero %.
%define 2 nat succ 1 %.
%define 1+1is2 (add 1 1 2) add/s add/z %.
%% explicit version of add/z
%% add/z-explicit  : {n:nat} add zero n n.
%% 1+1is2-explicit : add 1 1 2 = add/s (add/z-explicit 1).

Exercise: Multiplication

%sort mult {_ nat} {_ nat} {_ nat} %.
%term mult/z mult zero N zero %.
%term mult/s %pi (mult (succ M) N P') %<- (mult M N P) %<- (add N P P') %.
%% note that the arguments are "backwards"
%define 1*2is2 (mult 1 2 2) mult/s (add/s (add/s add/z)) mult/z %.

Mode, worlds total

%mode add %in %in %out %.
%worlds () (add _ _ _) %.
%total M (add M _ _) %.
%solve 1+1is2' : add 1 1 N %.
%% Examples of errors:
%% mult/bad-mode-output : mult zero N Q.
%% mult/bad-mode-input : mult (succ M) N zero
%%            <- mult M Q P.
%% %% do input coverage by removing cases
%% mult/bad-termination-1 : mult M N P
%%         <- mult M N P.
%% mult/bad-termination-2 : mult M N P
%%         <- mult N N P.
%% mult/bad-output-free : mult (succ M) N zero
%%       <- mult M N N.
%% mult/bad-output-cov : mult (succ M) N zero
%%            <- mult M N (succ P).
%mode mult %in %in %out %.
%worlds () (mult _ _ _) %.
%total M (mult M _ _) %.

Right-hand zero

%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 P} {_ add M (succ N) (succ P)} %.
%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 (add/s (%the (add M N P) D1)) (add/s D2))
  %<- (rhsucc D1 (%the (add M (succ N) (succ P)) D2)) %.
%% remark that type annotations are optional:
%% - : rhsucc add/z add/z.
%% - : rhsucc (add/s D1) (add/s D2)
%%      <- rhsucc D1 D2.
%worlds () (rhsucc _ _) %.
%total M (rhsucc M _) %.

Exercise: addition is commutative

%sort commute {_ add M N P} {_ add N M P} %.
%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 P) D)) D'')
  %<- (commute D (%the (add N M P) D'))
  %<- (rhsucc D' (%the (add N (succ M) (succ P)) D'')) %.
%worlds () (commute _ _) %.
%total D (commute D _) %.