Función McCarthy 91

La función McCarthy 91 es una función recursiva , definida por el científico informático John McCarthy como un caso de prueba para la verificación formal dentro de la informática .

La función McCarthy 91 se define como

${\displaystyle M(n)={\begin{cases}n-10,&{\mbox{si }}n>100{\mbox{ }}\\M(M(n+11)),&{\mbox{si }}n\leq 100{\mbox{ }}\end{cases}}}$

Los resultados de la evaluación de la función son M ( n )  =  91 para todos los argumentos enteros n  ≤  100, y M ( n )  = n − 10 para n > 100. De hecho, el resultado de M(101) también es 91 (101 - 10 = 91). Todos los resultados de M(n) después de n = 101 aumentan continuamente en 1, por ejemplo, M(102) = 92, M(103) = 93.   

La función 91 fue introducida en artículos publicados por Zohar Manna , Amir Pnueli y John McCarthy en 1970. Estos artículos representaron los primeros desarrollos hacia la aplicación de métodos formales a la verificación de programas . La función 91 fue elegida por ser recursiva anidada (en contraste con la recursión simple , como la definición de${\displaystyle f(n)}$mediante${\displaystyle f(n-1)}$Este ejemplo fue popularizado por el libro de Manna, Teoría Matemática de la Computación (1974). A medida que el campo de los Métodos Formales avanzaba, este ejemplo apareció repetidamente en la literatura de investigación. En particular, se considera un "problema desafiante" para la verificación automatizada de programas.

Es más fácil razonar sobre el flujo de control recursivo de cola , esta es una definición equivalente ( extensionalmente igual ):

${\displaystyle M_{t}(n)=M_{t}'(n,1)}$

${\displaystyle M_{t}'(n,c)={\begin{cases}n,&{\mbox{si }}c=0\\M_{t}'(n-10,c-1),&{\mbox{si }}n>100{\mbox{ y }}c\neq 0\\M_{t}'(n+11,c+1),&{\mbox{si }}n\leq 100{\mbox{ y }}c\neq 0\end{cases}}}$

Como uno de los ejemplos utilizados para demostrar dicho razonamiento, el libro de Manna incluye un algoritmo recursivo de cola equivalente a la función recursiva anidada 91. Muchos de los artículos que informan sobre una "verificación automatizada" (o prueba de terminación ) de la función 91 solo manejan la versión recursiva de cola.

Esta es una definición equivalente mutuamente recursiva de cola:

${\displaystyle M_{mt}(n)=M_{mt}'(n,0)}$

${\displaystyle M_{mt}'(n,c)={\begin{cases}M_{mt}''(n-10,c),&{\mbox{si }}n>100{\mbox{ }}\\M_{mt}'(n+11,c+1),&{\mbox{si }}n\leq 100{\mbox{ }}\end{cases}}}$

${\displaystyle M_{mt}''(n,c)={\begin{cases}n,&{\mbox{si }}c=0{\mbox{ }}\\M_{mt}'(n,c-1),&{\mbox{si }}c\neq 0{\mbox{ }}\end{cases}}}$

En un artículo de Mitchell Wand de 1980 , basado en el uso de continuaciones , se presentó una derivación formal de la versión recursiva de cola mutua a partir de la versión recursiva anidada.

Ejemplo A:

M(99) = M(M(110)) ya que 99 ≤ 100 = M(100) ya que 110 > 100 = M(M(111)) ya que 100 ≤ 100 = M(101) ya que 111 > 100 = 91 puesto que 101 > 100

Ejemplo 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) ... El patrón continúa aumentando hasta M(99), M(100) y M(101), exactamente como vimos en el ejemplo A). = M(101) ya que 111 > 100 = 91 puesto que 101 > 100

Aquí se muestra una implementación del algoritmo recursivo anidado en Python :

def mc91 ( n : int ) -> int : if n > 100 : return n - 10 else : return mc91 ( mc91 ( n + 11 ))

Aquí se muestra una implementación del algoritmo recursivo de cola en 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 )

Aquí hay una prueba de que la función McCarthy 91${\displaystyle M}$es equivalente al algoritmo no recursivo${\displaystyle M'}$definido como:

${\displaystyle M'(n)={\begin{cases}n-10,&{\mbox{si }}n>100{\mbox{ }}\\91,&{\mbox{si }}n\leq 100{\mbox{ }}\end{cases}}}$

Para n > 100, las definiciones de${\displaystyle M'}$y${\displaystyle M}$son lo mismo. Por lo tanto, la igualdad se deduce de la definición de${\displaystyle M}$.

Para n ≤ 100, se puede utilizar una fuerte inducción descendente desde 100:

Para 90 ≤ n ≤ 100,

M(n) = M(M(n + 11)), por definición = M(n + 11 - 10), ya que n + 11 > 100 = M(n + 1)

Esto se puede utilizar para demostrar que M ( n ) = M (101) = 91 para 90 ≤ n ≤ 100:

Se demostró anteriormente que M(90) = M(91) y M(n) = M(n + 1). = … = M(101), por definición = 101 − 10 = 91

M ( n ) = M (101) = 91 para 90 ≤ n ≤ 100 se puede utilizar como caso base de la inducción.

Para el paso de inducción descendente, sea n ≤ 89 y suponga M ( i ) = 91 para todo n < i ≤ 100, entonces

M(n) = M(M(n + 11)), por definición = M(91), por hipótesis, ya que n < n + 11 ≤ 100 = 91, según el caso base.

Esto prueba que M ( n ) = 91 para todo n ≤ 100, incluidos los valores negativos.

Donald Knuth generalizó la función 91 para incluir parámetros adicionales. ^{[ 1 ]} John Cowles desarrolló una prueba formal de que la función generalizada de Knuth era total, utilizando el demostrador de teoremas ACL2 . ^{[ 2 ]}

• Manna, Zohar; Pnueli, Amir (julio de 1970). "Formalización de propiedades de programas funcionales" . Journal of the ACM . 17 (3): 555– 569. doi : 10.1145/321592.321606 . S2CID 5924829 . 
• Manna, Zohar; McCarthy, John (1970). "Propiedades de los programas y lógica de funciones parciales". Machine Intelligence . 5. OCLC 35422131 . 
• Maná, Zohar (1974). Teoría Matemática de la Computación (4ª  ed.). McGraw-Hill. ISBN 9780070399105.
• Wand, Mitchell (enero de 1980). "Estrategias de transformación de programas basadas en la continuidad" . Journal of the ACM . 27 (1): 164– 180. doi : 10.1145/322169.322183 . S2CID 16015891 .