Unification under associativity and idempotence is of type nullary (Q580999)

Unification is concerned with solving equations given an equational theory. An important problem is to find representative sets of most general unifiers (solutions) for particular equational theories. In the paper it is shown that free idempotent semigroups (bands) including free constants have unification type zero. An example is constructed such that every complete set of unifiers contains redundant unifiers. This is the first known natural equational theory with this property.