Lambda calculus
- File size
- 5.8KB
- Lines of code
- 149
Lambda calculus
Abstract notation to describe functions and application, providing the basis for functional programming.
Introduction
- written as $\lambda$-calculus
- created by Alonzo Church
- can represent any turing machine
- by definition the world's smallest programming language
Quickstart
Datatypes
$\lambda$-calculus has 3 foundational datatypes.
1. Variable
* <name>
2. Function
* $\lambda$ <parameter>.<body>
* function parameter and body are . period-delimited
* functions are single parameter
3. Application
* <function><variable OR function>
In practice, it looks like this.
| Example | Explanation |
|---|---|
| $x$ | $x$ is a variable |
| $\lambda x . x$ | function definition for a function with parameter $x$ and body $x$ |
| $(\lambda x . x)a$ | function call for the previously declared function $\lambda x . x$ with the argument $a$ |
Free and Bound variables
- Free variable: variable that is never declared prior to its specification in a function body
- Bound variable: variable that is declared within both the function parameter and body
In practice, they look like this.
| Example | Explanation |
|---|---|
| $\lambda x . x$ | $x$ is a bound variable |
| $\lambda x . y$ | $y$ is a free variable |
Evaluation
- application evaluation is performed via $\beta$-reduction
- $\beta$-reduction: lexically-scoped substitution, a concept most of us are familiar with from foundational mathematical functions
- allows for higher-order functions, where functions themselves are provided as arguments to another function
In practice, it looks like this.
example 1
* $(\lambda x . x)a$ evaluates to $a$
example 2
* $(\lambda x . y)a$ evaluates to $y$
example 3
* $(\lambda x . (\lambda y . x ))a$ evaluates to $\lambda y . a$
* this is an example of a higher-order function evaluated using $\beta$-reduction