McCarthy Formalism

<h2 id="introduction">Introduction</h2>
<h3>McCarthy's notion of conditional expression</h3>
McCarthy (1960) described his formalism this way:<a class="footnote-ref" id="fnref:1" href="#fn:1">1</a>

"In this article, we first describe a formalism for defining functions recursively. We believe this formalism has advantages both as a programming language and as a vehicle for developing a theory of computation....
We shall need a number of mathematical ideas and notations concerning functions in general. Most of the ideas are well known, but the notion of conditional expression is believed to be new, and the use of conditional expressions permits functions to be defined recursively in a new and convenient way."
<h3>Minsky's explanation of the "formalism"</h3>
In <a href="/facts/Marvin_Minsky/HTU5MYLL">Marvin Minskys</a> 1967 book Computation: Finite and Infinite Machines, § 10.7 Conditional Expressions: The McCarthy Formalism, he describes the "formalism" as follows:

"Practical computer languages do not lend themselves to formal mathematical treatment--they are not designed to make it easy to prove theorems about the procedures they describe. In a paper by McCarthy [1963] we find a formalism that enhances the practical aspect of the recursive-function concept, while preserving and improving its mathematical clarity. ¶ McCarthy introduces "conditional expressions" of the form
f = (if p1 then e1 else e2)
where the ei are expressions and p1 is a statement (or equation) that may be true or false. ¶ This expression means
See if p1 is true; if so the value of f is given by e1.
IF p1 is false, the value of f is given by e2.
This conditional expression . . . has also the power of the minimization operator. . ..
The McCarthy formalism is like the general recursive (Kleene) system, in being based on some basic functions, composition, and equality, but with the conditional expression alone replacing both the primitive-recursive scheme and the minimization operator." (Minsky 1967:192-193)
Minsky uses the following operators in his demonstrations:<a class="footnote-ref" id="fnref:2" href="#fn:2">2</a>

<ul><li>Zero</li>
<li>Successor</li>
<li>Equality of numbers</li>
<li>Composition (substitution, replacement, assignment)<a class="footnote-ref" id="fnref:3" href="#fn:3">3</a></li>
<li>Conditional expression</li></ul>
From these he shows how to derive the predecessor function (i.e. DECREMENT); with this tool he derives the minimization operator necessary for "general" <a href="/facts/Recursion/CxSKxJoW">recursion</a>, as well as primitive-recursive definitions.

<h3>Expansion of IF-THEN-ELSE to the CASE operator</h3>
In his 1952 Introduction of Meta-Mathematics <a href="/facts/Stephen_Kleene/sKSax2se">Stephen Kleene</a> provides a definition of what it means to be a primitive recursive function:

"A function φ is primitive recursive in ψ1, ..., ψk (briefly Ψ), if there is a finite sequence φ1, ..., φk of (occurrences of) functions ... such that each function of the sequence is either one of the functions Ψ (the assumed functions), or an initial function, or an immediate dependent of preceding functions, and the last function φk is φ." (Kleene 1952:224)
In other words, given a "basis" function (it can be a constant such as 0), primitive recursion uses either the base or the previous value of the function to produce the value of the function; primitive recursion is sometimes called <a href="/facts/Mathematical_induction/KxAPqNrH">mathematical induction</a>
Minsky (above) is describing a two-CASE operator. A demonstration that the nested IF-THEN-ELSE—the "<a href="/facts/Case_statement/oQCWnGWh">case statement</a>" (or "switch statement")--is <a href="/facts/Primitive_recursive/4z97gRnl">primitive recursive</a> can be found in Kleene 1952:229<a class="footnote-ref" id="fnref:4" href="#fn:4">4</a> at "#F ('mutually-exclusive predicates')". The CASE operator behaves like a logical <a href="/facts/Multiplexer/lVro0Sfz">multiplexer</a> and is simply an extension of the simpler two-case logical operator sometimes called AND-OR-SELECT (see more at <a href="/facts/Propositional_formula/eEV8YrAI">Propositional formula</a>). The CASE operator for three cases would be verbally described as: "If X is CASE 1 then DO "p" else if X is CASE 2 then do "q" else if X is CASE "3" then do "r" else do "default".
Boolos-Burgess-Jeffrey 2002 observe that in a particular instance the CASE operator, or a sequence of nested IF-THEN-ELSE statements, must be both <a href="/facts/Mutually_exclusive/v139z4dJ">mutually exclusive</a>, meaning that only one "case" holds (is true), and <a href="/facts/Collectively_exhaustive/DCK4rxvW">collectively exhaustive</a>, meaning every possible situation or "case" is "covered". These requirements are a consequence of the determinacy of <a href="/facts/Propositional_logic/MNt5v31V">Propositional logic</a>; the correct implementation requires the use of <a href="/facts/Truth_table/4KsmArDW">truth tables</a> and <a href="/facts/Karnaugh_map/saFd8oNl">Karnaugh maps</a> to specify and simplify the cases; see more at <a href="/facts/Propositional_formula/eEV8YrAI">Propositional formula</a>. The authors point out the power of "definition by cases":

