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

M ( n ) = { n − 10 , if n > 100 M ( M ( n + 11 ) ) , if n ≤ 100 {\displaystyle M(n)={\begin{cases}n-10,&{\mbox{if }}n>100{\mbox{ }}\\M(M(n+11)),&{\mbox{if }}n\leq 100{\mbox{ }}\end{cases}}}

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 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 being nested-recursive (contrasted with single recursion, such as defining f ( n ) {\displaystyle f(n)} by means of f ( n − 1 ) {\displaystyle 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.

It is easier to reason about tail-recursive control flow, this is an equivalent (extensionally equal) definition:

M t ( n ) = M t ′ ( n , 1 ) {\displaystyle M_{t}(n)=M_{t}'(n,1)}

M t ′ ( n , c ) = { n , if c = 0 M t ′ ( n − 10 , c − 1 ) , if n > 100 and c ≠ 0 M t ′ ( n + 11 , c + 1 ) , if n ≤ 100 and c ≠ 0 {\displaystyle M_{t}'(n,c)={\begin{cases}n,&{\mbox{if }}c=0\\M_{t}'(n-10,c-1),&{\mbox{if }}n>100{\mbox{ and }}c\neq 0\\M_{t}'(n+11,c+1),&{\mbox{if }}n\leq 100{\mbox{ and }}c\neq 0\end{cases}}}

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 termination proof) of the 91 function only handle the tail-recursive version.

This is an equivalent mutually tail-recursive definition:

M m t ( n ) = M m t ′ ( n , 0 ) {\displaystyle M_{mt}(n)=M_{mt}'(n,0)}

M m t ′ ( n , c ) = { M m t ″ ( n − 10 , c ) , if n > 100 M m t ′ ( n + 11 , c + 1 ) , if n ≤ 100 {\displaystyle M_{mt}'(n,c)={\begin{cases}M_{mt}''(n-10,c),&{\mbox{if }}n>100{\mbox{ }}\\M_{mt}'(n+11,c+1),&{\mbox{if }}n\leq 100{\mbox{ }}\end{cases}}}

M m t ″ ( n , c ) = { n , if c = 0 M m t ′ ( n , c − 1 ) , if c ≠ 0 {\displaystyle M_{mt}''(n,c)={\begin{cases}n,&{\mbox{if }}c=0{\mbox{ }}\\M_{mt}'(n,c-1),&{\mbox{if }}c\neq 0{\mbox{ }}\end{cases}}}

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:

Example B:

Code

Here is an implementation of the nested-recursive algorithm in Python:

Here is an implementation of the tail-recursive algorithm in Python:

Proof

Here is a proof that the McCarthy 91 function M {\displaystyle M} is equivalent to the non-recursive algorithm M ′ {\displaystyle M'}defined as:

M ′ ( n ) = { n − 10 , if n > 100 91 , if n ≤ 100 {\displaystyle M'(n)={\begin{cases}n-10,&{\mbox{if }}n>100{\mbox{ }}\\91,&{\mbox{if }}n\leq 100{\mbox{ }}\end{cases}}}

For n > 100, the definitions of M ′ {\displaystyle M'} and M {\displaystyle M} are the same. The equality therefore follows from the definition of M {\displaystyle M}.

For n ≤ 100, a strong induction downward from 100 can be used:

For 90 ≤ n ≤ 100,

This can be used to show M(n) = M(101) = 91 for 90 ≤ n ≤ 100:

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

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. John Cowles developed a formal proof that Knuth's generalized function was total, using the ACL2 theorem prover.

  • Manna, Zohar; Pnueli, Amir (July 1970). . Journal of the ACM. 17 (3): 555–569. doi:. S2CID .
  • Manna, Zohar; McCarthy, John (1970). "Properties of programs and partial function logic". Machine Intelligence. 5. OCLC .
  • Manna, Zohar (1974). Mathematical Theory of Computation (4th ed.). McGraw-Hill. ISBN 9780070399105.
  • Wand, Mitchell (January 1980). . Journal of the ACM. 27 (1): 164–180. doi:. S2CID .