Talk:McCarthy Formalism

Request for expert

I remember hearing about this "formalism" in the mid-1970's but not much thereafter. It is as if it vanished. By use of the Dartmouth library I was able to find and copy for study one of McCarthy's papers but unable to find any other books, references or anything else with respect to his "Formalism" -- except a subchapter in Minsky's (1967) book; Minsky thought highly of his work. But there is something very odd in Minsky's analysis -- he doesn't add the identity function to his set of basic recursive operators (it is almost as if he made a mistake, or he missed something). And McCarthy's formalism seems to be just another selection of basic recursion operators that happens to include the IF-THEN-ELSE or CASE function in place of the (unbounded- or bounded-) mu-operator(s). All these guys are long gone so we can't ask them what is going on. Any help would be appreciated. As it stands now the article is quite incomplete. wvbaileyWvbailey 15:15, 28 May 2007 (UTC)

As of July 30, 2009 the situation is just as bad as noted above. I've added something from Boolos-Burgess-Jeffrey 2002 but we still need an expert. I remember (as noted above) that there was a time when the "McCarthy Formalism" was the greatest thing since peanut butter, but apparently he and his formalism have decayed into oblivion. This just goes to show you that there's nothing new under the sun, and dust to dust, ashes to ashes (to quote from the old testament poets). Wvbailey (talk) 02:40, 31 July 2009 (UTC)

This article is not needed

You are right, I have to see the Boolos-Burgess-Jeffrey you cite, to see the context. But it is something known since McCarthy published Recursive Functions of Symbolic Expressions ... was published in 1960. In that article he presented Lisp, there is a correspondence between McCarthy's symbolic expressions and recursive functions. Recursive functions are a computational system equivalent to Turing Machines, that means they have the same computational power. (See Church-Turing Thesis)

It is wrongly believed that Lisp is based in Lambda-calculus, other formalism equivalent to Turing-Machines, because McCarthy used Lambda-expressions to define functions, recursive functions. At that time McCarthy did not understood well Lambda-calculus (he says that in an article about Lisp circa 1980).

The great influential contribution of McCarthy was that his language had a very simple syntax, inductively defined, and a formal semantics was also given. (Before other seminal works like Backus-Naur form in algol report, and P.J. Landin A correspondence between ALGOL 60 and Church's Lambda-notation. Comm. ACM 8 (1965), 89-101; 158-165.)

I think that this subject should not be an article, but a notation in other entries maybe symbolic expressions or Lisp, and a section in Recursive functions.

You are right, symbolic expressions proved to be as important and fundamental (maybe more fundamental than) as arrays.

Arrays had a different impact as a foundational formalism than symbolic expressions because Fortran like languages were more popular than Keneth Iverson's APL, who treated them as an elegant algebraic programing formalism. (See: J.Backus, Can Programming be Liberated from Von Neumann Style? 1978, CACM) But influenced the very elegant functional languages FP,FFP,ML,Miranda,Haskell and other not very elegant but widely used in mathematical applications like Matlab, Octave, Scilab, SAGE.

In typed languages, lists are used. Lists are a case of McCarthy's symbolic expressions.

In few words I have no doubt of the importance of McCarthy's seminal work. But I think it does not deserves a separated entry in wikipedia.

On the other hand, this article has many mistakes to be fixed. I fixed some, but more work must be done, a work redundant with the contents in Recursive functions and symbolic expressions within Lisp article. — Preceding unsigned comment added by Elias (talk • contribs) 04:11, 14 February 2011 (UTC)

As creator of the article I do believe it has value as a separate article, but perhaps only in the historical sense. To include it in recursion theory or LISP would be a mistake because it has its own set of references, and its own history. The fact that Minsky calls it the McCarthy Formalism alone makes it a worthy entry. Note that one paper (1963) is missing, I couldn't find it even in the fancy mathematics sub-library in the Dartmouth library.

The fact that the CASE instruction reduces to the IF-THEN-ELSE construction, and the fact that the IF-THEN-ELSE software consruction can be built from what us hardware guys call the AND-OR-INVERT, and the fact that the AND-OR-INVERT and constants 0 and 1 form a basis of logic (like the Sheffer stroke, or NAND or NOR) is very important factoid. (But this particular tie-together and correspondence is not covered anywhere that I know of). It's almost as if it's waiting to be (re-)discovered.

RE change from substitution to composition: I'm away from my books but will check the Kleene terminology in a couple days. I beleive that plenty of people (e.g. Knuth in particular) use the words composition, substitution and assignment synonymously; I'll double check. I don't like the word "composition" myself; it's what a type-setter does, or a musician writing a musical score.

It is exactly the same idea! Functions are composed applying each one after other, $h\circ g\circ f$ also written $hgf$, like the notes in a music composition. That composition of functions corresponds to each step of a formal proof. Yes a program is a mathematical proof too.

I don't see it as an accurate description of what a computor (human) does when they are being a Lambek machine (cf B-B-J again). Bill Wvbailey (talk) 19:07, 14 February 2011 (UTC)

RE "composition" versus "substitution": I looked up the original reference(s) in both Kleene 1952 and Knuth 1973 to see what the usage of "composition" is. Kleene is very clear and uses the "schema of definition by substitution". Knuth introduces two more words: "replacement" and "assignment", words that he declares to be synonymous with "substitution" ("composition" does not appear in the index to his 1973 2nd edition of his 1968). So we have 4 words that seem to be synonyms. But perhaps there are nuances? I added another footnote and corrected the footnote that was there. While this may seem to be redundant (these footnotes re recursion) there is a nuance: Kleene's proof (and B-B-J's proof) that "Definition by cases" is primitive recursive, followed by the reduction of the CASE operator to the most-reduced IF-THEN-ELSE, followed by Minsky's observation that it can replace both the recrusion and mu-operators (i.e. the recursion-schema and the mu-operator). These are subtle wrinkles i.e. having to do with "bases of Turing-computability" that are distinct from classical recursion theory. Bill Wvbailey (talk) 23:20, 16 February 2011 (UTC)

