eduroam-prg-og-1-29-45.net.univ-paris-diderot.fr 2026-2-25:15:13:21

lambda calcul non typé.md

@@ -0,0 +1,25 @@
+---
+up:
+tags:
+aliases:
+---
+
+
+> [!definition] [[lambda calcul non typé]]
+> Soient $\mathcal{C}$ un ensemble de constantes et $\mathcal{X}$ un ensemble de variables
+> On définit par induction l'ensemble $\Lambda$ des formules du lambda-calcul
+>  - $\forall x \in \mathcal{X},\quad x \in \Lambda$
+>  - $\forall a \in \mathcal{C},\quad a \in \Lambda$
+>  - $\forall x \in \mathcal{X},\quad (\lambda x.M) \in \Lambda$
+>  - $\forall M, N \in \Lambda ,\quad (MN) \in \Lambda$
+^definition
+
+> [!info] Syntaxe
+> L'application est associative à gauche :
+>  - $M N O$ correspond à $((M N) O)$ (~~pas à $(M (N O))$~~)
+> Les $\lambda$-abstractions sont raccourcies comme suit : $\lambda $
+
+# Propriétés
+
+# Exemples
+