 | This article includes alist of references,related reading, orexternal links,but its sources remain unclear because it lacksinline citations. Please helpimprove this article byintroducing more precise citations.(October 2015) (Learn how and when to remove this message) |
TheMcCarthy 91 function is arecursive function, defined by thecomputer scientistJohn McCarthy as a test case forformal verification withincomputer science.
The McCarthy 91 function is defined as
The results of evaluating the function are given byM(n) = 91 for all integer argumentsn ≤ 100, andM(n) = n − 10 forn > 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.
The 91 function was introduced in papers published byZohar Manna,Amir Pnueli andJohn McCarthy in 1970. These papers represented early developments towards the application offormal methods toprogram verification. The 91 function was chosen for being nested-recursive (contrasted withsingle recursion, such as defining by means of). 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 abouttail-recursive control flow, this is an equivalent (extensionally equal) definition:
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" (ortermination proof) of the 91 function only handle the tail-recursive version.
This is an equivalentmutually tail-recursive definition:
A formal derivation of the mutually tail-recursive version from the nested-recursive one was given in a 1980 article byMitchell Wand, based on the use ofcontinuations.
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
Here is an implementation of the nested-recursive algorithm inPython:
defmc91(n:int)->int:ifn>100:returnn-10else:returnmc91(mc91(n+11))
Here is an implementation of the tail-recursive algorithm in Python:
defmc91(n:int)->int:returnmc91taux(n,1)defmc91taux(n:int,c:int)->int:ifc==0:returnnelifn>100:returnmc91taux(n-10,c-1)else:returnmc91taux(n+11,c+1)
Here is a proof that the McCarthy 91 function is equivalent to the non-recursive algorithmdefined as:
Forn > 100, the definitions of and are the same. The equality therefore follows from the definition of.
Forn ≤ 100, astrong induction downward from 100 can be used:
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 showM(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, letn ≤ 89 and assumeM(i) = 91 for alln <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 provesM(n) = 91 for alln ≤ 100, including negative values.
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 theACL2 theorem prover.[2]