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 确实可以读作句子 "if X is true, then there is a contradiction"，或者等效地，“X 是假的”。

但是用fix来证明X其实意义不大，因为fix作为推理原理是公然不正确的。库里的悖论更加微妙。

你如何证明X？

x :: X
x = _

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

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

但是现在我们有了一个假设x' :: X，我们可以再次展开X的定义得到f :: X -> Void。在 Curry 悖论的非正式描述中，没有明确的 "unfolding step"，但在 Haskell 中，当 X 是一个假设时，它对应于新类型构造函数上的模式匹配，或者当 X 时应用构造函数 X 是目标（实际上，正如我们上面所做的）：

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

最后，我们现在有f :: X -> Void和x' :: X，所以我们可以通过函数应用推导出Void：

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

Haskell 中的库里悖论？

Curry's paradox in Haskell?

haskell

recursion

logic

curry-howard