Algorithme de type principal
Algorithme de typage du lambda calcul à la Curry, qui teste la typabilité d'un $\lambda$-terme, et construit un type principal si il existe.
| Qualité | Numéro | Titre |
|---|---|---|
| 5 | 929 | Lambda-calcul pur comme modèle de calcul. Exemples.2021 |
| 4 | 25 | Analyses lexicale et syntaxique. Applications.2022 |
Utilisateur : sieghttct
Le programme ne parle que de $\lambda$-calcul pur, ça peut donc paraître étonnant de mettre du typage ici. Néanmoins, le typage d'un terme est une méthode efficace pour prouver qu'il est (fortement) normalisant ! C'est l'intérêt du théorème rappelé en début de développement.
Pour la leçon 923, le rapport 2017 rappelle aussi qu'on peut introduire des bouts d'analyse sémantique, cet algo y trouve donc aussi toute sa place.
Références :
Lectures on the Curry-Howard Isomorphism - M. H. Sørensen, P. Urzyczyn
Term rewriting and All That - Franz Baader
Utilisateur : Meven
Il faut pas mal adapter la version du bouquin.
Références :
Lambda Calculus With Types - H. Barendregt