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

Question

直观的逻辑，具有 build 性，是函数式编程中类型系统的基础。经典逻辑不是 build 性的，尤其是排中律 A ∨ ¬A(或其等价物，例如 double negation elimination 或 Pierce's law )。

但是，我们可以实现(构造)call-with-current-continuation运算符(AKA call/cc)，例如 Scheme .那么为什么 call/cc 没有 build 性呢？

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 theorem不持有 在调用/抄送的情况下。特别是， 术语不再具有唯一性 normal forms .

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