咖喱在Haskell中的悖论? [英] Curry's paradox in Haskell?

问题描述

Curry悖论 (以与当前编程语言相同的人的名字命名)是一种有可能以错误的逻辑进行的构造，从而使人们无法证明任何事情.

Curry's paradox (named after the same person as the present programming language) is a construction possible in a faulty logic that allows one to prove anything.

我对逻辑一无所知，但是有多难呢?

I know nothing about logic, but how hard can it be?

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或递归的情况下执行相同的操作?为什么?

• Is this a faithful translation? Why?
• Can I do the same without fix or recursion? Why?

推荐答案

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

The encoding of Curry's paradox looks more like this:

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

X的确可以读作句子如果X是真实的，那么就有矛盾"，或者等效地，"X是假的".

X can indeed be read as the sentence "if X is true, then there is a contradiction", or equivalently, "X is false".

但是使用fix来证明X并没有真正意义，因为fix作为推理原理公然不正确.咖喱的悖论更加微妙.

But using fix to prove X is not really meaningful, because fix is blatantly incorrect as a reasoning principle. Curry's paradox is more subtle.

您如何实际证明X?

x :: X
x = _

X是一个条件命题，因此您可以从假设其前提以表明其结论开始.此逻辑步骤对应于插入lambda. (建设性地，蕴涵的证明是从前提的证明到结论的证明的映射.)

X is a conditional proposition, so you can start by assuming its premise to show its conclusion. This logical step corresponds to inserting a lambda. (Constructively, a proof of an implication is a mapping from proofs of the premise to proofs of the conclusion.)

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

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

But now we have an assumption x' :: X, we can unfold the definition of X again to get f :: X -> Void. In informal descriptions of Curry's paradox, there is no explicit "unfolding step", but in Haskell it corresponds to pattern-matching on the newtype constructor when X is an assumption, or applying the constructor when X is the goal (in fact, as we did above):

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

最后，我们现在有f :: X -> Void和x' :: X，因此我们可以通过函数应用程序推断Void:

Finally, we now have f :: X -> Void and x' :: X, so we can deduce Void by function application:

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

这篇关于咖喱在Haskell中的悖论?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！