INJECTIVITY OF COMPOSITE FUNCTIONS

The problem of deciding injectivity of functions is addressed. The fun ctions under consideration are compositions of more basic functions fo r which information about injectivity properties is available. We pres ent an algorithm which will often be able to prove that such a composi te function is injective. This algorithm constructs a set of propositi onal Horn clause axioms from the function specification and the availa ble information about the basic functions. The existence of a proof of injectivity is then reduced to the problem of propositional Horn clau se deduction. Dowling and Gallier have designed several very fast algo rithms for this problem, the efficiency of which our algorithm inherit s. The proof of correctness of the algorithm amounts to showing soundn ess and completeness of the generated Horn clause axioms.