Lambda Calculus

Keywords

ver. 1.0.0

Introduction and development of functional programming from its theoretical roots through lambda-calculus syntax, encodings, and recursion via the Y combinator

This collection introduces functional programming and its theoretical foundations in mathematical logic and the lambda calculus, presents the formal syntax and reduction rules of the untyped lambda calculus, and shows how to encode conditionals, booleans, and natural numbers (Church-style). It concludes by explaining recursion in lambda calculus and constructing recursive arithmetic using the Y (fixed-point) combinator.

This node gathers the opening chapters of a functional programming text that move from high-level motivations and history into the formal machinery used to express computation without mutable state.

  • Historical and conceptual introduction
    • Contrasts the functional and imperative paradigms (name–value associations, lack of ordered side-effectful execution, repetition via recursion, immutable data).
    • Traces theoretical origins in mathematical logic and computability (Turing, Kleene, Church) and situates lambda calculus and denotational semantics as the foundations for functional languages.
  • Lambda calculus foundations
    • Defines abstraction, application, and variables with precise syntax.
    • Explains binding, scope, free vs. bound variables, and the core reduction conversions: α-conversion (renaming), β-reduction (application/substitution), and η-reduction (extensionality).
    • Discusses evaluation strategies (normal order vs. applicative order) and basic combinators (identity, self-application, pairing and projection patterns).
  • Encodings of higher-level constructs in the untyped lambda calculus
    • Shows how to represent booleans and conditional branching (true, false, cond/if-then-else) and build logical operations (not, and, or) purely as lambda terms.
    • Constructs natural numbers using Church-style and pair-based encodings, defines zero, successor, predicates (iszero), predecessor, and introduces syntactic conveniences such as currying and clearer if-then-else notation.
  • Recursion and arithmetic via fixed-point combinators
    • Explains why direct recursive definitions lead to infinite substitution and how self-application patterns and fixed-point (Y) combinators provide recursion in a language without named mutable bindings.
    • Uses the Y combinator to define recursive arithmetic and comparison routines: addition, multiplication, power, natural subtraction, equality, inequalities, and division.

Together these chapters show how the pure lambda calculus, guided by precise syntax and reduction rules, suffices to represent conditionals, data, and arbitrarily powerful recursive computations—forming the theoretical backbone for functional programming languages and techniques.

Units

Introduction 3/4

An introduction to functional programming principles, its historical theoretical roots in mathematical logic and lambda calculus, and its contrasts with imperative programming.

Elements of Lambda Calculus 3/4

Chapter 2 introduces the fundamental concepts, syntax, and reduction rules of the lambda calculus as a foundation for functional programming.

Conditions, Booleans and Integers 3/4

This chapter introduces untyped lambda calculus encodings for conditional expressions, boolean logic operations, natural numbers, and syntactic conveniences.

Recursion and Arithmetic 3/4

This chapter explores how recursion is formulated in the lambda calculus and functional programming, introducing the Y combinator to construct recursive arithmetic operations.