Théorie des types
Un article de Freepedia.
Il existe deux théories des types en mathématiques :
- la première (et la plus ancienne) est en fait une théorie des ensembles due à Bertrand Russell; trop lourde d'emploi, elle a été supplantée par la théorie de Zermelo-Frankel.
- la deuxième relève de l'informatique théorique et traite les collections d'objets comme des types et non comme des ensembles.
Dans cette deuxième théorie, les expressions mathématiques sont construites à l'aide de fonctions, où chaque fonction a un type qui décrit le type de ses arguments et le type de la valeur retournée. Les expressions sont bien formées lorsque les fonctions sont bien appliquées à des fonctions ayant le bon type.
Ce concept de type a deux domaines d'applications :
- les langages de programmation, surtout les langages fonctionnels typés,
- les systèmes de démonstration sur ordinateur.
Dans le cadre de la démonstration sur ordinateur, il y a une forte analogie entre les expressions bien formées et les démonstrations mathématiques correctes.
