Summer school 2008:Typed arithmetic expressions with sums 2

Arithmetic expressions with pairs and sums. (This solution involves output factoring, but no identity types. Dan posted a solution involving identity types, and Chris posted a solution that avoids output factoring.)

Numbers and strings are unchanged.

%sort nat %.
%name 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 char %.
%name char %.
%term a char %.
%term b char %.
%sort str %.
%name str %.
%term emp str %.
%term cons %pi char %-> str %-> str %.
%sort cat {_ str} {_ str} {_ str} %.
%mode cat %in %in %out %.
%term cat/e cat emp S S %.
%term cat/c %pi (cat (cons X S1) S2 (cons X S3)) %<- (cat S1 S2 S3) %.
%worlds () (cat _ _ _) %.
%total S (cat S _ _) %.

Typed expressions

Add a type for disjoint sums:

%sort tp %.
%name tp %.
%term number tp %.
%term string tp %.
%term prod %pi tp %-> tp %-> tp %.
%term sum %pi tp %-> tp %-> tp %.

Add injections as values, and case as an expression.

%sort val {_ tp} %.
%name val %.
%prec %postfix 1 val %.
%term num %pi nat %-> (number val) %.
%term lit %pi str %-> (string val) %.
%term pair %pi (T val) %-> (U val) %-> (prod T U val) %.
%term inl %pi (T val) %-> (sum T U val) %.
%term inr %pi (U val) %-> (sum T U val) %.
%sort exp {_ tp} %.
%name exp %.
%prec %postfix 1 exp %.
%term ret %pi (T val) %-> (T exp) %.
%term plus %pi (number exp) %-> (number exp) %-> (number exp) %.
%term append %pi (string exp) %-> (string exp) %-> (string exp) %.
%term let %pi (T exp) %-> (%pi (T val) %-> (U exp)) %-> (U exp) %.
%term fst %pi (prod T U exp) %-> (T exp) %.
%term snd %pi (prod T U exp) %-> (U exp) %.

For technical reasons, we bundle the branches of the case into a separate term with type cases; this makes the termination order more evident to STELF. An element of “cases T U V” is the branches for a “sum T U” whose result has tp “V”.

%sort cases {_ tp} {_ tp} {_ tp} %.
%term cases/i %pi (%pi (T val) %-> (V exp)) %-> (%pi (U val) %-> (V exp)) %-> (cases T U V) %.
%term case %pi (sum T U exp) %-> (cases T U V) %-> (V exp) %.

Add eval cases for case.

%sort eval {_ T exp} {_ T val} %.
%mode eval %in %out %.
%term eval/val eval (ret V) V %.
%term eval/plus
  %pi (eval (plus E1 E2) (num N))
  %<- (eval E1 (num N1))
  %<- (eval E2 (num N2))
  %<- (add N1 N2 N) %.
%term eval/append
  %pi (eval (append E1 E2) (lit S))
  %<- (eval E1 (lit S1))
  %<- (eval E2 (lit S2))
  %<- (cat S1 S2 S) %.
%term eval/let %pi (eval (let E1 ([x] E2 x)) A) %<- (eval E1 V) %<- (eval (E2 V) A) %.
%term eval/fst %pi (eval (fst E) A) %<- (eval E (pair A _)) %.
%term eval/snd %pi (eval (snd E) B) %<- (eval E (pair _ B)) %.

For “case” evaluation, we need an auxiliary relation “evalcase” to branch on inl vs. inr (output factoring).

%sort evalcase {_ sum T U val} {_ cases T U S} {_ S val} %.
%mode evalcase %in %in %out %.
%term eval/case %pi (eval (case E Cases) A) %<- (eval E V) %<- (evalcase V Cases A) %.
%term evalcase/inl %pi (evalcase (inl V1) (cases/i ([x] F1 x) ([y] F2 y)) A) %<- (eval (F1 V1) A) %.
%term evalcase/inr %pi (evalcase (inr V2) (cases/i ([x] F1 x) ([y] F2 y)) A) %<- (eval (F2 V2) A) %.

Then we use mutual induction to show evaluation total.

%worlds () (eval _ _) (evalcase _ _ _) %.
%total (E Cases) (eval E _) (evalcase _ Cases _) %.