Equational Generalization Problems with Atom-Variables

doi:10.1007/978-3-032-07021-0_8

Equational Generalization Problems with Atom-Variables

2026-01-01

0

PRE

AI

A

Alexander Baumgartner

T

Temur Kutsia

D

Daniele Nantes-Sobrinho *

M

Manfred Schmidt-Schauß

DOI：10.1007/978-3-032-07021-0_8

Original

Original request for help

Save

Abstract

En 中文

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 (A), commutative (C), and associative-commutative (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.

Keywords:

Generalization Problems

Binders

Equational Theories

Equational Generalization Problems with Atom-Variables

Abstract

Journal

Organization