MLambda JS

Editor

Syntax

Lambda abstruction

Variable (de Bruijn index)

Parentheses

Examples

λx.x

λf.λx.f x

Encoding other structures

• TRUE := λx.λy.x
• FALSE := λx.λy.y
• AND := λp.λq.p q p
• OR := λp.λq.p p q
• NOT := λp.p FALSE TRUE
• IFTHENELSE := λp.λa.λb.p a b

• PAIR := λx.λy.λf.f x y
• FIRST := λp.p TRUE
• SECOND := λp.p FALSE
• NIL := λx.TRUE
• NULL := λp.p (λx.λy.FALSE)

• Y := λg.(λx.g (x x)) (λx.g (x x))