Adr*_*nat 1 haskell typing lambda-calculus
我对Haskell中的函数有以下定义.
> q7 :: forall a. forall b. ((a -> b) -> a) -> a
我要么为它创建一个定义,要么说明为什么定义不存在.这是我的想法:
q7接受任何类型的a和b.该声明(a -> b) -> a将通过采取两个项目并返回后者来实施.现在,如果我再进一步,我可以返回同样的" a"来实现((a -> b) -> a) -> a.我看到在一个问题a和b可以是任何类型,因此对于每个实例a,可能a是不同的类型？例如,它可能是这样的((Int -> Bool) -> [Char]) -> Int吗？我可能谋杀了那种语法.如果有人有任何提示,或者有人可以确认或否认我的想法,我将非常感激!
这是不可能的,除非使用无限递归或运行时错误,因此无法终止.
我们可以证明这是不可能的,利用理论计算机科学的一些结果.我不知道是否有一种更简单的方式来表明它确实是不可能的.
如果有一种方法来编写具有该类型的终止程序,通过Curry-Howard对应,我们将得到逻辑公式((a -> b) -> a) -> a(这里,读->作"暗示")是命题直觉逻辑的定理.
这样的公式被称为Peirce定律,并且是直觉主义逻辑中无法证明的公式的关键例子之一(通过对比,它是经典逻辑中的定理).
作为证明Peirce定律不是直觉定理的一种相当简单的方法,人们可以运行命题直觉主义逻辑的决策程序,并观察它输出"不是定理".作为这样的程序,我们可以在Gentzen的LJ后续演算中搜索无切割证明:这样我们只需要检查有限(和小)数量的可能证明,并观察每次尝试都失败.