[FOM] Kleene's T predicate

Tue May 24 03:00:12 EDT 2016

To supplement Martin's detailed account of the facts about the S
and T predicates, I have a (now vague) memory of Kleene explaining
that "S" stood for "substitution", the main rule for deducing
equations from Herbrand-Goedel-Kleene systems of equations, and
"T" is simply the next letter in the alphabet; nothing more
profound than that.

As Martin explains, the move from S to T in Kleene (1943) was made
"to deal with the non-determinism of the equation calculus". In
some detail (to make a point further down),
      S(e,x,y) <==> y is the code of a computation from the
                    system with code e on the input x,
and there may be many y's and many output values on the same input
x; setting
      T(e,x,y) <==> S(e,x,y) & (forall t<y) not S(e,x,t)
admits at most one computation with each e and x and so each e
computes exactly one partial function. This, however, addresses
only a small part of the problem introduced by the indeterminacy
of the HGK computation model, as the connection between a system E
and the (partial) function it computes is generally obscure,
except for very simple systems: it depends, for example, on the
specific coding for tuples we use to pick "the least computation"
in defining T. The deterministic Turing machines used in Martin's
classic 1958 book provide a much tighter connection between the
computation model and the partial function it computes.

A different approach to this problem was taken by John McCarthy in
his classic 1963 paper "A basis for a mathematical theory of
computation" (google it). McCarthy adds conditionals to the
term-formation rules of the equation calculus and so he can
restrict himself to systems of equations in which each (partial) function
is "defined" by a single term equation. Each "recursive program"
          f_i(x_i) = E_i   (i=1, ..., K)
computes the tuple of least partial functions f*_1,...,f*_K which
satisfy its equations, a direct, coding-independent connection of
denotational and operational semantics which (in many cases)
provides trivial "correctness proofs" for programs. Recursive
programs also provide very simple proofs of some basic results of
elementary recursion theory, such as the so-called First Recursion
Theorem of Kleene; and they can be easily extended to yield a
theory of recursion on arbitrary sets from arbitrary functions and
relations. They are well-known to computer scientists, of course,
but not as much to logicians who work in "computability theory".

Yiannis Moschovakis

On Mon, May 23, 2016 at 8:07 PM, Martin Davis <martin at eipye.com> wrote:

> Trying to find a connection with Turing is hopelessly anachronistic. The
> first version of the T predicate was introduced in Kleene's paper "General
> Recursive Functions of Natural Numbers" Mathematische Annalen vol.
> 112(1936) 727-742.
> A footnote reads: "Presented to the American Mathematical Society,
> September 1935." The paper refers to works by Ackermann, Péter, Gödel, and
> Skolem, but not Turing. The formalism to which Kleene applies Gödel
> arithmetization in this paper is an equation calculus. Because it enables
> derivation of the values from recursion equations going beyond "primitive"
> (so named by Kleene in this paper) recursions, as for example the defining
> equations of Ackermann's function, Kleene spoke of "general recursive
> functions". The main result of this paper is that every general recursive
> function h can be written in the form:
>                     h(x) =  f(min y [g(x,y])
> where f and g are primitive recursive. This Kleene Normal Form Theorem
> turned proving the equivalence of different formulations of computability
> into a routine chore.
>
> What we think of as Kleene's T predicate was introduced in his "Recursive
> Predicates and Quantifiers," Transactions of the American Mathematical
> Society, vol. 53(1943)  41-73. What was called T in the 1936 paper is now
> called S, and T is defined from S by choosing the least of the values of
> one of the variables satisfying the predicate. This is to deal with the
> non-determinism of the equation calculus.
>
> In my anthology "The Undecidable" (available in a Dover reprint) are
> included both of these papers as well as notes taken by Kleene and Rosser
> (then graduate students) on Gödel's lectures in 1934 at which the idea of a
> formalism for general recursive functions was first mentioned.
>
> I had the idea that if one applied Kleene's methods to the Turing machine
> formalism there was no indeterminancy to deal with so the development could
> proceed more simply and smoothly. This is what led to my book
> "Computability and Unsolvability" published in 1958, but also available as
> a Dover reprint. I used the letter T as a tribute to Kleene.  It never
> occurred to me to consider that it was also Turing's initial.
>
> Martin
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160524/baedd308/attachment-0001.html>