Tại sao chúng ta có thể thực hiện cuộc gọi/cc, nhưng logic cổ điển (intuitionistic + call/cc) không mang tính xây dựng?

Question

Logic trực giác, mang tính xây dựng, là cơ sở cho các hệ thống kiểu trong lập trình hàm. Logic cổ điển không mang tính xây dựng, đặc biệt là luật bị loại trừ giữa A ∨ ¬A (hoặc các giá trị tương đương, chẳng hạn như double negation elimination hoặc Pierce's law).

Tuy nhiên, chúng tôi có thể triển khai (xây dựng) toán tử call-with-current-continuation (AKA gọi/cc), ví dụ như trong Scheme. Vậy tại sao không phải là gọi/cc mang tính xây dựng?

Answer 1

Vấn đề là với cuộc gọi/cc kết quả phụ thuộc vào thứ tự đánh giá. Hãy xem ví dụ sau trong Haskell. Giả sử chúng ta có cuộc gọi/cc hành

callcc :: ((a -> b) -> a) -> a 
callcc = undefined 

hãy định nghĩa

example :: Int 
example = 
    callcc (\s -> 
     callcc (\t -> 
      s 3 + t 4 
     ) 
    ) 

Cả hai chức năng là tinh khiết, vì vậy giá trị của example nên duy nhất xác định. Tuy nhiên, nó phụ thuộc vào thứ tự đánh giá. Nếu s 3 được đánh giá trước, kết quả là 3; nếu t 4 được đánh giá trước, kết quả là 4.

này tương ứng với hai ví dụ rõ rệt trong đơn nguyên tiếp tục (mà thực thi theo thứ tự):

-- the result is 3 
example1 :: (MonadCont m) => m Int 
example1 = 
    callCC (\s -> 
     callCC (\t -> do 
      x <- s 3 
      y <- t 4 
      return (x + y) 
     ) 
    ) 

-- the result is 4 
example2 :: (MonadCont m) => m Int 
example2 = 
    callCC (\s -> 
     callCC (\t -> do 
      y <- t 4 -- switched order 
      x <- s 3 
      return (x + y) 
     ) 
    ) 

Nó thậm chí phụ thuộc vào nếu một thuật ngữ được đánh giá ở tất cả hoặc không:

example' :: Int 
example' = callcc (\s -> const 1 (s 2)) 

Nếu s 2 được đánh giá, kết quả là 2, nếu không 1.

Điều này có nghĩa rằng Church-Rosser theorem không giữ trong sự hiện diện của cuộc gọi/cc. Cụ thể, các điều khoản không còn có duy nhất normal forms.

Có lẽ một khả năng là xem gọi/cc với tư cách là toán tử không xác định (kết hợp), kết hợp tất cả các kết quả có thể thu được bằng (không) đánh giá các cụm từ khác nhau theo thứ tự khác nhau. Kết quả của một chương trình sau đó sẽ là tập hợp của tất cả các hình thức bình thường như vậy có thể. Tuy nhiên, việc thực hiện cuộc gọi tiêu chuẩn/cc sẽ luôn chỉ chọn một trong số chúng (tùy thuộc vào thứ tự đánh giá cụ thể của nó).