Contrôle du calcul et limites du sens : fonctions, computation et types de G. Frege à A.Church / Wendy Hammache ; sous la direction de Jean-Baptiste Joinet

Date :

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : français / French

Russell -- Bertrand -- 1872-1970

Logique mathématique

Analyse fonctionnelle

Logique combinatoire

Types abstraits de données (informatique)

Joinet, Jean-Baptiste (Directeur de thèse / thesis advisor)

Gandon, Sébastien (1969-....) (Président du jury de soutenance / praeses)

Halimi, Brice (1971-....) (Rapporteur de la thèse / thesis reporter)

Martini, Simone (19..-... ; informaticien) (Rapporteur de la thèse / thesis reporter)

De Mol, Liesbeth (Membre du jury / opponent)

Numerico, Teresa (19..-....) (Membre du jury / opponent)

Université de Lyon (2015-....) (Organisme de soutenance / degree-grantor)

École doctorale de philosophie (Lyon ; Grenoble ; 2007-....) (Ecole doctorale associée à la thèse / doctoral school)

Université Jean Moulin (Lyon ; 1973-....) (Autre partenaire associé à la thèse / thesis associated third party)

Résumé / Abstract : 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.

Résumé / Abstract : 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.