McCarthy Formalism


In computer science and recursion theory the McCarthy Formalism of computer scientist John McCarthy clarifies the notion of recursive functions by use of the IF-THEN-ELSE construction common to computer science, together with four of the operators of primitive recursive functions: zero, successor, equality of numbers and composition. The conditional operator replaces both primitive recursion and the mu-operator.

Introduction

McCarthy's notion of ''conditional expression''

McCarthy described his formalism this way:

Minsky's explanation of the "formalism"

In his 1967 Computation: Finite and Infinite Machines, Marvin Minsky in his § 10.6 Conditional Expressions: The McCarthy Formalism describes the "formalism" as follows:
Minsky uses the following operators in his demonstrations:
From these he shows how to derive the predecessor function ; with this tool he derives the minimization operator necessary for "general" recursion, as well as primitive-recursive definitions.

Expansion of IF-THEN-ELSE to the CASE operator

In his 1952 Introduction of Meta-Mathematics Stephen Kleene provides a definition of what it means to be a primitive recursive function:
In other words, given a "basis" function, 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 mathematical induction
Minsky is describing a two-CASE operator. A demonstration that the nested IF-THEN-ELSE—the "case statement" --is primitive recursive can be found in Kleene 1952:229 at "#F ". The CASE operator behaves like a logical multiplexer and is simply an extension of the simpler two-case logical operator sometimes called AND-OR-SELECT. 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 mutually exclusive, meaning that only one "case" holds, and collectively exhaustive, meaning every possible situation or "case" is "covered". These requirements are a consequence of the determinacy of Propositional logic; the correct implementation requires the use of truth tables and Karnaugh maps to specify and simplify the cases; see more at Propositional formula. The authors point out the power of "definition by cases":
They prove, in particular, that the processes of substitution, graph relation, negation, conjunction, disjunction, bounded universal quantification, or bounded existential quantification can be used together with definition by cases to create new primitive recursive functions.