Computable Secrets

Lab / Lambda calculus

Lambda calculus interpreter

Name your building blocks on the definitions sheet, write a term that composes them, and watch it reduce to normal form — the next redex underlined at every step. Normal order, capture-avoiding, fuel-capped (Ω is welcome to try).

Sign in to save terms by name.

Library

Tested terms to start from — load one, run it, take it apart.

  • Booleans

    Church booleans: true and false are two-way choices, and logic is application.

  • Arithmetic

    Church numerals: two times three, reduced to five... no, six applications of f. Count them.

  • Pairs

    Data from functions alone: a pair is a function awaiting a selector.

  • Omega

    The self-application loop: every step reproduces the term. The fuel budget is the only way out.

Format
name = term               # a definition; usable on later lines
term                      # the remaining lines form the term to reduce

\x. e   or   λx. e       # abstraction (\x y. e sugars \x.\y. e)
f a b                     # application, left-associative
(f a) (\x. x)            # parentheses group

# '#' starts a comment. Reduction is normal order (leftmost-
# outermost, under binders), capture-avoiding, capped at 2,000
# steps and 4,000 printed characters.