Building Stuff with Lambda Calculus

Common kestrel and black-shouldered kite.

The Kestrel and the Kite. Photos by Jakub Hałun and Charles J. Sharp.

One of us always lies, and one of us always tells the truth.

— The Kestrel

A lambda is just a different way of writing a function. Like normal functions, it takes argument(s) and returns something. The expression λa.a reads as “takes a single argument a, and returns argument a”. This is the simplest lambda and it is the equivalent of $f(x) = x$ . It can take expression x as an argument from the right like so,

λa.a x => x.

This reads as “a function—which takes a and returns a—takes x and returns x”. That little => just means “becomes” or “can be reduced to”.

You can express all sorts of concepts in math and programming using just lambdas. Lets pick the coolest ones and build them from first principles.

A Flock of Functions #

Below are your standard named lambdas.

I = λa.a — Idiot: identity.

M = λa.aa — Mockingbird: omega.

K = λab.a — Kestrel: true, constant.

KI = λab.b — Kite: false, zero.

T = λab.ba — Thrush: not, switch.

W = λab.abb — Warbler: ?

C = λabc.acb — Cardinal: not.

B = λabc.a(bc) — Bluebird: compose, multiply.

V = λabc.cab — Vireo: pair, cons.

S = λabc.ac(bc) — Starling: ?

The Kite for example takes two arguments and returns the first one. It can take expressions x and y like so,

λab.a x y => λb.x y => x.

Note that arguments can be fed into functions one at a time. This one reduces in two steps.

Booleans (Church-encoded) #

We can express boolean logic just with lambdas. Recall the pattern

if boolean then x else y

In the context of an if statement, the essence of a boolean is a function that selects between two arguments. Well, that’s what we have in the Kestrel and the Kite.

TRUE = K = λab.a — Picks the first of two inputs.

FALSE = KI = λab.b — Picks the second of two inputs.

Take the expression BOOL x y. If BOOL = TRUE, then this reduces to x. If BOOL = FALSE, then this reduces to y. This is what an if statement does.

We can also do boolean logic.

NOT = C = λabc.acb — Swaps the second and thirds inputs. i.e.

NOT TRUE = FALSE

See if you can understand why this is true. We also have OR and AND.

OR = λpq.pKq

AND = λpq.pqKI

Natural Numbers (Church-encoded) #

ZERO = KI — Applies a function zero times. e.g.

ZERO f x = x

SUCC = SB = λnfx.f(nfx) — Successor: increases the value by one. e.g.

SUCC ZERO = 1
SUCC 1 = 2

SUCC = SB
     = (λabc.ac(bc)) B
     = λbc.(λxyz.x(yz)) c(bc)
     = λbc.λz.c((bc)z)
     = λbcz.c(bcz)
     = λnfx.f(nfx)
     = λnf.λx.f((nf)x)
     = λnf.(λabx.a(bx)) f(nf)
     = λcnf.cf(nf) (λabx.a(bx))
     = λnfx.Bf(nf)x

ADD = λab.a(SUCC)b — Successor of b, a times.

EXP = T — Swaps inputs. e.g.

EXP 3 2 = 2 3

“Twice thrice” = 9.

MUL = B — Compose arguments in a nested fashion.

MUL 3 2 = λc.3(2 c) = λc.6 c = 6

Pairs #

PAIR = V — Stores two values. (1, 2) represented by PAIR 1 2

FST = λp.pK — Gives the first element of pair.

FST (PAIR 1 2) = 1

SND = λp.pKI — Gives the second element of pair.

SND (PAIR 1 2) = 2

SET_FST = λcp.V c (SND p) — Pair with value c as the first element of pair p

SET_SND = λcp.V (FST p) c — Pair with value c as the second element of pair p

Φ = λp.V (SND p) (SUCC (SND p)) — Increment second element, store old value as first element

More Numerals #

ISZERO = λn.n(K(KI))K — is a Church numeral zero?

PRED = λn.FST (n Φ V((KI)(KI))) — Predecessor

SUB = λab.a PRED b — Subtract

LEQ = λab.ISZERO(SUB a b) — Less than or equal to

EQ = λab.AND(LEQ a b)(LEQ b a) — Equal to

Lists (cons-cell) #

NIL = KI — nil, empty list []

CONS = V — cons

ISNIL = λl.l(K(KI))K — is list empty?

HEAD = FST — head

TAIL = SND — tail

ELT = λnp.HEAD (n TAIL p) — returns the nth element

Lists (Church-encoded) #

NIL = λcn.n = KI

CONS = λhtcn.ch(tcn)

FOLD = λfzl.lfz = V — right fold (inherent to CE lists)

MAP = λfl.(l (λht.CONS(fh)t) NIL)

FILTER = λpl. l (λht. p h (CONS h t) t) NIL

REVERSE = TBD

SUM = FOLD ADD 0

PRODUCT = FOLD MUL 0

LENGTH = FOLD (λht.SUCC t) 0

Folding is part of the structure of these lists. List [1, 2, 3] can be represented by

CONS 1 (CONS 2 (CONS 3 NIL)) = λcn.c 1 (c 2 (c 3 n))

To sum a list you therefore do

(λcn.c 1 (c 2 (c 3 n))) ADD 0

Example #

CONS 3 NIL = λhtcn.ch(tcn) 3 NIL
           = λtcn.c3(tcn) NIL
           = λcn.c 3(NIL cn)
           = λcn.c 3 n

CONS 4 (CONS 3 NIL) = λhtcn.ch(tcn) 4 (λcn.c 3 n)
                    = (λtcn.c 4 (tcn)) (λcn.c 3 n)
                    = λcn.c 4 ((λcn.c 3 n) c n)
                    = λcn.c 4 (c 3 n)

FOLD ADD 0 (CONS 4 (CONS 3 NIL)) = (λfzl.lfz) ADD 0 (λcn.c 4 (c 3 n))
    = (λcn.c 4 (c 3 n)) ADD 0
    = (λn. ADD 4 (ADD 3 n)) 0
    = ADD 4 (ADD 3 0)
    = ADD 4 3
    = 7

Option Monad #

NONE = λsn.n = KI

SOME = λxsn.sx

ISSOME = λo.o(KK)KI

FROMMAYBE = λdo.oId

maybe1 = NONE

maybe2 = SOME 5
       = (λxsn.sx) 5
       = λsn.(s 5)

ISSOME NONE = KI

ISSOME (SOME val) = (λo.o(KK)KI) λsn.(s val)
                  = λsn.(s val)(KK)KI
                  = KK val
                  = (λab.a)K val
                  = K

Recursion #

Y = λf.(λx.f(xx))(λx.f(xx))