lamcalc

A pure lambda calculus interpreter written in Rust.

Features

• lam syntax — write lam x. x instead of λx.x
• Normal-order reduction — always finds a normal form if one exists
• Capture-avoiding substitution — correct alpha-renaming to prevent variable capture
• Integer literals — 0, 1, 42 etc. desugar to Church numerals at parse time
• Built-in Church encoding macros — TRUE, FALSE, ADD, MULT, Y, and 25+ more
• Interactive REPL with readline support (arrow keys, history)
• File runner for .lam source files
• Trace mode — see every beta reduction step

Usage

# Interactive REPL
lamcalc

# Evaluate a file
lamcalc examples/factorial.lam

# Evaluate inline expression
lamcalc -e "ADD 2 3"

# Show every reduction step
lamcalc --trace -e "(lam x. x) (lam y. y)"

# Set step limit (default: 100000)
lamcalc --steps 500000 examples/factorial.lam

Syntax

-- Abstraction (use lam, not λ)
lam x. body

-- Multi-parameter shorthand
lam x y z. body    -- same as: lam x. lam y. lam z. body

-- Application (left-associative)
f x y              -- same as: (f x) y

-- Integer literals (Church numerals)
0  1  2  42        -- desugar to Church numerals

-- Let bindings (in .lam files)
let name = expr
body_using_name

-- Comments
-- this is a comment
# this is also a comment

Built-in Keywords

Booleans

Keyword	Encoding
TRUE	lam x y. x
FALSE	lam x y. y
NOT	lam b. b FALSE TRUE
AND	lam b c. b c FALSE
OR	lam b c. b TRUE c
IF	lam b t f. b t f

Church Numerals

Integer literals (0, 1, 2, ...) desugar to Church numerals at parse time.

Keyword	Description
SUCC	Successor
PRED	Predecessor
ADD	Addition
MULT	Multiplication
EXP	Exponentiation
SUB	Subtraction (saturating)
MOD	Modulo (via Y)

Predicates

Keyword	Description
ZERO	Zero-test: ZERO 0 = TRUE, ZERO n = FALSE for n > 0
EQ	Numeric equality
LT	Less than
LEQ	Less than or equal

Combinators

Keyword	Description
Y	Y combinator (fixed point)
I	Identity: lam x. x
K	Constant: lam x y. x
S	lam x y z. x z (y z)
B	Composition: lam f g x. f (g x)
C	Flip: lam f x y. f y x
W	lam f x. f x x
OMEGA	Diverging term

Pairs & Lists

Keyword	Description
PAIR	Constructor
FST	First element
SND	Second element
NIL	Empty list
CONS	List cons
HEAD	List head
TAIL	List tail
ISNIL	Nil check

REPL Commands

Command	Description
:let name = expr	Bind a name in the session
:trace	Toggle trace mode on/off
:steps N	Set reduction step limit
:env	List session bindings
:clear	Clear session bindings
:help	Show help
:quit / :q	Exit

Examples

λ> ADD 2 3
lam f x. f (f (f (f (f x))))
  ↳ Church numeral: 5

λ> ZERO 0
lam a b. a
  ↳ TRUE

λ> :let fact = Y (lam f n. IF (ZERO n) 1 (MULT n (f (PRED n))))
λ> fact 4
lam f x. f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x))))))))))))))))))))))))
  ↳ Church numeral: 24

λ> :trace
Trace mode: ON
λ> (lam x. x) (lam y. y)
  (lam x. x) (lam y. y)
→ lam y. y
── 1 step
lam y. y

Building

cargo build --release
# Binary at: target/release/lamcalc