The goal of this lecture note is to implement a continuation-based interpreter (i.e., an interpreter in delimited continuation-passing style, that is to say whose continuation does not have a polymorphic codomain of answers) for the source language of the term project, and to prove that it satisfies the given specification of an interpreter in this term project.
We consider a simple language of arithmetic expressions:
Inductive arithmetic_expression : Type :=
Literal : nat -> arithmetic_expression
| Plus : arithmetic_expression -> arithmetic_expression -> arithmetic_expression
| Minus : arithmetic_expression -> arithmetic_expression -> arithmetic_expression.
Inductive source_program : Type :=
Source_program : arithmetic_expression -> source_program.
Interpreting an arithmetic expression either yields a natural number or it yields an error message due to a subtraction such as 2 - 3:
Inductive expressible_value : Type :=
Expressible_nat : nat -> expressible_value
| Expressible_msg : string -> expressible_value.
The following specification captures what is expected from the interpreter and from its auxiliary evaluation function:
Definition specification_of_evaluate (evaluate : arithmetic_expression -> expressible_value) :=
(forall n : nat,
evaluate (Literal n) = Expressible_nat n)
/\
((forall (ae1 ae2 : arithmetic_expression)
(s1 : string),
evaluate ae1 = Expressible_msg s1 ->
evaluate (Plus ae1 ae2) = Expressible_msg s1)
/\
(forall (ae1 ae2 : arithmetic_expression)
(n1 : nat)
(s2 : string),
evaluate ae1 = Expressible_nat n1 ->
evaluate ae2 = Expressible_msg s2 ->
evaluate (Plus ae1 ae2) = Expressible_msg s2)
/\
(forall (ae1 ae2 : arithmetic_expression)
(n1 n2 : nat),
evaluate ae1 = Expressible_nat n1 ->
evaluate ae2 = Expressible_nat n2 ->
evaluate (Plus ae1 ae2) = Expressible_nat (n1 + n2)))
/\
((forall (ae1 ae2 : arithmetic_expression)
(s1 : string),
evaluate ae1 = Expressible_msg s1 ->
evaluate (Minus ae1 ae2) = Expressible_msg s1)
/\
(forall (ae1 ae2 : arithmetic_expression)
(n1 : nat)
(s2 : string),
evaluate ae1 = Expressible_nat n1 ->
evaluate ae2 = Expressible_msg s2 ->
evaluate (Minus ae1 ae2) = Expressible_msg s2)
/\
(forall (ae1 ae2 : arithmetic_expression)
(n1 n2 : nat),
evaluate ae1 = Expressible_nat n1 ->
evaluate ae2 = Expressible_nat n2 ->
n1 <? n2 = true ->
evaluate (Minus ae1 ae2) = Expressible_msg (String.append "numerical underflow: -" (string_of_nat (n2 - n1))))
/\
(forall (ae1 ae2 : arithmetic_expression)
(n1 n2 : nat),
evaluate ae1 = Expressible_nat n1 ->
evaluate ae2 = Expressible_nat n2 ->
n1 <? n2 = false ->
evaluate (Minus ae1 ae2) = Expressible_nat (n1 - n2))).
Definition specification_of_interpret (interpret : source_program -> expressible_value) :=
forall evaluate : arithmetic_expression -> expressible_value,
specification_of_evaluate evaluate ->
forall ae : arithmetic_expression,
interpret (Source_program ae) = evaluate ae.
We shall first implement a continuation-based evaluator:
Fixpoint evaluate_cb (ae : arithmetic_expression) (k : nat -> expressible_value) : expressible_value :=
...
In words: when evaluating evaluate_cb ae k, if k is applied to a natural number, then this natural number is the result of evaluating ae. Otherwise, the result is an error message.
We shall then implement an interpreter that calls the continuation-based evaluator by supplying it an appropriate initial continuation:
Definition interpret (sp : source_program) : expressible_value :=
match sp with
Source_program ae =>
evaluate_cb ae (fun (n : nat) => Expressible_nat n)
end.
And we shall then prove that this interpreter satisfies specification_of_interpret:
Theorem interpret_satisfies_specification_of_interpret :
specification_of_interpret interpret.
The following Eureka lemma captures that for any arithmetic expression ae,
either evaluating ae as specified yields a number n and for any given continuation k, evaluating ae with k reduces to applying k to n,
or evaluating ae as specified yields an error message s and for any given continuation k, evaluating ae with k reduces to s:
Lemma about_evaluate_cb :
forall evaluate : arithmetic_expression -> expressible_value,
specification_of_evaluate evaluate ->
forall ae : arithmetic_expression,
(exists n : nat,
evaluate ae = Expressible_nat n
/\
forall k : nat -> expressible_value,
evaluate_cb ae k = k n)
\/
(exists s : string,
evaluate ae = Expressible_msg s
/\
forall k : nat -> expressible_value,
evaluate_cb ae k = Expressible_msg s).
This lemma is proved by structural induction on ae and the theorem follows as a corollary.