Fonction McCarthy 91 - McCarthy 91 function

La fonction McCarthy 91 est une fonction récursive , définie par l' informaticien John McCarthy comme un cas test pour la vérification formelle en informatique .

La fonction McCarthy 91 est définie comme

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

Les résultats de l'évaluation de la fonction sont donnés par M ( n ) = 91 pour tous les arguments entiers n 100, et M ( n ) = n − 10 pour n > 100. En effet, le résultat de M(101) est également 91 ( 101 - 10 = 91). Tous les résultats de M(n) après n = 101 augmentent continuellement de 1, par exemple M(102) = 92, M(103) = 93.

Histoire

La fonction 91 a été introduite dans des articles publiés par Zohar Manna , Amir Pnueli et John McCarthy en 1970. Ces articles représentaient les premiers développements vers l'application de méthodes formelles à la vérification de programmes . La fonction 91 a été choisie pour être imbriquée-récursive (contrairement à la récursivité simple , telle que la définition au moyen de ). L'exemple a été popularisé par le livre de Manna, Mathematical Theory of Computation (1974). Au fur et à mesure que le domaine des méthodes formelles avançait, cet exemple est apparu à plusieurs reprises dans la littérature de recherche. En particulier, il est considéré comme un « problème de défi » pour la vérification automatisée des programmes. ${\style d'affichage f(n)}$ ${\style d'affichage f(n-1)}$

Il est plus facile de raisonner sur le flux de contrôle récursif de queue , c'est une définition équivalente ( extensionnellement égale ) :

{\style d'affichage M_{t}(n)=M_{t}'(n,1)}

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

Comme l'un des exemples utilisés pour démontrer un tel raisonnement, le livre de Manna inclut un algorithme récursif de queue équivalent à la fonction 91 récursive imbriquée. La plupart des articles qui rapportent une « vérification automatisée » (ou une preuve de terminaison ) de la fonction 91 ne traitent que la version récursive de la queue.

Il s'agit d'une définition mutuellement récursive équivalente :

M_{mt}(n)=M_{mt}'(n,0)

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_{mt}''(n,c)={\begin{cases}n,&{\mbox{if }}c=0{\mbox{ }}\\M_{mt}'(n, c-1),&{\mbox{if }}c\neq 0{\mbox{ }}\end{cases}}

Une dérivation formelle de la version mutuellement récursive de la version imbriquée récursive a été donnée dans un article de 1980 par Mitchell Wand , basé sur l'utilisation de continuations .

Exemples

Exemple 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

Exemple 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

Voici une implémentation de l'algorithme imbriqué-récursif en Lisp :

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

Voici une implémentation de l'algorithme imbriqué-récursif en Haskell :

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

Voici une implémentation de l'algorithme imbriqué-récursif en OCaml :

let rec mc91 n =
  if n > 100 then n - 10
  else mc91 (mc91 (n + 11))

Voici une implémentation de l'algorithme tail-recursive en 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

Voici une implémentation de l'algorithme imbriqué-récursif en Python :

def mc91(n: int) -> int:
    """McCarthy 91 function."""
    if n > 100:
        return n - 10
    else:
        return mc91(mc91(n + 11))

Voici une implémentation de l'algorithme imbriqué-récursif en C :

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

Voici une implémentation de l'algorithme récursif de queue en C :

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

Preuve

Voici une preuve que

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

qui fournit un algorithme non récursif équivalent pour calculer . ${\style d'affichage M}$

Pour n > 100, l'égalité découle de la définition de . Pour n 100, une forte induction descendante à partir de 100 peut être utilisée. ${\style d'affichage M}$

Pour 90 n ≤ 100,

M(n) = M(M(n + 11)), by definition
     = M(n + 11 - 10), since n + 11 > 100
     = M(n + 1)

Donc M ( n ) = M (101) = 91 pour 90 n ≤ 100. Cela peut être utilisé comme cas de base.

Pour l'étape d'induction, soit n 89 et supposons que M ( i ) = 91 pour tout n < i ≤ 100, alors

M(n) = M(M(n + 11)), by definition
     = M(91), by hypothesis, since n < n + 11 ≤ 100
     = 91, by the base case.

Cela prouve que M ( n ) = 91 pour tout n 100, y compris les valeurs négatives.

La généralisation de Knuth

Donald Knuth a généralisé la fonction 91 pour inclure des paramètres supplémentaires. John Cowles a développé une preuve formelle que la fonction généralisée de Knuth était totale, en utilisant le prouveur du théorème ACL2 .

Les références

Manne, Zohar ; Pnueli, Amir (juillet 1970). « Formalisation des propriétés des programmes fonctionnels ». Journal de l'ACM . 17 (3) : 555-569. doi : 10.1145/321592.321606 .
Manne, Zohar ; McCarthy, John (1970). "Propriétés des programmes et logique de fonction partielle". Intelligence des machines . 5 . OCLC 35422131 .
Manne, Zohar (1974). Théorie mathématique du calcul (4e éd.). McGraw-Hill. ISBN 9780070399105.
Baguette, Mitchell (janvier 1980). "Stratégies de transformation de programme basées sur la continuité". Journal de l'ACM . 27 (1) : 164-180. doi : 10.1145/322169.322183 .

Languages

In other projects