Collected Lambda Calculus Functions

The following is a small collection of functions in the untyped lambda calculus which I feel are noteworthy for one reason or another, either by relevance to the foundations of lambda calculus (such as the combinators and natural numbers) or by utility to people who wish to actively make use of this Turing tarpit. Some of them are taken from Wikipedia (which tends to be very reliable on mathematical issues), while others (primarily the list functions) I derived myself.

Unless explicitly noted otherwise, natural numbers, booleans, pairs & lists, and all functions for dealing with them use the Church encodings of their values. Operations on other types (e.g., negative or non-integral numbers) are not defined, and if the reader desires them, he must construct such types and the operations on them himself (possibly with the use of pairs acting as typed unions). Additionally, functions for operating on numbers, lists, etc. are only meant for use on those types; if a value of the wrong type is supplied (e.g., if a list is passed to SUCC) or a non-Church encoded value is used, the results are undefined.

Common Combinators

Natural Numbers

Mathematical Operators


Given a boolean value b, the expression b t f will evaluate to t if b is true and to f if b is false. This allows conditional expressions to be written simply as a condition applied directly to the two possible results without the need for an IF function.

Numeric Comparison Operators

Pairs and Lists

Pairs and lists are structured the same way that they are in Lisp and its relatives: a pair is made up of two components, called the car and the cdr, and a list is either NIL (the empty list) or a pair whose cdr is another list (and whose car is an element of the enclosing list).

List Functions