| ||||
| ||||
![]() Title:Efficiency of a good but not linear nominal unification algorithm Conference:UNIF 2018 Tags:Binding operations, Efficiency, Unification and α-conversion Abstract: We present a nominal unification algorithm that runs in $O(n \times log(n) \times G(n))$ time, where $G$ is the functional inverse of Ackermann's function. Nominal unification generates a set of variable assignments if there exists one, that makes terms involving binding operations $\alpha$-equivalent. We preserve names while using special representations of de Bruijn numbers to enable efficient name management. We use Martelli-Montanari style multi-equation reduction to generate these name management problems from arbitrary unification terms.
Efficiency of a good but not linear nominal unification algorithm ![]() Efficiency of a good but not linear nominal unification algorithm | ||||
Copyright © 2002 – 2025 EasyChair |