纯Lambda微积分与函数

Question

我目前正在学习Haskell，并在大学里参加了一个关于函数式编程的相当理论的讲座。

我知道这纯粹是理论/学术问题，但我感兴趣的是如何用纯lambda微积分(即没有定义任何常数)来表达不同的简单函数。

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

True = \xy.x False = \xy.y

(\表示lambda符号)

如果它们是像这些选择器函数一样定义的，则If -条件可以很容易地定义为：

如果= \x.x

现在，我正在尝试为逻辑“和”-function提出一些简短的形式。我的第一个猜测是：

和= \xy.{(If x)(If y) True FalseE 220E 121False<>E 222}

因此，基本上，这个lambda函数将接收两个参数u，其中两个参数都必须输入为True/False。如果我用逻辑表的所有4个组合进行各种β-缩减，我就会得到正确的结果。

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

Answer 1

我们可以在你的回答上做些削减，以得到一个更好的答案。

先做些热身。显然是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

Answer 2

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

这是我所拥有的最好的。也许还有更优雅的配方，以冷静的方式看待bools。

Answer 3

教堂的布尔函数，对吗？:)为了好玩，我使用RankNTypes特性开发了一个小模块，以便尽可能接近原始的Lambda微积分版本。

所以，如果您启用RankNTypes

{-# LANGUAGE RankNTypes #-}

您可以将教会布尔人的类型表示为任何类型的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中，您可以得到丘奇布尔数的连接和分离的最初定义。我还写了一些函数，可以从普通的Bool和CBool (否定)和丘奇的自然数中来回翻译。您可以在https://github.com/rtraverso86/haskkit/blob/master/Haskkit/Data/Church.hs找到整个源代码。