McCarthy 91 function

<h2 id="history">History</h2>
The 91 function was introduced in papers published by <a href="/facts/Zohar_Manna/HhXzkaAx">Zohar Manna</a>, <a href="/facts/Amir_Pnueli/qJ7mMEXm">Amir Pnueli</a> and <a href="/facts/John_McCarthy_(computer_scientist)/ajKU4SdD">John McCarthy</a> in 1970. These papers represented early developments towards the application of <a href="/facts/Formal_methods/tw4FCWIb">formal methods</a> to <a href="/facts/Formal_verification/BYD4GnJR">program verification</a>. The 91 function was chosen for being nested-recursive (contrasted with <a href="/facts/Single_recursion/2uXo18Gv">single recursion</a>, 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 <a href="/facts/Tail_recursion/oLX6hfm3">tail-recursive</a> control flow, this is an equivalent (<a href="/facts/Extensionality/CwPNkVTW">extensionally equal</a>) 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 <a href="/facts/Termination_proof/T740cWY7">termination proof</a>) of the 91 function only handle the tail-recursive version.
This is an equivalent <a href="/facts/Mutual_recursion/fVkAoMFT">mutually</a> 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 <a href="/facts/Mitchell_Wand/6pKeqdx7">Mitchell Wand</a>, based on the use of <a href="/facts/Continuation/53gyBXrB">continuations</a>.

<h2 id="examples">Examples</h2>
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

<h2 id="code">Code</h2>
Here is an implementation of the nested-recursive algorithm in <a href="/facts/Lisp_(programming_language)/xJHA3CrX">Lisp</a>:

(defun mc91 (n)
 (cond ((<= n 100) (mc91 (mc91 (+ n 11))))
 (t (- n 10))))

Here is an implementation of the nested-recursive algorithm in <a href="/facts/Haskell/ydEsHuGy">Haskell</a>:

mc91 n 
 | n > 100 = n - 10
 | otherwise = mc91 $ mc91 $ n + 11

Here is an implementation of the nested-recursive algorithm in <a href="/facts/OCaml/ThBGLND8">OCaml</a>:

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 <a href="/facts/OCaml/ThBGLND8">OCaml</a>:

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 <a href="/facts/Python_(programming_language)/YbuGqofa">Python</a>:

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 <a href="/facts/C_(programming_language)/Ky2No763">C</a>:

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 <a href="/facts/C_(programming_language)/Ky2No763">C</a>:

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;
    }
}

<h2 id="proof">Proof</h2>
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 <a href="/facts/Strong_induction/KxAPqNrH">strong induction</a> 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.
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.

<h2 id="knuths-generalization">Knuth's generalization</h2>
<a href="/facts/Donald_Knuth/GozNzDM6">Donald Knuth</a> generalized the 91 function to include additional parameters.<a class="footnote-ref" id="fnref:1" href="#fn:1">1</a> John Cowles developed a formal proof that Knuth's generalized function was total, using the <a href="/facts/ACL2/h1RX6FSe">ACL2</a> theorem prover.<a class="footnote-ref" id="fnref:2" href="#fn:2">2</a>

<ul><li>Manna, Zohar; Pnueli, Amir (July 1970). <a href="https://doi.org/10.1145%2F321592.321606">"Formalization of Properties of Functional Programs"</a>. Journal of the ACM. 17 (3): 555–569. <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1145%2F321592.321606">10.1145/321592.321606</a>. <a href="/facts/S2CID_(identifier)/ldJsHa2Y">S2CID</a> <a href="https://api.semanticscholar.org/CorpusID:5924829">5924829</a>.</li>
<li>Manna, Zohar; McCarthy, John (1970). "Properties of programs and partial function logic". Machine Intelligence. 5. <a href="/facts/OCLC_(identifier)/Yqad8waq">OCLC</a> <a href="https://search.worldcat.org/oclc/35422131">35422131</a>.</li>
<li>Manna, Zohar (1974). Mathematical Theory of Computation (4th ed.). McGraw-Hill. <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 9780070399105.</li>
<li>Wand, Mitchell (January 1980). <a href="https://doi.org/10.1145%2F322169.322183">"Continuation-Based Program Transformation Strategies"</a>. Journal of the ACM. 27 (1): 164–180. <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1145%2F322169.322183">10.1145/322169.322183</a>. <a href="/facts/S2CID_(identifier)/ldJsHa2Y">S2CID</a> <a href="https://api.semanticscholar.org/CorpusID:16015891">16015891</a>.</li></ul>

<h2 id="references">References</h2>

<ol>
<li id="fn:1">Knuth, Donald E. (1991). "Textbook Examples of Recursion". Artificial Intelligence and Mathematical Theory of Computation: 207–229. arXiv:cs/9301113. Bibcode:1993cs........1113K. doi:10.1016/B978-0-12-450010-5.50018-9. ISBN 9780124500105. S2CID 6411737. <a href="9780124500105" target="_blank">9780124500105</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></li>
<li id="fn:2">Cowles, John (2013) [2000]. "Knuth's generalization of McCarthy's 91 function". In Kaufmann, M.; Manolios, P.; Strother Moore, J (eds.). Computer-Aided reasoning: ACL2 case studies. Kluwer Academic. pp. 283–299. ISBN 9781475731880. <a href="9781475731880" target="_blank">9781475731880</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></li>
</ol>

McCarthy 91 function open-in-new

McCarthy 91 function