Summer school 2008:Typed arithmetic expressions (extrinsic encoding)

This is Literate Twelf Code: here Status: %% OK %% Output: here.

Summer school 2008

Previous: Typed arithmetic expressions

Next: Exercises 1

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.

Raw syntax

tp : type.				%name tp T.
number : tp.
string : tp.

val : type.				%name val V.
num : nat -> val.
lit : str -> val.

exp : type.				%name exp E.
ret : val -> exp.
plus : exp -> exp -> exp.
append : exp -> exp -> exp.
let : exp -> (val -> exp) -> exp.

Typing judgement on raw syntax

ofv : val -> tp -> type.		%name ofv Dofv.
%mode ofv +V -T.

- : ofv (num _) number.
- : ofv (lit _) string.

of : exp -> tp -> type.			%name of Dof.
%mode of +E -T.

- : of (ret V) T <- ofv V T.
- : of (plus E1 E2) number <- of E1 number <- of E2 number.
- : of (append E1 E2) string <- of E1 string <- of E2 string.
- : of (let E1 ([x] E2 x)) T' <- of E1 T <- ({x:val} ofv x T -> of (E2 x) T').

Evaluation

Answers

ans : type.				%name ans A.
anum : nat -> ans.
astr : str -> ans.

ofa : ans -> tp -> type.		%name ofa Dofa.
%mode ofa +A -T.

- : ofa (anum _) number.
- : ofa (astr _) string.

Evaluation judgement on raw syntax

eval : exp -> ans -> type.
%mode eval +E1 -E2.

eval/val/num
   : eval (ret (num N)) (anum N).

eval/val/lit
   : eval (ret (lit S)) (astr S).

eval/plus
   : eval (plus E1 E2) (anum N)
      <- eval E1 (anum N1)
      <- eval E2 (anum N2)
      <- add N1 N2 N.

eval/append
   : eval (append E1 E2) (astr S)
      <- eval E1 (astr S1)
      <- eval E2 (astr S2)
      <- cat S1 S2 S.

eval/let
   : 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 _ _).

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

%total E (eval E _).

Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)
Error: 
Totality: Output of subgoal not covered
Output coverage error --- missing cases:
{E1:exp} {S1:str} |- eval E1 (astr S1).


%% ABORT %%

Summer school 2008

Previous: Typed arithmetic expressions

Next: Exercises 1