A theorem, also called the iteration theorem, that makes use of the lambda notation introduced by Church. Let 
denote the recursive
function of 
variables with Gödel number 
(where (1) is normally omitted). Then for every 
and 
, there exists a primitive
recursive function 
such that for all 
, 
, ..., 
,
 |
A direct application of the 
-
-
theorem is the fact that there exists a primitive
recursive function 
such that
 |
for all 
and 
.
The 
-
-
theorem is applied in the proof of the recursion theorem.
The 
-
-
theorem is the theoretical premise for a branch of computer
science known as partial evaluation.
