\documentclass[11pt,a4paper]{report}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}

\usepackage[top=3cm,bottom=3cm]{geometry}

\usepackage{amssymb}  % for \mathbb

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

\begin{document}

\title{Some classical results in inductive inference of recursive functions}
\author{Frank J. Balbach}
\maketitle

\begin{abstract}
This entry formalizes some classical concepts and results from inductive
inference of recursive functions. In the basic setting a partial recursive
function (``strategy'') must identify (``learn'') all functions from a set
(``class'') of recursive functions. To that end the strategy receives more and
more values $f(0), f(1), f(2), \ldots$ of some function $f$ from the given class
and in turn outputs descriptions of partial recursive functions, for example,
Gödel numbers. The strategy is considered successful if the sequence of outputs
(``hypotheses'') converges to a description of $f$. A class of functions
learnable in this sense is called ``learnable in the limit''. The set of all
these classes is denoted by LIM.

Other types of inference considered are finite learning (FIN), behaviorally
correct learning in the limit (BC), and some variants of LIM with restrictions
on the hypotheses: total learning (TOTAL), consistent learning (CONS), and
class-preserving learning (CP). The main results formalized are the proper
inclusions $\mathrm{FIN} \subset \mathrm{CP} \subset \mathrm{TOTAL} \subset
\mathrm{CONS} \subset \mathrm{LIM} \subset \mathrm{BC} \subset 2^{\mathcal{R}}$,
where $\mathcal{R}$ is the set of all total recursive functions.  Further
results show that for all these inference types except CONS, strategies can be
assumed to be total recursive functions; that all inference types but CP are
closed under the subset relation between classes; and that no inference type is
closed under the union of classes.

The above is based on a formalization of recursive functions heavily inspired by
the \emph{Universal Turing Machine} entry by
Xu~et~al.~\cite{Universal_Turing_Machine-AFP}, but different in that it models
partial functions with codomain \emph{nat option}. The formalization contains a
construction of a universal partial recursive function, without resorting to
Turing machines, introduces decidability and recursive enumerability, and proves
some standard results: existence of a Kleene normal form, the $s$-$m$-$n$
theorem, Rice's theorem, and assorted fixed-point theorems (recursion theorems)
by Kleene, Rogers, and Smullyan.
\end{abstract}

\tableofcontents

\newpage

% sane default for proof documents
\parindent 0pt\parskip 0.5ex

% generated text of all theories
\input{session}

\bibliographystyle{abbrv}
\bibliography{root}

\end{document}
