Elements of Lambda Calculus

Keywords

ver. 1.0.0

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

This text introduces the lambda ($\lambda$) calculus as the theoretical foundation for functional programming. It covers the concept of abstraction, formal syntax (names, functions, and applications), evaluation strategies (normal order and applicative order), fundamental functions (identity, self-application, function application, and pair constructors), variable binding rules (free vs. bound variables, scope), and reduction conversions ($\beta$-reduction, $\alpha$-conversion, and $\eta$-reduction).

Full summary

Overview of Lambda Calculus

Following a brief summary comparing imperative and functional programming paradigms, Chapter 2 introduces the $\lambda$ calculus, originally developed by Alonzo Church in the 1930s as a foundational model of computability and a formal framework for functional programming languages.

Core Concepts and Syntax

Abstraction and Specialisation: Abstraction generalizes expressions by introducing names in place of concrete values/operations, while specialisation replaces those names with concrete arguments.
BNF Syntax:
- <expression> ::= <name> | <function> | <application>
- <function> ::= λ<name>.<body>
- <application> ::= (<function expression> <argument expression>)
Evaluation Orders:
- Applicative Order: Evaluates argument expressions prior to substitution (similar to call-by-value).
- Normal Order: Passes unevaluated argument expressions directly into the function body (similar to call-by-name).

Basic Functions and Combinators

The text constructs several fundamental functions: - Identity Function: def identity = λx.x - Self-Application Function: def self_apply = λs.(s s) (which can lead to non-terminating evaluations when applied to itself) - Function Application: def apply = λfunc.λarg.(func arg) - Argument Selection and Pairing: - def select_first = λfirst.λsecond.first - def select_second = λfirst.λsecond.second - def make_pair = λfirst.λsecond.λfunc.((func first) second)

Formal Mechanics and Reductions

Scope, Free, and Bound Variables: Formal definitions establish when variable names are bound to an enclosing $\lambda$ abstraction versus when they remain free.
$\beta$-Reduction: The process of replacing all free occurrences of a function’s bound variable in its body with the provided argument expression.
$\alpha$-Conversion: Consistent renaming of bound variables to prevent variable capture and name clashes during substitution.
$\eta$-Reduction: Simplification of expressions of the form λ<name>.(<expression> <name>) directly to <expression>.

The chapter concludes with a concise reference summary and a series of review exercises covering expression structure analysis, step-by-step reduction, function equivalence proofs, and higher-order tuple construction.

Materials

Lecture notesThe unit written out, to read at your own paceOpen → SlidesThe deck to present fromOpen →

Source document

An Introduction To Functional Programming Through Lambda Calculus, Greg Michaelson, Dover Publications, 1989, 2011 — Page 12-38

← Introduction Conditions, Booleans and Integers →

--- title: "Elements of Lambda Calculus" keywords: - ver. 1.0.0 format: html: toc: false --- **Chapter 2 introduces the fundamental concepts, syntax, and reduction rules of the lambda calculus as a foundation for functional programming.** > This text introduces the lambda ($\lambda$) calculus as the theoretical foundation for functional programming. It covers the concept of abstraction, formal syntax (names, functions, and applications), evaluation strategies (normal order and applicative order), fundamental functions (identity, self-application, function application, and pair constructors), variable binding rules (free vs. bound variables, scope), and reduction conversions ($\beta$-reduction, $\alpha$-conversion, and $\eta$-reduction). ::: {.callout-note collapse="true" title="Full summary"} ### Overview of Lambda Calculus Following a brief summary comparing imperative and functional programming paradigms, Chapter 2 introduces the **$\lambda$ calculus**, originally developed by Alonzo Church in the 1930s as a foundational model of computability and a formal framework for functional programming languages. ### Core Concepts and Syntax - **Abstraction and Specialisation**: Abstraction generalizes expressions by introducing names in place of concrete values/operations, while specialisation replaces those names with concrete arguments. - **BNF Syntax**: - `<expression> ::= <name> | <function> | <application>` - `<function> ::= λ<name>.<body>` - `<application> ::= (<function expression> <argument expression>)` - **Evaluation Orders**: - **Applicative Order**: Evaluates argument expressions prior to substitution (similar to call-by-value). - **Normal Order**: Passes unevaluated argument expressions directly into the function body (similar to call-by-name). ### Basic Functions and Combinators The text constructs several fundamental functions: - **Identity Function**: `def identity = λx.x` - **Self-Application Function**: `def self_apply = λs.(s s)` (which can lead to non-terminating evaluations when applied to itself) - **Function Application**: `def apply = λfunc.λarg.(func arg)` - **Argument Selection and Pairing**: - `def select_first = λfirst.λsecond.first` - `def select_second = λfirst.λsecond.second` - `def make_pair = λfirst.λsecond.λfunc.((func first) second)` ### Formal Mechanics and Reductions - **Scope, Free, and Bound Variables**: Formal definitions establish when variable names are bound to an enclosing $\lambda$ abstraction versus when they remain free. - **$\beta$-Reduction**: The process of replacing all free occurrences of a function's bound variable in its body with the provided argument expression. - **$\alpha$-Conversion**: Consistent renaming of bound variables to prevent variable capture and name clashes during substitution. - **$\eta$-Reduction**: Simplification of expressions of the form `λ<name>.(<expression> <name>)` directly to `<expression>`. The chapter concludes with a concise reference summary and a series of review exercises covering expression structure analysis, step-by-step reduction, function equivalence proofs, and higher-order tuple construction. ::: ## Materials ::: {.hg-deck} <a class="hg-card" href="notes.qmd">Lecture notesThe unit written out, to read at your own paceOpen →</a> <a class="hg-card" href="slides.qmd">SlidesThe deck to present fromOpen →</a> ::: ## Source document - An Introduction To Functional Programming Through Lambda Calculus, _Greg Michaelson_, Dover Publications, 1989, 2011 — Page 12-38 ::: {.hg-nav} [← Introduction](../1_introduction/index.qmd){.hg-prev} [Conditions, Booleans and Integers →](../3_conditions_booleans_and_integers/index.qmd){.hg-next} :::