TY - GEN
T1 - Variants in the Infinitary Unification Wonderland
AU - Meseguer, José
N1 - Funding Information:
Acknowledgements. My warmest thanks to Santiago Escobar and Steven Eker for many discussions that have helped me arrive at the ideas presented here. I cordially thank the referees for their very helpful suggestions to improve the paper. This work has been partially supported by NRL under contract N00173-17-1-G002.
Publisher Copyright:
© 2020, Springer Nature Switzerland AG.
PY - 2020
Y1 - 2020
N2 - So far, results about variants, the finite variant property (FVP), and variant unification have been developed for equational theories E∪ B where B is a set of axioms having a finitary unification algorithm, and the equations E, oriented as rewrite rules E→, are convergent modulo B. The extension to the case when B has an infinitary unification algorithm, for example because of non-commutative symbols having associative axioms, seems undeveloped. This paper takes a first step in developing such an extension. In particular, the relationships between the FVP and the boundedness properties, the identification of conditions on E∪ B ensuring FVP, and the effective computation of variants and variant unifiers are explored in detail. The extension from the finitary to the infinitary case includes both surprises and opportunities.
AB - So far, results about variants, the finite variant property (FVP), and variant unification have been developed for equational theories E∪ B where B is a set of axioms having a finitary unification algorithm, and the equations E, oriented as rewrite rules E→, are convergent modulo B. The extension to the case when B has an infinitary unification algorithm, for example because of non-commutative symbols having associative axioms, seems undeveloped. This paper takes a first step in developing such an extension. In particular, the relationships between the FVP and the boundedness properties, the identification of conditions on E∪ B ensuring FVP, and the effective computation of variants and variant unifiers are explored in detail. The extension from the finitary to the infinitary case includes both surprises and opportunities.
UR - http://www.scopus.com/inward/record.url?scp=85099064331&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85099064331&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-63595-4_5
DO - 10.1007/978-3-030-63595-4_5
M3 - Conference contribution
AN - SCOPUS:85099064331
SN - 9783030635947
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 75
EP - 95
BT - Rewriting Logic and Its Applications - 13th International Workshop, WRLA 2020, Revised Selected Papers
A2 - Escobar, Santiago
A2 - Martí-Oliet, Narciso
PB - Springer
T2 - 13th International Workshop on Rewriting Logic and Its Applications, WRLA 2020
Y2 - 20 October 2020 through 22 October 2020
ER -