チェーンコンプリートのコンセプトは何ですか？

Question

私はリチャード・バードの「Thinking Functionally with Haskell」という本を読んでいて、というコンセプトのチェーンコンプリートに遭遇しました。 それは言う：

プロパティPは、チェーンが完全に呼び出されXS0、XS1、...が制限XSとの部分リストのシーケンスであり、かつP（XSN）は、すべてのnについて成り立つ、その後、P（XSたび場合）も成り立つ。チェーンの完全なプロパティの例として

、それは言う：

E1とE2は普遍的数量化自由変数を含むHaskellの式ですべての方程式E1 = E2は、チェーン完了しています。

この例がチェーンの完全性のプロパティにどのように適合しているか理解していません。また、不等式e1 =/= e2が必ずしもチェーン完全ではないことも述べている。これらの性質を理解するにはどうすればいいですかチェーンコンプリート -ness？

しかし、これは必ずしもハスケルに関する質問ではなく、数学の観点からの質問です。

Answer 1

例を示します。

リストxs_1, xs_2, ...のリストが増加しており、制限がxsであるとします。

kごとに、map id xs_kはxs_kに等しくなります。

チェーンの完全性（AKAスコットの連続性）によって、map id xsはxsになります。

これは、限界リストでのみ検証することによって、制限リストxsのプロパティを無限である可能性があることを証明する方法を提供します。ここで

直感xsの制限リストであること、つまり、各xs_kはxsまたはフォームx1:x2:...:xn:undefinedの一部短いプレフィックスに等しくなければなりません。ループ計算（例えば、無限再帰）を表す、未定義のテールに注意してください。このため、f xs_kとf xsを比較すると、後者は少なくとも前者と同じである必要があります。ここでの一般的な考え方は、より多くの、または定義された入力を渡すと、より多くの出力または定義された出力が得られるということです。数学的には、この概念はスコットオーダーの単調性によって捕捉される。

スコットオメガ連続性、またはチェーン完全性、さらに進んでいます。これはf xsが配列f xs_kの限界とまったく同じであることを示しています。最終結果は近似値のfの結果で近似されます。おおまかな言葉では、入力を収束させることによって出力を収束させることができます。

不等式は完全なチェーンでは機能しません。確かに無限リストとしてxs = [0..]、近似はxs_k = 0:...:k:undefinedとしてください。 がxsと等しくないことは明らかであり、それぞれについてはkである。しかし、我々はその不等式の限界をとらない。xsはxsと等しくないと述べる。

結論として、ここでの話題はかなり広範囲です。興味があれば、例えばWinskelの本を読むなど、意味論的意味論について読んでみることをお勧めします。