[FOM] Regarding McCarthy's Approach

[Harvey Friedman]

On Tue, May 24, 2016 at 3:00 AM, Yiannis N. Moschovakis
<ynm at math.ucla.edu> wrote:

> 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".

I kind of recall this important McCarthy paper from long ago, and I
took a brief glance at it just now. I have some thoughts about this
approach

One idea that occurred to me is whether there is an even simpler such
"coding free" treatment of partial recursive functions, say, without
the need for conditionals.

There appears to be such, and I have no idea to whom this should be CREDITED.

Instead of directly treating partial recursive functions, we instead
treat r.e. subsets of the N^k.

MOST LIBERAL VERSION

A program consists of finitely many clauses of the following form:

If phi_1 and ... and phi_n holds then psi holds.

Here n >= 0, and each phi_i is an atomic formula in successor and 0.
I.e., Each phi_i is of the form

R(t_1,...,t_k)

where the t's are expressions involving 0, variables, and the
successor operation.

The semantics is as follows. Suppose X is the set of R's used in the
program. A realization is a map h from X into relations on N of the
corresponding dimension where all of the clauses holds universally.

THEOREM. Every program has a (necessarily unique) least realization.
I.e., a realization h, where for any realization h', each h(R) is a
subset of h'(R).

By r.e. set, we mean an r.e. subset of some N*k.

THEOREM (universality). The components of every least realization are
r.e. Every r.e. set is an element of some least realization. Every
finite set of r.e. sets is a subset of some least realization.

THEOREM. The set of programs whose least realization consists entirely
of nonempty relations is complete r.e.

LESS LIBERAL VERSIONS

Here are two demands that can be simultaneously placed on programs so
that the universality above still holds.

1. All terms are of the form 0,v,v', where v is a variable and ' means
successor.
2. The number of conjuncts used in each clause is at most 2.
3. Only one relation symbol is used in the program.

COMPLEXITY

The complexity of a program can be conveniently defined as the total
number of occurrences of 0, variables, and ' (the successor symbol).

RESERACH PROGRAM. Get good lower and upper bounds on the least
complexity of a program whose least realization contains a given
interesting r.e. set. Call this the program complexity of the given
r.e. set.

For example, what can we say about the program complexity of

i. The set of all nonnegative even integers.
ii.The set of all nonnegative odd integers.
iii. The residue classes in N.
iv. The set of all squares in N.
v. The set of all {(n,2n): n in N}.
etcetera

These problems at some point will need a computer to solve.

Harvey Friedman