Proofs: Innermost reduction

The stack machine performs exactly the leftmost-innermost reduction full

This proof shows: correctness.

We use the pseudocode of the page and the notation of the term rewriting pages. $R$ is a list of rules $l_1 \to r_1, \ldots, l_m \to r_m$, each with $l_j \notin V$ and $\mathrm{Var}(r_j) \subseteq \mathrm{Var}(l_j)$. For a term $s$ whose arguments are all normal forms, the root rule of $s$ is the first $l_j \to r_j$ in the list with a match $\tau$, $l_j\tau = s$, if there is one.

Leftmost-innermost reduction. A redex of $t$ is a position $p$ such that $t|_p$ is an instance of some left side. It is innermost if no position strictly below $p$ is a redex. Two different innermost redexes are not prefixes of each other, so they are ordered from left to right by the lexicographic order of positions. The leftmost-innermost step contracts the leftmost innermost redex with the first rule of the list that matches there. Write $\mathrm{LI}(t)$ for the sequence of leftmost-innermost steps from $t$; it is finite and ends in a normal form, or it is infinite.

Lemma 1 (decomposition). Let $t = f(w_1, \ldots, w_n)$. Then $\mathrm{LI}(t)$ is the concatenation of: $\mathrm{LI}(w_1)$ placed at position $1$; if it ends in $v_1$, then $\mathrm{LI}(w_2)$ placed at position $2$; and so on; and, if all of them end, with $s = f(v_1, \ldots, v_n)$: nothing if $s$ is a normal form, otherwise the root step $s \to r_j\tau$ by the root rule of $s$ followed by $\mathrm{LI}(r_j\tau)$.

Proof. Let $i$ be least such that $w_i$ is not a normal form. Every redex of $t$ is either the root or below some position $k$. The root is not innermost, since $w_i$ has a redex. A redex $kq$ with $k > i$ lies to the right of every redex $iq'$, and $w_i$ has an innermost redex $q'$, which is innermost in $t$ too, because the positions below $iq'$ in $t$ are those below $q'$ in $w_i$. Redexes below $k < i$ do not exist. So the leftmost-innermost redex of $t$ is $i$ followed by the leftmost-innermost redex of $w_i$, with the same rule, and the step changes only the argument $w_i$. Repeating this, $t$ is reduced inside $w_i$ exactly as $\mathrm{LI}(w_i)$ reduces $w_i$, as long as that sequence goes on. If it ends, we continue with the next argument that is not a normal form. When all arguments are normal forms, the only possible redex is the root, which is then innermost; the step uses the root rule. $\square$

Lemma 2 (substituted values are normal). If all arguments of $s$ are normal forms and $l\tau = s$ with $l \notin V$, then $x\tau$ is a normal form for each $x \in \mathrm{Var}(l)$.

Proof. $x$ occurs in $l$ at some position $q \ne \varepsilon$, since $l$ is not a variable. Then $x\tau = s|_q$ is a subterm of an argument of $s$, and a subterm of a normal form is a normal form. $\square$

The machine. A task $\mathrm{EVAL}(u, \sigma, p)$ asks for the normal form of $u\sigma$, where every value of $\sigma$ is a normal form (for the input term, $\sigma$ is empty; a variable of the input is a normal form, because no left side is a variable). The position $p$ is where $u\sigma$ sits in the whole term, and is used only for the trace.

Lemma 3 (one task). Suppose the machine pops $\mathrm{EVAL}(u, \sigma, p)$ with task stack $T$ below it and value stack $W$. Then, before the task stack returns to $T$, the machine makes exactly the steps of $\mathrm{LI}(u\sigma)$, each at $p$ followed by the position of the step in $u\sigma$, and with the same rule. If $\mathrm{LI}(u\sigma)$ is finite and ends in $v$, the machine reaches the state with task stack $T$ and value stack $W\,v$. If it is infinite, the task stack never returns to $T$. (With a bound $B$, the machine stops at line L9 when it is about to make its $(B+1)$-st step; up to that moment the same statement holds for the steps made.)

