diff options
Diffstat (limited to 'lambda-calcul/support/newcrafts-2025.md')
| -rw-r--r-- | lambda-calcul/support/newcrafts-2025.md | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/lambda-calcul/support/newcrafts-2025.md b/lambda-calcul/support/newcrafts-2025.md index 713e3e5..3506d52 100644 --- a/lambda-calcul/support/newcrafts-2025.md +++ b/lambda-calcul/support/newcrafts-2025.md @@ -13,7 +13,7 @@ author: --- - + ## λ-Calculus Syntax @@ -27,8 +27,12 @@ A term from the λ-Calculus is either: Terms from the λ-Calculus can be _rewritten_ using various rules the two main ones being: -* α-renaming: `(lam (x) x)` ⟹ `(lam (y) y)` -* β-reduction: `((lam (x) body) term)` ⟹ `body[x ← term]` +* α-renaming: + + > `(lam (x) x)` ⟹ `(lam (y) y)` +* β-reduction: + + > `((lam (x) body) term)` ⟹ `body[x ← term]` ## λ-Calculus Extensions @@ -38,14 +42,14 @@ Terms from the λ-Calculus can be _rewritten_ using various rules the two main o * Local definitions: `(let ((id (lam (x) x))) (id foo))` * Global definitions: `(def id (lam (x) x))` ----- +## λ-Calculus Extensions * Primitive data: * booleans: `true`, `false` * numbers: `12`, `0.27` * strings: `"λ-calculus rocks"` -## λ-Calculus Typing +## Typed λ-Calculus * The λ-Calculus is the favorite playground of type theorists * There's a whole zoo of type systems we won't dive into (see you next year!) @@ -54,12 +58,12 @@ Terms from the λ-Calculus can be _rewritten_ using various rules the two main o ## The Code - + ## Action - + ## Conclusion - + |