Modèles de calcul(s)
Cette thèse a pour objectif d’étudier, clarifier, et formaliser la notion de modèle de calcul. En informatique théorique, plusieurs instances de modèles de calcul existent: machines de Turing, fonctions récursives, lambda-calcul, etc. Ce sont autant de manières de conceptualiser la notion intuitive de “procédure effective”, et de circonscrire formellement les conditions pour qu’une telle procédure puisse être exécutée par un ordinateur. En ce sens, un modèle de calcul est un objet mathématique abstrait de considérations pratiques (contraintes de temps et d’espace). La thèse de Church-Turing énonce que ces modèles capturent la notion de fonction calculable, permettant de les considérer comme équivalents. Mais si ces modèles calculent les mêmes fonctions, ils ne les calculent pas toujours de la même manière. Le point de vue de la thèse de Church-Turing suffit-il alors à définir ce qu’est un modèle de calcul? Permet-il d’englober ce qui fait leurs caractéristiques communes et par la même occasion de déterminer ce qui les distingue mutuellement? Formaliser la notion ellemême de modèle de calcul permettrait d’en faire des objets mathématiques à part entière et donc d’en établir une théorie répondant à ces différentes interrogations.
Models of computation(s)
The aim of this thesis is to study, clarify and formalize the notion of model of computation. Within computer science, different instances of models of computation exist : Turing machines, recursive functions, lambda-calculus, etc. These are various ways of conceptualizing the intuitive notion of “effective procedure”, and to formally circumscribe the conditions for such a procedure to be run on a computer. In this sense, a model of computation is a mathematical object free from practical considerations (constraints of time and space). The Church-Turing thesis states that the different models of computation all capture the notion of computable function, and thus allows to state their equivalence. But if these models compute the same functions, they don’t necessarily compute them in the same way. Is the Church-Turing point of view sufficient in order to give a satisfactory definition of a model of computation? Does it allow us to consider all their common characteristics and following that determine what distinguishes them? Formalizing the notion of model of computation itself would make them fully mathematical objects and thus result in a theory answering these multiple queries.