Lambda-calcul simplement typé
variante du lambda-calcul avec des types / De Wikipedia, l'encyclopédie encyclopedia
Cher Wikiwand IA, Faisons court en répondant simplement à ces questions clés :
Pouvez-vous énumérer les principaux faits et statistiques sur Lambda-calcul simplement typé?
Résumez cet article pour un enfant de 10 ans
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 est fortement normalisant.