haskell - スコットでエンコードされたリストを折りたたむ非再帰的な用語はありますか?

Question

次のようなスコットでエンコードされたリストがあるとします。

scott = (\ c n -> c 1 (\ c n -> c 2 (\ c n -> c 3 (\ c n -> n))))

この種のリストを受け取り、それを実際のリスト ( [1,2,3]) に変換する関数が必要ですが、そのような関数は再帰できません。つまり、これは eta-beta 正規形でなければなりません。その機能はありますか？

Answer 1

OK、やってみます。私はこれについての専門家ではないので、遠慮なく訂正してください。

任意のxとの場合、に変換可能な項に還元されるxs場合でなければなりません。toList (\c n -> c x xs)x : toList xs

これは、 someおよびc x xsに適用して左辺を に還元した場合にのみ可能です。だから。(ちなみに、これは私が適切な厳密な議論を考えることができなかった部分です。私にはいくつかのアイデアがありましたが、あまり良いものはありませんでした。ヒントをいただければ幸いです)。(\c n -> c x xs)cntoList ~ (\f -> f ? ?)

今では、その場合に違いありませんc x xs ~ (x : toList xs)。しかし、xとxsは別個の普遍変数であり、右辺で発生する唯一の変数であるため、方程式はミラーのパターン フラグメントにあり、したがってc ~ (\x xs -> x : toList xs)その最も一般的な解です。

したがって、いくつかのtoListに削減する必要があります。再帰的な発生はいつでも展開できるため、明らかに通常の形式を持つことはできません。(\f -> f (\x xs -> x : toList xs) n)ntoList