Summer school 2008:Typed arithmetic expressions with sums

Arithmetic expressions with pairs and sums, where the answer type is values.

For an alternate version of sums that doesn’t involve output factoring, see Chris’s solution. For a version that uses output factoring but avoids identity types, see William’s solution.

%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

%sort tp %.
%name tp %.
%term number tp %.
%term string tp %.
%term prod %pi tp %-> tp %-> tp %.
%term sum %pi tp %-> tp %-> tp %.
%sort val {_ tp} %.
%name val %.
%prec %postfix 1 val %.
%term num %pi nat %-> (number val) %.
%term lit %pi str %-> (string val) %.
%term pair %pi (U val) %-> (T val) %-> (prod U T val) %.
%term inl %pi (U val) %-> (sum U T val) %.
%term inr %pi (T val) %-> (sum U T 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 U T exp) %-> (U exp) %.
%% (fst e)
%term snd %pi (prod U T exp) %-> (T exp) %.
%% (snd e)
%term case
  %pi (sum T U exp)
  %-> (%pi (T val) %-> (V exp))
  %-> (%pi (U val) %-> (V exp))
  %-> (V exp) %.

Evaluation

For simplicity, take answers to be values.

%sort eval {_ T exp} {_ T val} %.
%mode eval %in %out %.
%% eval
%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) A1) %<- (eval E (pair A1 A2)) %.
%term eval/snd %pi (eval (snd (%the (prod T1 T2 exp) E)) A2) %<- (eval E (pair A1 A2)) %.
%term eval/case/inl %pi (eval (case E E1 E2) A') %<- (eval E (inl A1)) %<- (eval (E1 A1) A') %.
%term eval/case/inr %pi (eval (case E E1 E2) A') %<- (eval E (inr A2)) %<- (eval (E2 A2) A') %.
%worlds () (eval _ _) %.

We can write the obvious rules for evaluation, but STELF can’t prove this definition total. The reason is that the output coverage checker looks at each constant in isolation, not at the whole set of constants. In this case, it flags an error on the case eval/case/inl:

%total E (eval E _) %.

because it doesn’t notice that the next constant, eval/case/inr, covers the other possible output of evaluating E. We can fix this using a technique called output factoring.

Output factored evaluation

%sort id {_ A exp} {_ A exp} %.
%term refl id E E %.
%sort eval'-case {E' V exp} {E sum T U exp} {E1} {E2} {_ id E' (case E E1 E2)} {_ sum T U val} {_ V val} %.
%mode eval'-case %in %in %in %in %in %in %out %.
%sort eval' {_ T exp} {_ T val} %.
%mode eval' %in %out %.
%% eval'-case
%term eval'-case/inl %pi (eval'-case _ E E1 E2 refl (inl A1) A) %<- (eval' (E1 A1) A) %.
%term eval'-case/inr %pi (eval'-case _ E E1 E2 refl (inr A2) A) %<- (eval' (E2 A2) A) %.
%% eval'
%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) A1) %<- (eval' E (pair A1 A2)) %.
%term eval'/snd %pi (eval' (snd (%the (prod T1 T2 exp) E)) A2) %<- (eval' E (pair A1 A2)) %.
%term eval'/case
  %pi (eval' (case E E1 E2) A')
  %<- (eval' E A)
  %<- (eval'-case (case E E1 E2) E E1 E2 refl A A') %.
%worlds () (eval' _ _) (eval'-case _ _ _ _ _ _ _) %.
%total (E E') (eval'-case E' _ _ _ _ _ _) (eval' E _) %.

The constant eval'/case uses output factoring: the subsidiary case-analysis of the result of eval' E A is broken out into a separate lemma, eval'-case. This solves the above problem, because while output coverage cannot be split across multiple constants, input coverage certainly can. However, because eval'-case recursively calls eval', the two relations must be proved total using mutual induction. This is why we

• write both type families and modes before writing any constants
• declare their worlds and modes at once
• use the mutual termination metric (E E')

However, there is an additional subtlety that we need to address. You might think eval'-case could be defined as follows:

%term eval'-case \ ({E sum T U exp\} \ ({E1 %pi (T val) %-> (V exp\)} \ ({E2 %pi (U val) %-> (V exp\)} %pi (sum T U val) %-> (A val) %-> %type))) %.
%mode eval'-case %in %in %in %in %out %.
%term eval'-case/inl %pi (eval'-case E E1 E2 (inl A1) A) %<- (eval' (E1 A1) A) %.
%term eval'-case/inr %pi (eval'-case E E1 E2 (inr A2) A) %<- (eval' (E2 A2) A) %.

The problem is that STELF can’t justify the recursive calls to eval' on E1 and E2. In fact, why does this recursion pattern work at all? The reason is that we don’t call eval'-case on just any E1 and E2, but on subexpressions of the E that eval' was originally called with. Thus, when we call back to eval' from eval'-case, it’s on a smaller expression.

We make this invariant evident to STELF as follows:

• when eval' calls eval'-case, we pass in the original expression (case E E1 E2) that eval' was called with
• this argument is used as termination metric for eval-case'
• we constrain this position to be a case-analysis using an identity type, so that we don’t have extraneous cases to consider.

This explains the somewhat-convoluted code above.