From 002e8883709214c96a171d216af3868fe34ceeb9 Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Thu, 6 Nov 2025 07:17:25 +0100 Subject: revealjs version of slides --- lambda-calcul/support/newcrafts-2025.md | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) (limited to 'lambda-calcul/support/newcrafts-2025.md') 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: --- -![](biface.jpg) +![](./biface.jpg) ## λ-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 -![](repo.jpg) +![](./repo.jpg) ## Action -![](eruption.jpg) +![](./eruption.jpg) ## Conclusion -![](gatsby.jpeg) +![](./gatsby.jpeg) -- cgit v1.3.1