评估lambda演算：如果为假，则为false

Question

lambda演算有以下表达式：

e ::=           Expressions
      x         Variables
      (λx.e)    Functions
      e e       Function application

从这个基础，我们可以定义一些额外的结构，如布尔值和条件语句：

let true = (λx.(λy.x))
false = (λx.(λy.y))
if = (λcond.(λthen.(λelse.cond then else)))

显示您的工作，显示以下程序的评估：if false false true。

也许if(false (then false ( else true then true)))？

但这只是意味着它意味着什么。 if false then false else true then true。

我不知道如何处理它。

Answer 1

有定义

true = (λx.(λy.x))
false = (λx.(λy.y))
if = (λcond.(λthen.(λelse.cond then else)))

定义，意味着

true x y = x
false x y = y
if cond then else = cond then else

因此，例如，

   if true true false
-- if cond then else   = cond then else
                       = true true false
                     --  true x    y      = x
                                          = true

这里没有更多的定义，所以我们有结果。

现在你可以试试你的例子了。

Answer 2

“if”，“true”和“false”不是具有含义的语言关键词，它们只是（元语言）函数的名称。 类似地，“cond”，“then”和“else”是函数参数;这些话并不意味着什么。

我认为如果你使用无意义的标识符，这实际上更容易理解（这纯粹是一个符号操作练习）。

定义无意义的

a = (λx.(λy.x))
b = (λx.(λy.y))
c = (λx.(λy.(λz.x y z)))

并评估

   c b b a
—> (λx.(λy.(λz.x y z))) b b a
—> (λy.(λz.b y z)) b a
—> (λz.b b z) a
—> b b a
—> (λx.(λy.y)) b a
—> ...

你最终会得到(λx.(λy.x))，这是“a”（“true”）的定义。

Answer 3

另一种方法：

   if false false true
   {substituting name for definition}
-> (λcond.(λthen.(λelse.cond then else))) false false true
   {beta reduction}
-> (λthen.(λelse.false then else)) false true
   {beta reduction}
-> (λelse.false false else) true
   {beta reduction}
-> false false true
   {substituting name for definition}
-> (λx.(λy.y)) false true
   {beta reduction}
-> (λy.y) true
   {beta reduction}
-> true
   {substituting name for definition}
-> (λx.(λy.x))

您可以使用this page上的交互式解释器自己运行它。但是解释器只支持单字母变量名，因此您必须输入表达式：

(λc.(λt.(λe.c t e))) (λx.(λy.y)) (λx.(λy.y)) (λx.(λy.x))