Khái niệm chuỗi hoàn chỉnh là gì?

Question

Tôi đang đọc cuốn sách được gọi là 'Suy nghĩ về chức năng với Haskell' của Richard Bird và bắt gặp khái niệm về Chuỗi hoàn thành về cảm ứng qua danh sách vô hạn. Nó nói:

Một P sở hữu được gọi là chuỗi hoàn chỉnh nếu bất cứ khi nào xs0, xs1, ... là một chuỗi các danh sách phần với xs giới hạn, và P (xsn) giữ cho tất cả n, sau đó P (xs) cũng nắm giữ.

Như một ví dụ về tài sản hoàn thành chuỗi, nó nói:

Tất cả các phương trình e1 = e2, nơi e1 và e2 là Haskell biểu thức liên quan đến các biến miễn phí phổ biến định lượng, là chuỗi hoàn chỉnh.

Tôi đang gặp khó khăn để hiểu ví dụ này phù hợp với đặc tính của chuỗi hoàn chỉnh tại đây như thế nào. Và nó cũng cho biết sự bất bình đẳng e1 =/= e2 không nhất thiết là chuỗi hoàn chỉnh. Làm thế nào để tôi hiểu các thuộc tính này về điều này Chuỗi Hoàn thành -ness?

Bằng cách này, điều này có thể không nhất thiết phải là câu hỏi liên quan đến Haskell, mà là một câu hỏi về toán học.

Answer 1

Đây là một ví dụ.

Giả sử bạn có chuỗi danh sách ngày càng tăng xs_1, xs_2, ... với giới hạn xs.

Đối với mỗi k, chúng tôi có rằng map id xs_k bằng xs_k.

Bằng cách hoàn thành chuỗi (AKA Scott liên tục), chúng tôi nhận được rằng map id xs là xs.

Điều này cho chúng ta cách chứng minh các thuộc tính trên danh sách giới hạn xs, có thể vô hạn bằng cách xác minh chúng chỉ trên xấp xỉ xs_k.

Trực giác ở đây là, đối với xs là danh sách giới hạn, mỗi xs_k phải bằng xs hoặc một số tiền tố ngắn hơn của biểu mẫu x1:x2:...:xn:undefined. Lưu ý đuôi không xác định, biểu diễn tính toán vòng lặp (ví dụ: đệ quy vô hạn). Bởi vì điều này, nếu chúng ta so sánh f xs_k và f xs, chúng ta thấy rằng sau này phải ít nhất là kết thúc như trước đây. Ý tưởng chung ở đây là nếu chúng ta chuyển một đầu vào nhiều hơn hoặc được định nghĩa, chúng ta sẽ nhận được một đầu ra nhiều hơn hoặc được xác định. Về mặt toán học, khái niệm này bị bắt bởi sự đơn điệu trên thứ tự Scott.

Scott omega-continuity, hoặc chain completeeness, đi xa hơn. Nó cho chúng ta biết f xs chính xác là giới hạn của chuỗi f xs_k. Kết quả cuối cùng được ước tính bằng kết quả của f trên các xấp xỉ. Nói cách thô ráp, bạn có thể làm cho đầu ra hội tụ bằng cách làm cho đầu vào hội tụ.

Bất bình đẳng không hoạt động theo kiểu hoàn chỉnh của chuỗi. Thực tế, hãy lấy xs = [0..] làm danh sách vô hạn và xấp xỉ xs_k = 0:...:k:undefined. Rõ ràng là xs_k không bằng xs, cho mỗi k.Nhưng chúng tôi không lấy giới hạn của sự bất bình đẳng đó, mà sẽ nêu rằng xs không bằng xs.

Kết luận, chủ đề ở đây khá rộng. Nếu bạn quan tâm, tôi khuyên bạn nên đọc về ngữ nghĩa biểu thị, ví dụ như đọc sách của Winskel.