为什么我们可以实现call/cc，但是经典逻辑(直觉+调用/cc)不是建设性的？

Question

直觉逻辑是功能程序设计中类型系统的基础，具有建设性。经典逻辑不是建设性的，特别是排除的中间A、A、A(或它的等价物，如双重否定消除或皮尔斯定律)的定律。

但是，我们可以实现(构造) 用电流呼叫-继续操作符(AKA /cc)，例如在方案中。那么，为什么调用/抄送不是建设性的呢？

Answer 1

问题是，对于call/cc，结果取决于评估的顺序。考虑Haskell中的以下示例。假设我们有call/cc运算符

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

让我们来定义

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

这两个函数都是纯的，因此应该唯一地确定example的值。然而，这取决于评估顺序。如果首先计算s 3，则结果是3；如果首先计算t 4，则结果是4。

这相当于连续单(强制命令)中的两个不同的例子：

-- 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)
        )
    )

它甚至取决于是否对某个术语进行了评估：

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

如果计算s 2，则结果为2，否则为1。

这意味着在call/cc存在的情况下，丘奇-罗瑟定理 不保存。特别是，术语不再具有唯一的 正规形式。

也许一种可能是将call/cc看作是一个非确定性(非建设性)运算符，它将(不)按不同顺序计算不同子项所获得的所有可能结果结合起来。然后，程序的结果将是所有这些可能的范式的集合。然而，标准的调用/cc实现总是只选择其中的一个(取决于其特定的评估顺序)。