diff options
| author | kitty piapiac <kcp@bsd.computer> | 2024-10-03 06:13:41 +0100 |
|---|---|---|
| committer | kitty piapiac <kcp@bsd.computer> | 2024-10-03 06:13:41 +0100 |
| commit | 69a6187804aff44f48fe9047895e8c027ad5bf3f (patch) | |
| tree | 9ca02720f3ed94512b77e490fadf62969842e544 /notes/lambda-calculus.md | |
Diffstat (limited to 'notes/lambda-calculus.md')
| -rw-r--r-- | notes/lambda-calculus.md | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/notes/lambda-calculus.md b/notes/lambda-calculus.md new file mode 100644 index 0000000..98221eb --- /dev/null +++ b/notes/lambda-calculus.md @@ -0,0 +1,29 @@ +--- +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> + + |