私は「Real World Haskell」に取り組んでおり、「折り畳みの普遍性と表現力に関するチュートリアル」という無料の PDF につながっています。「折り目」が「普遍的」であることを強調しています。私は彼の「普遍的」の定義に取り組んでおり、すでにそれを消化するのに時間を費やしている人たちに聞きたいです:可能な限り簡単で専門用語のない英語で説明してください、「折り畳みの普遍的な特性」? この「普遍的な財産」とは何で、なぜ重要なのでしょうか?
ありがとう。
私は「Real World Haskell」に取り組んでおり、「折り畳みの普遍性と表現力に関するチュートリアル」という無料の PDF につながっています。「折り目」が「普遍的」であることを強調しています。私は彼の「普遍的」の定義に取り組んでおり、すでにそれを消化するのに時間を費やしている人たちに聞きたいです:可能な限り簡単で専門用語のない英語で説明してください、「折り畳みの普遍的な特性」? この「普遍的な財産」とは何で、なぜ重要なのでしょうか?
ありがとう。
(専門用語モードオフ:-)
普遍性は、2つの式が等しいことを証明する方法にすぎません。(これが専門用語の「証明原理」の意味です。)普遍性は、これら2つの方程式を証明できれば
g [] = v
g (x:xs) = f x (g xs)
次に、追加の方程式を結論付けることができます
g = fold f v
逆もまた真ですが、の定義を拡張するだけでそれを示すのは簡単ですfold
。普遍性ははるかに深い性質です(これは、なぜそれが真実であるかがあまり明白ではないという、ぎこちない言い方です)。
これを行うことがまったく興味深い理由は、帰納法による証明を回避できるためです。これは、ほとんどの場合、回避する価値があります。
この論文では、次の 2 つのプロパティを定義しています。
g [] = v
g (x : xs) = f x (g xs)
そして、それはそれらの特性を満たす関数であるだけfold
でなく、それらの特性を満たす唯一の関数であると述べています。その点で独特であるということは、論文が使用している意味でそれを「普遍的」にするものです.
foldの特性は、適切なパラメーターを指定すれば、他のすべてのリスト再帰関数と同等のリスト再帰関数であるということです。
このプロパティは、リスト内のアイテムに適用される関数をパラメーターとして受け入れるためです。
たとえば、単純な合計関数を作成した場合、次のようになります。
sum [] = 0
sum (head:tail) = head + (sum tail)
次に、アイテムを結合するために使用する(+)演算子を渡すことにより、実際にはfold関数として記述できます。
sum list = foldl (+) 0 list
したがって、リストに対して単純かつ再帰的に機能する関数は、fold関数として書き直すことができます。その同等性はそれが保持する特性です。例外なく、これらすべての線形リスト再帰アルゴリズムで機能するため、彼はこのプロパティをユニバーサルと呼んでいると思います。
彼が説明するように、このプロパティが非常に役立つ理由は、他のすべてのアルゴリズムが実際にfoldと同等であることを示すことができるため、foldについて何かを証明することで、他のすべてのアルゴリズムでもそれを証明できるからです。
私は個人的に折り畳み機能を理解するのが難しいと思ったので、時々私はこのように見える自分のものを使用しました:
-- forall - A kind of for next loop
-- list is list of things to loop through
-- f is function to perform on each thing
-- c is the function which combines the results of f
-- e is the thing to combine to when the end of the list is reached
forall :: [a] -> (a->b) -> (b->b->b) -> b -> b
forall [] f c e = e
forall (x:xs) f c e = c (f x) (forall xs f c e)
(これは、リスト内の各項目に関数fを適用するという追加機能があるため、実際にはfoldlよりもわずかに強力です。)
さて、誰も私の機能について何も証明しませんでした。しかし、それは問題ではありません。私の関数が実際にはフォールド関数であることを示すことができるからです。
forall l f c e = foldl c e (map fn l)
したがって、foldについて証明されたすべてのことは、私のforall関数、および私のプログラム全体でのそのすべての使用にも当てはまることが証明されています。(forallとfoldlへのさまざまな呼び出しのそれぞれでどのような関数cが提供されるかを考慮する必要さえないことに注意してください、それは問題ではありません!)
ウィキペディアで新しい(私にとって)エントリ「UniversalProperty」を見つけました。それはこの質問にたくさんの光を当てます。リンク は次のとおりです。それから、私は(暫定的に)次のように結論付けます。
合わせて、これらの2つのポイントは、「普遍性」という用語の意味を捉えているようです。
シリーズの以前の投稿を読まずに理解するのは少し難しいかもしれませんが、カテゴリの観点から普遍的なプロパティを説明していますが、この投稿では、fold の普遍的なプロパティ、およびマップとフィルターの詳細なカテゴリ別の説明を提供します。
http://jeremykun.com/2013/09/30/the-universal-properties-of-map-fold-and-filter/
まだ書いていませんが、フォローアップでは、これを一般化して (そして、より抽象的ではありますが、理解しやすくします)、一般的なデータ構造に対する「折り畳みのような」操作にします。
ユニバーサル プロパティとは何かについて詳しくは、この投稿を参照してください: http://jeremykun.com/2013/05/24/universal-properties/
シリーズのすべての投稿へのリンクはこちら: http://jeremykun.com/main-content/
実際、現在受け入れられている答えは、フォールドについて普遍的な性質が何を言っているのかを理解する最も簡単な方法です。上記にリンクされている記事は、問題の論文には存在しない圏論を介して、より詳細な技術的説明を提供するだけです。ただし、普遍的なプロパティは専門用語のないステートメントよりもはるかに深いプロパティであるという、受け入れられた回答のステートメントには同意しません。折り畳みの普遍的な特性は、圏論で物事を分析する性質に従って、最初と最後のオブジェクトの言語に箱詰めされているだけの、まったく同じステートメントです。この分析は、その自然な一般化のために、まさに価値があります。