= Solution
For finite acyclic chains, define the <abstraction function> recursively by
$$
\boxed{\alpha(\mathrm{NIL})=[],\qquad\alpha(p)=[p]\mathbin{+\!+}\alpha(p.\mathrm{tail})\quad(p\ne\mathrm{NIL}).}
$$
Here the <list> contains <linked list nodes> themselves. For an extension storing a value `value`, its value-level <abstraction function> is $\alpha_v(p)=[p.\mathrm{value}]\mathbin{+\!+}\alpha_v(p.\mathrm{tail})$. Finiteness and absence of a <graph cycle> ensure that these recursive definitions terminate. A <dummy header node> is excluded by applying $\alpha$ to its `tail`.
Back to article page
