Lambda Learner

An iPad app that teaches lambda calculus from zero and lets you watch a computation happen one step at a time. It has four chapters of lessons, a playground that shows all of its work, and a lambda calculus interpreter written in pure Swift underneath.

I built this for the WWDC25 Swift Student Challenge, and it was picked as one of the winners.

Lambda calculus in plain terms

Lambda calculus is a tiny programming language from the 1930s. It has three ideas and nothing else:

1. Variables. Names like x, y, f.
2. Functions. λx. x means "a function that takes x and hands it right back". The λ just marks where a function begins.
3. Calling a function. (λx. x) y means "call that function with y". The answer is y.

That's the whole language. There are no numbers, no true or false, no if statements. You build every one of those out of functions, and that's exactly what the chapters walk you through. Every functional language today, Swift closures included, traces back here.

Screenshots

What's in the app

Pick a chapter from the sidebar. Each one opens with two tabs: Learn and Playground.

Learn

Four chapters, meant to be read in order.

Chapter	What you'll get out of it
1. Introduction to Lambda Calculus	Where it came from (Church, Turing, and why their ideas turned out to be the same), the three building blocks, and the notation rules that make expressions readable.
2. The Inner Workings	Variables, scope, why λx. x and λy. y are the same function, and how substitution actually works.
3. Beta Reduction	How an expression gets evaluated, the difference between normal order and call-by-value, what a "normal form" is, and why some expressions never finish.
4. Encoding Power	Building true and false, logic gates, pairs, and numbers out of nothing but functions. Ends with practice exercises and a set of challenge problems with hints and solutions.

Lessons are full of green Try in Interpreter buttons. Tap one and the expression lands in the interpreter, ready to run. Chapters 1 and 4 also have a Show REPL toggle that slides the interpreter in as a side panel, so you can read and experiment without switching tabs.

Playground

The interpreter on its own. Type an expression, hit Evaluate, and read the trace.

