% This is in plain Tex.

% FORMATING
\magnification=\magstep1
\nopagenumbers
\font\eightrm=cmr8
\font\eighttt=cmtt8
\hsize=11cm
\vsize=17.5cm
\voffset=2\baselineskip
\hoffset=1.7truecm
\headline={\Headline}
\def\Headline{\ifnum\pageno=1 \hfil \else\ifodd\pageno%
   \righthead\else\lefthead\fi\fi}
\def\lefthead{\hfil{\eightrm EDWARD NELSON}\hfil}
\def\righthead{\hfil{\eightrm RAMIFIED RECURSION AND INTUITIONISM} \hfil}
\def\foot#1{
  {\baselineskip=9pt 
   \setbox\strutbox=\hbox{\vrule height7pt depth2pt width0pt}%
   \def\textindent##1{\llap{##1}}%
   \def\sl{\eightsl}\def\bf{\eightbf}\def\rm{\eightrm}%
   \eightrm\footnote{}{#1}}}
\def\footnoterule{}
\skip\footins=\medskipamount

%MACROS
\def\W{\hbox{$\cal W$}}
\def\z{{0}}
\def\o{{1}}
\def\epsi{\hbox{$\epsilon$}}
\def\forallst{\forall^{\rm st}}
\def\existsst{\exists^{\rm st}}
\def\impst{\buildrel \rm st \over \to}
\def\iff{\allowbreak\hskip8pt plus2pt minus3pt\mathrel{\hbox{$\leftrightarrow$}}\
hskip8pt plus2pt minus3pt}
\def\iffF{\allowbreak\leftrightarrow}
\def\imp{\allowbreak\hskip8pt plus2pt minus3pt\mathrel{\hbox{$\rightarrow$}}\hskip8pt plus2pt minus3pt}
\def\impP{\allowbreak\rightarrow}
\def\andD{\allowbreak\mathrel{\&}}
\def\and{\allowbreak\hskip7pt plus2pt minus3pt\mathrel{\&}\hskip7pt plus2pt minus
3pt}
\def\orR{\allowbreak\kern1pt\lor\kern1.25pt}
\def\or{\allowbreak\hskip7pt plus2pt minus3pt\mathrel{\hbox{$\vee$}}\hskip7pt plus2pt minus3pt}
\def\Pair(#1,#2){\langle#1,#2\rangle}
\def\Sing(#1){\{#1\}}
\def\ii#1.{{\it#1}}
\def\.{\cdot}
\def\ro#1{{\rm #1}}
\def\S{{\rm S}}
\def\secsign{\mathhexbox 278}

%TEXT
\phantom.\bigskip

\centerline{\bf RAMIFIED RECURSION AND INTUITIONISM}\medskip

\centerline{\it Edward Nelson}\smallskip

\centerline{\it Department of Mathematics}\smallskip

\centerline{\it Princeton University}\bigskip

Both Jean-Louis Callot and Georges Reeb had a strong interest in the 
relationship between computers and nonstandard analysis, and Reeb
was a dedicated intuitionist. These are the themes of this talk
given to honor their memory. First I shall give a brief introduction
to recent work on ramified recursion, expressed in language familiar
to nonstandard analysts, and then I shall sketch an approach to a
constructive logic of the feasible.
\foot{\noindent 
{\eighttt http://www.math.princeton.edu/$\scriptstyle\sim$nelson/papers.html}
is the URL for this paper. It is in the public domain.}
\bigskip

\centerline{\bf I.~Ramified recursion}\medskip

The 1930s witnessed a flowering of mathematical logic. One of the
achievements of this period was the creation by Turing, G\"odel,
and Church of the theory of recursive functions, work that laid
the theoretical foundations for the study of computers. With the
advent of high-speed computers, attention focused on {\it feasible\/}
computations as opposed to computations possible in principle.

The usual model for a feasible computation is that of {\it polynomial
time functions}, functions that can be evaluated in time that is
bounded by a polynomial in the lengths of their arguments. This
notion is robust under changes in the model of computation
(Turing machine, register machine, etc.). If a class of functions
is characterized by time of evaluation, if it is closed under 
composition (and this is necessary to have a sensible theory), and
if it contains one function requiring time $|x|^{1+\varepsilon}$
(where $|x|$ is the length of the argument~$x$ and
$\varepsilon>0$), then it contains all polynomial time
functions. On the other hand, a function that is not polynomial time
cannot be regarded as feasible for all arguments. But is must be
emphasized that the notion is an abstract one, not to be confounded
with the pragmatic notion of a function that is computable in
practice.

Let me observe that I am using the familiar word ``function'' when
``construction of a function'' would be more precise. We are 
dealing not with Platonic functions, two of which are the same if
they have the same values (whatever that may mean), but with
{\it programs}.

It is well known that there is no syntactical description of all
(total) recursive functions. If there were a list of them all, then
Cantor's diagonal argument would yield another. G\"odel cut this
Gordian knot by giving a Platonic definition of recursive function.
A recursive function is a program that terminates for all inputs,
and Turing showed that the halting problem (to decide whether a
program terminates for all inputs) is undecidable.

But Cantor's diagonal argument does not apply to the class of polynomial
time functions and this raises the question as to whether a
syntactical characterization of the class is possible. The answer is
yes, as was proved in a fundamental paper~[1] by Stephen Bellantoni
and Stephen Cook. A complete account, together with related
developments, is in Bellantoni's thesis~[2]. Here I shall follow
the beautiful treatment by Daniel Leivant~[3], with some changes
in terminology derived from nonstandard analysis.

Let \W\ be the {\it free word algebra\/} with the constant~\epsi\ 
(denoting the empty string) and the unary functions~\z\ and \o.
Thus \W\ consists of all strings of zeroes and ones. We call
certain strings {\it standard}, with the assumptions that \epsi\ is
standard and if $x$ is standard, so are $\z x$ and $\o x$.

Consider the smallest class of functions mapping $\W^n$, for some~$n$
depending on the function, to~\W, containing \epsi, \z, and \o,
closed under composition, and closed under {\it string recursion\/};
i.e., such that if $g_{\epsi}$, $g_{\z}$, and~$g_{\o}$ are in the class
then so is~$f$ defined by
$$\eqalign{f(\epsi,\vec x)&=g_{\epsi}(\vec x),\cr
f(\z y,\vec x)&=g_{\z}\big(y,\vec x,f(y,\vec x)\big),\cr
f(\o y,\vec x)&=g_{\o}\big(y,\vec x,f(y,\vec x)\big).\cr}$$
This is the class of {\it primitive recursive functions\/} on~\W,
and it contains many infeasible functions.

Let us make a slight change. Consider functions~$f$ some of whose
arguments are required to be standard; we write them before a semicolon,
so that in $f(\vec z;\vec w)$ the~$\vec z$ are standard and the~$\vec w$
are arbitrary. Such functions are called {\it sorted}. Then we modify
recursion by requiring that $f$~be defined only for standard~$y$,
but with the recursion arguments of $g_0$ and~$g_1$ unrestricted.
That is, {\it ramified recursion\/} is constructed as follows:
$$\eqalign{f(\epsi,\vec z;\vec w)&=g_{\epsi}(\vec z;\vec w),\cr
f(\z y,\vec z;\vec w)&=g_{\z}\big(y,\vec z;\vec w,f(y,\vec z;\vec w)\big),\cr
f(\o y,\vec z;\vec w)&=g_{\o}\big(y,\vec z;\vec w,f(y,\vec z;\vec w)\big).\cr}$$
Let $\cal P$ be the smallest class of functions containing \epsi, \z, and \o\ 
and closed under composition and ramified recursion; then the main theorem is
that the functions in~$\cal P$ all of whose arguments are standard is 
precisely the class of polynomial time functions.

This is a beautiful and astonishing result. The proof is ingenious and not
very long. Notice that there is no arithmetic in the hypotheses of the 
theorem; the polynomial bounds are a consequence of ramified recursion.
There are many related results and I urge you to read the references.\bigskip

\centerline{\bf II.~Intuitionism}\medskip

The results of Bellantoni, Cook, and Leivant concern functions. It seems
worthwhile to construct a full-fledged logic of the feasible, and I shall
sketch how this might be done. Such a logic must be constructive, so I begin
with a brief review of intuitionism.

Stephen Cole Kleene was the mathematician who saw most deeply
into the nature of
intuitionism, with his notion of {\it recursive realizabilility\/}; see [4]
and~[5]. I shall discuss realizability for formulas of arithmetic; the
modifications necessary to discuss the free word algebra~\W\ are minor;
for example, induction for~\W\ should be formulated as
$$\rm A_x(\epsi)\and \forall x[A\imp A_x(\z x)\and A_x(\o x)] \imp A.$$
The function symbols are~0, S ({\it successor\/}), +, and $\cdot$.
The logical operators are 
$$\neg\ \andD\ \impP\ \forall\ \orR\ \exists$$
We can eliminate $\neg$ by regarding $\rm\neg A$ as an abbreviation for
$\rm A\impP \S0=0$. The intuitionistic semantics is epistemological,
rather than ontological like the classical semantics, and to an intuitionist
a formula is an incomplete communication of knowledge.

The notion of realizability is most simply expressed by introducing some
{\it additional function symbols}. Listed with variables to show the
placement of arguments, these are
$$\Pair(x,y)\quad\pi_1x\quad\pi_2x\quad\gamma(x,y,z)\quad
x\Sing(y)\quad\rho(x,y)\quad\Lambda xy.$$

A \ii code.\/ is a term formed with these function symbols and the
function symbols of arithmetic such that the first argument of each
occurrence of~$\Lambda$ is a variable.
I have called $\Lambda$ a function symbol, but in many
respects it is similar to a quantifier symbol.
An occurrence of the variable~x in the code~c is
{\it $\Lambda$-free\/} in case it is not in a part of~c of the
form $\rm\Lambda xb$.
We use the abbreviation $\rm c_x(b)$ for the code
obtained by substituting~b for all
$\Lambda$-free occurrences of~x in~c, with the tacit understanding that
b~is \ii $\Lambda$-substitutable.\/ for~x in~c (meaning
that there is no $\Lambda$-free occurrence of~x
in any part $\rm\Lambda yd$ of~c where y~occurs in~b),
and similarly for
$\rm c_{x_1\ldots x_\nu}(b_1\ldots b_\nu)$.

We use n to stand for a variable-free term of arithmetic.
A code is {\it reduced\/} by making the following replacements
as long as possible, say in
the order listed:\medbreak

\halign{\hfil\qquad\qquad#&\qquad$\rm#$\hfil&\qquad$\rm#$\hfil\cr
&replace\colon&by\colon\cr
\noalign{\vskip6pt}
(R1)&\pi_1\langle a,b\rangle&a\cr
(R2)&\pi_2\langle a,b\rangle&b\cr
(R3)&\gamma(a,b,\langle1,c\rangle)&a\{c\}\cr
(R4)&\gamma(a,b,\langle2,c\rangle)&b\{c\}\cr
(R5)&\rho(n+0,c)&\rho(n,c)\cr
(R6)&\rho(n+Sm,c)&\rho(S(n+m),c)\cr
(R7)&\rho(n\.0,c)&\rho(0,c)\cr
(R8)&\rho(n\.Sm,c)&\rho(n\.m+n,c)\cr
(R9)&\rho(0,c)&\pi_1c\cr
(R10)&\rho(Sn,c)&\big((\pi_2c)\{n\}\big)\{\rho(n,c)\}\cr
(R11)&(\Lambda xa)\{b\}&a_x(b)\cr}\medbreak

Notice that with incorrect code, such as
$$\rm(\Lambda xx\{x\})\{\Lambda xx\{x\}\},$$
this process may never terminate. We use $$\rm c\Rightarrow c'$$
to indicate that the code~c reduces to~$\rm c'$.

The reduction rules (R1)--(R11) express the intended meaning of the
additional function symbols. The ordered pair $\rm\Pair(a,b)$ has
first and second projections~$\pi_1$ and~$\pi_2$. The
value of the function~a on the argument~b is $\rm a\Sing(b)$. 
These are not necessarily
numerical-valued functions, but code-valued functions where the code
may itself be a function. Since the reduction rules are given
explicitly, these are recursive functions, but since the process
may not terminate, they are partial functions. We use~$\gamma$ 
to choose which of two functions~a and~b to apply to the
argument~c. We use~$\rho$ for recursion: the rules (R5)--(R8)
convert~n to a numeral, (R9)~gives the beginning of the recursion,
and (R10)~gives the recursion step. By~(R11), $\rm\Lambda xa$ is
the partial function taking~b to what (if anything)
$\rm a_x(b)$ reduces to.

Now we can define ``c realizes C'', where
c~is a $\Lambda$-closed code and C~is a closed formula:
\medskip

(C1)~if C is atomic, c realizes C in case
C is true;\smallskip

(C2)~if C is $\rm A\andD B$, c realizes C in case $\rm\pi_1c$
realizes~A and $\rm\pi_2c$ realizes~B;\smallskip

(C3)~if C is $\rm A\impP B$, c realizes C in case for all~a, if a
realizes~A, then $\rm c\Sing(a)$ realizes~B;\smallskip

(C4)~if C is $\rm\forall xA$, c realizes C in case for all
n, $\rm c\Sing(n)$ realizes $\rm A_x(n)$;\smallskip

(C5)~if C is $\rm A\orR B$, c realizes C in case $\rm c\Rightarrow\Pair
(1,a)$
(for some a)
and a~realizes~A, or $\rm c\Rightarrow\Pair(2,b)$ (for some b) and
b~realizes~B;\smallskip

(C6)~if C is $\rm\exists yA$, c realizes C in case
$\rm c\Rightarrow\Pair(n,a)$
(for some n and a)
and a~realizes $\rm A_y(n)$.\medbreak

\noindent For a formula D whose free variables are $\rm x_1$, \dots,
$\rm x_\nu$, d realizes D in case $\rm\Lambda x_1\ldots\Lambda x_\nu d$
realizes the closure of~D.

Kleene formulated recursive realizability so as to ensure that the
theorems of intuitionistic arithmetic would all be realizable.
David Nelson undertook to establish that this is the case, and did
so in~[6]. Here are the realization codes for the axioms (nonlogical and
logical) of intuitionistic arithmetic. (Note that $\to$ is associated
from right to left.)\medbreak

\halign{\hfil#&\quad$#$\hfil&\quad$#$\hfil\cr
1.&\neg\ \ro Sx=0&0\cr
2.&\ro Sx=\ro Sy\impP x=y&0\cr
3.&x+0=x&0\cr
4.&x+\ro Sy=\ro S(x+y)&0\cr
5.&x\.0=0&0\cr
6.&x\.\ro Sy=x\.y+x&0\cr
7.&\rm A_x(0)\andD\forall x[A\to A_x(Sx)]\to A&\Lambda b\rho(\ro x,b)\cr
8.&x=x&0\cr
9.&x=y\to\ro Sx=\ro S y&0\cr
10.&x_1=y_1\to x_2=y_2\to x_1+x_2=y_1+y_2&0\cr
11.&x_1=y_1\to x_2=y_2\to x_1\.x_2=y_1\.y_2&0\cr
12.&x_1=y_1\to x_2=y_2\to x_1=x_2\to y_1=y_2&0\cr
13.&\rm A\to B\to A&\Lambda a\Lambda b a\cr
14.&\rm[A\to B]\to[A\to B\to C]\to A\to C&\Lambda p\Lambda q\Lambda aq\{a\}\{p\{a\}\}\cr
15.&\rm A\to B\to A\andD B&\Lambda a\Lambda b\langle a,b\rangle\cr
16.&\rm A\andD B\to A&\Lambda c{\rm \pi_1}c\cr
17.&\rm A\andD B\to B&\Lambda c{\rm \pi_2}c\cr
18.&\rm A\to A\vee B&\Lambda a\langle 1,a\rangle\cr
19.&\rm B\to A\vee B&\Lambda b\langle 2,b\rangle\cr
20.&\rm [A\to C]\to[B\to C]\to A\vee B\to C&\Lambda p\Lambda q\Lambda r\gamma(p,q,r)\cr
21.&\rm [A\to B]\to[A\to\neg B]\to\neg A&\Lambda p\Lambda q\Lambda aq\{a\}
\{p\{a\}\}\cr
22.&\rm\neg A\to A\to B&0\cr
23.&\rm A_x(a)\to\exists xA&\Lambda y\langle\ro a,y\rangle\cr
24.&\rm\forall xA\to A_x(a)&\Lambda yy\{\ro a\}\cr}\medbreak

As an example, let us verify that the code given for the propositional
axiom scheme~(14) does realize it. (This axiom scheme justifies the use 
of deduction in mathematical reasoning: one introduces a hypothesis~A,
proves B and $\rm B\impP C$ and thereby~C on the basis of it, and then
discharges the hypothesis by concluding $\rm A\impP C$.) Let D be
$$\rm [A\to B]\to[A\to B\to C]\to A\to C$$
and let d~be
$$\Lambda p\Lambda q\Lambda aq\{a\}\{p\{a\}\}.$$ 
Let $\rm d_1$ realize 
$\rm A\impP B$. By~(C3), to show that d realizes~D we must show that
$\rm d\{d_1\}$ realizes $\rm [B\to C]\to A\vee B\to C$. But by~(R11),
$$\rm d\{d_1\}\Rightarrow \Lambda q\Lambda aq\{a\}\{\ro d_1\{a\}\}.$$
Let $\rm d_2$ realize $\rm A\to B\to C$. We need to show that
$$\big(\Lambda q\Lambda aq\{a\}\{\ro d_1\{a\}\}\big)\{\ro d_2\},$$
which reduces to $\Lambda a\ro d_2\{a\}\{\ro d_1\{a\}\}$, realizes
$\rm A\to C$. Let $\rm d_3$ realize~A. We need to show that
$$\big(\Lambda a\ro d_2\{a\}\{\ro d_1\{a\}\}\big)\{\ro d_3\},$$
which reduces
to $\rm d_2\{d_3\}\{\ro d_1\{d_3\}\}$, realizes~C. But since
$\rm d_3$ realizes~A and
$\rm d_2$ realizes $\rm A\to B\to C$, $\rm d_2\{d_3\}$ realizes
$\rm B\to C$, and since $\rm d_1$ realizes \hbox{$\rm A\impP B$},
$\rm d_1\{d_3\}$ realizes B; consequently,
$\rm d_2\{d_3\}\{\ro d_1\{d_3\}\}$ does realize~C.

We also have the following three {\it rules of inference}.
(For rule (25), let $\rm y_1$, \dots~$\ro y_\mu$ be the
variables occurring free in~A but not in~B; for rules (26) and~(27),
let w~be
a variable that does not occur in A or~B):\medbreak

\noindent25. If a is code for A and c is code for $\rm A\to B$, then
the code for B is
$\rm(c\{a\})_{y_1\ldots y_\mu}(0\ldots0)$.\smallskip

\noindent26. If c is code for $\rm A\to B$ and x is not free in~B,
then the code for $\rm\exists x A\impP B$ is
$\rm\Lambda w((\Lambda xc)\{\pi_1w\})\{\pi_2w\}$.\smallskip

\noindent27. If c is code for $\rm A\to B$ and x is not free in~A,
then the code for $\rm A\impP\forall xB$ is
$\rm\Lambda w\Lambda xc\{w\}$.\medbreak

Then for any proof of a theorem in intuitionistic arithmetic, we have an
algorithm (a polynomial time algorithm!) for producing a realization code
for it, and Nelson proved that this code realizes the theorem.

Since $\S0=0$ is not realizable, a consequence of this argument is that
$\S0=0$ is not a theorem of intuitionistic arithmetic; that is, the theory
is consistent. The reason that conflict with G\"odel's second theorem
is avoided is that the notion of realizability cannot itself be expressed
within arithmetic. \bigskip

\centerline{\bf III.~Logic of the feasible}\medskip

How should this be modified for a logic of polynomial time computation?
For intuitionistic arithmetic, the realization codes are recursive
partial functions; for the feasible arithmetic of~\W,
they should be polynomial 
time functions. But we have a choice: to consider ordinary functions
or sorted functions. Let us choose the latter since this gives a
richer theory. Then in addition to~(C4) we have\medskip

(C4$'$)~if C is $\rm\forallst xA$, c realizes C in case for all
standard~n, $\rm c\{n\}$ realizes $\rm A_x(n)$.\medskip

\noindent More interestingly, in addition to (C3) we have\medskip

(C3$'$)~if C is $\rm A\impst B$, c realizes C in case for all
standard~a, if a realizes~A then $\rm c\{a\}$ realizes~B.\medskip

\noindent Notice that $\rm\forallst xA$ is weaker than $\rm\forall xA$
but $\rm A\impst B$ is stronger than \hbox{$\rm A\impP B$}.

Now we can realize induction for \W\ in the form
$$\rm A_x(\epsi)\and \forall x[A\imp A_x(\z x)\and A_x(\o x)] \imp 
\forallst xA.$$
But there is one axiom that cannot be feasibly realized, and the
problem comes in a surprising place: the logical axiom scheme~(14)
of the propositional calculus. $\big($Notice that~(21) can be
regarded as a special case of~(14) in which C~is $\S0=0$.$\big)$
This is because in the realization code
$\Lambda p\Lambda q\Lambda aq\{a\}\{p\{a\}\}$ the~$a$ appears in two
places. When we replace the variables $p$ and $q$ by realization
codes $\rm d_1$ and $\rm d_2$, the function
$$a \mapsto \ro d_2\{a\}\{\ro d_1\{a\}\}$$
is not polynomial time. The $\ro d_2\{a\}$ may reduce in polynomial
time, but
there is no polynomial bound on the time it takes to evaluate a code 
$\ro d_2\{a\}$ of
a given length on an argument $\ro d_1\{a\}$.

The problem of constructing a propositional
calculus suitable for feasible reasoning demands investigation.
\bigbreak

\centerline{\bf IV.~A personal note}\medskip

One of the most treasured experiences of my life is my friendship
with Georges Reeb. 
We had many strong discussions together, intuitionist
versus formalist. What he created was unique in my experience. His rare
spirit, gentle but fiercely demanding of the highest standards, 
inspired a group of younger mathematicians with an unmatched ethos of
collegiality. And their discoveries are extraordinary.

Reeb found, and led others to find, not only knowledge and beauty
in mathematics, but also virtue.
His insights into the nature of
mathematics will point the way towards the mathematics of the future.
\bigskip

\centerline{\bf References}\medskip

\frenchspacing \parskip=\smallskipamount \parindent=0pt

[1]~Stephen Bellantoni and Stephen Cook, ``A new recursion-theoret\-ic
characterization of the poly-time functions'', {\it Computational
Complexity}, 2:97--110, 1992.

[2]~Stephen Bellantoni, {\it Predicative Recursion and Computational 
Complexity}, Ph.D. Thesis, University of Toronto, 1992. Available
online,
{\tt ftp://ftp.cs.toronto.edu/pub/reports/theory/cs-92-264.ps.Z}

[3]~Daniel Leivant, {\it Ramified recurrence and computational
complexity I: Word recurrence and poly-time}, in Peter Cole and
Jeffrey Remmel, editors, {\it Feasible Mathematics II}, 
Perspectives in Computer Science, pages 320-343, 
Birkhauser-Boston, New York, 1994.

[4]~Stephen Cole Kleene, ``On the interpretation of intuitionistic
number theory'', {\it Journal of Symbolic Logic\/} 10, 109--124, 1945.

[5]~Stephen Cole Kleene, {\it Introduction to Metamathematics}, 
North-Hol\-land, Amsterdam, 1980 (originally published in 1952),

[6]~David Nelson, ``Recursive functions and intuitionistic number 
theory'', {\it Transactions of the American Mathematical Society\/} 61,
307--368, 1947.\medskip

\tt nelson@math.princeton.edu

\bye
