Unification of Drags and Confluence of Drag Rewriting

Jean-Pierre Jouannaud (1) , Fernando Orejas (2)

1 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
2 UPC - Universitat Politècnica de Catalunya = Université polytechnique de Catalogne [Barcelona]

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.

Keywords: Drags; graphs; unification; confluence

Domains: Computation and Language [cs.CL]; Logic in Computer Science [cs.LO]

Jean-Pierre Jouannaud, Fernando Orejas. Unification of Drags and Confluence of Drag Rewriting. 2022. ⟨hal-02562152v4⟩