プレスバーガー算術
プレスバーガー算術は、自然数における加法演算と等号関係のみを扱う一階述語論理体系です。この体系は、1929年にモイジェシュ・プレスバーガーによって提唱されました。プレスバーガー算術の特徴は、乗法演算を含まない点にあります。これは、乗法を扱うペアノ算術よりも体系が弱いことを意味しますが、同時に決定可能性という重要な性質を保持していることにつながります。
プレスバーガー算術の言語は、以下の要素で構成されます。
定数: 0と1
関数: 加法演算子「+」
述語: 等号「=」
公理は、以下の論理式を全称閉包したものです。
1. ¬(0 = x + 1) (0は任意の自然数の後者ではない)
2. x + 1 = y + 1 → x = y （後者の等号は元の数の等号を意味する）
3. x + 0 = x （0は加法に関する単位元）
4. x + (y + 1) = (x + y) + 1 （加法の結合法則）
5. 数学的帰納法の公理図式：
P(x) をプレスバーガー算術の言語による自由変数xを含む一階述語論理式とすると、以下の論理式は公理です。
(P(0) ∧ ∀x(P(x) → P(x + 1))) → ∀y P(y)
この公理図式は無限個の公理を表しており、有限個の公理で置き換えることはできません。このため、プレスバーガー算術は有限公理化不可能であるといえます。
プレスバーガー算術は、以下の重要な性質を持っています。
無矛盾性: 任意の文とその否定が同時に証明されることはありません。
完全性: 任意の文は証明可能であるか、その否定が証明可能かのどちらかです。
決定可能性: 任意の文が定理であるかどうかを判定するアルゴリズムが存在します。これは、プレスバーガー算術の言語で記述された任意の閉じた論理式について、その真偽を機械的に判定できることを意味します。
しかし、プレスバーガー算術では、因数分解や素数といった概念を形式化することはできません。一般的に、乗法に関する自然数の概念は不完全性や決定不能性につながるため、プレスバーガー算術では乗法を定義することが避けられています。ただし、個々の具体的な命題であれば形式化は可能です。たとえば、「すべての自然数は偶数または奇数である」という命題は、プレスバーガー算術で証明可能です。
プレスバーガー算術の決定問題は計算可能ですが、その計算複雑性は非常に高いことが知られています。具体的には、その複雑性は漸近的に二重指数関数的であることが、FischerとRabinによって証明されています。これは、問題の規模が大きくなるにつれて、計算量が指数関数的に増加し、実用的な計算が困難になる場合があることを示しています。
プレスバーガー算術は、形式的検証やプログラムの分析、特に整数演算を含むソフトウェアの検証において有用です。例えば、配列の添え字の範囲チェックやループの停止性判定などに用いられています。その決定可能性と表現力によって、プログラムの正当性を保証する上で重要な役割を果たします。
Cooper, D. C., 1972, "Theorem Proving in Arithmetic without Multiplication" in B. Meltzer and D. Michie, eds., Machine Intelligence Vol. 7.
Enderton, Herbert (2001). A mathematical introduction to logic (2nd ed.).
Ferrante, Jeanne, and Charles W. Rackoff, 1979. The Computational Complexity of Logical Theories.
Fischer, Michael J.; Rabin, Michael O. (1974). “Super-Exponential Complexity of Presburger Arithmetic”.
G. Nelson and D. C. Oppen (Apr 1978). “A simplifier based on efficient decision algorithms”.
Mojżesz Presburger, 1929, "Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt"
Ryan Stansifer (September 1984). Presburger's Article on Integer Arithmetic: Remarks and Translation (PDF) (Technical Report).
William Pugh, 1991, "The Omega test: a fast and practical integer programming algorithm for dependence analysis,".
Reddy, C. R., and D. W. Loveland, 1978, "Presburger Arithmetic with Bounded Quantifier Alternation."
Young, P., 1985, "Gödel theorems, exponential difficulty and undecidability of arithmetic theories: an exposition"
Oppen, Derek C. (1978). “A 222pn Upper Bound on the Complexity of Presburger Arithmetic” (PDF).
Berman, L. (1980). “The Complexity of Logical Theories”.
Nipkow, T (2010). “Linear Quantifier Elimination”.
King, Tim; Barrett, Clark W.; Tinelli, Cesare (2014). “Leveraging linear and mixed integer programming for SMT”.
online prover A Java applet proves or disproves arbitrary formulas of Presburger arithmetic (In German)
[1] A complete Theorem Prover for Presburger Arithmetic by Philipp Rümmer
プレスバーガー算術の構成
プレスバーガー算術の言語は、以下の要素で構成されます。
定数: 0と1
関数: 加法演算子「+」
述語: 等号「=」
公理は、以下の論理式を全称閉包したものです。
1. ¬(0 = x + 1) (0は任意の自然数の後者ではない)
2. x + 1 = y + 1 → x = y （後者の等号は元の数の等号を意味する）
3. x + 0 = x （0は加法に関する単位元）
4. x + (y + 1) = (x + y) + 1 （加法の結合法則）
5. 数学的帰納法の公理図式：
P(x) をプレスバーガー算術の言語による自由変数xを含む一階述語論理式とすると、以下の論理式は公理です。
(P(0) ∧ ∀x(P(x) → P(x + 1))) → ∀y P(y)
この公理図式は無限個の公理を表しており、有限個の公理で置き換えることはできません。このため、プレスバーガー算術は有限公理化不可能であるといえます。
プレスバーガー算術の特性
プレスバーガー算術は、以下の重要な性質を持っています。
無矛盾性: 任意の文とその否定が同時に証明されることはありません。
完全性: 任意の文は証明可能であるか、その否定が証明可能かのどちらかです。
決定可能性: 任意の文が定理であるかどうかを判定するアルゴリズムが存在します。これは、プレスバーガー算術の言語で記述された任意の閉じた論理式について、その真偽を機械的に判定できることを意味します。
しかし、プレスバーガー算術では、因数分解や素数といった概念を形式化することはできません。一般的に、乗法に関する自然数の概念は不完全性や決定不能性につながるため、プレスバーガー算術では乗法を定義することが避けられています。ただし、個々の具体的な命題であれば形式化は可能です。たとえば、「すべての自然数は偶数または奇数である」という命題は、プレスバーガー算術で証明可能です。
プレスバーガー算術の計算複雑性
プレスバーガー算術の決定問題は計算可能ですが、その計算複雑性は非常に高いことが知られています。具体的には、その複雑性は漸近的に二重指数関数的であることが、FischerとRabinによって証明されています。これは、問題の規模が大きくなるにつれて、計算量が指数関数的に増加し、実用的な計算が困難になる場合があることを示しています。
応用
プレスバーガー算術は、形式的検証やプログラムの分析、特に整数演算を含むソフトウェアの検証において有用です。例えば、配列の添え字の範囲チェックやループの停止性判定などに用いられています。その決定可能性と表現力によって、プログラムの正当性を保証する上で重要な役割を果たします。
参考文献
Cooper, D. C., 1972, "Theorem Proving in Arithmetic without Multiplication" in B. Meltzer and D. Michie, eds., Machine Intelligence Vol. 7.
Enderton, Herbert (2001). A mathematical introduction to logic (2nd ed.).
Ferrante, Jeanne, and Charles W. Rackoff, 1979. The Computational Complexity of Logical Theories.
Fischer, Michael J.; Rabin, Michael O. (1974). “Super-Exponential Complexity of Presburger Arithmetic”.
G. Nelson and D. C. Oppen (Apr 1978). “A simplifier based on efficient decision algorithms”.
Mojżesz Presburger, 1929, "Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt"
Ryan Stansifer (September 1984). Presburger's Article on Integer Arithmetic: Remarks and Translation (PDF) (Technical Report).
William Pugh, 1991, "The Omega test: a fast and practical integer programming algorithm for dependence analysis,".
Reddy, C. R., and D. W. Loveland, 1978, "Presburger Arithmetic with Bounded Quantifier Alternation."
Young, P., 1985, "Gödel theorems, exponential difficulty and undecidability of arithmetic theories: an exposition"
Oppen, Derek C. (1978). “A 222pn Upper Bound on the Complexity of Presburger Arithmetic” (PDF).
Berman, L. (1980). “The Complexity of Logical Theories”.
Nipkow, T (2010). “Linear Quantifier Elimination”.
King, Tim; Barrett, Clark W.; Tinelli, Cesare (2014). “Leveraging linear and mixed integer programming for SMT”.
外部リンク
online prover A Java applet proves or disproves arbitrary formulas of Presburger arithmetic (In German)
[1] A complete Theorem Prover for Presburger Arithmetic by Philipp Rümmer
もう一度検索
【記事の利用について】
タイトルと記事文章は、記事のあるページにリンクを張っていただければ、無料で利用できます。
※画像は、利用できませんのでご注意ください。
【リンクついて】
リンクフリーです。