TD: Abstract Machines

Exercise 1

1. $\vert ρ \vert_{sea_2} = \vert ρ \vert_{sub} + \vert H \vert$

At each $sea_2$ transition, the size of the heap is incremented by one, thus so is $\vert ρ \vert_{sub} + \vert H \vert$. And the only way to decrease $\vert H \vert$, is to execute a $sub$ transition: $\vert H \vert$ is decremented by one iff one $sub$ transition is performed.

That is, once $\vert H \vert$ has been increased, $\vert ρ \vert_{sub} + \vert H \vert$ remains constant until another $sea_2$ transition is executed.

More concisely: $sea_2$ is the only transition incrementing $\vert H \vert$, and $sub$ is the only one decrementing it, so $\vert H \vert = \vert ρ \vert_{sea_2} - \vert ρ \vert_{sub}$ holds.

2. $\vert E \vert + \vert H \vert ≤ \vert ρ \vert_β$

Every entry in the environment and/or the heap is an explicit substitution. But explicit substitutions can only be created by $β$ transitions (one $β$ transition ⟹ creation of one explicit substitution).

3. $\vert ρ \vert_{sea_2} ≤ \vert ρ \vert_{β, sub}$

\[\vert ρ \vert_{sea_2} = \vert ρ \vert_{sub} + \vert H \vert ≤ \vert ρ \vert_{sub} + \vert ρ \vert_β - \vert E \vert ≤ \vert ρ \vert_{β, sub}\]

4.

The code is increased in size only by $sea_2$. All subterms of the code, stack, heap and the environment are subterms of the initial term $t_0$.

So if we have $\leadsto^k_{sea_1}$, then $k ≤ \vert t_0 \vert$

Any sequence is of the form:

\[\underbrace{\leadsto^\ast_{sea_1}}_{≤ \vert t_0 \vert} \leadsto^\ast_{¬ sea_1} \underbrace{\leadsto^\ast_{sea_1}}_{≤ \vert t_0 \vert} \leadsto^\ast_{¬ sea_1} ⋯\]

So

\[\vert ρ_{sea_1} \vert ≤ \vert t_0 \vert \cdot \underbrace{\vert ρ_{¬ sea_1} \vert}_{= \vert ρ \vert_β + \vert ρ \vert_{sub} + \vert ρ \vert_{sea_2}} ≤ \vert t_0 \vert \cdot (2 \vert ρ \vert_{β, sub})\]

Other possibility: the only way to increase the code size is the perform $sea_2$, and between two $sea_2$, there can be at most $\vert t_0 \vert$ $sea_1$.

Exercise 2

1.

$\leadsto_{sub\circ}$ can be followed only by $β$ and $sub\circ$.

Same thing for $\leadsto_{sub\bullet}$.

2.

\[\leadsto_{sub\bullet} ≤ \vert ρ \vert_{β, sub \circ}\]

3.

The effect of $sub \circ$ is to turn a white substitution inside $H$ into a black one in $E$ (that will remain black), and white substitutions are created by $β$’s. So

\[\vert ρ \vert_{sub \circ} ≤ \vert ρ \vert_β\]

4.

\[\vert ρ_{sub \circ, sub \bullet} \vert ≤ 3 \vert ρ \vert_β\]

Note that we have

\[\leadsto_{sub \bullet} \leadsto_{sub \circ}^\ast \leadsto_β\]

So:

\[\leadsto_{sub \bullet} ≤ \vert ρ \vert_β + 1\]

Difference between the two machines: the second one avoids detours of putting used substitutions back into the heap.