---
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