Non-Deterministic Abstract Machines - Université de Lorraine Accéder directement au contenu
Rapport Année : 2022

Non-Deterministic Abstract Machines

Machines abstraites non déterministes

Résumé

We present a generic design of abstract machines for nondeterministic programming languages, such as process calculi or concurrent lambda calculi, that provides a simple way to implement them. Such a machine traverses a term in the search for a redex, making non-deterministic choices when several paths are possible and backtracking when it reaches a dead end, i.e., an irreducible subterm. The search is guaranteed to terminate thanks to term annotations the machine introduces along the way. We show how to automatically derive a non-deterministic abstract machine from a zipper semantics-a form of structural operational semantics in which the decomposition process of a term into a context and a redex is made explicit. The derivation method ensures the soundness and completeness of the machines w.r.t. the zipper semantics.
Nous proposons une présentation uniforme des machines abstraites pour les langages non déterministes, tels que les calculs de processus ou les lambda-calculs concurrents, qui permet de les implémenter facilement. Une telle machine traverse le terme à la recherche d’un redex, en faisant des choix arbitraires lorsque plusieurs chemins sont possibles, et en retournant en arrière lorsqu’elle atteint un cul-de-sac, c’est-à-dire un terme irreductible. Nous garantissons la terminaison de la recherche grâce aux annotations que la machine ajoute en cours de route. Nous montrons comment dériver automatiquement une machine non déterministe depuis une sémantique zipper—une forme de sémantique opérationnelle structurelle dans laquelle la décomposition d’un terme en un contexte et un redex apparaît explicitement. La méthode de dérivation garantit la correction et la complétude de la machine par rapport à la sémantique zipper.
Fichier principal
Vignette du fichier
RR-9475.pdf (970.85 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03545768 , version 1 (27-01-2022)
hal-03545768 , version 2 (01-07-2022)

Identifiants

  • HAL Id : hal-03545768 , version 2

Citer

Małgorzata Biernacka, Dariusz Biernacki, Serguei Lenglet, Alan Schmitt. Non-Deterministic Abstract Machines. [Research Report] RR-9475, Inria. 2022, pp.1-33. ⟨hal-03545768v2⟩
237 Consultations
151 Téléchargements

Partager

Gmail Facebook X LinkedIn More