# Closures break induction in correctness proof of interpreter

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)}$$

• And what you're trying to prove is true? Commented Feb 3 at 14:03
• @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? Commented Feb 3 at 14:27

## 1 Answer

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.

• 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 :) Commented Feb 20 at 18:54