• Verbosity picks how much you see. None shows the parsed input and the answer. Low adds every reduction step. High adds a short English line explaining each rename and substitution.
• Rename Free Variables gives fresh names (like X`0) to any variable you never bound, so a stray y in your input can't be mistaken for a bound one in the output.
• Help opens a guide of tappable examples covering syntax, booleans, and numerals. The play button next to each one drops it straight into the input box.

Reading the output

Every line in the trace starts with a symbol that tells you what kind of step it is.

Prefix	Meaning
λ >	Your input, as the parser understood it (fully parenthesised).
δ >	A built-in name like true or plus was swapped for its definition.
Δ >	The whole expression after all the built-in names have been swapped.
α >	Two variables shared a name and would have clashed, so one got renamed.
β >	A function was called: its argument got substituted into its body. This is the actual computation.
ε >	A free variable was renamed (only when the toggle is on).
>>>	The final answer. Nothing left to reduce.
↳ equivalent to:	The answer has the same shape as a built-in term, so the app tells you which one.

Here's a real trace. pair a b bundles two values together and first pulls the first one back out. At Low verbosity, first (pair a b) prints:

λ > (first ((pair a) b))
    δ > expanded 'first' into '(λp. (p true))'
    δ > expanded 'true' into '(λt. (λf. t))'
    δ > expanded 'pair' into '(λx. (λy. (λf. ((f x) y))))'
Δ > ((λp. (p (λt. (λf. t)))) (((λx. (λy. (λf. ((f x) y)))) a) b))
β > ((λp. (p (λt. (λf. t)))) ((λy. (λf. ((f a) y))) b))
β > ((λp. (p (λt. (λf. t)))) (λf. ((f a) b)))
β > ((λf. ((f a) b)) (λt. (λf. t)))
β > (((λt. (λf. t)) a) b)
β > ((λf. a) b)
β > a
>>> a

Read it top to bottom. The three δ lines unpack the names. The Δ line is the expression with nothing hidden. Each β line is one function call, and the term shrinks every time until only a is left.

The equivalence line is my favourite part. Type λt. λf. t and the app will tell you that's true. Type plus two three and after a long chain of β steps you'll get a term the app recognises as five. It's checking the shape of the result, so variable names don't matter.

Writing expressions

What you want	How to write it	Example
A function	λx. body, \x. body, or lambda x. body	λx. x
Several parameters	λx y. body	λt f. t is short for λt. λf. t
Call a function	put the argument after it, with a space	(λx. x) y
Grouping	parentheses	not (and true false)
A comment	# to end of line	# identity

A few rules the lexer enforces:

• Variable names are lowercase letters and digits only. X or Foo will be rejected with an "Unexpected character" error.
• Function calls group to the left, so f a b means (f a) b.
• The body of a λ extends as far right as it can, so λx. x y means λx. (x y).

Commands

Type these into the same input box.

Command	What it does
env	Lists every name the interpreter knows and its definition.
unbind <name>	Removes a built-in name, in case you want to define the concept yourself in a chapter exercise.
help	A quick reference.

Built-in terms

These names are available from the start. Under the hood each one is just a function, and env will show you the exact text.

Logic

Name	Definition	In words
true	λt. λf. t	takes two things, returns the first
false	λt. λf. f	takes two things, returns the second
if	λp. λa. λb. p a b	if true a b gives a, if false a b gives b
and	λa. λb. a b a
or	λa. λb. a a b
not	λb. b false true

Numbers (Church numerals)

The number n is "a function that applies f to x n times". So two is λf. λx. f (f x).

Name	Definition
zero … five	λf. λx. x through λf. λx. f (f (f (f (f x))))
incr	λn. λf. λy. f (n f y)
plus	λm. λn. m incr n
times	λm. λn. m (plus n) zero
iszero	λn. n (λy. false) true

Pairs and lists

Each of these has a Lisp-style alias too.

Name	Alias	Definition
pair	cons	λx. λy. λf. f x y
first	car	λp. p true
second	cdr	λp. p false
nil	empty	λx. true
null	isempty	λp. p (λx. λy. false)

Trees

Name	Definition
tree	λd. λl. λr. pair d (pair l r)
datum	λt. first t
left	λt. first (second t)
right	λt. second (second t)

Guard rails

Lambda calculus makes it easy to write something that never finishes. The app protects you in two places:

• Before running. The parser refuses expressions that look like the omega combinator (λx. x x applied to itself) and tells you why.
• While running. The reducer gives up after 1000 nested reduction steps and reports which term it was stuck on.

Typos are reported with a line and column number, plus the offending line with a ^ under the problem.

How the interpreter works

The code under LambdaLearner/Interpreter/ is a straight pipeline. Each stage is its own file.

1. Lexer turns your text into tokens: λ, (, names, and so on.
2. Parser turns tokens into a tree of three node types: Abstraction (a function), Application (a call), and Variable.
3. BindingResolver walks the tree and replaces any free variable that matches a built-in name with that name's definition. This is the δ step.
4. Reducer does the real work. For each call it simplifies the function, then the argument, renames anything that would clash (α), substitutes (β), and keeps going, including inside function bodies, until nothing changes.
5. Logger records every step as a LogEntry and publishes them to SwiftUI, which is how the playground gets its colour-coded trace.

At the end the result is hashed by structure (ignoring variable names) and compared against the hashes of every built-in. A match is what produces the ↳ equivalent to: line.

Running it

You'll need Xcode 16 or newer and an iOS 18 simulator or device.

git clone https://github.com/flash1729/Lambda-Learner.git
open Lambda-Learner/LambdaLearner.xcodeproj

Pick an iPad simulator and hit Run. iPhone is supported too, though the split-view layout was designed with an iPad screen in mind.

Using the interpreter in your own project

The interpreter has no dependency on the app's UI. Copy the LambdaLearner/Interpreter/ folder into any Swift project on an Apple platform and use it like this:

import Foundation

let interpreter = Interpreter(options: InterpreterOptions(
    verbosity: .high,
    renameFreeVars: false,
    showEquivalent: true
))

let (result, error) = interpreter.evaluate("plus one two")

if let term = result {
    print(stringify(term))   // (λf. (λx. (f (f (f x)))))
}

// Every step is in interpreter.logger.logEntries.
// Logger is an ObservableObject, so you can drop the entries straight into a SwiftUI List.
for entry in interpreter.logger.logEntries {
    print(entry.formattedMessage)
}

evaluate returns the reduced term and an optional error. The two error types you'll care about are ParseError and RecursionDepthError.

Rough edges

Things I know about and haven't gotten to yet.

• The parser understands name = term bindings, but the playground doesn't route them through, so you can't define new names from the input box yet.
• The omega-combinator check is a simple text match. It can occasionally flag an expression that would have terminated fine.
• Variable names have to be lowercase.

Contributing

Issues and pull requests are welcome. More built-in terms, more chapters, better error messages, performance work, anything that helps someone understand this stuff a bit faster.