Theory Recursion
section ‹General Recursion›
theory Recursion imports Iteration
begin
text‹The initiality theorems from the previous section support iteration principles.
Next we extend the results to general recursion. The difference between
general recursion and iteration is that the former also considers
the (source) ``items" (terms and abstractions), and not only the
(target) generalized items, appear in the recursive clauses.
(Here is an example illustrating the above difference for the standard case
of natural numbers:
\\- Given a number n, the operator ``add-n" can be defined by iteration:
\\--- ``add-n 0 = n",
\\--- ``add-n (Suc m) = Suc (add-n m)".
Notice that, in right-hand side of the recursive clause, ``m" is not used ``directly", but only
via ``add-n" -- this makes the definition iterative. By contrast, the following
definition of predecessor is trivial form of recursion (namely, case analysis),
but is {\em not} iteration:
\\--- ``pred 0 = 0",
\\--- ``pred (Suc n) = n".
)
We achieve our desired extension by augmenting the notion of model
and then essentially inferring recursion (as customary)
from
[iteration having as target the product between the term model and the original model].
As a matter of notation: remember we are using for generalized items
the same meta-variables as for ``items" (terms and abstractions).
But now the model operators will take both items and generalized items.
We shall prime the meta-variables for items (as in X', A', etc).
›
subsection ‹Raw models›