Unification of drags and confluence of drag rewriting

Autor: Jouannaud, Jean-Pierre, Orejas, Fernando
Přispěvatelé: Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Universitat Politècnica de Catalunya [Barcelona] (UPC), Jouannaud, Jean-Pierre, Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Laboratoire de Méthodes Formelles, Université de Paris-Saclay, Université de Paris Saclay, Universitat Politècnica de Catalunya. Departament de Ciències de la Computació, Universitat Politècnica de Catalunya. ALBCOM - Algorísmia, Bioinformàtica, Complexitat i Mètodes Formals
Rok vydání: 2023
Předmět:
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO]
unification
InformationSystems_INFORMATIONINTERFACESANDPRESENTATION(e.g.
HCI)
Logic
[INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE]
GeneralLiterature_MISCELLANEOUS
[INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL]
Theoretical Computer Science
Physics::Fluid Dynamics
Computer Science::Logic in Computer Science
ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION
Drags
Algorismes computacionals
ComputingMethodologies_COMPUTERGRAPHICS
graphs
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Confluence
ACM: D.: Software
Computer algorithms
ACM: F.: Theory of Computation
Informàtica::Informàtica teòrica::Algorísmica i teoria de la complexitat [Àrees temàtiques de la UPC]
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
Computational Theory and Mathematics
Unification
[INFO.INFO-CL] Computer Science [cs]/Computation and Language [cs.CL]
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
confluence
Computer Science::Programming Languages
Astrophysics::Earth and Planetary Astrophysics
Graphs
Software
Zdroj: Journal of Logical and Algebraic Methods in Programming
Journal of Logical and Algebraic Methods in Programming, 2023, 131, pp.26. ⟨10.1016/j.jlamp.2022.100845⟩
ISSN: 2352-2208
DOI: 10.1016/j.jlamp.2022.100845
Popis: Drags are a recent, natural generalization of terms which admit arbitrary cycles. A key aspect of drags is that they can be equipped with a composition operator so that rewriting amounts to replace a drag by another in a composition. In this paper, we develop a unification algorithm for drags that allows to check the local confluence property of a set of drag rewrite rules. This work is partially supported by MCIN/AEI /10.13039/501100011033 under grant PID2020-112581GB-C21.
Databáze: OpenAIRE
Externí odkaz: