Generalization problems in languages with binders involve computing the most common structure between expressions while respecting bound variable renaming and freshness constraints. These problems often lack a least general solution. However, leveraging nominal techniques, we previously demonstrated that a semantic approach with atom-variables enables the elimination of redundant solutions and allows for computing unique least general generalizations (LGGs). In this work, we extend this approach to handle associative ( \(\texttt {A}\) ), commutative ( \(\mathtt{{C}}\) ), and associative-commutative ( \(\mathtt{{AC}}\) ) equational theories. A key challenge arises from solving equivariance problems while taking into account these equational theories, as identifying redundant generalizations requires recognizing when one expression (with binders) is a renaming of another while possibly considering permutations of sub-expressions. This unexpected interaction between renaming and equational reasoning made this particularly difficult, necessitating semantic tests modulo theories within the equivariance algorithm.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Equational Generalization Problems with Atom-Variables

  • Alexander Baumgartner,
  • Temur Kutsia,
  • Daniele Nantes-Sobrinho,
  • Manfred Schmidt-Schauß

摘要

Generalization problems in languages with binders involve computing the most common structure between expressions while respecting bound variable renaming and freshness constraints. These problems often lack a least general solution. However, leveraging nominal techniques, we previously demonstrated that a semantic approach with atom-variables enables the elimination of redundant solutions and allows for computing unique least general generalizations (LGGs). In this work, we extend this approach to handle associative ( \(\texttt {A}\) ), commutative ( \(\mathtt{{C}}\) ), and associative-commutative ( \(\mathtt{{AC}}\) ) equational theories. A key challenge arises from solving equivariance problems while taking into account these equational theories, as identifying redundant generalizations requires recognizing when one expression (with binders) is a renaming of another while possibly considering permutations of sub-expressions. This unexpected interaction between renaming and equational reasoning made this particularly difficult, necessitating semantic tests modulo theories within the equivariance algorithm.