CODEWITHSUNDEEP
lambdacomputer-sciencelambda-calculus
Alan Chan
Alan Chan

Reputation: 3

How do you reduce this lambda calculus expression?

How do you reduce this lambda calculus expression? I am trying to reduce NOT FALSE to TRUE with lambda calculus with the given definitions:

NOT = (λb.λx.λy.b y x)
FALSE = (λx.λy.y)
TRUE = (λx.λy.x)

Upvotes: 0

Views: 263

Answers (2)

Mulan
Mulan

Reputation: 135357

Given -

NOT = (λb.λx.λy.b y x)
FALSE = (λx.λy.y)
TRUE = (λx.λy.x)

Evaluate -

NOT FALSE
---
 \
(λb.λx.λy.b y x) FALSE      β [b := FALSE]
 --       -      -----
          _______/
         /
(λx.λy.FALSE y x)

Already we can see that NOT simply reverses the arguments to FALSE, which is effectively the same thing as TRUE. By reducing inside the lambda, we can prove they evaluate to the same result -

(λx.λy.FALSE y x) 
       -----
         \
(λx.λy.(λx.λy.y) y x)       β [x := y]
        --       -
         
(λx.λy.(λy.y) x)            β [y := x]
        __    _
         ____/
        /
(λx.λy.x)                   = TRUE

Upvotes: 0

alias
alias

Reputation: 30460

  NOT FALSE
= { expand definitions }
  (λb.λx.λy.b y x) (λx.λy.y)
= { beta-reduce, alpha-rename to avoid capture }
  λx.λy.(λa.λb.b) y x 
= { beta-reduce inside lambda, twice }
  λx.λy.x
= { definition of TRUE }
  TRUE

Upvotes: 0

Related Questions