---
title: lambda calculus
published: 2024-09-26T00:54:15+0100
---

:::::{.notice}
**Lambda calculus** is a turing-complete system for expressing computations using only **[functions]** and **[application]**. Expressions can be one of a few elements:

Syntax              Description   Example
----------------    ------------  --------
VAR                 Variable      `x`
(λVAR.expr)         Function      `λx.x`
(FUNCTION expr)     [Application] `(λx.x)a`

Parentheses can be removed when it doesn't introduce ambiguity.
:::::

### Application
Evaluation is done via substitution.

When the expression `(λx.x)a` is evaluated, all occurences of **x** in the function's body are replaced with **a**. So, `(λx.x)a` evaluates to **a**.

### Functions
<details>
<summary>The most basic function is the **identity function**, `λx.x`.</summary>
<p>The function `λx.x` binds the variable "x" in the definition `λx` to the body `.x`. You can think of it like the function `f(x) = x`.</p>
</details>