Download PDFOpen PDF in browser

Efficiency of a good but not linear nominal unification algorithm

EasyChair Preprint no. 243

8 pagesDate: June 8, 2018


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.


Keyphrases: Binding operations, de bruijn number, efficiency, unification, α-conversion

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
  author = {Weixi Ma and Jeremy Siek and David Christiansen and Daniel Friedman},
  title = {Efficiency of a good but not linear nominal unification algorithm},
  howpublished = {EasyChair Preprint no. 243},
  doi = {10.29007/9x4c},
  year = {EasyChair, 2018}}
Download PDFOpen PDF in browser