cours/lambda calcul non typé.md

up, tags, aliases

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