functional-programming - 为什么我们可以实现 call/cc，但经典逻辑（直觉 + call/cc）却没有建设性？

Question

直观的逻辑，具有建设性，是函数式编程中类型系统的基础。经典逻辑不是建设性的，尤其是排中律A ∨ ¬A（或其等价物，例如双重否定消除或皮尔斯定律）。

但是，我们可以实现（构造）call-with-current-continuation运算符（AKA call/cc），例如在Scheme中。那么为什么call/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.

这对应于 continuation monad（强制执行顺序）中的两个不同示例：

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

这意味着Church-Rosser 定理在call/cc存在时不成立。特别是，术语不再具有唯一的范式。

也许一种可能性是将call/cc视为一个非确定性（非建设性）运算符，它结合了通过（不）以各种顺序评估不同子项获得的所有可能结果。那么程序的结果将是所有这些可能的范式的集合。然而，标准的call/cc实现将始终只选择其中一个（取决于其特定的评估顺序）。