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)}
… excerpt ends here. Continue reading the full article.
