Talk:McCarthy Formalism

From Wikipedia, the free encyclopedia
Jump to: navigation, search
WikiProject Mathematics (Rated Start-class, Low-priority)
WikiProject Mathematics
This article is within the scope of WikiProject Mathematics, a collaborative effort to improve the coverage of Mathematics on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.
Mathematics rating:
Start Class
Low Priority
 Field:  Foundations, logic, and set theory
WikiProject Computer science (Rated Start-class)
WikiProject icon This article is within the scope of WikiProject Computer science, a collaborative effort to improve the coverage of Computer science related articles on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.
Start-Class article Start  This article has been rated as Start-Class on the project's quality scale.
 ???  This article has not yet received a rating on the project's importance scale.
 
Note icon
This article has been marked as needing immediate attention.

Request for expert[edit]

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[edit]

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 (talkcontribs) 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. 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[edit]

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)