lambda calculus

lambda_fun.coffee

assert = require 'assert'

ZERO = (f) -> (x) -> x
ONE  = (f) -> (x) -> f(x)
TWO  = (f) -> (x) -> f(f(x))

toInt = (n) -> n((x) -> x + 1)(0)

assert 0 is toInt(ZERO)
assert 1 is toInt(ONE)
assert 2 is toInt(TWO)

INC = (n) -> (f) -> (x) -> f(n(f)(x))

THREE = INC(TWO)

assert 3 is toInt(THREE)

PLUS = (m) -> (n) -> (f) -> (x) -> m(f)(n(f)(x))

FIVE = PLUS(TWO)(THREE)

assert 5 is toInt(FIVE)

TRUE = (x) -> (y) -> x # Kestrel
FALSE = (x) -> (y) -> y # ZERO

# alternate:
# FALSE = K(I)
# FALSE = TRUE((x) -> x)
#       = ((x) -> (y) -> x)((x) -> x)
#       = (y) -> (x) -> x

toBool = (b) -> b(true)(false)

assert toBool(TRUE)
assert not toBool(FALSE)

IS_ZERO = (n) -> n((x) -> FALSE)(TRUE)

assert     toBool(IS_ZERO(ZERO))
assert not toBool(IS_ZERO(ONE))
assert not toBool(IS_ZERO(FIVE))

IF_THEN_ELSE = (p) -> (a) -> (b) -> p(a)(b)

assert toInt(TWO) is toInt(IF_THEN_ELSE(TRUE)(TWO)(FIVE))

AND = (p) -> (q) -> p(q)(p)

assert     toBool(AND(TRUE)(TRUE))
assert not toBool(AND(TRUE)(FALSE))
assert not toBool(AND(FALSE)(TRUE))
assert not toBool(AND(FALSE)(FALSE))

OR = (p) -> (q) -> p(p)(q)

assert     toBool(OR(TRUE)(TRUE))
assert     toBool(OR(TRUE)(FALSE))
assert     toBool(OR(FALSE)(TRUE))
assert not toBool(OR(FALSE)(FALSE))

CONS = (x) -> (y) -> (f) -> f(x)(y)
NIL = (f) -> TRUE
CAR = (l) -> l(TRUE)
CDR = (l) -> l(FALSE)

assert 1 is toInt(CAR(CONS(ONE)(TWO)))
assert 2 is toInt(CDR(CONS(ONE)(TWO)))

MY_LIST = CONS(ONE)(CONS(TWO)(CONS(THREE)(NIL)))
assert 3 is toInt(CAR(CDR(CDR(MY_LIST))))

IS_NIL = (l) -> l((x) -> (y) -> FALSE)

assert not toBool(IS_NIL(MY_LIST))
assert not toBool(IS_NIL(CDR(MY_LIST)))
assert not toBool(IS_NIL(CDR(CDR(MY_LIST))))
assert     toBool(IS_NIL(CDR(CDR(CDR(MY_LIST)))))

Y = (f) -> ((g) -> (n) -> f(g(g))(n))(
            (g) -> (n) -> f(g(g))(n))

LENGTH = Y((r) -> (l) -> IF_THEN_ELSE(IS_NIL(l))(ZERO)((f) -> (x) -> (INC(r(CDR(l))))(f)(x)))

assert 3 is toInt(LENGTH(MY_LIST))
assert 2 is toInt(LENGTH(CDR(MY_LIST)))
assert 1 is toInt(LENGTH(CDR(CDR(MY_LIST))))
assert 0 is toInt(LENGTH(CDR(CDR(CDR(MY_LIST)))))

DEC = (n) -> CAR(n((x) -> CONS(CDR(x))(INC(CDR(x))))(CONS(ZERO)(ZERO)))

assert 2 is toInt(DEC(THREE))
assert 1 is toInt(DEC(DEC(THREE)))
assert 0 is toInt(DEC(DEC(DEC(THREE))))
assert 0 is toInt(DEC(DEC(DEC(DEC(THREE)))))