1 files changed, 216 insertions, 0 deletions
diff --git a/lambda-calcul/support/2024-10-10.md b/lambda-calcul/support/2024-10-10.md
new file mode 100644
index 0000000..390ff10
--- /dev/null
+++ b/lambda-calcul/support/2024-10-10.md
@@ -0,0 +1,216 @@
+% Lambda Nantes \newline Compréhension, Interprétation et implémentation du $\lambda$-calcul
+% **Workshop 1:** 10 Octobre 2024 @ **Palo IT Nantes**
+% **Arnaud Bailly** (Cardano Foundation) et **Xavier Van de Woestyne** (Tarides)
+
+# Une nouvelle formule !
+
+> En complément des présentations (habituelles), on voudrait proposer
+> un nouveau format, plus interactif, potentiellement plus accessible
+> et probablement plus _transportable_ en visio-conférence !
+
+\pause
+
+- Des **workshops interactifs**
+- **Indépendants** des langages et technologies (tout est le bienvenu)
+- **Pérennes** dans le temps (en permettant notamment plusieurs
+  sessions sur un même sujet)
+- Construction du platforme web pour le **suivi** des workshops (dans
+  un futur _proche_)
+  
+# Pleins d'idées de sujets
+
+- **Compréhension, interprétation et implémentation du
+  $\lambda$-calcul**
+
+- Implémentation d'applications web, **dans un style fonctionnel**
+  (pour remplacer, par exemple, les affreuses applications
+  propriétaires que l'on utilise, comme Meetup, et **parce que c'est
+  très rigolo de réinventer la roue !**)
+
+- **Vos sujets** (en tant que suggestion, en tant qu'organisateurs, ce
+  _que vous voulez_), nous somme très ouverts à la contribution et à
+  l'apprentissage
+
+# Compréhension, Interprétation et implémentation du $\lambda$-calcul
+
+> On dit souvent qu'une compréhension fine du $\lambda$-calcul, la
+> base de la programmation fonctionnelle est nécéssaire pour la
+> comprendre.
+
+\pause 
+
+> **Je prétend que c'est faux** (de la même manière qu'une
+> compréhension fine de la théorie des catégories) n'est absolument un
+> prérequis (ou une nécéssité) pour faire du Haskell efficacement.
+
+# Alors pourquoi ce premier Workshop ?
+
+- **Ça permet de s'initier à la construction d'un langage**
+- C'est tout de même intéressant
+- Le $\lambda$-calcul permet de **comprendre** certains points
+  théoriques liés à la compilation et l'interprétation de langages de
+  programmation
+- Permet de se familiariser avec certains encodages dans des langages
+  plus riches
+- Ça se découpe bien en plusieurs parties
+
+# C'est quoi le $\lambda$-calcul ?
+
+- Un système formel inventé dans les années 30, par **Alonzo Church**
+  qui décrit/fonde les concepts de **fonctions et d'applications de
+  fonctions** (qui est, en fait, un langage de programmation théorique)
+  
+- Premier formalisme permettant de décrire et caractériser **les
+  fonctions récursives**, permettant de décrire la notion de
+  **calculabilité** (que l'on appellera, plus tard, la
+  _Turing-completude_)\newline\newline
+  
+\pause
+
+> Comme pour le modèle de Herbrand-Gödel et les machines de turing, il
+> est un des fondaments de la calculabilité, donc de la programmation
+> et offre le même niveau d'expressivité.
+
+
+# Aujourd'hui
+
+- Base conceptuelle des langages de programmations fonctionnels
+  modernes (laissant à la machine de Turing le rôle de base
+  conceptuelle des langages impératifs)
+  
+- Permet de servir de base pour des modèles de programmations
+  (certains motifs de conceptions par exemple)
+  
+- Sert le travail de l'ingénieur quotidiennement, notamment pour la
+  construction d'outils (ie: _refactor Engine_ qui est généralement
+  une conséquence de la $\beta$-reduction ou encore l'indexation
+  d'occurences via des formes de normalisation)
+  
+- Permet d'implémenter des langages en étant étendu, de servir de
+  cible de compilation et aussi d'outil de comparaison entre des
+  langages (via des procédés d'analyse sémantique)\pause
+  
+- Permet d'organiser des Workshops (dans lesquels on pourra ajouter
+  des fonctionnalités, un système de type etc) !
+
+# Une grammaire **incroyablement** simple !
+
+Les constituants du $\lambda$-calcul sont appelés des
+$\lambda$-termes.
+
+## Variables : `<nom>`
+`x` est une variable de nom `x`.
+
+## Abstraction : $\lambda$`<paramètres>.<corps>`
+
+$\lambda x. x$ est la fonction **identité**.
+
+## Application : `<fonction><lambda-terme>`
+
+($\lambda x. x$)`a`, on applique l'identité à `a`.
+
+
+# En d'autres termes: 
+
+```
+Term (M, N, O, ...):
+    M ::= x    (variable)
+    M ::= λx.M (abstraction)
+    M ::= M N  (application)
+```
+
+
+> Comment résoudre des fonctions à plusieurs argument ? La
+> **curryfication** !
+
+# Avec quelques conventions de parenthèsages
+
+```
+(M)       ≡ M 
+λx.(M N)  ≡ λx.M N 
+λx.(λy.M) ≡ λx.λy.M
+(M N) O   ≡ M N O
+```
+
+
+---
+
+Avec ces trois éléments, on peut déjà construire beaucoup de choses !
+Le fait d'utiliser uniquement des fonctions et des applications pour
+encoder des choses s'appelle l'utilisation de
+**church-encodings**. (La base de l'OOP en vrai)
+
+## Des booléens
+
+- `TRUE  := λx.λy.x`
+- `FALSE := λx.λy.y`
+
+\pause
+
+- `AND   := λp.λq.p q p`
+- `OR    := λp.λq.p p q`
+- `NOT   := λp.p FALSE TRUE`
+
+\pause
+
+- `IFTD  := λp.λa.λb.p a b`
+
+---
+
+## De l'arithmétiques
+
+- `0    := λfx.x`
+- `1    := λfx.f x`
+- `2    := λfx.f (f x)`
+- `3    := λfx.f (f (f x))`
+- etc.
+
+\pause
+
+- `SUCC := λn.λf.λx.f (n f x)`
+- `PLUS := λm.λn.m SUCC n`
+- etc.
+
+
+# Première étape: décrire un AST
+
+Un **AST** (ou, Arbre de Syntaxe Abstrait) est une représentation
+manipulable de notre syntaxe.
+
+Avec un AST, on peut, par exemple, considérer que les deux expressions
+sont équivalentes :
+
+- `let     f x     = x    + 1`
+- `let f x = (+) x 1`
+
+Il est usuel d'utiliser des **sommes** pour décrire les différentes
+branches (souvent récursives) de notre arbre !
+
+# Concepts de variables **libres**
+
+> **Une peu naïvement** : Ensembles des variables qui ne sont pas des
+> arguments (dans un scope donné). Par exemple:
+
+```
+λx.x    # Pas de variables libres
+λx.x+y  # y est libre
+```
+
+Quand une variable n'est pas libre, elle est **liée**
+
+# Réductions
+
+Permettant de décrire des équivalence de Lambda Termes.
+
+- $\alpha$-conversion: la **résolution des noms** (`λx.x` = `λy.y`)
+  (qui entraine des **Substitutions**)
+- $\beta$-conversion: l'**application de fonction** (`(λx.x × + 2) 7`
+  = `7 + 2` = `9`)
+- $\eta$-reduction: `(λx.f x)` = `f` si `x` n'est pas **libre**
+
+La base de stratégie d'évaluation et d'optimisation ! (En effet, on
+réduira généralement durant l'évaluation d'un programme)
+
+---
+
+On a suffisamment de "bases" pour démarrer !