Extra Variables Can Be Eliminated from Functional Logic Programs

Programs in modern functional logic languages are rewrite systems following the constructor discipline but where confluence and termination are not required, thus defining possibly non strict and non-deterministic functions. While in practice and in some theoretical papers rewrite rules can contain extra variables in right hand sides, some other works and techniques do not consider such possibility. We address in this paper the question of whether extra variables can be eliminated in such kind of functional logic programs, proving the soundness and completeness of an easy solution that takes advantage of the possibility of non-confluence. Although the focus of the paper is mainly theoretical, we give some first steps towards the practical usability of the technique