Constrained narrowing for conditional equational theories modulo axioms
详细信息 查看全文
- 作者：Andrew Cholewaa ; acholew2@illinois.edu" class="auth_mail" title="E-mail the corresponding author ; Santiago Escobarb ; sescobar@dsic.upv.es" class="auth_mail" title="E-mail the corresponding author ; José ; Meseguera ; meseguer@illinois.edu" class="auth_mail" title="E-mail the corresponding author
- 关键词：Narrowing modulo ; Conditional narrowing ; Constrained variants ; Constrained unification ; Layered narrowing
- 刊名：Science of Computer Programming
- 出版年：2015
- 出版时间：15 November 2015
- 年：2015
- 卷：112
- 期：part_P1
- 页码：24-57
- 全文大小：915 K
文摘
For an unconditional equational theory (Σ,E) whose oriented equations 
are confluent and terminating, narrowing provides an E -unification algorithm. This has been generalized by various authors in two directions: (i) by considering unconditional equational theories (Σ,E∪B) where the are confluent, terminating and coherent modulo axioms B , and (ii) by considering conditional equational theories. Narrowing for a conditional theory (Σ,E∪B) has also been studied, but much less and with various restrictions. In this paper we extend these prior results by allowing conditional equations with extra variables in their conditions, provided the corresponding rewrite rules are confluent, strictly coherent, operationally terminating modulo B and satisfy a natural determinism condition allowing incremental computation of matching substitutions for their extra variables. We also generalize the type structure of the types and operations in Σ to be order-sorted. The narrowing method we propose, called constrained narrowing, treats conditions as constraints whose solution is postponed. This can greatly reduce the search space of narrowing and allows notions such as constrained variant and constrained unifier that can cover symbolically possibly infinite sets of actual variants and unifiers. It also supports a hierarchical method of solving constraints. We give an inference system for hierarchical constrained narrowing modulo B and prove its soundness and completeness.
are confluent and terminating, narrowing provides an E -unification algorithm. This has been generalized by various authors in two directions: (i) by considering unconditional equational theories (Σ,E∪B) where the are confluent, terminating and coherent modulo axioms B , and (ii) by considering conditional equational theories. Narrowing for a conditional theory (Σ,E∪B) has also been studied, but much less and with various restrictions. In this paper we extend these prior results by allowing conditional equations with extra variables in their conditions, provided the corresponding rewrite rules are confluent, strictly coherent, operationally terminating modulo B and satisfy a natural determinism condition allowing incremental computation of matching substitutions for their extra variables. We also generalize the type structure of the types and operations in Σ to be order-sorted. The narrowing method we propose, called constrained narrowing, treats conditions as constraints whose solution is postponed. This can greatly reduce the search space of narrowing and allows notions such as constrained variant and constrained unifier that can cover symbolically possibly infinite sets of actual variants and unifiers. It also supports a hierarchical method of solving constraints. We give an inference system for hierarchical constrained narrowing modulo B and prove its soundness and completeness.