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.

• Type: Journal
• Year: 2010
• Where: FLOPS
• Authors: Naoki Nishida, Masahiko Sakai
• Keywords: Automated Reasoning, FLOPS 2010, Important Properties, Injectivity, Linear Treeless Functions