The McCarthy 91 function is a
recursive function, defined by the
computer scientist John McCarthy as a test case for
formal verification
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal met ...
within
computer science
Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to practical disciplines (includi ...
.
The McCarthy 91 function is defined as
:
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
In computer science, formal methods are mathematically rigorous techniques for the specification, development, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the exp ...
to
program verification
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal metho ...
. The 91 function was chosen for being nested-recursive (contrasted with
single 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 about
tail-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" (or
termination proof) of the 91 function only handle the tail-recursive version.
This is an equivalent
mutually tail-recursive definition:
:
:
:
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
In computer science, a continuation is an abstract representation of the control state of a computer program. A continuation implements ( reifies) the program control state, i.e. the continuation is a data structure that represents the computati ...
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))
= 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
Code
Here is an implementation of the nested-recursive algorithm in
Lisp:
(defun mc91 (n)
(cond ((<= n 100) (mc91 (mc91 (+ n 11))))
(t (- n 10))))
Here is an implementation of the nested-recursive algorithm in
Haskell
Haskell () is a general-purpose, statically-typed, purely functional programming language with type inference and lazy evaluation. Designed for teaching, research and industrial applications, Haskell has pioneered a number of programming lan ...
:
mc91 n
, n > 100 = n - 10
, otherwise = mc91 $ mc91 $ n + 11
Here is an implementation of the nested-recursive algorithm in
OCaml:
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
OCaml:
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
Python
Python may refer to:
Snakes
* Pythonidae, a family of nonvenomous snakes found in Africa, Asia, and Australia
** ''Python'' (genus), a genus of Pythonidae found in Africa and Asia
* Python (mythology), a mythical serpent
Computing
* Python (pro ...
:
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
C:
int mc91(int n)
Here is an implementation of the tail-recursive algorithm in
C:
int mc91(int n)
int mc91taux(int n, int c)
Proof
Here is a proof that
:
which provides an equivalent non-recursive algorithm to compute
.
For ''n'' > 100, equality follows from the definition of
. For ''n'' ≤ 100, a
strong induction
Mathematical induction is a method for proving that a statement ''P''(''n'') is true for every natural number ''n'', that is, that the infinitely many cases ''P''(0), ''P''(1), ''P''(2), ''P''(3), ... all hold. Informal metaphors help ...
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)
So ''M''(''n'') = ''M''(101) = 91 for 90 ≤ ''n'' ≤ 100.
This can be used as base case.
For the 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.
Knuth's generalization
Donald Knuth
Donald Ervin Knuth ( ; born January 10, 1938) is an American computer scientist, mathematician, and professor emeritus at Stanford University. He is the 1974 recipient of the ACM Turing Award, informally considered the Nobel Prize of computer sc ...
generalized the 91 function to include additional parameters.
John Cowles developed a formal proof that Knuth's generalized function was total, using the
ACL2
ACL2 ("A Computational Logic for Applicative Common Lisp") is a software system consisting of a programming language, created by Timothy Still it was an extensible theory in a first-order logic, and an automated theorem prover. ACL2 is designed t ...
theorem prover.
References
*
*
*
*
{{John McCarthy
Formal methods
Recurrence relations