Lambda-calcul simplement typé

Carte Commune · n° 451178

Le lambda-calcul simplement typé est une variante du lambda-calcul qui se différencie de ce dernier par la présence de types. Il a été développé par Alonzo Church pour pallier l'incohérence du lambda-calcul non typé, due au paradoxe de Curry, et servir de fondements aux mathématiques. Le lambda-calcul simplement typé partage un lien fort avec la logique propositionnelle minimale au travers de l'isomorphisme de Curry-Howard. Il peut également être vu comme une version simplifiée d'un langage de programmation fonctionnelle. De plus, toutes les fonctions définissables dans le lambda-calcul simplement typé terminent : le lambda-calcul simplement typé est fortement normalisant.

Lire sur Wikipédia