A circuit-like notation for lambda calculus | Hacker News
Lately, I’ve been playing around with inventing a visual writing system for lambda calculus.
Lambda calculus (λ-calculus) is a sort of proto-functional-programming, originally invented by Alonzo Church while he was trying to solve the same problem that led Turing to invent Turing machines. It’s another way of reasoning about computation.
Python’s lambda is an idea that was borrowed from λ-calculus. In Python, you can use a lambda expression like the following in order to define a function that returns the square of a number:
square = lambda x: x * x
In λ-calculus, the idea is the same: we create a function by using λ to specify which arguments a function takes in, then we give an expression for the function’s return value. Pure lambda calculus doesn’t include operators of any sort – just functions being applied to other functions – so if we try to write a square function, we have to suppose that multiply is a function of two variables that has already been defined:
square = λx. multiply x x
The square function, once defined, can be applied to arguments and evaluated into something simpler.
square 4 = (λx. multiply x x) 4
= multiply 4 4
= 16
One of the cool things about lambda calculus is that we can represent most common programming abstractions using λ-calculus, even though it’s nothing but functions: numbers, arithmetic, booleans, lists, if statements, loops, recursion… the list goes on. Before I introduce the visual writing system I’ve been using, let’s take a detour and discuss how we can represent numbers and arithmetic using lambda calculus.
Alonzo Church figured out how to represent numbers as lambda functions; these numbers are referred to as Church numerals.
We can represent any nonnegative integer as long as we have two things: (1) a value for zero, and (2) a successor function, which returns n + 1 for any number n. To represent numbers as functions, then, we require that z (zero) and s (successor) be passed in as arguments, and go from there. Each number is actually secretly a function of those two inputs.
zero = λs. λz. z
one = λs. λz. s z
two = λs. λz. s (s z)
three = λs. λz. s (s (s z))
The actual details of how to implement zero and successor should be implemented as are left as someone else’s problem — we can survive without them. All we care about is that our numbers do the right thing, given whatever zero and successor someone may provide.
What about addition? Addition is a function that takes in two numbers (let’s call them x and y), and produces a number representing their sum. To sum them together, we’ll want to produce a number that applies s, the successor function, a total of x + y times. For example, we could first apply it y times to the zero, then apply it x more times to that result.
plus = λx. λy. (λs. λz. x s (y s z))
Let’s try proving that one plus one equals two. In λ-calculus, this proof looks like the following: