4

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

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

''eq''s''s''s'ks''s''s'ks''s'kk'keq'''s'ks'kk'kk''s'kk'k false 'k true 'k true

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

4

3 に答える 3

8

一部の教科書では、Iを（（SK）K）の単なるエイリアスとして定義しています。この場合、それらはdefinitionemごとに（用語として）同一です。それらの同等性を（関数として）証明するには、同等性が再帰的であることを証明するだけで済みます。これは、再帰性公理型スキームによって実現できます。

  • 命題「E = E」は推論可能です（再帰性公理型、ここでメタ変数Eで示される可能な用語ごとにインスタンス化されます）

したがって、次のように、あなたの質問は別のアプローチを調査していると思います：コンビネータIが複合項（（SK）K）の単なるエイリアスとして定義されていない場合、それ自体がスタンドアロンの基本的なコンビネータ定数として導入され、その操作的意味論公理型によって明示的に宣言されている

  • ``（I E）= E ''は推論可能です（I-公理型）

私はあなたの質問が尋ねると思います

還元の関数として使用した場合、そのようなスタンドアロン定義のIが（（SK）K）とまったく同じように動作する ことを、正式に（システム内に残っている）推論できるかどうか。

できると思いますが、より強力なツールに頼らなければなりません。通常の公理スキームでは不十分だと思います。拡張性（関数の等式）も宣言する必要があります。それが要点です。外延性を公理として形式化したい場合は、自由変数でオブジェクト言語を拡張する必要があります。

コンビネータ論理を構築するためにそのようなアプローチを採用する必要があると思います。そのため、オブジェクト言語での変数の使用も許可する必要があります。もちろん、私は「ただの」無料の貴重品を意味します。束縛変数を使用することは不正行為であり、コンビネータ論理の領域内に留まらなければなりません。無料の変数を使用することは不正行為ではなく、正直なツールです。したがって、私たちはあなたが必要とした正式な証明を行うことができます。

単純な等式公理と推論規則（遷移性、反射性、対称性、ライプニッツ規則）に加えて、等式の拡張性推論規則を追加する必要があります。これが自由変数が重要なポイントです。

Csörnyei2007：157-158で、私は次のアプローチを見つけました。このようにして証明ができると思います。

いくつかの意見：

ほとんどの公理は実際には公理スキームであり、無限に多くの公理インスタンスで構成されています。インスタンスは、考えられるすべてのE、F、G項に対してインスタンス化する必要があります。ここでは、メタ変数にイタリックを使用しています。

公理スキームの表面的な無限の性質は、有限時間で取り組むことができるため、計算可能性の問題を引き起こしません。私たちの公理システムは再帰的です。これは、特定の命題が公理型のインスタンスであるかどうかを、巧妙なパーサーが有限時間で（さらに非常に効果的に）決定できることを意味します。したがって、公理スキームの使用は、理論的問題も実際的問題も引き起こしません。

今、私たちのフレームワークを見てみましょう：

言語

アルファベット

定数：次の3つは定数と呼ばれます：K、S、I。

定数Iを追加したのは、コンビネータIを複合項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-公理型）
  • `` I E = E ''は推論可能です（I-公理型）

3番目の変換公理（私が支配する）を追加したのは、あなたの質問が、コンビネータIをSKKのエイリアス/マクロとして定義していないことを前提としているためです。

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

  • `` 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）

質問

それでは、あなたの質問を調査しましょう。これまでに定義された控除制度は、あなたの質問を証明するほど強力ではないと思います。

命題「I = S K K」は推論可能ですか？

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

E F = G Fが推論可能である場合、E = Gも推論可能です

仕事をするのに失敗するでしょう：これは私たちが望むものを生み出さないことがわかります。それを使用して、私たちはそれを証明することができます

`` I E = S K KE ''は推論可能です

各Eタームインスタンスについてですが、これらの結果はの個別のインスタンスにすぎず、全体としてさらに推論するために使用することはできません。具体的な結果（無限に多い）しかなく、要約することはできません。

  • E：= Kにも当てはまります
  • E：= Sに当てはまります
  • E：= KK にも当てはまります
  • 。
  • 。
  • 。

..。

これらの断片化された結果インスタンスを単一の優れた結果に要約して、拡張性を示すことはできません。これらの価値の低いフラグメントを、それらを一緒に溶かして単一のより価値のある結果にする推論規則を漏斗に注ぐことはできません。

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

  • 変数xがEでもFでもない項の一部ではなく、ステートメント（E x）=（F x）が推論可能である場合、E = Fも推論可能です（推論の拡張規則）

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

（備考：より正確には、推論の拡張規則は、より慎重な方法で形式化する必要があります。すべての可能なオブジェクト変数x、y、z ...にメタ変数xを導入し、すべての可能なオブジェクト変数に別の種類のメタ変数Eを導入します。用語インスタンス。しかし、2種類のメタ変数とオブジェクト変数のこの区別は、ここではそれほど教訓的ではなく、質問にあまり影響を与えません。）

証拠

ここで、「I = S KK 」という 命題を証明しましょう。

左側の手順：

  • 命題`` I x = x''は、インスタンス化[ E：=x]を使用したI-公理型スキームのインスタンスです。

右側の手順：

  • 命題"SK K x = K x （K x ） "は、インスタンス化[ E：= K、F：= K、G：= x]を持つS公理型のインスタンスであるため、推論可能です。
  • 命題" Kx （K x）= x"は、インスタンス化[ E：= x、F：= K x]を持つK公理型のインスタンスであるため、推論可能です。

平等の推移性：

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

平等の対称性：

  • 「SKKx = x」を使用すると、「x = S KKx 」を 推測できます。

平等の推移性：

  • 「Ix=x」と「x=S K K x」を使用して、 「I x = S KKx 」を推測できます。

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

  • 命題"Ix = S K K x "は、推論の拡張規則の最初の前提と一致します：（ E x）=（F x）、インスタンス化[ E：= I、F：= SKK ] 。したがって、結論も成り立つ必要があります。つまり、同じインスタンス化（[ E：= I、F：= S K K ]）で " E = F "となり、命題 " I = S K K "、quoderatdemonstrandum。

Csörnyei、Zoltán（2007）：ラムダ計算。funkcionálisprogramozásalapjai。ブダペスト：Typotex。ISBN-978-963-9664-46-3。

于 2009-09-08T15:43:57.387 に答える
3

I を公理として定義する必要はありません。以下から始めます。

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

であるため、 はと同様に恒等関数です。SKanything = anythingSKanythingI

だから、I = SKKそしてI = SKS。I を公理として定義する必要はありません。SKK をエイリアス化する構文シュガーとして定義できます。

S と K の定義は公理にすぎません。

于 2009-09-03T17:54:37.150 に答える
0

通常の公理はベータの平等のために完全ですが、イータの平等を与えません。カレーは、ベータ-イータの平等の完全性を得るために、通常のものに対する約30の公理のセットを見つけました。それらは、Hindley＆Seldinのコンビネータとラムダ計算の概要にリストされています。

カリーズの最後の問題であるロジャー・ヒンドリーは、ラムダ計算間のマッピングから必要となる可能性のあるいくつかの追加のdesiderataをリストし、それらすべてを満たすマッピングがないことに注意します。あなたはおそらくすべての基準についてあまり気にしないでしょう。

于 2010-02-01T13:31:54.377 に答える