問題タブ [church-encoding]

私は、教会でエンコードされたデータ型を Scala で実装する方法を考え出そうとしています。consttype のファーストクラス関数が必要になるため、ランク n 型が必要なようですforAll a. a -> (forAll b. b -> b)。

ただし、次のようにペアをエンコードできました。

リストの場合、エンコードできましたcons：

ただし、空のリストはより問題があり、Scala コンパイラーに型を統一させることができませんでした。

上記の定義が与えられた場合、次のものがコンパイルされるように、nil を定義できますか?

スキームを使用して、教会の数字をかなり簡単に定義できます。

ただし、これでは、 が 0 で (f (ff)) が 1 であることを簡単に認識できません(f f)。これらの数字を読みやすくする方法はありますか? 理想的なのは次のとおりです。

例はスキームにありますが、私は任意のリスプで答えます。

次のステップで立ち往生しています。誰かが私を助けることができれば、それは素晴らしいことです:

私の手順は次のとおりです。

括弧は大丈夫ですか？私は置換と括弧について本当に混乱しています。このような問題に対処するための正式で簡単な手法はありますか?

私はSMLで練習していて、次のように定義されたチャーチ数を実装する必要がある小さな割り当てを行っています。

例val

私はすでに関数を実装しました：

SUCチャーチ数の後継を返します。

今、私は関数を実装する必要があります

（前の、現在の数字）のタプルを返します。使用は許可されていませんchurchToInt。チャーチ数を直接使用する必要があります。どうやらこれは特定の引数を渡すことによって1行で解決可能です。

SUC正しい数字になるまで何度も使うことを考えていましたが、2つのチャーチ数を比較する方法がありません。私はこれに完全に固執しています。

私は SICP を使って作業していますが、問題 2.6によって私は困惑しています。チャーチ数を扱う場合、0 と 1 を特定の公理を満たす任意の関数にエンコードするという概念は理にかなっているように思われます。さらに、ゼロの定義と add-1 関数を使用して個々の数を直接定式化することは理にかなっています。プラス演算子を形成する方法がわかりません。

これまでのところ、私はこれを持っています。

lambda calculusのウィキペディアのエントリを調べたところ、 plus の定義は PLUS := λmnfx.mf (nfx) であることがわかりました。その定義を使用して、次の手順を定式化することができました。

私が理解していないのは、以前に派生したプロシージャによって提供された情報のみを使用して、そのプロシージャを直接派生させる方法です。厳密な証明のような形式でこれに答えることができる人はいますか? 直感的には何が起こっているのか理解できると思いますが、Richard Feynman がかつて言ったように、「構築できなければ、理解することはできません...」

Haskell で教会の数字を実装しようとしていますが、ちょっとした問題が発生しました。Haskell は無限型について不平を言っています

チェックが発生します: 無限型を構築できません: t = (t -> t1) -> (t1 -> t2) -> t2

引き算をしようとすると。私は自分のラムダ計算が有効であることを 99% 確信しています (そうでない場合は教えてください)。私が知りたいのは、関数で haskell を機能させるためにできることがあるかどうかです。

教会の数字は、次のような言語の新しいラムダ部分を使用して、C++0x (C++11?) で表現できます。

Boost.Bind と C++03 を使用して教会の数字を表現することはできますか? もしそうなら、どのように？

私が読んでいるコンピュータープログラムの構造と解釈の本は、ゼロとインクリメント関数を定義することによって教会の数字を提示しています

これは私にはかなり複雑に思え、それを理解して 1 つ ( λf.λx. f x) と 2 つ( ) を導出するのに非常に長い時間がかかりましたλf.λx. f (f x)。

ゼロを空のラムダとして、代わりにこの方法で数値をエンコードする方がはるかに簡単ではないでしょうか?

λ. λこれで、1 つ ( ) と 2 つ( ) などを導出するのは簡単λ. λ. λです。

これは、ラムダで数値を表現するためのはるかに明白で直感的な方法のように思えます。このアプローチには何らかの問題があり、教会の数字がそのように機能する正当な理由がありますか? このアプローチはすでに証明されていますか?

次のように定義されている教会リストを操作するには、haskell マップ関数を実装する必要がありました。

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

この演習のサンプル ソリューションは次のとおりです。

このソリューションがどのように機能するのかわかりませんし、そのような関数を作成する方法もわかりません。私はすでにラムダ計算と教会数の経験がありますが、この演習は私にとって大きな頭痛の種であり、来週の試験のためにそのような問題を理解して解決できなければなりません. そのような問題を解決する方法を学ぶことができる良い情報源を教えてください。または、それがどのように機能するかについて少しガイダンスを教えてください

Church encoding (別名 Visitor Pattern) は、データを関数として表現する方法です:

あなたが定義することができます

. 何でも関数として表現できるのは素晴らしいことですが、最初のバージョンの方がすっきりしていて、言語拡張 (明示的) を必要としないため、常に好ましいと思っていましたforall。ただし、公共図書館で教会がエンコードしたデータを見つけることができます。それを使用する利点は何ですか？

公共図書館における教会のエンコーディングの例:

• 繰り返す
• リビジョン管理モナド
• （リストを拡張するのを手伝ってください）