A Compositional Semantic Basis for the Analysis of
Equational Horn Programs
Author
María Alpuente, Moreno Falaschi and Germán Vidal
Abstract
We introduce a compositional characterization of the operational semantics
of equational Horn programs. Then we show that this semantics and the
standard operational semantics based on (basic) narrowing coincide. We
define an abstract narrower mimicking this semantics, and show how it can
be used as a basis for efficient AND-compositional program analysis. As an
application of our framework, we show a compositional analysis to detect
the unsatisfiability of an equation set with respect to a given
equational theory.
We also show that our method allows us to perform computations and analysis
incrementally in a Constraint Equational setting and that the test of
satisfiability in this setting can be done in parallel.
Keywords
Semantic analysis, compositionality, equational
logic programming, conditional term rewriting systems.