我一直在自学这些东西,所以我当然希望我能做对……
正如 nm 所提到的,Haskell 的类型对于这个问题非常重要。类型系统限制了可以形成的表达式,特别是 lambda 演算的最基本类型系统禁止自我应用,这最终为您提供了一种非图灵完备的语言。图灵完备性被添加到基本类型系统之上,作为语言的额外功能(fix :: (a -> a) -> a
运算符或递归类型)。
这并不意味着你不能在 Haskell 中实现它,而是这样的实现不会只有一个操作符。
方法#1:从这里实现第二个示例单点组合逻辑基础,并添加一个fix
函数:
iota' :: ((t1 -> t2 -> t1)
-> ((t5 -> t4 -> t3) -> (t5 -> t4) -> t5 -> t3)
-> (t6 -> t7 -> t6)
-> t)
-> t
iota' x = x k s k
where k x y = x
s x y z = x z (y z)
fix :: (a -> a) -> a
fix f = let result = f result in result
现在您可以用iota'
和编写任何程序fix
。解释这是如何工作的有点复杂。(编辑:请注意,这iota'
与λx.x S K
原始问题中的不同;它λx.x K S K
也是图灵完备的。在这种情况下,iota'
程序将与iota
程序不同。我已经尝试过iota = λx.x S K
Haskell 中的定义;它类型检查,但是当您尝试k = iota (iota (iota iota))
并s = iota (iota (iota (iota iota)))
遇到类型错误时。)
方法#2:可以使用这种递归类型将无类型的 lambda 演算表示法嵌入到 Haskell 中:
newtype D = In { out :: D -> D }
D
基本上是一种类型,其元素是从D
到的函数D
。我们必须In :: (D -> D) -> D
将一个D -> D
函数转换为一个普通的D
,并out :: D -> (D -> D)
做相反的事情。因此,如果我们有x :: D
,我们可以通过 do 自行应用它out x x :: D
。
给它,现在我们可以写:
iota :: D
iota = In $ \x -> out (out x s) k
where k = In $ \x -> In $ \y -> x
s = In $ \x -> In $ \y -> In $ \z -> out (out x z) (out y z)
In
这需要来自and的一些“噪音” out
;Haskell 仍然禁止您将 aD
应用于 a D
,但我们可以使用In
andout
来解决这个问题。你实际上不能对 type 的值做任何有用的事情D
,但你可以围绕相同的模式设计一个有用的类型。
编辑: iota 基本上是λx.x S K
, whereK = λx.λy.x
和S = λx.λy.λz.x z (y z)
. 即,iota 采用两个参数的函数并将其应用于 S 和 K;因此,通过传递一个返回其第一个参数的函数,你得到 S,并通过传递一个返回其第二个参数的函数,你得到 K。所以如果你可以用 iota 编写“返回第一个参数”和“返回第二个参数”,你可以用iota写S和K。但是S 和 K 足以获得图灵完备性,因此您也可以在讨价还价中获得图灵完备性。事实证明,您可以使用 iota 编写必要的选择器函数,因此 iota 足以实现图灵完备。
因此,这将理解 iota 的问题简化为理解 SK 演算。