Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Imperative programming / 3 / a / Solution

For finite acyclic chains, define the abstraction function recursively byHere 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}]++{\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.