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

Question

直觉逻辑是建设性的,是函数式编程中类型系统的基础.经典逻辑不是建设性的,特别是被排除的中间A∨¬A(或其等价物,例如双重否定消除或皮尔斯定律)的定律.

但是,我们可以实现(构造)call-with-current-continuation运算符(AKA call/cc),例如在Scheme中.那么为什么不打电话/ 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视为非确定性(非建设性)运算符,其结合通过(不)以各种顺序评估不同子项而获得的所有可能结果.然后,程序的结果将是所有这些可能的正常形式的集合.但是,标准调用/ cc实现将始终只选择其中一个(取决于其特定的评估顺序).