McCarthy 91 function
This article includes a improve this article by introducing more precise citations. (October 2015) ) |
The McCarthy 91 function is a recursive function, defined by the 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 > 100. Indeed, the result of M(101) is also 91 (101 - 10 = 91). All results of M(n) after n = 101 are continually increasing by 1, e.g. M(102) = 92, M(103) = 93.
History
The 91 function was introduced in papers published by
It is easier to reason about
As one of the examples used to demonstrate such reasoning, Manna's book includes a tail-recursive algorithm equivalent to the nested-recursive 91 function. Many of the papers that report an "automated verification" (or
This is an equivalent mutually tail-recursive definition:
A formal derivation of the mutually tail-recursive version from the nested-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 increasing till M(99), M(100) and M(101), exactly as we saw on the example A) = M(101) since 111 > 100 = 91 since 101 > 100
Code
Here is an implementation of the nested-recursive algorithm in Lisp:
(defun mc91 (n)
(cond ((<= n 100) (mc91 (mc91 (+ n 11))))
(t (- n 10))))
Here is an implementation of the nested-recursive algorithm in Haskell:
mc91 n
| n > 100 = n - 10
| otherwise = mc91 $ mc91 $ n + 11
Here is an implementation of the nested-recursive algorithm in OCaml:
let rec mc91 n =
if n > 100 then n - 10
else mc91 (mc91 (n + 11))
Here is an implementation of the tail-recursive algorithm in OCaml:
let mc91 n =
let rec aux n c =
if c = 0 then n
else if n > 100 then aux (n - 10) (c - 1)
else aux (n + 11) (c + 1)
in
aux n 1
Here is an implementation of the nested-recursive algorithm in Python:
def mc91(n: int) -> int:
"""McCarthy 91 function."""
if n > 100:
return n - 10
else:
return mc91(mc91(n + 11))
Here is an implementation of the nested-recursive algorithm in C:
int mc91(int n)
{
if (n > 100) {
return n - 10;
} else {
return mc91(mc91(n + 11));
}
}
Here is an implementation of the tail-recursive algorithm in C:
int mc91(int n)
{
return mc91taux(n, 1);
}
int mc91taux(int n, int c)
{
if (c != 0) {
if (n > 100) {
return mc91taux(n - 10, c - 1);
} else {
return mc91taux(n + 11, c + 1);
}
} else {
return n;
}
}
Proof
Here is a proof that the McCarthy 91 function is equivalent to the non-recursive algorithm defined as:
For n > 100, the definitions of and are the same. The equality therefore follows from the definition of .
For n ≤ 100, a
For 90 ≤ n ≤ 100,
M(n) = M(M(n + 11)), by definition = M(n + 11 - 10), since n + 11 > 100 = M(n + 1)
This can be used to show M(n) = M(101) = 91 for 90 ≤ n ≤ 100:
M(90) = M(91), M(n) = M(n + 1) was proven above = … = M(101), by definition = 101 − 10 = 91
M(n) = M(101) = 91 for 90 ≤ n ≤ 100 can be used as the base case of the induction.
For the downward induction step, let n ≤ 89 and assume M(i) = 91 for all n < i ≤ 100, then
M(n) = M(M(n + 11)), by definition = M(91), by hypothesis, since n < n + 11 ≤ 100 = 91, by the base case.
This proves M(n) = 91 for all n ≤ 100, including negative values.
Knuth's generalization
Donald Knuth generalized the 91 function to include additional parameters.[1] John Cowles developed a formal proof that Knuth's generalized function was total, using the ACL2 theorem prover.[2]
References
- S2CID 6411737.
- ISBN 9781475731880.
- Manna, Zohar; Pnueli, Amir (July 1970). "Formalization of Properties of Functional Programs". Journal of the ACM. 17 (3): 555–569. S2CID 5924829.
- Manna, Zohar; McCarthy, John (1970). "Properties of programs and partial function logic". Machine Intelligence. 5. OCLC 35422131.
- Manna, Zohar (1974). Mathematical Theory of Computation (4th ed.). McGraw-Hill. ISBN 9780070399105.
- Wand, Mitchell (January 1980). "Continuation-Based Program Transformation Strategies". Journal of the ACM. 27 (1): 164–180. S2CID 16015891.