Library of λ

Fundamental functions #

• 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: ?

Booleans (Church-encoded) #

• TRUE = K = λab.a — Picks the first of two inputs.
• FALSE = KI = λab.b — Picks the second of two inputs.
• NOT = C = λabc.acb — Swaps the second and thirds inputs. i.e.
• OR = λpq.pKq
• AND = λpq.pqKI

Natural numbers (Church-encoded) #

• ZERO = KI — Applies a function zero times. e.g.
• SUCC = SB = λnfx.f(nfx) — Successor: increases the value by one.
• ADD = λab.a(SUCC)b — Successor of b, a times.
• EXP = T — Swaps inputs. e.g.
• MUL = B — Compose arguments in a nested fashion.

Pairs #

• PAIR = V — Stores two values. (1, 2) represented by PAIR 1 2
• FST = λp.pK — Gives the first element of pair.
• SND = λp.pKI — Gives the second element of pair.
• 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

Option monad #

• NONE = λsn.n = KI
• SOME = λxsn.sx
• ISSOME = λo.o(KK)KI
• FROMMAYBE = λdo.oId

Recursion #

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