5
$\begingroup$

I'm trying to prove the correctness of an interpreter for a simple extension of untyped lambda-calculus with De Bruijn indices. The interpreter is bounded, i.e. in order to ensure its finiteness it has an additional parameter $n \in \mathbb N$ that decreases with each recursive call. The function returns $\bot$ when $n = 0$.

This is the signature of the interpreter: $\mathcal E : (\mathbb N, Env, E) \to (Val \cup \{\bot\})$

Where $Env$ is the set of environments, represented as lists of values accessed with De Bruijn indices, $E$ is the set of expressions and $Val$ is the set of values:

$$ \begin{aligned} E &::= \lambda E \mid EE \mid A \mid B \mid \texttt{if } E \texttt{ then } E \texttt{ else } E \mid x \in Var \mid V\\ A &::= \textit{integer operations...} \\ B &::= \textit{boolean operations...} \\ V &::= \texttt{True} \mid \texttt{False} \mid c \in \mathbb Z \mid \texttt{Closure} (\rho, E) \end{aligned} $$

Soundness theorem

$$\forall e, \rho, n, v . \mathcal E (n, \rho, e) = v \implies \langle e, \rho \rangle \to^* v$$

I.e.: If $e$ evaluates to $v$ under the initial environment $\rho$ and in a finite number of steps, then there exists a finite proof that it does, which uses the rules of the small-step semantics I describe in the "appendix" of this post.

Proof Attempt Sketch

I tried to prove the theorem by induction on $e$.

Base Cases

The base cases are lambdas, values and variables. I managed to prove these cases with ease.

  • Lambdas: Let $e = \lambda e'$. First off, the case in which $n = 0$ can be eliminated, since it makes the premise of the theorem false (ex falso...). If $n = Sm$, by the definition of the interpreter we get that the value $v$ must be $\texttt{Closure}(\rho, e')$. The case can be shown to work by applying the LAMBDA rule, some properties of the star closure and the VALUE rule.
  • Values: trivial.
  • Variables: Use rule VAR-KO to eliminate the case in which the variable is not in the environment. Then, it's a matter of applying the VAR-OK rule and the definition of the interpreter, plus some property of the star closure.
Inductive cases (problem is here!!!)

The most complex inductive case, and the one that is giving me problems, is the case of application: $e = e_1e_2$. The inductive HPs are: $$ \forall \rho, n, v . \mathcal E (n, \rho, e_1) = v \implies \langle e_1, \rho \rangle \to^* v \quad \text{(IHe1)} $$ $$ \forall \rho, n, v . \mathcal E (n, \rho, e_2) = v \implies \langle e_2, \rho \rangle \to^* v \quad \text{(IHe2)} $$

By applying these to the definition of $\mathcal E$ and doing some case checking (the evaluations of $e_1$ and $e_2$ cannot be $\bot$ by Hp), from the inductive hypotheses we obtain that for some $\rho'$ and $e'$:

$$ \forall \rho, n \langle e_1, \rho \rangle \to^* \texttt{Closure}(\rho', e') $$

and for some $v'$:

$$ \forall \rho, n, \langle e_2, \rho \rangle \to^* v' $$

At this point we use an auxiliary lemma:

If $\langle e_1, \rho \rangle \to^* \texttt{Closure}(\rho', e')$ and $\langle e_2, \rho \rangle \to^* v'$, then: $$ \langle e_1e_2, \rho\rangle \to^* \langle \texttt{Closure}(\rho', e') v', \rho\rangle$$

Which is easily shown by induction.

We thus obtain: $$ \langle e_1e_2, \rho\rangle \to^* \langle e', \texttt{bind} (\rho', v') \rangle $$ and: $$ \mathcal E (S m, \rho, e_1e_2) = \mathcal E (m, \texttt{bind}(\rho', v'), e') = v $$

But we have no induction hypothesis on $e'$, of the form:

$$ \forall \rho, n, v . \mathcal E(n, \rho, e') = v \implies \langle e', \rho \rangle \to^* v \quad \text{(Fake-Hp)} $$

which would allow us to conclude the proof. Do you have any suggestions on how I should finish the proof I sketched in this post?

Appendix: Interpreter definition and semantics

What follows is a partial definition of the interpreter (leaving out the non-relevant portions..)

$$ \begin{aligned} \mathcal E (0, \_, \_) &:= \bot\\ \mathcal E (S n, \rho, \lambda e) &:= \texttt{Closure}(\rho, e)\\ \mathcal E (S n, \rho, v) &:= v &\text{$v \in Val$}\\ \mathcal E (S n, \rho, e_1e_2) &:= \begin{cases} \mathcal E (n, \texttt{bind}(\rho', \mathcal E(n, \rho, e_2)), e) & \text{if } \mathcal E (n, \rho, e_1) = \texttt{Closure}(\rho', e) \\ \bot &\text{otherwise} \end{cases} \\ \mathcal E (S n, \rho, x) &:= \begin{cases} \mathcal E (n, \rho, \rho[x]) & \text{if $\rho[x] \neq \bot$}\\ \bot & \text{otherwise} \end{cases} &\text{$x \in Var$}\\ \end{aligned} $$ Now for the small-step semantics: The intermediate values of the computation have form $\langle e, \rho \rangle$ where $\rho$ is the environment of evaluation. The termination values are the elements of the set $V' = V \cup\{\bot\}$, where $$V = \{\texttt{True}, \texttt{False}, \texttt{Closure}(e, \rho), c \in \mathbb Z\}$$

  • Law for transforming lambdas into closures $$ \dfrac{}{\langle \lambda e, \rho \rangle \to \langle \texttt{Closure} (\rho, e), \rho \rangle}\label{redlambda} \quad \text{(LAMBDA)}$$
  • For all values $v \in Val$: $$ \dfrac{}{\langle v, \rho \rangle \to v} \quad \text{(VALUE)}$$
  • Laws for variables: $$ \dfrac {\rho[x] = v}{\langle x, \rho \rangle \to v} \quad \text{(VAR-OK)} $$ $$ \dfrac {\rho[x] = \bot}{\langle x, \rho \rangle \to \bot} \quad \text{(VAR-KO)} $$
  • Laws for application: $$ \dfrac{\langle e_1 , \rho \rangle \to \langle e_1' , \rho \rangle} {\langle e_1 e_2, \rho \rangle \to \langle e_1' e_2, \rho \rangle}\quad\text{(APPLY-1)}$$

$$ \dfrac{\langle e_2, \rho \rangle \to \langle e_2', \rho \rangle} {\langle v_1 e_2, \rho \rangle \to \langle v_1 e_2', \rho \rangle}\quad\text{(APPLY-2)}$$

$$ \dfrac{} {{\langle (\texttt{Closure} (\rho', e)) v_2, \rho \rangle \to \langle e, \texttt{bind} (\rho', v_2) \rangle}}\quad\text{(APPLY-3)}$$

Where bind adds $v_2$ to the environment, adding it "on top" of the list that represents it.

$$ \dfrac{}{\langle v\, e_2, \rho \rangle \to \bot} \quad\text{(APPLY-KO)} $$

$\endgroup$
2
  • $\begingroup$ And what you're trying to prove is true? $\endgroup$ Commented Feb 3 at 14:03
  • $\begingroup$ @AndrejBauer I think it should. The rules and interpreter are fairly simple, and I made them side by side. What's your take on this? $\endgroup$ Commented Feb 3 at 14:27

1 Answer 1

3
+25
$\begingroup$

You must strengthen the theorem to be proved by induction. In the $e_1e_2$ case, the current induction hypothesis just tells you that $e_1$ reduces to a closure, but not anything more about how the enclosed expression reduces. Another hint that something is missing is that in the $\lambda x . e$ case (and the closure case which is hidden under "values"), you don't make use of the induction hypothesis on $e$, which is precisely about how $e$ reduces.

You will have more luck with a proof by induction on a recursive property like the following:

$P(e) = ``\forall n \rho v,\; \mathcal{E}(n,\rho,e) = v \implies (\rho,e) \to^\star v \wedge (\forall \rho' e',\; v = \mathbf{Closure}(\rho',e') \implies P(e'))"$

This creates new problems that you will have to figure out (Now it's too strong for the case of variables, how to weaken it a bit? Is this recursive property even well-defined? (if not, how to make it so?)). Hopefully this gets the ball rolling for you.

$\endgroup$
1
  • $\begingroup$ I'm certain your suggestion is on the right track; I did not manage to complete the proof but I feel like this got me closer. Thanks :) $\endgroup$ Commented Feb 20 at 18:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.