4

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

type Churchlist t u = (t->u->u)->u->u

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

[] := λc. λn. n
[1,2,3] := λc. λn. c 1 (c 2 (c 3 n))

mapChurch :: (t->s) -> (Churchlist t u) -> (Churchlist s u)
mapChurch f l = \c n -> l (c.f) n

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

conc2Church l1 l2 c n = l1 c (l2 c n)

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

4

1 に答える 1

4

本物のタプルを使いたいですか、それとも教会のタプルを使いたいですか? 前者とします。

したがって、目的の型シグネチャから始めます。2 つの異なる を取り込んで、タプルChurchlistの を生成する必要があります。Churchlist

churchZip :: Churchlist a u -> Churchlist b u -> Churchlist (a,b) u

これをどのように実装しますか？Churchlists はそれらを折りたたむ関数によって表されることを思い出してください。したがって、結果が である場合Churchlist (a,b) uは、型の関数の形式が必要になります((a,b) -> u -> u) -> u -> u(これは結局、型 synonym と同等Churchlist (a,b) uです)。

churchZip l1 l2 c n = ???

次のステップは何ですか？まあ、それは依存します。l1空ですか？どうl2ですか？どちらかがそうである場合、結果を空のリストにする必要があります。それ以外の場合は、各リストの最初の要素をペアにして、残りを ChurchZip します。

churchZip l1 l2 c n
  | isEmpty l1 || isEmpty l2 = n
  | otherwise                = c (churchHead l1, churchHead l2)
                                 (churchZip (churchTail l1) (churchTail l2) c n

これにより、いくつかの疑問が生じます。

  • この関数を再帰的に記述できますか? 純粋なラムダ計算では、固定小数点演算子 (別名 y コンビネーター) を使用して再帰関数を作成する必要があります。
  • churchHead、churchTail、および はありますかisEmpty? それらを書いてもよろしいですか？あなたはそれらを書くことができますか？
  • この関数を構造化するより良い方法はありますか? 折り畳みを使って何でもできます (覚えておいてください、l1実際l2には折り畳み機能自体がそれ自体です)。

この点に到達することは、リストの教会のコード化をしっかりと理解していることを前提として、純粋に機械的です。これは宿題なので、深く考えるのはあなたに任せます。

于 2012-03-23T22:26:30.143 に答える