Unification under one-sided distributivity with a multiplicative unit

Abstract

Unification in the equationsl theory of one-sided distributivity (x ^* (y+z)=x ^* y + x^*z) and a multiplicative unit (x ^* l = l ^* x = x) is shown to be decidable. The decision algorithm splits the problem into two independent ones: One for terms representing 1- sums, i.e., terms that are built from the symbol 1 and +. This problem can be solved using the decision algorithm for associativity including constant restrictions. The associativity stems from the associativity of the ^*-symbol for 1-sums. The other subproblem is of a different kind. The associativity comes from (rather restricted) second-order terms. The idea here is to flatten terms of the form t ₁ ^*(t ₂ ^*...^* t _{n- 1} ^* t _n )...) to t ₁ ^* t ₂ ^*...^* t _n− 1^*t_n and permitting associative variables. The corresponding final problems can be solved using the decision algorithm for associativity including constant restrictions given by K. Schulz.