TD: Abstract Machines

Exercise 1

1. $|\rho {|}_{se{a}_2}=|\rho {|}_{sub}+|H|$

At each $se{a}_2$ transition, the size of the heap is incremented by one, thus so is $|\rho {|}_{sub}+|H|$. And the only way to decrease $|H|$, is to execute a $sub$ transition: $|H|$ is decremented by one iff one $sub$ transition is performed.

That is, once $|H|$ has been increased, $|\rho {|}_{sub}+|H|$ remains constant until another $se{a}_2$ transition is executed.

More concisely: $se{a}_2$ is the only transition incrementing $|H|$, and $sub$ is the only one decrementing it, so $|H|=|\rho {|}_{se{a}_2}-|\rho {|}_{sub}$ holds.

2. $|E|+|H|\le |\rho {|}_{\beta }$

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

3. $|\rho {|}_{se{a}_2}\le |\rho {|}_{\beta ,sub}$

4.

The code is increased in size only by $se{a}_2$. All subterms of the code, stack, heap and the environment are subterms of the initial term $t_0$.

So if we have ${⇝}_{se{a}_1}^k$, then $k\le |t_0|$

Any sequence is of the form:

So

Other possibility: the only way to increase the code size is the perform $se{a}_2$, and between two $se{a}_2$, there can be at most $|t_0|$ $se{a}_1$.

Exercise 2

1.

${⇝}_{sub\circ }$ can be followed only by $\beta$ and $sub\circ$.

Same thing for ${⇝}_{sub\bullet }$.

2.

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 $\beta$’s. So

4.

Note that we have

So:

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