Opérationnel et catégorique modèles de PCF : l'adressage des machines et la distribution semirings - Thèses et HDR CNRS en sciences cognitives Accéder directement au contenu
Thèse Année : 2024

Opérationnel et catégorique modèles de PCF : l'adressage des machines et la distribution semirings

Operational and categorical models of PCF : addressing machines and distributing semirings

Nicolas Munnich
  • Fonction : Auteur
  • PersonId : 1402259
  • IdRef : 279401779

Résumé

Despite being introduced over 60 years ago, PCF remains of interest. Though the quest for a satisfactory fully abstract model of PCF was resolved around the turn of the millennium, new models of PCF still frequently appear in the literature, investigating unexplored avenues or using PCF as a lens or tool to investigate some other mathematical construct. In this thesis, we build upon our knowledge of models of PCF in two distinct ways: Constructing a brand new model, and building upon existing models. Addressing Machines are a relatively new type of abstract machine taking inspiration from Turing Machines. These machines have been previously shown to model the full untyped ?- calculus. We build upon these machines to construct Extended Addressing Machines (EAMs) and endow them with a type system. We then show that these machines can be used to obtain a new and distinct fully abstract model of PCF: We show that the machines faithfully simulatePCF in such a way that a PCF term terminates in a numeral exactly when the corresponding Extended Addressing Machine terminates in the same numeral. Likewise, we show that every typed Extended Addressing Machine can be transformed into a PCF program with the same observational behaviour. From these two results, it follows that the model of PCF obtained by quotienting typable EAMs by a suitable logical relation is fully abstract. There exist a plethora of sound categorical models of PCF, due to its close relationship with the ?-calculus. We consider two similar models (which are also models of Linear Logic) that are based on semirings: Weighted models, using semirings to quantify some internal value, and Multiplicity models, using semirings to linearly model functions (model the exponential !). We investigate the intersection between these two models by investigating the conditions under which two monads derived from specific semirings distribute. We discover that whether or not a semiring has an idempotent sum makes a large difference in its ability to distribute. Our investigation leads us to discover the notion of an unnatural distribution, which forms a monad on a Kleislicategory. Finally, we present precise conditions under which a particular distribution can form between two semirings.
Bien qu'elle ait été introduite il y a plus de 60 ans, PCF reste intéressante. Bien que la quête d'un modèle satisfaisant et totalement abstrait de PCF ait été résolue au tournant du millénaire, de nouveaux modèles de PCF apparaissent encore fréquemment dans la littérature, explorant des voies inexplorées ou utilisant PCF comme une lentille ou un outil pour étudier une autre construction mathématique. Dans cette thèse, nous nous appuyons sur notre connaissance des modèles de PCF de deux manières distinctes : En construisant un tout nouveau modèle, et en s'appuyant sur les modèles existants. Les machines d'adressage sont un type relativement nouveau de machine abstraite qui s'inspire des machines de Turing. Il a déjà été démontré que ces machines peuvent modéliser l'ensemble du ?-calcul non typé. Nous nous appuyons sur ces machines pour construire des machinesd'adressage étendues (EAM) et les doter d'un système de type. Nous montrons ensuite que ces machines peuvent être utilisées pour obtenir un nouveau modèle entièrement abstrait et distinct de PCF : Nous montrons que les machines simulent fidèlement PCF de telle sorte qu'un terme PCF se termine par un chiffre exactement lorsque la machine d'adressage étendue correspondante se termine par le même chiffre. De même, nous montrons que chaque machine d'adressage étendue typée peut être transformée en un programme PCF avec le même comportement d'observation. De ces deux résultats, il découle que le modèle de PCF obtenu en quotientant les EAM typables par une relation logique appropriée est totalement abstrait. Il existe une pléthore de modèles catégoriels solides de PCF, en raison de sa relation étroite avec le ?-calcul. Nous considérons deux modèles similaires (qui sont aussi des modèles de logique linéaire) qui sont basés sur des sémirings : Les modèles pondérés, qui utilisent les sémirations pour quantifier une valeur interne, et les modèles de multiplicité, qui utilisent les sémirations pour modéliser linéairement des fonctions (modèle de l'exponentielle !). Nous étudionsl'intersection entre ces deux modèles en examinant les conditions sous lesquelles deux monades dérivées de sémirings spécifiques se distribuent. Nous découvrons que le fait qu'un semi-anneau ait ou non une somme idempotente fait une grande différence dans sa capacité à distribuer. Notre étude nous conduit à découvrir la notion de distribution non naturelle, qui forme une monade sur une catégorie de Kleisli. Enfin, nous présentons des conditions précises sous lesquelles une distribution particulière peut se former entre deux semis.

Domaines

Informatique
Fichier principal
Vignette du fichier
edgalilee_th_2024_munnich.pdf (1.17 Mo) Télécharger le fichier
Origine Version validée par le jury (STAR)

Dates et versions

tel-04649592 , version 1 (16-07-2024)

Identifiants

  • HAL Id : tel-04649592 , version 1

Citer

Nicolas Munnich. Opérationnel et catégorique modèles de PCF : l'adressage des machines et la distribution semirings. Computer science. Université Paris-Nord - Paris XIII, 2024. English. ⟨NNT : 2024PA131015⟩. ⟨tel-04649592⟩
0 Consultations
0 Téléchargements

Partager

Gmail Mastodon Facebook X LinkedIn More