コンビネータ論理公理

https://stackoverflow.com/questions/1374896

21-09-2019
|

質問

私はコンビネータロジックを使用して定理を証明する実験を行っており、これは有望に見えますが、1 つ障害があります。コンビネータロジックでは、次のことが真実であることが指摘されています。I = SKK ですが、これは定理ではなく、公理として追加する必要があります。追加する必要がある公理の完全なリストを知っている人はいますか?

編集：もちろん、I = SKK であることを手動で証明することはできますが、何かを見逃していない限り、それは等価性を伴うコンビネータロジックのシステム内の定理ではありません。そうは言っても、I を SKK にマクロ展開するだけです...しかし、私はまだ重要なことを見逃しています。通常の一階論理の矛盾を簡単に解決する一連の節 p(X) と ~p(X) を取得し、それらを SK に変換し、置換を実行し、S と K のすべての呼び出しを評価すると、私のプログラムは、以下（ここではUnlambdaのバックティックに「」を使用しています）：

''eq ''s ''s 'ks ''s ''s 'ks ''s 'k k 'k eq ''s ''s 'k s 'k k 'k k ''s 'k k 'k false 「本当だよ」本当だよ

おそらく私に必要なのは、部分呼び出し 'k と ''s を処理するための適切なルールのセットのようですが、それらのルールがどうあるべきなのかがわかりません。この分野で見つけることができる文献はすべてそのために書かれています。対象読者はプログラマーではなく数学者です。一度理解すれば、おそらく答えは非常に簡単だと思います。

解決

教科書によっては次のように定義されています私単なる別名として ((S K) K). 。この場合、それらは（用語として）同一です 定義に従って. 。それらの等価性を (関数として) 証明するには、等価性が再帰的であることを証明するだけで済みます。これは、再帰性公理スキームによって達成できます。

という提案「E = E'' は推論可能です (反射性 公理スキーム。ここではメタ変数によって示される可能な項ごとにインスタンス化されます。 E)

したがって、以下では、あなたの質問は別のアプローチを検討していると思います。コンビネータの場合私として定義されていません 単なる別名 複合項の場合 ((S K) K), として紹介されていますが、 スタンドアロンの基本的なコンビネータ 独自の定数。その操作セマンティクスは宣言されています。 公理によって明示的に スキーム

