Haskellで小さな関数型プログラミング言語を書いていますが、（==）の実装方法の定義が見つかりません。これはかなりトリッキーなようですが、
4 に答える
14
Haskellは「型クラス」の概念を使用しています。実際の定義は次のようなものです。
class Eq a where
(==) :: a -> a -> Bool
-- More functions follow, for more complex concepts of equality (eg NaN)
次に、独自のタイプに対してそれを定義できます。例えば：
-- Eq can't be automatically derived, because of the function
data Foo = Foo Int (Char -> Bool)
-- So define it here
instance Eq Foo where
(Foo x _) == (Foo y _) = x == y
于 2009-10-09T21:07:27.683 に答える
11
あなたの質問はとてもとても興味深いと思います。あなたがあなたの質問の背後にある理論的ルーツを知りたいということも意味しているのなら、私たちはHaskellから抽象化し、より一般的なアルゴリズムの概念であなたの質問を調査することができると思います。Haskellに関しては、次の2つの事実が重要だと思います。
- 機能はHaskellの一級市民です
- Haskellはチューリング完全です
しかし、私はまだ議論をしていません（言語の強さがここで正確に重要である方法）。
特定のケースの可能性がありますが、包括的であるためのノーゴー定理
ルーツでは、コンピュータサイエンスの2つの定理が答えを提供すると思います。技術的な詳細から抽象化したい場合は、ラムダ計算（またはコンビネータ論理）で質問を調査できます。それらに平等を定義することはできますか？したがって、最初にラムダ計算またはコンビネータ論理の分野に限定しましょう。
これらのアルゴリズムアプローチはどちらも非常にミニマルであることに注意する必要があります。それらには「事前定義された」データ型はなく、数値、ブール値、リストもありません。しかし、巧妙な方法で、それらすべてを模倣することができます。
- ブール値の代わりに、射影（セレクター）関数（Church booleans）を使用できます。
- Cユニオン（またはC ++クラスの継承）の代わりに、継続を使用できます。より正確に言えば、簡潔でわかりやすい方法で実装できるのはケース分析です。
- 関数の合成を繰り返す関数（チャーチ数）を使用して、自然数を模倣できます。
- 洗練された代数的手法（カタモルフィズム）を使用してリストとツリーを実装できます。
したがって、ラムダ計算やコンビネータ論理などの最小限の「関数型言語」でも、すべての意味のあるデータ型を模倣できます。必要なデータ型を模倣する巧妙なシーンでラムダ関数（またはコンビネータ）を使用できます。
さて、最初にこれらのミニマルな関数型言語であなたの質問に答えて、答えがHaskell固有のものなのか、それとももっと一般的な定理の単なる結果なのかを見てみましょう。
- ベームの定理は次のように規定しています。以前に与えられた2つの異なる式（コンピューターを停止し、フリーズさせない）に対して、与えられた2つの式が意味的に同じであるかどうかを正しく判断する適切なテスト関数を常に記述できます（Csörnyei2007：132、 = Th 7.2.2）。ほとんどの実際的なケース（リスト、ツリー、ブール値、数値）では、ベームの定理は、適切な特定の等式関数を常に記述できることを示しています。Tromp 1999：Sec2のリストの例を参照してください。
- Scott-Curryの決定不能性の定理は、すべての一般的な平等関数が、考えられる各シーンにとって意味のあるものとして記述される可能性があることを除外しています（Csörnyei2007：140、= Th7.4.1）。
ゴー定理
データ型を「実装」した後、それに対応する等式関数を記述できます。ほとんどの実際的なケース（リスト、数値、ケース分析の選択）の場合、対応する等式関数に欠けている神秘的な「データ型」はありません。この肯定的な答えは、ベームの定理によって提供されます。
2つのチャーチ数を取り、それらが等しいかどうかに答えるチャーチ数等式関数を書くことができます。2つの（教会）ブール値を取り、それらが等しいかどうかに答える別のラムダ関数/コンビネータを書くことができます。さらに、純粋なラムダ計算/ CLでリストを実装でき（提案された方法はカタモルフィズムの概念を使用することです）、次に、ブール値のリストの同等性に答える関数を定義できます。チャーチ数のリストの平等に答える別の関数を書くことができます。ツリーを実装することもできます。その後、ツリーの同等性に答える関数を記述できます（ブール値、および別のチャーチ数）。
このジョブの一部を自動化できますが、すべてを自動化することはできません。一部の（すべてではない）等式関数を自動的に導出できます。ツリーとリストの特定のマップ関数、およびブール値と数値の等式関数が既にある場合は、ブール値ツリー、ブールリスト、数値リスト、数値ツリーの等式関数を自動的に導出できます。
ノーゴー定理
しかし、すべての可能な「データ型」に対して機能する単一の全自動等式関数を定義する方法はありません。ラムダ計算でデータ型を指定してコンクリートを「実装」する場合、通常、そのシーンに対して特定の等式関数を計画する必要があります。
さらに、2つのラムダ項を取り、2つのラムダ項が縮小されたときに同じように動作するかどうかに答えるラムダ関数を定義する方法はありません。さらに、2つのラムダ項の表現（引用）を取り、2つの元のラムダ項が縮小されたときに同じように動作するかどうかに答えるラムダ関数を定義する方法はありません（Csörnyei2007：141、Conseq 7.4.3）。そのノーゴーの答えは、Scott-Curryの決定不能性定理（Csörnyei2007：140、Th 7.4.1）によって提供されます。
他のアルゴリズムアプローチでは
上記の2つの答えは、ラムダ計算とコンビネータ論理に限定されていないと思います。同様の可能性と制限は、他のいくつかのアルゴリズムの概念にも当てはまります。たとえば、2つの単項関数のゲーデル数を取り、これらのエンコードされた関数が拡張的に同じように動作するかどうかを決定する再帰関数はありません（Monk 1976：84、= Cor5.18）。これはライスの定理の結果です（Monk 1976：84、= Th 5.17）。ライスの定理は形式的にはスコット・カリーの決定不能性の定理に非常に似ているように感じますが、私はまだそれを考慮していません。
非常に制限された意味での包括的平等
包括的な同等性テストを提供するコンビネータ論理インタープリター（停止、正規形の用語に制限されている）を作成したい場合は、次のように実装します。
- 検討中の両方のコンビネータ論理用語を通常の形式に減らします。
- そして、それらが用語と同一であるかどうかを確認します。
もしそうなら、それらの縮小されていない元の形式も意味的に同等であったに違いありません。
ただし、この方法はいくつかの実用的な目標に適していますが、これは重大な制限がある場合にのみ機能します。数値、リスト、ツリーなどを操作して、期待どおりの結果が得られるかどうかを確認できます。私のクイン（純粋なコンビネータ論理で書かれている）は、この制限された平等の概念を使用しており、このクワインには非常に洗練された構造（コンビネータ論理自体に実装された用語ツリー）が必要ですが、それで十分です。
この制限された平等の概念の限界が何であるかはまだわかりませんが、平等の正しい定義と比較すると、非常に制限されていると思います。その使用の背後にある動機は、制限されていないものとは異なり、まったく計算可能であるということです。平等の概念。
この制限は、この制限された平等の概念が通常の形式のコンビネータに対してのみ機能するという事実からもわかります。反例として、制限された平等概念は、IΩ = Ωかどうかを チェックできませんが、2つの項が相互に変換できることはよくわかっています。
私はまだ、この制限された平等の概念の存在が、スコット・カリーの決定不可能性定理とライスの定理によって主張された否定的な結果とどのように関連しているかを考慮しなければなりません。どちらの定理も部分関数を扱っていますが、これがどのように正確に重要であるかはまだわかりません。
拡張性
しかし、制限された平等の概念にはさらに制限があります。拡張性の概念を扱うことはできません。たとえば、少なくとも2つの引数に適用された場合、SKはKIと同じように動作するという事実にもかかわらず、 SKがKI に何らかの形で関連していることに気づきません。
後者の例は、より詳細に説明する必要があります。SK とKI は用語と同一ではないことがわかっています：SK≢KI 。しかし、両方をそれぞれ任意の2つの引数XとYに適用すると、関連性がわかります。
- S K XY⊳KY （X Y） ⊳Y _ _ _ _
- KIXY⊳IY⊳Y _ _ _ _ _ _ _ _
そしてもちろん、 Y≡Y 、任意のYに対して。
もちろん、これらのメタ変数に代入されるそのようなCL項インスタンスは無限に存在する可能性があるため、可能なXおよびY引数インスタンスごとにそのような関連性を「試す」ことはできません。しかし、私たちはこの無限の問題にとらわれる必要はありません。オブジェクト言語（コンビネータ論理）を（自由）変数で拡張すると、次のようになります。
- Kは用語です
- Sは用語です
- すべての（自由）変数は用語です（改行、これは変更です！）
- XとYの両方が用語である場合、（X Y）も用語です
- 他の方法で条件を取得することはできません
それに応じて、適切な方法で削減ルールを定義します。そうすれば、無限の可能性のあるインスタンスを持つメタ変数に依存することなく、「有限」の方法で平等の外延的定義を述べることができます。
したがって、自由変数がコンビネータ論理用語で許可されている場合（オブジェクト言語は独自のオブジェクト変数で拡張されます）、拡張性をある程度実装できます。私はまだこれを考慮していません。上記の例では、表記を使用できます
S K = 2 K I
（Curry＆Feys＆Craig 1958：162、= 5 C 5 ）、 S Kxy とKIx yが等しいことが証明できるという事実に基づいています（すでに拡張性に頼ることなく）。ここで、xとyは、方程式スキームのCL項の無限に多くの可能なインスタンスのメタ変数ではありませんが、オブジェクト言語自体の第一級市民です。したがって、この方程式はもはや方程式スキームではなく、単一の方程式です。
理論的研究に関しては、すべてのnに対して= n個のインスタンスの「結合」によって=を意味することができます。
あるいは、その帰納的定義が拡張性も考慮に入れるように、平等を定義することができます。拡張性を扱う推論規則をもう1つ追加します（Csörnyei2007：158）。
- ..。
- ..。
- E、Fがコンビネータであり、xが（オブジェクト）変数であり、xがEにもFにも含まれていない場合、E x = FxからE=Fを 推測 できます。
次の反例が示すように、含まないことに関する制約は重要です。K x ≠＆nbsp; I 、 K x x = Ixで あるにもかかわらず。2つの（偶然に同一の）変数オカレンスの「役割」は完全に異なります。そのような発生率を除いて、それが制約の動機です。-
この新しい推論規則の使用は、定理S K x = KIx を どのように証明できるかを示すことで例示できます。
- S K = K I xはすでに保持されていることが証明されているため、保持されていると見なされます。以下の 証明 を参照 してください 。
- S K x y = K I x yはすでに成立していることが証明されているため、 S K x = KIxが成立すると見なされます。以下を参照してください。
- S K x y = K I x yは、拡張性に頼ることなく証明できます。必要なのは、使い慣れた変換ルールだけです。
これらの残りの推論規則は何ですか？ここにそれらがリストされています（Csörnyei2007：157）：
変換公理スキーム：
- `` K E F = E ''は推論可能です（K-公理型）
- `` S F G H = F H（G H）''は推論可能です（S-公理型）
平等公理スキームと推論規則
- `` 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）
参考文献
- Csörnyei、Zoltán（2007）：ラムダ計算。funkcionálisprogramozásalapjai。ブダペスト：Typotex。ISBN-978-963-9664-46-3。
- カリー、ハスケルB.＆フェイズ、ロベール＆クレイグ、ウィリアム（1958）。コンビネータ論理。巻 私は。アムステルダム：北ホラント出版社。
- マドア、デビッド（2003）。Unlambdaプログラミング言語。Unlambda：関数型プログラミング言語の悪夢が叶います。
- モンク、J。ドナルド（1976）。数理論理学。数学の大学院テキスト。ニューヨーク•ハイデルベルク•ベルリン：Springer-Verlag。
- Tromp、John（1999）。バイナリラムダ計算とコンビネータ論理。著者のジョンのラムダ計算とコンビネータ論理プレイグラウンドからPDFとPostscriptでダウンロードできます。
付録
ベームの定理
ベームの定理が、ほとんどの実際のケースで、意味のあるデータ型に対して適切な等式テスト関数を確実に記述できるという事実とどのように関連しているかについては、まだ明確に説明していません（純粋なラムダ計算やコンビネータ論理などの最小限の関数型言語でも）。
声明
- EとFをラムダ計算の2つの異なる閉じた項とします。
- 両方を通常の形にします。
次に、定理は、それらを適切な一連の引数に適用することで同等性をテストするための適切な方法があると主張しています。言い換えると、自然数nと一連の閉じたラムダ項G 1、G 2、G 3、... G nが存在するため、これらをこの一連の引数に適用すると、それぞれfalseとtrueになります。
- E G 1 G 2 G 3 ... Gn⊳false _ _ _
- F G 1 G 2 G 3 ... Gn⊳true _ _ _
ここで、trueとfalseは、よく知られている、子羊の飼いならされた、管理が容易で区別可能な2つのラムダ用語です。
- true≡λxy。 _ _ _ バツ
- false≡λxy。 _ _ _ y
応用
この定理を利用して、純粋なラムダ計算で実用的なデータ型を実装するにはどうすればよいでしょうか。この定理の暗黙の適用は、リンクリストをコンビネータ論理で定義できる方法によって例示されます（Tromp 1999：Sec2）。
于 2009-10-10T12:25:29.793 に答える
8
(==)型クラスの一部ですEq。インスタンス化するタイプごとに、個別の実装が提供されますEq。したがって、実装を見つけるには、通常、タイプが定義されている場所を確認する必要があります。
于 2009-10-09T21:30:16.110 に答える
-3
私には宿題のようなにおいがします。なぜそれが難しいと思うのかを詳しく説明します。MLとさまざまなLispがどのように問題を解決しようとしているのかを見ることができます。他の言語のインタプリタ/コンパイラのソースコードを調べることもできます。いくつかは研究を念頭に置いて書かれています。
于 2009-10-13T04:52:14.393 に答える