"...in more complicated examples, definition by cases makes it far easier to establish the (primitive) recursiveness of important functions. This is mainly because there are a variety of processes for defining new relations from old that can be shown to produce new (primitive) recursive relations when applied to (primitive) recursive relations." (Boolos-Burgess-Jeffrey 2002:74)
They prove, in particular, that the processes of <a href="/facts/Substitution_of_variables/vjWdXCDF">substitution</a>, graph relation (similar to the <a href="/facts/Identity_relation/wh0QoWzS">identity relation</a> that plucks out (the value of) a particular variable from a list of variables), <a href="/facts/Negation/q5AQBvBj">negation</a> (logical NOT), <a href="/facts/Logical_conjunction/62uyyn1d">conjunction</a> (logical AND), <a href="/facts/Disjunction/jbI2EGlM">disjunction</a> (logical OR), bounded <a href="/facts/Universal_quantification/agNmvJKN">universal quantification</a>, or bounded <a href="/facts/Existential_quantification/hHveaBYo">existential quantification</a> can be used together with definition by cases to create new primitive recursive functions (cf Boolos-Burgess-Jeffrey 2002:74-77).

<h2 id="see-also">See also</h2>
<ul><li><a href="/facts/Association_list/1tqXLc1s">Association list</a></li>
<li><a href="/facts/De_Bruijn_index/MCN7dhr5">De Bruijn index</a></li></ul>
<h2 id="notes">Notes</h2>

<ul><li><a href="/facts/John_McCarthy_(computer_scientist)/ajKU4SdD">McCarthy, John</a> (1960). <a href="https://doi.org/10.1145%2F367177.367199">"Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I"</a>. Communications of the ACM. 3 (4): 184–195. <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1145%2F367177.367199">10.1145/367177.367199</a>.</li>
<li><a href="/facts/George_S._Boolos/K969uIhT">George S. Boolos</a>, <a href="/facts/John_P._Burgess/vVxaBgbr">John P. Burgess</a>, and <a href="/facts/Richard_C._Jeffrey/fL2rpek3">Richard C. Jeffrey</a>, 2002, Computability and Logic: Fourth Edition, Cambridge University Press, Cambridge UK, <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 0-521-00758-5 paperback.</li>
<li><a href="/facts/John_McCarthy_(computer_scientist)/ajKU4SdD">John McCarthy</a> (1963), <a href="http://www-formal.stanford.edu/jmc/basis.html">A Basis for a Mathematical Theory of Computation</a>, Computer Programming and Formal Systems, pp. 33-70.</li>
<li><a href="/facts/Marvin_Minsky/HTU5MYLL">Marvin Minsky</a> (1967), Computation: Finite and Infinite Machines, Prentice-Hall Inc, Englewood Cliffs, NJ.</li></ul>

<h2 id="references">References</h2>

<ol>
<li id="fn:1">McCarthy 1960. - McCarthy, John (1960). "Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I". Communications of the ACM. 3 (4): 184–195. doi:10.1145/367177.367199. <a href="https://doi.org/10.1145%2F367177.367199" target="_blank">https://doi.org/10.1145%2F367177.367199</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></li>
<li id="fn:2">Minsky (1967) does not include the identity operator in his description of primitive recursive functions. Why this is the case is not known. <a href="/wiki/Primitive_recursive_function" target="_blank">/wiki/Primitive_recursive_function</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></li>
<li id="fn:3">Various authors use various names for this operation. Kleene calls it: "the schema of definition by substitution. The expression for the ambiguous value of φ is obtained by substitution of expressions for the ambiguous values of χ1, . . ., χm for the variables of ψ . . .. the function φ defined by an application of this schema we sometimes write ast Smn(ψ, 1, . . ., χm." (Kleene 1952:220). Knuth names it the "all-important replacement operation (sometimes called assignment or substitution)", and he symbolizes it with the " ← " arrow, e.g. "m ← n" means the value of variable m is to be replaced by the current value of variable n" (cf Knuth 1973:3). <a href="#fnref:3" class="footnote-back-ref">↩</a></li>
<li id="fn:4">Kleene's 5 primitive recursion "schema" include the following:
zero constant: 0 or may be 0()successor: S(0) = "1", S(1) = "2", etc.projection: Uin(x1 , ..., xn) = xi, the xi's are "parameters" fixed throughout the calculation, and Uin project one of them out, the notation πin(x1, ..., xn) = xi is also used.substitution φ(x1 , ..., xn) = ψ(χ1(x1 , ..., xn), ..., χm(x1 , ..., xn))primitive recursion; cf Kleene 1952:219. <a href="#fnref:4" class="footnote-back-ref">↩</a></li>
</ol>

McCarthy Formalism open-in-new

McCarthy Formalism