 McCarthy 91 function

The McCarthy 91 function is a recursive function, defined by computer scientist John McCarthy as a test case for formal verification within computer science.
The McCarthy 91 function is defined as
The results of evaluating the function are given by M(n) = 91 for all integer arguments n ≤ 100, and M(n) = n − 10 for n ≥ 101.
Contents
History
The 91 function was introduced in papers published by Zohar Manna, Amir Pnueli and John McCarthy in 1970. These papers represented early developments towards the application of formal methods to program verification. The 91 function was chosen for having a complex recursion pattern (contrasted with simple patterns, such as defining f(n) by means of f(n − 1)). The example was popularized by Manna's book, Mathematical Theory of Computation (1974). As the field of Formal Methods advanced, this example appeared repeatedly in the research literature. In particular, it is viewed as a "challenge problem" for automated program verification.
Often, it is easier to reason about nonrecursive computation. As one of the examples used to demonstrate such reasoning, Manna's book includes a nonrecursive algorithm that simulates the original (recursive) 91 function. Many of the papers that report an "automated verification" (or termination proof) of the 91 function only handle the nonrecursive version.
A formal derivation of the nonrecursive version from the recursive one was given in a 1980 article by Mitchell Wand, based on the use of continuations.
Examples
Example A:
M(99) = M(M(110)) since 99 ≤ 100 = M(100) since 110 > 100 = M(M(111)) since 100 ≤ 100 = M(101) since 111 > 100 = 91 since 101 > 100
Example B:
M(87) = M(M(98)) = M(M(M(109))) = M(M(99)) = M(M(M(110))) = M(M(100)) = M(M(M(111))) = M(M(101)) = M(91) = M(M(102)) = M(92) = M(M(103)) = M(93) .... Pattern continues = M(99) (same as example A) = 91
Code
Here is how John McCarthy may have written this function in Lisp, the language he invented:
(defun mc91 (n) (cond ((<= n 100) (mc91 (mc91 (+ n 11)))) (t ( n 10))))
Here is an implementation of the nonrecursive algorithm in C:
int mccarthy(int n) { int c; for (c = 1; c != 0; ) { if (n > 100) { n = n  10; c; } else { n = n + 11; c++; } } return n; }
Proof
Here is a proof that the function behaves as expected.
For 90 ≤ n < 101,
M(n) = M(M(n + 11)) = M(n + 11  10), where n + 11 >= 101 since n >= 90 = M(n + 1)
So M(n) = 91 for 90 ≤ n < 101.
We can use this as a base case for induction on blocks of 11 numbers, like so:
Assume that M(n) = 91 for a ≤ n < a + 11.
Then, for any n such that a  11 ≤ n < a,
M(n) = M(M(n + 11)) = M(91), by hypothesis, since a ≤ n + 11 < a + 11 = 91, by the base case.
Now by induction M(n) = 91 for any n in such a block. There are no holes between the blocks, so M(n) = 91 for n < 101. We can also add n = 101 as a special case.
Knuth's generalization
Donald Knuth generalized the 91 function to include additional parameters. John Cowles developed a formal proof that Knuth's generalized function was total, using the ACL2 theorem prover.
References
 Zohar Manna and Amir Pnueli (July 1970). "Formalization of Properties of Functional Programs". Journal of the ACM 17 (3): 555–569. doi:10.1145/321592.321606.
 Zohar Manna and John McCarthy (1970). "Properties of programs and partial function logic". Machine Intelligence 5.
 Zohar Manna. Mathematical Theory of Computation. McGrawHill Book Company, NewYork, 1974. Reprinted in 2003 by Dover Publications.
 Mitchell Wand (January 1980). "ContinuationBased Program Transformation Strategies". Journal of the ACM 27 (1): 164–180. doi:10.1145/322169.322183.
 Donald E. Knuth (1991). "Textbook Examples of Recursion". Artificial intelligence and mathematical theory of computation. arXiv:cs/9301113.
 John Cowles (2000). "Knuth's generalization of McCarthy's 91 function". ComputerAided reasoning: ACL2 case studies. Kluwer Academic Publishers. pp. 283–299. http://www.cs.utexas.edu/users/moore/acl2/workshop1999/Cowlesabstract.html.
John McCarthy Artificial intelligence • Circumscription • Dartmouth Conferences • Frame problem • Garbage collection • Lisp • McCarthy 91 function • Situation calculus • Space fountain • Vera WatsonCategories: Formal methods
 Recurrence relations
Wikimedia Foundation. 2010.
Look at other dictionaries:
McCarthy Building (Chicago, Illinois) — McCarthy Building McCarthy Building on the southwest corner of Block 37. General information Location 32 West Washington Street Chicago, Illinois … Wikipedia
McCarthy Formalism — In computer science and recursion theory the McCarthy Formalism (1963) 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 the four of… … Wikipedia
John McCarthy (computer scientist) — Infobox Scientist name = John McCarthy image width= 200px caption = John McCarthy at a summit in 2006 birth date = birth date and age192794 birth place = Boston, Massachusetts, USA residence = USA nationality = American field = Computer… … Wikipedia
Μrecursive function — In mathematical logic and computer science, the μ recursive functions are a class of partial functions from natural numbers to natural numbers which are computable in an intuitive sense. In fact, in computability theory it is shown that the μ… … Wikipedia
μrecursive function — In mathematical logic and computer science, the μ recursive functions are a class of partial functions from natural numbers to natural numbers which are computable in an intuitive sense. In fact, in computability theory it is shown that the μ… … Wikipedia
Mary McCarthy (CIA) — For other people of the same name, see Mary McCarthy. Mary O Neil McCarthy (born 1945) is a former United States Central Intelligence Agency (CIA) employee who last worked in the Office of the Inspector General. In her career, she was an… … Wikipedia
James McCarthy — Bishop James F. McCarthy (born July 9, 1942) was an auxiliary bishop in the Archdiocese of New York, who resigned from his parish assignment during the 2002 sex scandal in the Roman Catholic Church.His first assignment was to the Church of Saint… … Wikipedia
Tak (function) — Tak is a recursive mathematical function defined as def tak( x, y, z) unless y < x z else tak( tak(x 1, y, z), tak(y 1, z, x), tak(z 1, x, y) ) endend It is often used as a benchmark for languages with optimization for recursion.tak() vs.… … Wikipedia
Fonction de McCarthy n°91 — La fonction f91 de McCarthy est une fonction dont voici le programme en Pascal : function f91(n : CARDINAL) : CARDINAL; begin if n > 100 then begin f91 := n 10; end else begin f91 := f91(f91(n+11)); end {if}; end {f91}; Portail de la… … Wikipédia en Français
Artificial intelligence — AI redirects here. For other uses, see Ai. For other uses, see Artificial intelligence (disambiguation). TOPIO, a humanoid robot, played table tennis at Tokyo International Robot Exhibition (IREX) 2009.[1] Artificial intelligence ( … Wikipedia