Towards Generalization Methods for Purely Idempotent Equational Theories

Description

In Generalisation de termes en theorie equationnelle. Cas associatif-commutatif, a pair of terms was presented over the language { f (, ), g(, ), a, b}, where f and g are interpreted over an idempotent equational theory, i.e. g(x, x) = x and f (x, x) = x, resulting in an infinite set of generalizations. While this result provides an answer to the complexity of the idempotent generalization problem for arbitrarily idempotent equational theories (theories with two or more idempotent functions) the complexity of generalization for equational theories with a single idempotent function symbols was left unsolved. We show that the two idempotent function symbols example can be encoded using a single idempotent function and two uninterpreted constants thus proving that idempotent generalization, even with a single idempotent function symbol, can result in an infinite set of generalizations. Based on this result we discuss approaches to handling generalization within idempotent equational theories.

Period	07 Jul 2018
Event title	UNIF 2018
Event type	Conference
Location	United KingdomShow on map