Significance of McCarthy 91 function in Computer Science

Question

While learning recursion i came across the McCarthy 91 function which returns the value 91 for all integer arguments n <= 101, and n - 10 for n > 101.

 int McCarthy(int n)
 {
   if (n > 100)
     return n - 10;
   return McCarthy(McCarthy(n+11));
 }

int main()
{
  printf(" %d ", McCarthy(45));
  return 0;
}

I was just curious to know what is its significance in Computer Science? The Wikipedia article says that it is used as a test case for formal verification. What does that mean.?

Can someone simplify its usage for me?

Answer 1

Imagine you are writing a C compiler, which accepts programs like the one you wrote and produces executable code. You want to test that your compiler works correctly. You make a test case that is the recursive definition of the function as you wrote it, and assert that when you run the compiled code you get the easy to calculate result (in this case the program should output 91). Difficult test cases like this would be particularly useful if you are starting to write optimizations for compiling recursive calls.

Imagine that instead of writing a compiler, you are writing a program that tries to write a proof, like you would write in a math class. The inputs to the program might be a set of transformations like the algebra laws you use to write a proof, and a statement that the program attempts to prove. This branch of computer science is called formal verification. Statements involving the McCarthy 91 function are difficult to prove. For example (for all x <= 100, M(x) == 91) would be very difficult to prove. This would be a very hard problem for your proof writing program and transformations to produce a proof of.