# Theory Partial_Recursive

chapter ‹Partial recursive functions›
theory Partial_Recursive
imports Main "HOL-Library.Nat_Bijection"
begin
text ‹This chapter lays the foundation for Chapter~\ref{c:iirf}.
Essentially it develops recursion theory up to the point of certain
fixed-point theorems. This in turn requires standard results such as the
existence of a universal function and the $s$-$m$-$n$ theorem. Besides these,
the chapter contains some results, mostly regarding decidability and the
Kleene normal form, that are not strictly needed later. They are included as
relatively low-hanging fruits to round off the chapter.
The formalization of partial recursive functions is very much inspired by the
Universal Turing Machine AFP entry by Xu
et~al.~\<^cite>‹"Universal_Turing_Machine-AFP"›. It models partial recursive
functions as algorithms whose semantics is given by an evaluation function.
This works well for most of this chapter. For the next chapter, however, it
is beneficial to regard partial recursive functions as ``proper'' partial
functions. To that end, Section~\ref{s:alternative} introduces more
conventional and convenient notation for the common special cases of unary
and binary partial recursive functions.
Especially for the nontrivial proofs I consulted the classical textbook by
Rogers~\<^cite>‹"Rogers87"›, which also partially explains my preferring the
traditional term ``recursive'' to the more modern ``computable''.›
section ‹Basic definitions›
subsection ‹Partial recursive functions›
text ‹To represent partial recursive functions we start from the same
datatype as Xu et~al.~\<^cite>‹"Universal_Turing_Machine-AFP"›, more specifically
from Urban's version of the formalization. In fact the datatype @{text recf}
and the function @{text arity} below have been copied verbatim from it.›