7

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

我对逻辑一无所知,但它有多难?

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递归的情况下做同样的事情吗?为什么?
4

1 回答 1

4

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

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

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

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

你如何实际证明X

x :: X
x = _

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

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

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

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

最后,我们现在有了f :: X -> Voidand ,所以我们可以通过函数应用x' :: X来推断:Void

x :: X
x = X (\x'@(X f) -> f x')
于 2019-10-12T13:51:41.293 回答