Оценка лямбда-исчисления: если false false false true

Question

Лямбда-исчисление имеет следующие выражения:

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

«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 2

Другой подход:

   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))

Answer 3

Определение

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

Здесь больше нет определений, которые можно применить, поэтомуу нас есть наш результат.

Теперь вы можете попробовать разработать свой пример.