Geodesic
Unification of Higher-order Patterns modulo Simple Syntactic Equational Theories
Discrete mathematics & theoretical computer science, Tome 4 (2000-2001) no. 1.

Voir la notice de l'article provenant de la source Episciences

We present an algorithm for unification of higher-order patterns modulo simple syntactic equational theories as defined by Kirchner [14]. The algorithm by Miller [17] for pattern unification, refined by Nipkow [18] is first modified in order to behave as a first-order unification algorithm. Then the mutation rule for syntactic theories of Kirchner [13,14] is adapted to pattern E-unification. If the syntactic algorithm for a theory E terminates in the first-order case, then our algorithm will also terminate for pattern E-unification. The result is a DAG-solved form plus some equations of the form λ øverlinex.F(øverlinex) = λ øverlinex. F(øverlinex^π ) where øverlinex^π is a permutation of øverlinex When all function symbols are decomposable these latter equations can be discarded, otherwise the compatibility of such equations with the solved form remains open. 
@article{DMTCS_2000_4_1_a0,
     author = {Boudet, Alexandre},
     title = {Unification of {Higher-order} {Patterns} modulo {Simple} {Syntactic} {Equational} {Theories}},
     journal = {Discrete mathematics & theoretical computer science},
     publisher = {mathdoc},
     volume = {4},
     number = {1},
     year = {2000-2001},
     doi = {10.46298/dmtcs.270},
     language = {en},
     url = {http://geodesic.mathdoc.fr/articles/10.46298/dmtcs.270/}
}
TY  - JOUR
AU  - Boudet, Alexandre
TI  - Unification of Higher-order Patterns modulo Simple Syntactic Equational Theories
JO  - Discrete mathematics & theoretical computer science
PY  - 2000-2001
VL  - 4
IS  - 1
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/articles/10.46298/dmtcs.270/
DO  - 10.46298/dmtcs.270
LA  - en
ID  - DMTCS_2000_4_1_a0
ER  - 
%0 Journal Article
%A Boudet, Alexandre
%T Unification of Higher-order Patterns modulo Simple Syntactic Equational Theories
%J Discrete mathematics & theoretical computer science
%D 2000-2001
%V 4
%N 1
%I mathdoc
%U http://geodesic.mathdoc.fr/articles/10.46298/dmtcs.270/
%R 10.46298/dmtcs.270
%G en
%F DMTCS_2000_4_1_a0
Boudet, Alexandre. Unification of Higher-order Patterns modulo Simple Syntactic Equational Theories. Discrete mathematics & theoretical computer science, Tome 4 (2000-2001) no. 1. doi : 10.46298/dmtcs.270. http://geodesic.mathdoc.fr/articles/10.46298/dmtcs.270/

Cité par Sources :