diff options
Diffstat (limited to 'lambda-calcul/support/newcrafts-2025.md')
| -rw-r--r-- | lambda-calcul/support/newcrafts-2025.md | 61 |
1 files changed, 61 insertions, 0 deletions
diff --git a/lambda-calcul/support/newcrafts-2025.md b/lambda-calcul/support/newcrafts-2025.md new file mode 100644 index 0000000..c80e453 --- /dev/null +++ b/lambda-calcul/support/newcrafts-2025.md @@ -0,0 +1,61 @@ +--- +title: How I learnt to love typed λ-calculus +subtitle: "**A NewCrafts 2025 Hands-On Lab**" +date: 2025-11-06 +author: +- Arnaud Bailly +- Emmanuel Gaillot +--- + +## Introduction + +> An experimental workshop to explore the computational foundation of the universe, and have fun + +--- + + + +## λ-Calculus Syntax + +A term from the λ-Calculus is either: + +* A _Symbol_: `x`, `y`, `Foo`, `++`... +* An _Abstraction_: `(lam (x) x)` +* An _Application_: `(foo bar)` + +## λ-Calculus Rules + +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]` + +## λ-Calculus Extensions + +* Syntactic sugar: + * `(lam (x) (lam (y) y))` ⟹ `(lam (x y) y)` + * `((foo bar) baz)` ⟹ `(foo bar baz)` +* Local definitions: `(let ((id (lam (x) x))) (id foo))` +* Global definitions: `(def id (lam (x) x))` + +---- + +* Primitive data: + * booleans: `true`, `false` + * numbers: `12`, `0.27` + * strings: `"λ-calculus rocks"` + +## λ-Calculus Typing + +* 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!) +* Search for _λ Cube_online... +* We'll introduce _Simply Typed λ-Calculus_ aka. $\lambda_{\rightarrow}$ + +## Action + + + +## Conclusion + + |