Abstract

In this paper we study the non-determinism between the inference rules of the lazy narrowing calculus LNC of Middeldorp, Okui, and Ida. We show that all non-determinism can be removed without losing the important completeness property by restricting the underlying term rewriting systems to left-linear confluent constructor systems and interpreting equality as strict equality. For the subclass of orthogonal constructor systems the resulting narrowing calculus is shown to have the nice property that solutions computed by different derivations starting from the same goal are incomparable.

BibTeX Entry

@article{MO-JSC98,
 author    = "Aart Middeldorp and Satoshi Okui",
 title     = "A Deterministic Lazy Narrowing Calculus",
 journal   = "Journal of Symbolic Computation",
 volume    = 25,
 number    = 6,
 pages     = "733--757",
 year      = 1998,
 doi       = "10.1006/jsco.1997.0197"
}