Constrained narrowing for conditional equational theories modulo axioms

Andrew Cholewa, Santiago Escobar, José Meseguer

Research output: Contribution to journalArticlepeer-review


For an unconditional equational theory (Σ, E)whose oriented equations ΣEare 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 ΣEare 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 ΣEare confluent, strictly coherent, operationally terminating modulo Band satisfy a natural determinismcondition 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 variantand constrained unifierthat can cover symbolically possibly infinite sets of actual variants and unifiers. It also supports a hierarchicalmethod of solving constraints. We give an inference system for hierarchical constrained narrowing modulo Band prove its soundness and completeness.

Original languageEnglish (US)
Pages (from-to)24-57
Number of pages34
JournalScience of Computer Programming
Issue numberP1
StatePublished - 2015


  • Conditional narrowing
  • Constrained unification
  • Constrained variants
  • Layered narrowing
  • Narrowing modulo

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'Constrained narrowing for conditional equational theories modulo axioms'. Together they form a unique fingerprint.

Cite this