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 Universal
Turing Machine entry by Xu et al., but different in that it
models partial functions with codomain 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. |
BibTeX: |
@article{Inductive_Inference-AFP,
author = {Frank J. Balbach},
title = {Some classical results in inductive inference of recursive functions},
journal = {Archive of Formal Proofs},
month = aug,
year = 2020,
note = {\url{http://isa-afp.org/entries/Inductive_Inference.html},
Formal proof development},
ISSN = {2150-914x},
}
|