問題タブ [church-encoding]

私はこの質問に言及しています

ラムダ計算では、リストは次のようにエンコードされます。

チャーチリストに実装できる他のリスト関数について考えており、2つのチャーチリストを連結するconc2関数を正常に作成しました。

また、通常のリストでzipWithのように動作するzipWithChurchも試しました。しかし、私は解決策を見つけることができません。誰か助けてもらえますか？

Haskellのラムダ計算、特にチャーチ数で遊んでいます。私は次のように定義しています：

これは機能します：

これは発生チェックで失敗します：

私は自分の定数で遊んだことがありますが、それらは正しいようiszeroです。multこれを入力可能にする方法はありますか？自分のやっていることはあまりにもクレイジーだとは思いませんでしたが、何か間違ったことをしているのではないでしょうか。

または具体的に言うと、なぜfoldrを使用してリストをエンコードし、反復を使用して数値をエンコードするのですか?

長文の導入で申し訳ありませんが、質問したいことの名前をどのように挙げればよいかよくわからないので、最初にいくつかの説明をする必要があります. これは、この CAMcCann の投稿から大きく引き出されていますが、これは私の好奇心を完全に満足させるものではありません。また、ランク n 型と無限の怠惰な問題についても手短に説明します。

データ型を関数としてエンコードする 1 つの方法は、ケースごとに 1 つの引数を受け取る「パターン マッチング」関数を作成することです。各引数は、そのコンストラクターに対応する値を受け取り、すべての引数が同じ結果の型を返す関数です。

これはすべて、非再帰型の場合に期待どおりに機能します

ただし、パターン マッチングとの優れた類似性は、再帰型ではうまくいきません。私たちは次のようなことをしたくなるかもしれません

しかし、これらの再帰的な型定義を Haskell で書くことはできません! 通常の解決策は、コンス/成功ケースのコールバックを、再帰の最初のレベルだけでなく、すべてのレベルに強制的に適用することです (つまり、フォールド/イテレータを記述します)。このバージョンrでは、再帰型が次のような戻り値の型を使用します。

このバージョンは機能しますが、一部の関数の定義が非常に難しくなります。たとえば、リストの "tail" 関数や数値の "predecessor" 関数を書くことは、パターン マッチングを使用できる場合は簡単ですが、代わりに折り畳みを使用する必要がある場合は注意が必要です。

だから私の本当の質問に：

1. フォールドを使用したエンコーディングが、仮想の「パターン マッチング エンコーディング」と同じくらい強力であることをどのように確認できますか? パターンマッチングを介して任意の関数定義を取得し、代わりに折り畳みのみを使用して機械的に変換する方法はありますか? (もしそうなら、これはまた、foldr に関して、tail や foldl などのトリッキーな定義をあまり魔法のようにしないようにするのにも役立ちます)

2. Haskell 型システムが「パターンマッチング」エンコーディングで必要な再帰型を許可しないのはなぜですか? . 経由で定義されたデータ型で再帰型のみを許可する理由はありdataますか? 再帰代数データ型を直接消費する唯一の方法はパターン マッチングですか? 型推論アルゴリズムと関係がありますか?

dlist パッケージDListには、多数のインスタンスを持つデータ型が含まれていますが、Foldableorは含まれていませんTraversable。私の考えでは、これらは最も「リストに似た」型クラスの 2 つです。DListこれらのクラスのインスタンスではないパフォーマンス上の理由はありますか?

また、パッケージはと を実装しますが、他の折りたたみ機能は実装foldrしません。unfoldr

誰かが置換を使用して、数値「ゼロ」または残りの自然数を取得する方法を説明できますか?

たとえば、値: 「ゼロ」

この式を別の式に適用すると:

次に置換を使用します。

私は何が欠けていますか？これらの数式をどのように解釈すればよいですか?

教会の数字の次のデータコンストラクターを見ました

しかし、これは単数です。このように Haskell で 2 進数のデータ コンストラクターを実装するにはどうすればよいでしょうか?

私はこれを試しました：

この後、次のようにエンコードされた 10 進数 5 を取得できます。BinC [One,Zero,One]

しかし、私はここで何かが欠けていると思います。私の解決策は、教会の解決策ほど賢くないようです。当然のことながら、私は教会ではありません。少し考えてみると、私の解決策はリストに依存しているのに対し、Nat はリストのような外部構造に依存していないことがわかりました。

2 進数にも Succ 型コンストラクタを使用して、Church と同様のソリューションを作成できますか? はいの場合、どのように？私はたくさん試しましたが、私の脳はリストやその他のそのような構造の必要性を取り除くことができないようです.

ラムダ計算で二項指数演算子を定義しようとしています。たとえば、演算子CARATです。たとえば、この演算子は、数値 2 のラムダ エンコーディングと数値 4 のラムダ エンコーディングの 2 つの引数を取り、数値 16 のラムダ エンコーディングを計算します。答えが正しいか間違っているかはわかりませんが、1 日かかりましたそうするために。私は教会の数字の定義を使用しました。

これが私の答えです。私の答えが間違っている場合は修正してください。正しい方法で正確に行う方法はわかりません。誰かが知っているなら、短い答えを理解するのを手伝ってください。

1 を加算する後継関数 は、とnextで自然数を定義できます。zeronext

next上記の結論から、関数を次のように定義できます。

したがって、安全に証明できます…。

追加は、後継者の単なる反復です。これで、 の観点から足し算を定義できるようになりましたnext。

「next」とそれに続く「two」に値を代入した後、上記の形式をさらに次のように縮小できます。

つまり4つ。

同様に、掛け算は足し算の繰り返しです。したがって、乗算は次のように定義されます。

「three」、「next」、続いて「add」、さらに「next」の値を代入した後、上記の形式は次のように縮小されます。

すなわち6。

最後に、累乗は反復乗算によって定義できます

累乗関数をCARATと呼ぶと仮定

ここで、上記の式を簡約して「next」と「four」を代入し、さらに簡約すると、次の形式が得られます

つまり、16 です。

私は本から、Church Numerals の後継者は (\lambda nf x. f (nfx) ) の形式であることを読みました。

昨夜、私はこれを思いついた: (\lambda ab c. (ab) (bc) )

後継機能としての機能も果たしていると思います。ただし、削減が正しいと 100% 確信しているわけではありません。誰か調べて教えてくれませんか？

以下は私の要約です: 教会の数字を (\lambda f x. f^nx) とします。ここで、f^nx は実際には (f(f(f(f...(x)))) の短縮バージョンです。これは数値 n を表します。期待される結果は n+1、つまり (\lambda f x. f^{n+1} x) になるはずです。

(\lambda ab c. (ab) (bc) )(\lambda f x. f^nx)

= (\lambda b c. ( (\lambda f x. f^nx) b) (bc) ) // a 置換

= (\lambda b c. ( (\lambda x. b^nx) (bc) ) // f を置換

= (\lambda b c. ( (\lambda x. b^nx) (bc) ) // 100% 確実ではありません。x を (bc) に置き換えることはできますか?

= (\lambda b c. ( b^n (bc) )

= (\lambda b c. ( b^(n+1) c )

特にステップ 3 から 4 へのこの削減は正しいですか? ありがとう！