HAMMACHE Wendy

Dès le début du XXe siècle, la question significationnelle devient une préoccupation majeure en logique mathématique, tandis qu'elle faisait jusqu'alors l'objet d'une certaine insouciance. Comme cause de cet intérêt soudain, le paradoxe de Russell exhibe une situation d'auto-application générant des contradictions. La faille de sens qui en résulte est plurielle. À la plus petite échelle, elle concerne la possibilité pour une expression d'être construite dans un système, tandis qu'elle n’a pas de dénotation. À une échelle plus large, elle désigne le gouffre dans lequel tombe le système qui autorise la dérivation de l'antinomie. La solution envisagée par Russell à cette dérive significationnelle est celle d'une hiérarchie régulant l'application de fonctions ; la notion de "type" émerge ainsi, désignant les échelon de cette hiérarchie. Le typage s'impose comme contrôle du calcul et, dans le même temps, comme régulation du sens. Conservant ce caractère régulateur, les types se métamorphosent cependant au cours du XXe siècle. Ces transformations sont parallèles aux évolutions de la notion de "fonction" et de celle de "computation".
Notre étude historico-philosophique se concentre essentiellement sur les systèmes fonctionnels du XXe siècle et, en particulier, le λ-calcul de Church, à la fois dans sa version pure et dans sa version typée. Nous étudions les métamorphoses de la régulation des processus computationnels, en lien la délimitation de la signification. Dans ce contrôle parallèle du calcul et du sens, la notion de type joue un rôle majeur : de la théorie des types de Russell jusqu'aux systèmes de type de Coppo et Dezani, nous tâcherons d'identifier la nature de ce rôle.

Mots-clés : types, signification, calcul.

Since the early twentieth century, the problem of meaning has become a subject of concern in mathematical logic, while until then, it slightly has been neglected. The cause of this sudden interest is Russell's paradox: it exhibits a situation of self-application which entails some contradictions. The crack in meaning brought by this paradox is multifaceted. On the tiniest scale, it involves the possibility to build a non-denoting statement within a system. On a larger scale, it concerns the abyss into which a system falls when it allows the derivation of the antinomy. Russell's answer to this loss of meaning lies in the building of a hierarchy that regulates the application of functions. The notion of type rises in these circumstances: as a stage of this hierarchy. Thus typing becomes an ideal tool for the control of computation alongside a regulation of meaning. During the twentieth century, types are subjet of metamorphoses, but they retain, more or less, this feature of regulation. This goes with the evolution of the concept of "function and that of "calculus", or rather, of "computation", gradually considered for its processual character.
Our investigation, both historical and philosophical, mainly focuses on the functional systems of the twentieth century, especially Church's λ-calculus, in its pure and typed versions. We analyze the metamorphoses of the regulation of computational processes, closed to the boundaries of meaning. Into such a parallel control of computation and meaning, the notion of type plays a leading role we aim at identifying the nature, from Russell's ramified theory of types to Coppo and Dezani's intersection type systems for λ-calculus.

Keywords : types, meaning, computation

Directeur de thèse : Jean-Baptiste JOINET

Membres du jury :

Président du jury : Sébastien GANDON