Summer school 2008:Typed arithmetic expressions (extrinsic encoding)

Here we take a more traditional approach to representing syntax, by first giving a definition of raw syntax, with a separate judgement defining the well-typed expressions. This is called an extrinsic encoding.

Numbers and strings are as before.

%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) %.
%% addition is a total function on closed terms of type nat
%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 _ _) %.

Raw syntax

%sort tp %.
%name tp %.
%term number tp %.
%term string tp %.
%sort val %.
%name val %.
%term num %pi nat %-> val %.
%term lit %pi str %-> val %.
%sort exp %.
%name exp %.
%term ret %pi val %-> exp %.
%term plus %pi exp %-> exp %-> exp %.
%term append %pi exp %-> exp %-> exp %.
%term let %pi exp %-> (%pi val %-> exp) %-> exp %.

Typing judgement on raw syntax

%sort ofv {_ val} {_ tp} %.
%name ofv %.
%mode ofv %in %out %.
%term _ ofv (num _) number %.
%term _ ofv (lit _) string %.
%sort of {_ exp} {_ tp} %.
%name of %.
%mode of %in %out %.
%term _ %pi (of (ret V) T) %<- (ofv V T) %.
%term _ %pi (of (plus E1 E2) number) %<- (of E1 number) %<- (of E2 number) %.
%term _ %pi (of (append E1 E2) string) %<- (of E1 string) %<- (of E2 string) %.
%term _
  %pi (of (let E1 ([x] E2 x)) T')
  %<- (of E1 T)
  %<- ({x val} %pi (ofv x T) %-> (of (E2 x) T')) %.

Evaluation

Answers

%sort ans %.
%name ans %.
%term anum %pi nat %-> ans %.
%term astr %pi str %-> ans %.
%sort ofa {_ ans} {_ tp} %.
%name ofa %.
%mode ofa %in %out %.
%term _ ofa (anum _) number %.
%term _ ofa (astr _) string %.

Evaluation judgement on raw syntax

%sort eval {_ exp} {_ ans} %.
%mode eval %in %out %.
%term eval/val/num eval (ret (num N)) (anum N) %.
%term eval/val/lit eval (ret (lit S)) (astr S) %.
%term eval/plus
  %pi (eval (plus E1 E2) (anum N))
  %<- (eval E1 (anum N1))
  %<- (eval E2 (anum N2))
  %<- (add N1 N2 N) %.
%term eval/append
  %pi (eval (append E1 E2) (astr S))
  %<- (eval E1 (astr S1))
  %<- (eval E2 (astr S2))
  %<- (cat S1 S2 S) %.
%term eval/let %pi (eval (let E1 ([x] E2 x)) A) %<- (eval E1 (anum N)) %<- (eval (E2 (num N)) A) %.

Evaluation is not total because of run-time type errors! (e.g., try appending two numbers).

%worlds () (eval _ _) %.

STELF gives this error, refering to the first recursive call of eval/plus.

%total E (eval E _) %.