Towards Deciding Second-order Unification Problems Using Regular Tree Automata

Tomer Libal 1, 2, *
* Auteur correspondant
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : The second-order unification problem is undecidable [5]. While unification procedures, like Huet's pre-unification, terminate with success on unifiable problems, they might not terminate on non-unifiable ones. There are several decidability results for unification problems with infinitely-many pre-unifiers, such as for monadic second-order problems [3]. These results are based on the regular structure of the solutions of these problems and by computing minimal unifiers. Beyond the importance of the knowledge that searching for unifiers of decidable problems always terminates, one can also use this information in order to optimize unification algorithms, such as in the case for pattern unification [10]. Nevertheless, being able to prove that the unification problem of a certain class of unification constraints is decidable is far from easy. Some results were obtained for certain syntactic restrictions on the problems (see Levy [8] for some results and references) or on the unifiers (see Schmidt-Schauß [11], Schmidt-Schauß and Schulz [12, 13] and Je˙ z [7] for some results). Infinitary unification problems, like the ones we are considering, might suggest that known tools for dealing with the infinite might be useful. One such tool is the regular tree automaton. The drawback of using regular automata for unification is, of course, their inability to deal with variables. In this paper we try to overcome this obstacle and describe an ongoing work about using regular tree automata [1] in order to decide more general second-order unification problems. The second-order unification problems we will consider are of the form λz n .x 0 t. = λz n .C(x 0 s) where C is a non-empty context [2] and x 0 does not occur in t or s. We will call such problems cyclic problems. An important result in second-order unification was obtained by Ganzinger et al. [4] and stated that second-order unification is undecidable already when there is only one second-order variable occurring twice. The unification problem they used for proving the undecidability result was an instance of the following cyclic problem. Note that we chose to use in the definition only unary second-order variables but that this restriction should not be essential. x 0 (w 1 , g(y 1 , a)) = g(y 2 , x 0 (w 2 , a)) (1) Our decidability result is obtained by posing one further restriction over cyclic problems which is based on the existence and location of variables other than the cyclic one. A sufficient condition for the decidability of second-order unification problems was given by Levy [8]. This condition states that if we can never encounter, when applying Huet's pre-unification procedure [6] to a problem, a cyclic equation, then the procedure terminates. It follows from this result that deciding second-order unification problems depends on the ability to decide cyclic problems. The rules of Huet's procedure (PUA) are given in Fig. 1. Imitation partial bindings and projection partial bindings are defined in [14] and are denoted, respectively, by PB(f, α) and PB(i, α) where α is a type, Σ a signature f ∈ Σ and i > 0.
Liste complète des métadonnées

Littérature citée [14 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01242233
Contributeur : Tomer Libal <>
Soumis le : vendredi 11 décembre 2015 - 16:10:05
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : samedi 29 avril 2017 - 13:03:34

Fichier

paper.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01242233, version 1

Citation

Tomer Libal. Towards Deciding Second-order Unification Problems Using Regular Tree Automata. 29th International Workshop on Unification, Jun 2015, Warsaw, Poland. 〈hal-01242233〉

Partager

Métriques

Consultations de la notice

275

Téléchargements de fichiers

38