评估 lambda 演算：if false false true

Question

The lambda calculus has the following expressions:
e ::=           Expressions
      x         Variables
      (λx.e)    Functions
      e e       Function application
From this base, we can define a number of additional constructs, such as Booleans and conditional statements:
let true = (λx.(λy.x))
false = (λx.(λy.y))
if = (λcond.(λthen.(λelse.cond then else)))
Showing your work, show the evaluation of the following program: 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))

您可以运行自己使用上的交互式解释器第页。但解释器只支持一个字母的变量名，所以你必须输入表达式：

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

评估 lambda 演算：if false false true

Evaluating lambda calculus: if false false true

lambda

scheme

lambda-calculus

semantics