Equational Generalization Problems with Atom-Variables

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

2026-01-01

PRE

Alexander Baumgartner

Temur Kutsia

Daniele Nantes-Sobrinho *

Manfred Schmidt-Schauß

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

原文链接

原文求助

摘要

En 中文

包含绑定符的语言中的泛化问题涉及在尊重绑定变量重命名和新鲜性约束的同时计算表达式之间的最常见结构。这些问题通常缺乏最一般的解决方案。然而，利用名义技术，我们先前证明了原子变量的语义方法能够消除冗余解，并允许计算唯一的泛化最小公共结构（LGGs）。在本工作中，我们将此方法扩展以处理结合性（A）、交换性（C）和结合-交换性（AC）方程理论。一个关键挑战来自于解决等变性问题时需要考虑这些方程理论，因为识别冗余泛化要求识别一个（含绑定符的）表达式何时是另一个的重命名，同时可能考虑子表达式的排列。重命名与方程推理之间的这种意外交互使得这一问题尤为困难，需要在等变性算法中引入模理论的语义测试。

Keyword:

Generalization Problems

Binders

Equational Theories