haskell - 库里在 Haskell 中的悖论？

Question

Curry's paradox (以与当前编程语言相同的人命名)是一种可能在错误逻辑中的构造，它允许人们证明任何事情。

我对逻辑一无所知，但它有多难？

module Main where

import Data.Void
import Data.Function

data X = X (X -> Void)

x :: X
x = fix \(X f) -> X f

u :: Void
u = let (X f) = x in f x

main :: IO ()
main = u `seq` print "Done!"

它肯定会循环。 (GHC怎么知道？!)

% ghc -XBlockArguments Z.hs && ./Z
[1 of 1] Compiling Main             ( Z.hs, Z.o )
Linking Z ...
Z: <<loop>>

这是忠实的翻译吗？为什么？

如果没有 fix 我可以这样做吗？还是递归？为什么？

Answer 1

库里悖论的编码看起来更像这样:

x :: X
x = X (\x'@(X f) -> f x')

X确实可以读作“如果 X 为真，则存在矛盾”，或者等效地，“ X 为假”。

但是使用 fix证明 X没有真正的意义，因为 fix作为推理原则是公然不正确的。库里的悖论更加微妙。

你如何证明 X ?

x :: X
x = _

X是一个条件命题，所以你可以先假设它的前提来证明它的结论。这个逻辑步骤对应于插入一个 lambda。 ( build 性地，蕴涵证明是从前提证明到结论证明的映射。)

x :: X
x = X (\x' -> _)

但现在我们有一个假设 x' :: X ，我们可以展开 X的定义再次获得 f :: X -> Void .在 Curry 悖论的非正式描述中，没有明确的“展开步骤”，但在 Haskell 中，它对应于 newtype 构造函数上的模式匹配 X是一个假设，或者在 X 时应用构造函数是目标(事实上，正如我们上面所做的那样):

x :: X
x = X (\x'@(X f) -> _)

最后，我们现在有 f :: X -> Void和 x' :: X , 所以我们可以推导出 Void按功能应用:

x :: X
x = X (\x'@(X f) -> f x')