Sciweavers

FLOPS
2008
Springer

Termination of Narrowing in Left-Linear Constructor Systems

13 years 5 months ago
Termination of Narrowing in Left-Linear Constructor Systems
Narrowing extends rewriting with logic capabilities by allowing free variables in terms and replacing matching with unification. Narrowing has been widely used in different contexts, ranging from theorem proving (e.g., protocol verification) to language design (e.g., it forms the basis of so called functional logic languages). Surprisingly, the termination of narrowing has been mostly overlooked. In this paper, we present new techniques for proving the termination of narrowing in left-linear constructor systems--a widely accepted class of systems in functional and functional logic programming--that allow us to reuse existing methods in the extensive literature on termination of rewriting.
Germán Vidal
Added 26 Oct 2010
Updated 26 Oct 2010
Type Conference
Year 2008
Where FLOPS
Authors Germán Vidal
Comments (0)