マッカーシー91関数

マッカーシー91 関数は、コンピュータ科学者のジョンマッカーシーによってコンピュータサイエンスにおける形式検証のテストケースとして定義された再帰関数です。

マッカーシー91関数は次のように定義される。

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

関数の評価結果は、 n ≤ 100 のすべての整数引数に対してM ( n ) = 91となり、 n > 100 に対してM ( n ) = n − 10となります。実際、M(101) の結果も 91 (101 - 10 = 91) となります。n = 101 以降の M(n) の結果はすべて 1 ずつ増加します。例えば、M(102) = 92、M(103) = 93 となります。

歴史

91関数は、1970年にゾハル・マンナ、アミール・プヌエリ、ジョン・マッカーシーによって発表された論文で導入されました。これらの論文は、形式手法をプログラム検証に適用する初期の発展を代表していました。91関数が選ばれたのは、ネストされた再帰的であるからです（を用いて定義するなどの単一再帰とは対照的です）。この例は、マンナの著書『計算の数学的理論』 （1974年）によって広く知られるようになりました。形式手法の分野が発展するにつれて、この例は研究文献に繰り返し登場しました。特に、これは自動プログラム検証における「課題問題」と見なされています。 $f(n)$ $f(n-1)$

末尾再帰制御フローについて推論する方が簡単です。これは同等の（拡張的に等しい）定義です。

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{ and }}c\neq 0\\M_{t}'(n+11,c+1),&{\mbox{if }}n\leq 100{\mbox{ and }}c\neq 0\end{cases}}

こうした推論を示す例として、マンナの著書には、ネストされた再帰関数91と等価な末尾再帰アルゴリズムが含まれています。91関数の「自動検証」（または停止性証明）を報告する論文の多くは、末尾再帰バージョンのみを扱っています。

これは、同等の相互末尾再帰定義です。

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

相互末尾再帰バージョンを入れ子再帰バージョンから正式な導出は、継続の使用に基づいて、ミッチェルワンドによる 1980 年の論文で示されました。

例

例A:

M(99) = M(M(110)) 99 ≤ 100 なので = M(100) 110 > 100なので = M(M(111)) 100 ≤ 100 なので = M(101) 111 > 100なので = 91 101 > 100 なので

例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) .... パターンはM(99)、M(100)、M(101)まで増加し続けます。これは例Aで見た通りです。 = M(101) 111 > 100なので = 91 101 > 100 なので

コード

以下はPythonでのネストされた再帰アルゴリズムの実装です。

def mc91 ( n : int ) -> int : n > 100の場合: n - 10を返し、そうでない場合: mc91 ( mc91 ( n + 11 ))を返します

以下は Python での末尾再帰アルゴリズムの実装です。

def mc91 ( n : int ) -> int : return mc91taux ( n , 1 )       def mc91taux ( n : int , c : int ) -> int : c == 0の場合: nを返すelif n > 100 の場合: mc91taux ( n - 10 , c - 1 )を返すelse : mc91taux ( n + 11 , c + 1 )を返す

証拠

McCarthy 91 関数が次のように定義される非再帰アルゴリズムと同等であることの証明を次に示します。 $M$ $M'$

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

n > 100の場合、との定義は同じです。したがって、の定義から等式が成り立ちます。 $M'$ $M$ $M$

n ≤ 100の場合、100 から下方への強い誘導を使用することができます。

90 ≤ n ≤ 100の場合、

M(n) = M(M(n + 11))、定義により = M(n + 11 - 10)、n + 11 > 100なので = M(n + 1)

これを使って、 90 ≤ n ≤ 100 に対してM ( n ) = M (101) = 91 であることを示すことができます。

M(90) = M(91)、M(n) = M(n + 1)は上で証明された。 ＝ … = M(101)、定義により = 101 − 10 = 91

M ( n ) = M (101) = 91（90≤n≤100の場合）は、帰納法の基本ケースとして使用できます。

下方誘導ステップでは、n ≤ 89とし、n < i ≤ 100のすべてについてM ( i ) = 91と仮定すると、

M(n) = M(M(n + 11))、定義により = M(91)、仮説により、n < n + 11 ≤ 100であるため = 91、基本ケースによる。

これにより、負の値も含め、 n≤100のすべてにおいてM ( n )=91であることが証明されます。

クヌースの一般化

ドナルド・クヌースは91関数を一般化し、追加のパラメータを含めた。^[1]ジョン・カウルズはACL2定理証明器を用いて、クヌースの一般化された関数が完全関数であることを正式に証明した。^[2]

参考文献

^ Knuth, Donald E. (1991). 「教科書的な再帰の例」.人工知能と計算の数学的理論: 207– 229. arXiv : cs/9301113 . Bibcode : 1993cs......1113K. doi : 10.1016/B978-0-12-450010-5.50018-9. ISBN 9780124500105. S2CID 6411737。
^ Cowles, John (2013) [2000]. 「KnuthによるMcCarthyの91関数の一般化」. Kaufmann, M.; Manolios, P.; Strother Moore, J. (編).コンピュータ支援推論：ACL2のケーススタディ. Kluwer Academic. pp. 283– 299. ISBN 9781475731880。

マンナ, ゾハル; プヌエリ, アミール (1970年7月). 「関数型プログラムの特性の形式化」. Journal of the ACM . 17 (3): 555– 569. doi : 10.1145/321592.321606 . S2CID 5924829.
マンナ、ゾハール；マッカーシー、ジョン（1970）「プログラムの特性と部分関数論理」機械知能5 OCLC 35422131
マナ、ゾハル (1974)。計算の数学理論(第 4 版)。マグロウヒル。ISBN 9780070399105。
ワンド、ミッチェル (1980年1月). 「継続ベースのプログラム変換戦略」. Journal of the ACM . 27 (1): 164– 180. doi : 10.1145/322169.322183 . S2CID 16015891.

[1] Knuth, Donald E. (1991). 「教科書的な再帰の例」.人工知能と計算の数学的理論: 207– 229. arXiv : cs/9301113 . Bibcode : 1993cs......1113K. doi : 10.1016/B978-0-12-450010-5.50018-9. ISBN 9780124500105. S2CID 6411737。

[2] Cowles, John (2013) [2000]. 「KnuthによるMcCarthyの91関数の一般化」. Kaufmann, M.; Manolios, P.; Strother Moore, J. (編).コンピュータ支援推論：ACL2のケーススタディ. Kluwer Academic. pp. 283– 299. ISBN 9781475731880。