SKILL

Learn Typed Lambda Calculus

What you will be able to do

• Given a lambda expression, identify its parts (variables, abstractions, applications) and perform beta-reduction step by step.
• Given a typing context and a lambda term, derive the term’s type using the typing rules (variable, abstraction, application, pairing, projection) or explain why the term is ill-typed.
• Explain why the simply typed lambda calculus prevents self-application and guarantees termination, and why these properties matter for the semiotic universe’s syntactic layer.
• State the Curry-Howard correspondence: types are propositions, terms are proofs, beta-reduction is proof normalization. Given a type, identify the corresponding logical proposition, and vice versa.

Prerequisites

None. This skill is a starting point in the curriculum dependency graph.

The typed lambda calculus lesson uses formal notation (inference rules, Greek letters, subscripts). A reader comfortable with the idea that symbols can be defined and manipulated according to rules will be fine. No prior knowledge of logic, type theory, or programming is assumed — though readers who have programmed in a language with first-class functions (Scheme, JavaScript, Python) will find the intuitions familiar.

Lessons

1. [Gap: no concrete-first lambda calculus lesson exists yet. The vault contains emsenn’s Anatomy of Things babble, which builds lambda calculus intuitions from Scheme code — starting with literal values, progressing through nested functions to closures, adding one concept per step. A proper lesson following this approach (concrete examples first, formal notation second) would be the ideal entry point. Until that lesson is written, readers with programming experience can read the babble for intuition before proceeding to the formal lesson below.]

2. Typed Lambda Calculus — the core lesson: untyped lambda calculus, adding types (base types, function types, product types), typing rules, structural properties, the Curry-Howard correspondence, worked examples.

After completing this skill, the relational lambda calculus concept note shows how the same formal system arises from the relationality derivation rather than being stipulated. This is optional but connects the mathematics to emsenn’s philosophical project.

Scope

This skill covers the simply typed lambda calculus (STLC) with base types, function types, and product types. It does not cover:

• Polymorphism (System F, dependent types) — a significant extension where types themselves can be abstracted over. Important for Lean and Agda but not required for the semiotic universe specification.
• Recursive types or general recursion — the simply typed calculus has no fixed-point combinator and guarantees termination. The relational lambda calculus adds a fix operator; that extension is covered in the relationality derivation, not here.
• Category-theoretic semantics (cartesian closed categories) — the typed lambda calculus is the internal language of a cartesian closed category, but this skill does not develop that connection.
• Implementation — how to build a type checker or evaluator. The anatomy-of-things babble touches on implementation in Scheme, but this skill focuses on the formal system, not on writing code.
• The semiotic universe’s use of typed lambda calculus — that is covered by learn-semiotic-universe, which lists this skill as a prerequisite. This skill provides the lambda calculus; that skill uses it.

Verification

After completing the typed lambda calculus lesson:

1. Write the type of the composition function: given $f:A\to B$ and $g:B\to C$, what is the type of $\lambda x.g(fx)$? Derive it step by step using the typing rules.
2. Explain why $\lambda x.xx$ cannot be typed in the simply typed lambda calculus. What equation would its type have to satisfy?
3. State what logical proposition corresponds to the type $A\to (B\to A)$, and write a term that inhabits it.