{'fraction_non_alphanumeric': 0.02564102564102564, 'fraction_numerical': 0.016826923076923076, 'mean_word_length': 4.8915094339622645, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Unital Anti-Unification: Type and Algorithms

Unital equational theories are deﬁned by axioms that assert the existence of the unit element for 9 some function symbols. We study anti-uniﬁcation (AU) in unital theories and address the problems 10 of establishing generalization type and designing anti-uniﬁcation algorithms. First, we prove that 11 when the term signature contains at least two unital functions, anti-uniﬁcation is of the nullary 12 type by showing that there exists an AU problem, which does not have a minimal complete set of 13 generalizations. Next, we consider two special cases: the linear variant and the fragment with only 14 one unital symbol, and design AU algorithms for them. The algorithms are terminating, sound, 15 complete, and return tree grammars from which the set of generalizations can be constructed. 16 Anti-uniﬁcation for both special cases is ﬁnitary. Further, the algorithm for the one-unital fragment 17 is extended to the unrestricted case. It terminates and returns a tree grammar which produces an 18 inﬁnite set of generalizations. At the end, we discuss how the nullary type of unital anti-uniﬁcation 19 might aﬀect the anti-uniﬁcation problem in some combined theories, and list some open questions.