``(私 E) = E'' は推論可能です (I-公理 スキーム）

あなたの質問はこうだと思います

そのようなスタンドアロンで定義されたものを (システム内に残ったまま) 形式的に推測できるかどうか私まさに次のように動作します ((S K) K), 、リダクションの関数として使用される場合?

できると思いますが、より強力なツールに頼る必要があります。私は、通常の公理スキームでは十分ではなく、拡張性プロパティ (関数の等価性) も宣言する必要があると推測しています。それが重要な点です。拡張性を公理として形式化したい場合は、オブジェクト言語を次のように拡張する必要があります。 自由変数.

私は、組み合わせロジックを構築するためにそのようなアプローチを採用する必要があり、オブジェクト言語での変数の使用も許可する必要があると思います。もちろん、「ただ」という意味です無料貴重品。バインドされた変数を使用することは不正行為となるため、組み合わせロジックの範囲内に留まらなければなりません。無料の変数の使用は不正行為ではなく、誠実なツールです。したがって、私たちはあなたが要求した正式な証明を行うことができます。

単純な等式公理と推論規則 (推移性、再帰性、対称性、ライプニッツ規則) に加えて、 拡張性 平等の推論規則。ここが自由変数が重要なポイントです。

チョルニエイ 2007 では次のように述べています。157-158 では、次のアプローチを見つけました。この方法で証明できると思います。

いくつかのコメント:

公理のほとんどは実際には 公理スキーム, 、無限に多くの公理インスタンスで構成されます。インスタンスは可能な限りすべてインスタンス化する必要があります E, F, G 条項。ここではメタ変数に斜体を使用しています。

公理スキームの表面的な無限の性質は、有限時間内で取り組むことができるため、計算可能性の問題を引き起こすことはありません。私たちの公理システムは 再帰的. 。これは、賢いパーサーが、与えられた命題が公理スキームのインスタンスであるかどうかを有限時間内に (さらに非常に効率的に) 判断できることを意味します。したがって、公理スキームの使用は理論上も実際上も問題を引き起こしません。

ここで私たちのフレームワークを考えてみましょう。

言語

アルファベット

定数:次の 3 つは定数と呼ばれます。 K, S, 私.

定数を追加しました私あなたの質問はコンビネータを定義していないことを前提としているからです私ただのとして エイリアス/マクロ 複合項の場合 S K K, しかし、それ自体はスタンドアロンの定数です。

定数は太字のローマ字大文字で表します。

申請書のサイン:「アプリケーション」の記号 @ だけで十分です (引数 2 の接頭表記)。糖衣構文として、ここでは明示的なアプリケーション記号の代わりに括弧を使用します。明示的な開始 (および終了) 記号を使用します。

変数:コンビネータロジックはバインドされた変数やスコープなどを利用しませんが、自由変数を導入することができます。これらは糖衣構文であるだけでなく、推論システムも強化できるのではないかと思います。あなたの質問にはそれらの使用が必要になると思います。列挙可能な無限セット (定数と括弧記号が互いに素である) は変数のアルファベットとして機能します。ここでは、フォーマットされていないローマ字の小文字 x、y、z... でそれらを示します。

条項

用語は帰納的に定義されます。

定数はすべて項です
あらゆる変数は項です
もし E は用語であり、 F も用語です、そしてまた (E F) は用語です

私は時々、糖衣構文として実用的な規則を使用します。書く

E F G H

の代わりに

(((E F) G) H).

控除

変換公理スキーム:

``K E F = E'' は推論可能です (K公理 スキーム）
``S F G H = F H (G H)」は推論可能です(S公理 スキーム）
``私 E = E'' は推論可能です (I-公理 スキーム）

3 番目の変換公理を追加しました (私ルール) あなたの質問は、私たちがそうでないことを前提としているからです。 定義済み コンビネーター私のエイリアス/マクロとして S K K.

等価公理スキームと推論規則

``E = E'' は推論可能です (反射性 公理）
もし "E = F" は推論可能です、それでは "F = E" も推測可能です (対称推論規則)
もし "E = F" は推論可能であり、"F = G" も推論可能ですが、"E = G" は還元可能です (推移性 ルール）
もし "E = F" は推論可能です、それでは "E G = F G" も推測可能です (ライプニッツの法則 I)
もし "E = F" は推論可能です、それでは "G E = G F" も推測可能です (ライプニッツ則 II)

質問

それでは、あなたの質問を調査しましょう。これまでに定義された控除システムは、あなたの質問を証明するには十分強力ではないと推測します。

という提案です」私 = S K K「推理できる？

問題は、関数の等価性を証明しなければならないことです。2 つの関数が同じように動作する場合、それらは同等であると見なされます。関数は引数に適用されるように機能します。考えられるそれぞれの引数に適用した場合、両方の関数が同じように動作することを証明する必要があります。またしても無限大の問題です！ここでは公理スキームは役に立たないと思います。何かのようなもの

もし E F = G F は演繹可能です、そしてまた E = G 推論可能です

その仕事は失敗します:これでは私たちが望むものは得られないことがわかります。それを使用すると、次のことが証明できます

``私 E = S K K E” は推理可能です

それぞれに E しかし、これらの結果は個別のインスタンスにすぎず、全体としてさらなる演繹に使用することはできません。具体的な結果 (無限に多く) しかなく、それらを要約することはできません。

それは保持されます E := K
保持します E := S
それは保持されます E := K K
.
.
.

...

これらの断片化された結果インスタンスを、拡張性を示す単一の優れた結果に要約することはできません。これらの価値の低いフラグメントを、より価値のある単一の結果に溶かすような推論ルールをファネルに注ぎ込むことはできません。

私たちは控除システムの力を強化する必要があります。私たちは問題を把握できる正式なツールを見つけなければなりません。あなたの質問は拡張性につながります。拡張性の必要性を宣言することで、*****任意*****のインスタンスに対して成り立つ命題を提示できると思います。だからこそ、オブジェクト言語内で自由な変数を許可する必要があると私は考えています。次の追加の推論規則が機能すると推測します。

変数 x が項の一部ではない場合、どちらも E または F, 、およびステートメント (E x) = (F x) は推論可能です。 E = F も演繹可能です (拡張性 推論規則)

この公理の難しい点は、混乱を招きやすいことです。x は物体変数、つまりオブジェクト言語の完全に解放され尊重される部分である一方で、 E そして G はメタ変数。オブジェクト言語の一部ではなく、公理スキームの簡潔な表記にのみ使用されます。

（述べる：より正確には、推論の拡張性規則は、より慎重な方法で形式化する必要があります。メタ変数バツ可能な限りすべての物体変数 x、y、z...、および別の種類の変数メタ変数 E 可能な限りすべての 用語インスタンス. 。ただし、2 種類のメタ変数とオブジェクト変数のこの区別は、ここではそれほど教訓的なものではなく、あなたの質問にはあまり影響しません。)

証拠

では、「」という命題を証明しましょう。私 = S K K''.

左側の手順:

という提案「私 x = x'' は次のインスタンスです。 I-公理 インスタレーションを使用したスキーム [E := x]

右側の手順:

提案」S K K x = K バツ（K x)" は、 S公理 インスタンス化を伴うスキーム [E := K, F := K, G := x]、したがって、演繹可能です
提案」K バツ（K x) = x" は次のインスタンスです。 K公理 インスタンス化を伴うスキーム [E := x、 F := K x]、したがって、それは演繹可能です

等価性の推移性:

声明 "S K K x = K バツ（K x)" は、次の最初の前提条件と一致します。 推移性 推論規則とステートメント「K バツ（K x) = x」は、この推論規則の 2 番目の前提と一致します。インスタンス化は [E := S K K バツ、 F := K バツ（K バツ）、 G = x]。したがって、次の結論も成り立ちます。 E = G. 。同じインスタンス化で結論を書き直すと、ステートメントが得られます。S K K x = x」なので、これは演繹可能です。

等価性の対称性:

「」を使用するS K K x = x」であれば、「x =」と推測できます。 S K K バツ"

等価性の推移性:

「」を使用する私 x = x」および「x = S K K x"、推測できます"私 x = S K K バツ"

これで、重要なポイントへの道が開かれました。

提案」私 x = S K K x" は、次の最初の前提条件と一致します。拡大推論規則:(E x) = (F x)、インスタンス化 [E := 私, F := S K K]。したがって、結論も成り立つはずです、つまり、「E = F" 同じインスタンス化 ([E := 私, F := S K K])、命題が得られます。私 = S K K"、quoderat Demonstranum。

ゾルタン・チョルニエイ (2007): ラムダカルクルス。アラプジャイの機能プログラム。 ブダペスト:タイポテックス。ISBN-978-963-9664-46-3。

他のヒント

あなたは公理としてIを定義する必要はありません。以下で起動します：

I.x = x
K.x y = x
S.x y z = x z (y z)

SKanything = anythingので、その後、SKanythingはちょうどIように、恒等関数です。

だから、I = SKKとI = SKS。公理としてIを定義する必要はありません、あなたはSKKのエイリアスのシンタックスシュガーとしてそれを定義することができます。

SとKの定義はあなたが唯一の公理です。

通常の公理は、ベータ版の平等のための完全なですが、ETAの平等を与えることはありません。カレーは、β-ETAの平等のための完全性を得るために、通常のものに30程度の公理の集合を発見しました。彼らは、コンビネータとラムダ計算のにヒンドリー＆Seldinののはじめに記載されています。

ロジャー・ヒンドリー、カレーの最後の問題に、リストのいくつかの追加の要望を我々私たちはそれらのすべてを満たすマッピングを持っていないことをラムダ計算とノートの間のマッピングから勧めします。あなたはおそらくのすべての基準についてはあまり気にしません。

ライセンス： CC-BY-SA と帰属

所属していません StackOverflow