Có bất kỳ thuật ngữ không đệ quy nào lặp lại trên danh sách được mã hóa bằng scott không?

Question

Giả sử rằng tôi có một danh sách scott-encoded như:

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

Tôi muốn có một chức năng tiếp nhận loại đó của danh sách và chuyển đổi nó vào một danh sách thực tế ([1,2,3]), ngoại trừ chức năng như vậy không thể được đệ quy. Nghĩa là, nó phải ở dạng bình thường eta-beta. Chức năng đó có tồn tại không?

Answer 1

OK, tôi cho nó một shot. Cảm thấy tự do để sửa tôi, bởi vì tôi không phải là một chuyên gia về điều này.

Đối với tùy ý x và xs, phải là trường hợp toList (\c n -> c x xs) giảm xuống một cụm từ có thể chuyển đổi thành x : toList xs.

Điều này chỉ có thể xảy ra nếu chúng tôi giảm phía bên tay trái sang c x xs bằng cách áp dụng (\c n -> c x xs) cho một số c và n. Vì vậy, toList ~ (\f -> f ? ?). (BTW, đây là phần mà tôi không thể nghĩ ra một cuộc tranh luận khắt khe tốt đẹp; tôi có một số ý tưởng nhưng không có ý tưởng nào tốt đẹp. Tôi rất vui khi được nghe lời khuyên).

Bây giờ, phải là trường hợp c x xs ~ (x : toList xs). Nhưng vì x và xs là các biến phổ biến riêng biệt và chúng là các biến duy nhất xảy ra ở phía bên tay phải, phương trình nằm trong Miller's pattern fragment và do đó c ~ (\x xs -> x : toList xs) là giải pháp chung nhất của nó.

Vì vậy, toList phải giảm xuống (\f -> f (\x xs -> x : toList xs) n) đối với một số n. Rõ ràng, toList không thể có dạng bình thường, vì chúng tôi luôn có thể mở ra sự xuất hiện đệ quy.