McCarthy 91 function: Difference between revisions

Revision as of 03:32, 7 May 2003

Latest revision as of 13:19, 10 July 2025

(118 intermediate revisions by 82 users not shown)

Line 1:

{{no footnotes|date=October 2015}}

In [[discrete mathematics]], the '''McCarthy 91 function''' is a [[recursive]] function which takes the value 91 for all positive integers less than 102. Conceived by [[computer scientist]] [[John McCarthy]].

The '''McCarthy 91 function''' is a [[Recursion (computer science)|recursive function]], defined by the [[computer scientist]] [[John McCarthy (computer scientist)|John McCarthy]] as a test case for [[formal verification]] within [[computer science]].

The McCarthy 91 function is defined as

:<math>M(n)=\left\{\begin{matrixcases}
n - 10, & \mbox{if }n > 100\mbox{ } \\
M(M(n+11)), & \mbox{if }n \le 100\mbox{ }
\end{matrixcases}\right.</math>

The results of evaluating the function are given by ''M''(''n'')&nbsp;=&nbsp;91 for all integer arguments ''n''&nbsp;≤&nbsp;100, and ''M''(''n'')&nbsp;=&nbsp;''n''&nbsp;&minus;&nbsp;10 for ''n'' &gt; 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.

Examples:

==History==

M(99) = M(M(110)) since 99 <math>\le</math> 100

The 91 function was introduced in papers published by [[Zohar Manna]], [[Amir Pnueli]] and [[John McCarthy (computer scientist)|John McCarthy]] in 1970. These papers represented early developments towards the application of [[formal methods]] to [[formal verification|program verification]]. The 91 function was chosen for being nested-recursive (contrasted with [[single recursion]], such as defining <math>f(n)</math> by means of <math>f(n-1)</math>). 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.

= M(100) since 110 > 100

In particular, it is viewed as a "challenge problem" for automated program verification.

= M(M(111)) since 100 <math>\le</math> 100

= M(101) since 111 > 100

= 91 since 101 > 100

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

:<math>M_t(n)= M_t'(n,1)</math>

:<math>M_t'(n, c)=\begin{cases}

n, & \mbox{if }c = 0\\

M_t'(n-10, c-1), & \mbox{if }n > 100\mbox{ and } c \ne 0 \\

M_t'(n+11, c+1), & \mbox{if }n \le 100\mbox{ and } c \ne 0

\end{cases}

</math>

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 [[mutual recursion|mutually]] tail-recursive definition:

:<math>M_{mt}(n)= M_{mt}'(n,0)</math>

:<math>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 \le 100\mbox{ }

\end{cases}</math>

:<math>M_{mt}''(n,c)=\begin{cases}

n, & \mbox{if }c = 0\mbox{ } \\

M_{mt}'(n,c-1), & \mbox{if }c \ne 0\mbox{ }

\end{cases}</math>

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 [[continuation]]s.

==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))

Line 26 ⟶ 60:

= 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(99101) since 111 > 100

(same as= above91 proof) since 101 > 100

==Code==

Here is an implementation of the nested-recursive algorithm in [[Python (programming language)|Python]]:

<syntaxhighlight lang="python">

def mc91(n: int) -> int:

if n > 100:

return n - 10

else:

return mc91(mc91(n + 11))

</syntaxhighlight>

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

<syntaxhighlight lang="python">

def mc91(n: int) -> int:

return mc91taux(n, 1)

def mc91taux(n: int, c: int) -> int:

if c == 0:

return n

elif n > 100:

return mc91taux(n - 10, c - 1)

else:

return mc91taux(n + 11, c + 1)

</syntaxhighlight>

==Proof==

Here is a proof that the McCarthy 91 function <math>M</math> is equivalent to the non-recursive algorithm <math>M'</math>defined as:

:<math>M'(n)=\begin{cases}

n - 10, & \mbox{if }n > 100\mbox{ } \\

91, & \mbox{if }n \le 100\mbox{ }

\end{cases}</math>

