Sciweavers

Share
FLOPS
2010
Springer

Proving Injectivity of Functions via Program Inversion in Term Rewriting

8 years 5 months ago
Proving Injectivity of Functions via Program Inversion in Term Rewriting
Injectivity is one of the important properties for functions while it is undecidable in general and decidable for linear treeless functions. In this paper, we show new sufficient conditions for injectivity of functions in term rewriting, which are based on program inversion. More precisely, we show that functions defined by non-erasing, convergent and sufficiently complete constructor rewrite systems are injective if the corresponding inverse-computation rewrite systems generated by the inversion framework are innermost-confluent. By using this property, we also show a syntactic sufficient-condition of injectivity.
Naoki Nishida, Masahiko Sakai
Added 25 Jan 2011
Updated 25 Jan 2011
Type Journal
Year 2010
Where FLOPS
Authors Naoki Nishida, Masahiko Sakai
Comments (0)
books