
Using Corollary 6.3.6, show that if X® TX (doesn't depend on G and) is well founded then so is GxX® T( GxX). Without using cartesian closure, formulate and prove directly the parametric version of Proposition 6.3.9, and hence of the General Recursion Theorem 6.3.13.
Explain how the case M = List(X) corresponds to a stack, and how M = N suffices if a does not depend on X. The last map QxM® Q is itself defined by recursion over M: to what part of the execution of a recursive program does it correspond?