1961-1963 reference

Here's the 1963 reference, from an archive of McCarthy's homepage: A BASIS FOR A MATHEMATICAL THEORY OF COMPUTATION∗ JOHN McCARTHY 1961–1963 [This 1963 paper was included in Computer Programming and Formal Sys- tems, edited by P. Braffort and D. Hirshberg and published by North-Holland. An earlier version was published in 1961 in the Proceedings of the Western Joint Computer Conference.] — Preceding unsigned comment added by 83.79.48.222 (talk) 11:30, 4 January 2014 (UTC)

Downloaded it! Thanks, BillWvbailey (talk) 14:24, 4 January 2014 (UTC)

I browsed that article and it is a very interesting research program related to the advice taker project.

I agree that this article should be deleted, but reading the Lisp article, one find many misunderstandings on the genesis of lisp.

The 1963 article that you kindly linked makes clear why McCarthy developed lisp.

why not instead work McCarthy's article to explain LISP in it's context and the evolution that each topic had the years after it's publication?

The concern that WvBailey has about recursive functions, is maybe gone at this time. If not don't worry, it takes some time to unlearn misleading meanings of terms that block the correct understanding of many theoretical concepts. I passed through that process too.

The class of recursive functions comprehends functions that include.

1. $z()=0$ a constant function,
2. $s(x)=x+1$ a successor function,
3. $\pi _{i}^{n}(x_{0},x_{1},\ldots ,x_{n-1})=x_{i}$ where $0\leq i<n$, a projection function,
4. $h(x_{0},x_{1},\ldots ,x_{n-1})=g(f_{0}(x_{0},x_{1},\ldots ,x_{n-1}),\ldots ,f_{m-1}(x_{0},x_{1},\ldots ,x_{n-1}))$ the generalized composition. A composition of a function $g:\mathbb {N} ^{m}\to \mathbb {N}$ with $m$ functions $f_{j}:\mathbb {N} ^{n}\to \mathbb {N}$ where $0\leq j<m$,
5. $h(x_{0},\ldots ,x_{n-1},0)=f(x_{0},\ldots ,x_{n-1})$ the base case, and $h(x_{0},\ldots ,x_{n-1},y+1)=g(x_{0},\ldots ,x_{n-1},y,h(x_{0},\ldots ,x_{n-1},y))$ the inductive case of a primitive recursive function.

Any set of formulas with the above structure form primitive recursive functions.

They are important because they can compute functions on naturals, they are a formal system equivalent to Turing Machines and Lambda Calculus, for that reason McCarthy extended them to compute symbolic expressions adding a conditional expression to have the same computing power as the above primitive recursive functions plus sixth one called minimization, to form the partial recursive functions.

6. $g(x_{0},\ldots ,x_{n-1})=\mu _{y}(f(x_{0},\ldots ,x_{n-1},y)=0)$ the least $y$ which makes $f(x_{0},\ldots ,x_{n-1},y)=0$, iterating from 0. It is a partial function because there is no warranty that such $y$ can be found.

The 4th pattern, generalized composition in the case where $m=1$ and $n=1$ is the function composition defined as follows $h(x)=g(f(x))$ although the notation $(g\circ f)(x)$ [pronounced "$g$ after $f$"] is used instead of $h(x)$.

Composition is different from substitution, substitution is about replacing a variable by an assigned value in a given environment. $(x+y)[\![x\mapsto 3,y\mapsto 5]\!]\Rightarrow ^{*}(3+5)$

The recursive functions were used to in completeness and incompleteness Gödel proofs. Because they can be used to convert formulas to/from numbers and their encoding too (see Gödel numbers) which together with a Cantor's diagonal method is used to prove Gödel incompleteness theorem. — Preceding unsigned comment added by 2806:107E:C:2568:218:DEFF:FE2B:1215 (talk) 02:27, 6 April 2018 (UTC)