Proof. We show, for each $N \ge 0$, that the first $N$ steps the machine makes during the task (if it makes that many) are the first $N$ steps of $\mathrm{LI}(u\sigma)$, and that the finite-case conclusion holds whenever $\mathrm{LI}(u\sigma)$ has fewer than $N$ steps. This is by induction on $N$, and inside it by induction on the size of $u$.

If $u$ is a variable, line L4 pushes $u\sigma$, which is a normal form, and makes no step: $\mathrm{LI}(u\sigma)$ is empty, and the claim holds.

If $u = f(u_1, \ldots, u_n)$, line L5 pushes $\mathrm{BUILD}(f, n, p)$ and the tasks $\mathrm{EVAL}(u_i, \sigma, p\,i)$ with $u_1$ on top. The machine pops $\mathrm{EVAL}(u_1, \sigma, p\,1)$ first. Since $u_1$ is smaller than $u$, the inner induction hypothesis applies: the machine makes the steps of $\mathrm{LI}(u_1\sigma)$ at $p\,1$, and if they end in $v_1$, it pushes $v_1$ and goes on with $u_2$, and so on. If one of these sequences is infinite, the machine never pops the $\mathrm{BUILD}$ task, and by Lemma 1 $\mathrm{LI}(u\sigma)$ is that same infinite sequence after the finite ones before it. Otherwise the machine pops $\mathrm{BUILD}(f, n, p)$ with $v_1, \ldots, v_n$ on top of $W$ in this order; line L6 takes them off and forms $s = f(v_1, \ldots, v_n)$. Line L7 finds the root rule of $s$. If there is none, $s$ is a normal form, line L8 pushes it, and by Lemma 1 the steps made are exactly $\mathrm{LI}(u\sigma)$, which ends in $s$. If there is one, $l_j \to r_j$ with match $\tau$, line L10 makes the root step $s \to r_j\tau$ at $p$, which is the next step of $\mathrm{LI}(u\sigma)$ by Lemma 1, and pushes $\mathrm{EVAL}(r_j, \tau, p)$. By Lemma 2 the values of $\tau$ are normal forms, so this task has the required form. The machine has already made at least one step during the task, so fewer than $N$ steps remain to be compared, and the outer induction hypothesis (for a smaller $N$, with $u$ arbitrary) applies to the new task: its steps are those of $\mathrm{LI}(r_j\tau)$ at $p$, and if they end in $v$, it pushes $v$ and the task stack is $T$ again. By Lemma 1 this is the rest of $\mathrm{LI}(u\sigma)$.

The bound only stops the machine before a step, so it does not change the steps made before it. $\square$

Theorem. On input $t$, $R$ and no bound, the algorithm returns $(v, k)$ exactly when $\mathrm{LI}(t)$ is finite with $k$ steps and ends in the normal form $v$, and the recorded trace is $\mathrm{LI}(t)$. If $\mathrm{LI}(t)$ is infinite, the algorithm does not stop. With a bound $B$, it returns $(v, k)$ when $\mathrm{LI}(t)$ has $k \le B$ steps, and it returns $\bot$ after exactly $B$ steps otherwise.

Proof. Line L1 starts with the single task $\mathrm{EVAL}(t, \emptyset, \varepsilon)$, $T$ and $W$ empty. Apply Lemma 3. In the finite case the task stack becomes empty with $W = v$, the loop of line L2 ends, and line L11 returns $v$ and the step count, which line L10 increased once per step. In the infinite case the task stack never empties. With a bound $B$, line L9 returns $\bot$ exactly when a $(B+1)$-st step is about to be made, that is, when $\mathrm{LI}(t)$ has more than $B$ steps. The returned $v$ is a normal form of $t$ because each step is a step of $\to_R$, and the end of $\mathrm{LI}(t)$ has no redex. $\blacksquare$