Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Nominal anti-unification

Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret

TL;DR

This work studies nominal anti-unification for terms-in-context, aiming to compute least general generalizations when a finite base of atoms is used. A central challenge is equivariance: determining a permutation of atoms that makes two terms $\alpha$-equivalent within a freshness context. The authors prove existence and uniqueness of the $A$-based lgg (modulo $\alpha$-equivalence and renaming) and present a rule-based algorithm running in $O(n^5)$ time with $O(n^4)$ space, avoiding translations to higher-order unification. The approach yields a practical solution with a implemented library, and the results have potential applications in inductive learning and cloning detection where bindings are essential.

Abstract

We study nominal anti-unification, which is concerned with computing least general generalizations for given terms-in-context. In general, the problem does not have a least general solution, but if the set of atoms permitted in generalizations is finite, then there exists a least general generalization which is unique modulo variable renaming and $α$-equivalence. We present an algorithm that computes it. The algorithm relies on a subalgorithm that constructively decides equivariance between two terms-in-context. We prove soundness and completeness properties of both algorithms and analyze their complexity. Nominal anti-unification can be applied to problems were generalization of first-order terms is needed (inductive learning, clone detection, etc.), but bindings are involved.

Nominal anti-unification

TL;DR

This work studies nominal anti-unification for terms-in-context, aiming to compute least general generalizations when a finite base of atoms is used. A central challenge is equivariance: determining a permutation of atoms that makes two terms -equivalent within a freshness context. The authors prove existence and uniqueness of the -based lgg (modulo -equivalence and renaming) and present a rule-based algorithm running in time with space, avoiding translations to higher-order unification. The approach yields a practical solution with a implemented library, and the results have potential applications in inductive learning and cloning detection where bindings are essential.

Abstract

We study nominal anti-unification, which is concerned with computing least general generalizations for given terms-in-context. In general, the problem does not have a least general solution, but if the set of atoms permitted in generalizations is finite, then there exists a least general generalization which is unique modulo variable renaming and -equivalence. We present an algorithm that computes it. The algorithm relies on a subalgorithm that constructively decides equivariance between two terms-in-context. We prove soundness and completeness properties of both algorithms and analyze their complexity. Nominal anti-unification can be applied to problems were generalization of first-order terms is needed (inductive learning, clone detection, etc.), but bindings are involved.
Paper Structure (2 sections, 3 theorems, 8 equations, 1 figure)

This paper contains 2 sections, 3 theorems, 8 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Nominal Terms

Key Result

theorem thmcountertheorem

Let $F$ be a set of freshness formulas and $\nabla$ be a freshness context. Then ${{\sf FC}}(F) \subseteq \nabla$ iff $\nabla\vdash a\# t$ for all ${ a\# t}\in F$.

Figures (1)

  • Figure 1: The tree form and positions of the term $f(a.b.g((a\, b){\mkern 1mu\cdot \mkern 1mu} X,a), h(c))$.

Theorems & Definitions (4)

  • theorem thmcountertheorem
  • corollary thmcountercorollary
  • lemma thmcounterlemma
  • definition thmcounterdefinition