問題タブ [church-encoding]

ラムダ式:λx.λy.x(xy)があり、その整数表現を推測することになっています。特に教会のエンコーディングと教会の数字についてたくさん読んだことがありますが、何の数字かわかりません。3 歳児が理解できるように説明してもらえますか、またはウィキペディアよりも優れたリソースを紹介してもらえますか?

Haskell について学び始めたばかりで、Haskell でラムダ計算を使用しようとしています。教会の数字を数値に変換するこの式を見つけましたが、この式の 0 が何を意味するのかわかりません。どこにも見つかりません：

私を混乱させるのは最後のゼロです。それはこのラムダ式の基本ケースですか、それともいくつかの引数ですか?

わかりましたので、ラムダ計算の基本を実装しようとしています。ここに行きます。

私の番号:

それらの部分的に (実際には、非) 適用されたバージョンは、次のようになります。

続行する前に、いくつかの型を定義します。

関数succは次のようになります (アプリケーションの順序は正確にそのようにする必要があります!ここで定義を取りました):

そして、適用されていないバージョンは次のように恐ろしいものになります。

ご容赦ください。不足しているタイプは次のとおりです。

しかし、私はそのadd機能に行き詰まっています。タイプと定義に準拠している場合（ここでも同様）、次のようになります

aしかし、私は一般的なタイプの数になりたいですFFZ[Z]。

では、足し算はどのように定義すればよいのでしょうか?

私は Haskell の初心者で、このガイドで説明されているように、自然数の Church エンコーディングを実装しようとしています。

2 つの教会の数字の間の分割を実装したいと思います。

ch_div倍数の割り算 ( など9 / 3) では機能しますが、分数 ( など9 / 2) では機能しません。

sucbeforeを省略するdiv_recと、後者では機能しますが、前者では機能しません。

両方のケースで機能する除算を定義するにはどうすればよいですか?

これらがそれぞれの教会の数字の最も一般的なタイプである理由を理解するのに苦労しています:

私はすべての教会の数字が同じタイプであると思っていました :

また、 add 演算子の一般的な型を見つけるにはどうすればよいですか

どんな助けでも本当に感謝します、ありがとう!

とよく言われます

「これらの用語を使用して、ブール値の真偽をテストする操作を実行できる」という意味で True と False を表します。

しかし、それは型指定されていないラムダ計算でのみ真であるように見えるという点で、重要な警告を隠しています。これらの値を haskell に差し込むだけで、関数を記述できます。

型レベルで tru と fls を区別します。次のように言うのはどれほど間違っている/本当でしょうか:

• STLCではtru、タイプとfls'Boolean'True'False
• STLC では、(強制された) 型付きの値(tru :: ∀ t . t → t → t)であり、(fls :: ∀ t . t → t → t)True と False を表します (そして型なしでは、よくあることです)

編集：@Daniel Wagnerの回答のおかげで、質問でSTLCではなく2次ラムダ計算を考えていたことに気づきました。

Church エンコーディングを使用すると、組み込みの ADT システムを使用せずに、任意の代数データ型を表すことができます。たとえば、次のNatように表すことができます (Idris の例)。

Pair次のように表すことができます。

等々。さて、これらの型、コンストラクター、マッチャーを書くことは非常に機械的な作業です。私の質問は次のとおりです: ADT を型レベルの仕様として表現し、型自体 (つまりNat/ Par) と、それらの仕様から自動的にコンストラクター/デストラクタを派生させることは可能でしょうか? 同様に、これらの仕様を使用してジェネリックを導出できますか? 例：

次のように定義された構造体と型を考えると、2 つの数値を乗算する関数を記述する必要があります。それをするのに苦労しています。どんなアドバイスでも大歓迎です。

私はHaskellの初心者です。

クラスの型のインスタンスを作成する方法があるかどうかを探しています。

data や newtype を使わずにこのコードを動作させる方法はありますか?

モジュールを GHCi にロードしようとすると、次のように表示されます。

私はSwift 3でChurch Numeralsを実装しようとしています.現在、私は持っています:

私の関数numToChurchのこの行で：

「非エスケープ パラメータ 'f' を閉じると、エスケープできる可能性があります」というコンパイル時エラーが発生し続けます。応急処置として、推奨される変更を受け入れて @escaping を含めました。

しかし、変更を行った後でも、同じエラーが表示され続け、「f:」の後に別の @escaping を追加することをお勧めします。これは、関数パラメーターを @escaping としてマークして、関数型プログラミングのためにパラメーターを保存またはキャプチャできることをコンパイラーに伝えることに関係していることを理解しています。しかし、なぜこのエラーが発生し続けるのかわかりません。

元のエスケープしない質問が解決されました

Swiftの続きで教会のエンコーディングを理解するのに役立ちます: