Abstract :
In general, functional programs are assumed to be non-ambiguous. A simple way to handle ambiguous definitions is to replace them by non-ambiguous ones containing complement problems, which in turn have to be transformed into explicit expressions. Finding an explicit formulation for a complement problem is the same as eliminating negation from the corresponding equational formula. This problem was already shown decidable for complement problems interpreted inT( ), and inT( )/=EwhenEis a permutative theory of Malʹcev. Here, we show that negation elimination is also decidable for linear complement problems interpreted inT( )/=AC, whereACis a set of associative and commutative axioms. We present a system of rules that transforms any linear complement problem into simple formulae, and we give a decision test for simple formulae which serves as a basis for the development of a negation elimination algorithm. In the case of non-linearAC-complement problems even satisfiability is an open problem, but we will show, using the previous results, that satisfiability is decidable for a particular class of non-linear problems: when variables do not occur directly belowAC-function symbols. Finally, we generalize the negation elimination results to a wider class of equational formulae moduloAC.
