Chain Complete的概念是什麼？

Question

我正在閱讀理查德·伯德的一本名爲「思考功能與哈斯克爾」的書，並且遇到了關於無限列表上的歸納的鏈完成的概念。 它說：

的屬性P稱爲鏈完整，如果每當XS0，XS1，...是部分列表與限制XS的序列，和P（XSN）適用於所有n，則P（XS ）也成立。

作爲鏈的完整屬性的一個例子，它表示：

所有等式E1 = E2，其中E1和E2是涉及普遍量化自由變量的Haskell表達式，是鏈的完整。

我很難理解這個例子如何適合鏈完整的屬性在這裏。它也表示不平等e1 =/= e2不一定是鏈完整的。我該如何理解這些屬性Chain Complete -ness？順便說一下，這可能不一定是關於Haskell的問題，而是數學方面的一個問題。

Answer 1

下面是一個例子。

假設您有一個遞增的列表序列xs_1, xs_2, ...，其限制爲xs。

對於每k，我們有map id xs_k等於xs_k。

通過鏈完整性（AKA Scott連續性），我們得到map id xs是xs。

這給了我們一種方法來證明極限列表xs上的屬性，它們可能是無限的，只需在它們的近似值xs_k上驗證它們即可。

的直覺這裏是，對於xs是一個限制列表，每個xs_k必須等於或xs形式x1:x2:...:xn:undefined的一些短前綴。注意未定義的尾部，表示循環計算（例如無限遞歸）。因此，如果我們比較f xs_k和f xs，我們發現後者必須至少與前者一樣終止。這裏的一般想法是，如果我們通過更多或者定義的輸入，我們會得到更多或者定義的輸出。在數學上，這個概念是通過Scott命令的單調性來捕獲的。

斯科特歐米伽連續性或鏈條完整性更進一步。它告訴我們f xs與序列f xs_k的限制完全相同。最終結果近似爲近似值f的結果。粗略地說，可以通過使輸入收斂來使輸出收斂。

不平等不以鏈完整的方式工作。確實，以xs = [0..]作爲無限列表，並且近似值爲xs_k = 0:...:k:undefined。很明顯，xs_k不等於xs，對於每個k。但是我們並沒有考慮到這種不平等的侷限性，因爲xs並不等於xs。

結論是，這裏的主題非常廣泛。如果您有興趣，我建議您閱讀有關指稱語義學，例如閱讀溫斯克爾的書。