For ''n'' &gt; 100, the definitions of <math>M'</math> and <math>M</math> are the same. The equality therefore follows from the definition of <math>M</math>.

For ''n'' ≤ 100, a [[strong 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 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.

Here's a sample McCarthy 91 program in Java:

For the downward induction step, let ''n'' ≤ 89 and assume ''M''(''i'') = 91 for all ''n'' &lt; ''i'' ≤ 100, then

public class McCarthy extends Object

{

static int count = -1;

M(n) = M(M(n + 11)), by definition

public McCarthy()

= M(91), by hypothesis, since n &lt; n + 11 ≤ 100

{

= 91, }by the base case.

This proves ''M''(''n'') = 91 for all ''n'' ≤ 100, including negative values.

public int Mc91(int n)

{

count = count + 1;

== Knuth's generalization ==

System.out.println("Number after " + count + " iteration(s): " + n);

if ( n < 0 )

{

System.out.println("\n Not a positive integer");

System.exit(-1);

}

[[Donald Knuth]] generalized the 91 function to include additional parameters.<ref>{{cite journal |first=Donald E. |last=Knuth | title = Textbook Examples of Recursion | year = 1991 | journal = Artificial Intelligence and Mathematical Theory of Computation |pages=207–229 |doi=10.1016/B978-0-12-450010-5.50018-9 | arxiv = cs/9301113| bibcode = 1993cs........1113K |isbn=9780124500105 |s2cid=6411737 }}</ref> [[John Cowles (mathematician)|John Cowles]] developed a formal proof that Knuth's generalized function was total, using the [[ACL2]] theorem prover.<ref>{{cite book |first=John |last=Cowles | chapter = Knuth's generalization of McCarthy's 91 function |editor-first=M. |editor-last=Kaufmann |editor2-first=P. |editor2-last=Manolios |editor3-first=J |editor3-last=Strother Moore | title = Computer-Aided reasoning: ACL2 case studies | publisher = Kluwer Academic |isbn=9781475731880 |year=2013 |orig-year = 2000 | pages = 283–299 |chapter-url = http://www.cs.utexas.edu/users/moore/acl2/workshop-1999/Cowles-abstract.html}}</ref>

if ( n > 100 )

{

return n-10;

}

== References ==

if ( n < 101 )

{{Reflist}}

{

* {{cite journal |first1=Zohar |last1=Manna |first2=Amir |last2=Pnueli |title=Formalization of Properties of Functional Programs |journal=Journal of the ACM |date=July 1970 |volume=17 |issue=3 |pages=555–569 |doi=10.1145/321592.321606|s2cid=5924829 |doi-access=free }}

return Mc91(Mc91(n+11));

* {{cite journal |first1=Zohar |last1=Manna |first2=John |last2=McCarthy |title=Properties of programs and partial function logic |journal=Machine Intelligence |year=1970 |volume=5 |oclc=35422131}}

}

* {{cite book |first=Zohar |last=Manna |title=Mathematical Theory of Computation |publisher=McGraw-Hill |year=1974 |edition=4th |isbn=9780070399105}}

* {{cite journal |first=Mitchell |last=Wand |title=Continuation-Based Program Transformation Strategies |journal=Journal of the ACM |date=January 1980 |volume=27 |issue=1 |pages=164–180 |doi=10.1145/322169.322183|s2cid=16015891 |doi-access=free }}

{{John McCarthy}}

return 0;

}

[[Category:Articles with example C code]]

public static void main(String[] args)

[[Category:Articles with example Haskell code]]

{

[[Category:Articles with example Lisp (programming language) code]]

McCarthy yorick1 = new McCarthy();

[[Category:Articles with example OCaml code]]

int yorick = Integer.parseInt(args[0]);

[[Category:Articles with example Python (programming language) code]]

System.out.println("\n Number: " + yorick);

[[Category:Formal methods]]

System.out.println("Final Number: " + yorick1.Mc91(yorick));

[[Category:Recurrence relations]]

}

}