Pure Lambda微积分 - 和函数

我目前正在学习Haskell，并且还参加了一个关于大学函数式编程的理论性讲座。我知道这是纯粹的理论/学术问题，但我感兴趣的是如何简单地用纯lambda演算（即没有定义任何常量）来表达不同的简单函数。Pure Lambda微积分 - 和函数

我的一些演讲材料定义布尔值，例如：

真 = \ xy.x
假 = \ xy.y

（\表示lambda符号）

如果它们像这些选择器函数一样定义，那么if-con dition可以很容易地定义为：

如果 = \ x.x中

现在，我试图想出一些简写形式逻辑“和” - 函数。我的第一猜测是：

和 = \ XY {（如果 x）的[（如果 Y）真假] 假}

所以基本上这个lambda函数会接收2个参数uv，其中必须输入True/False。如果我用逻辑表的所有4个组合进行各种β减少，我会得到正确的结果。

尽管如此，这个功能看起来有点难看，我正在考虑让它更加优雅。这里有什么建议？

来源

2014-06-30 Rodney

也许相关：http：//stackoverflow.com/questions/2398503/query-on-booleans-in-lambda-calculus –

@ A.E ++，尤指。特殊的答案http://stackoverflow.com/questions/2398503/query-on-booleans-in-lambda-calculus/2399127#2399127那里。 –

我们可以简化您的答案，以获得更丰富的答案。

首先一些热身。显然IF x ==> x和TRUE TRUE FALSE ==> TRUE和FALSE TRUE FALSE ==> FALSE如果x是一个布尔然后x TRUE FALSE ==> x。

现在我们减少

\x y . (IF x) ((IF y) TRUE FALSE) FALSE 
\x y .  x ( y TRUE FALSE) FALSE -- using IF x   ==> x 
\x y .  x ( y   ) FALSE -- using y TRUE FALSE ==> y 
\x y . x y FALSE       -- clean up

这个表述仍与真值表工作

AND TRUE TRUE = TRUE TRUE FALSE = TRUE 
AND FALSE TRUE = FALSE TRUE FALSE = FALSE 
AND TRUE FALSE = TRUE FALSE FALSE = FALSE 
AND FALSE FALSE = FALSE FALSE FALSE = FALSE

来源

2014-06-30 23:34:14

启发。这是我想要的。谢谢！ – Rodney

那么，and True是身份函数，and False是返回False的常量函数，所以我们可以使用它。

and = \x. if x id (const False)

其具有很好的对称性与

or = \x. if x (const True) id

（其中

id = \x. x 
const = \x y. x

）

用于除水的共用图案在参数列表的末尾取数据，其经常使用无点风格的优雅作品，所以如果你定义了：

cond = \t f b. b t f

，那么你可以表达

and = cond id (const False) 
or = cond (const True) id

这是我已经得到了最好。通过冷静观察布尔，可能还有更优雅的配方。

来源

2014-06-30 23:34:03 luqui

教会的布尔值，对不对？ :)我使用RankNTypes功能开发了一个小模块，以便尽可能接近原始Lambda演算版本。

因此，如果您启用RankNTypes：

{-# LANGUAGE RankNTypes #-}

您可能代表教会的boolean类型的功能a -> a -> a任何类型a，因此具有真假非常类似你这样的紧凑表示。尽管如此，在这里键入将允许我们更自由地编写函数。

type CBool = forall a. a -> a -> a 

ctrue :: CBool 
ctrue t f = t 

cfalse :: CBool 
cfalse t f = f

现在，用这些术语写成的连词怎么样？假设您有一个左操作数l和右操作数r这两个都是CBool，即功能a -> a -> a或者返回您的第一个或第二个参数取决于它是否是ctrue或cfalse。您可以通过输入r作为第一个参数，并将l本身作为第三个参数来评估此功能。如果l是ctrue，那么它将评估为它的第一个参数，即r：如果它再次为ctrue，那么我们的结合是满足的。在其他情况下，将返回cfalse。

cand :: CBool -> CBool -> CBool 
cand l r = l r l

该析取可以用类似的方式表示，具有直接评估表示输入中给定的布尔值函数的相同技巧。除了这里，你会交换两个参数评估l：如果l是ctrue，它将返回l本身否则一切都取决于r的价值

cor :: CBool -> CBool -> CBool 
cor l r = l l r

通过启用RankNTypes，我认为这是最接近你在Lambda微积分中得到Church的布尔数的连接和分离的原始定义。我还写了函数来从常规布尔和CBool，否定以及同样风格的教会自然数来回翻译。你可以在https://github.com/rtraverso86/haskkit/blob/master/Haskkit/Data/Church.hs找到整个源代码。

来源

2014-07-01 08:51:30

Pure Lambda微积分 - 和函数

回答

相关问题