Efficiency of a Good but not Linear Nominal Unification Algorithm

## Authors: Weixi Ma, Jeremy Siek, David Christiansen and Daniel Friedman

## Paper Information

Title: | Efficiency of a Good but not Linear Nominal Unification Algorithm |

Authors: | Weixi Ma, Jeremy Siek, David Christiansen and Daniel Friedman |

Proceedings: | UNIF Extended abstracts |

Editors: | Mauricio Ayala-Rincon and Philippe Balbiani |

Keywords: | α-conversion, Binding operations, Efficiency, Unification |

Abstract: | ABSTRACT. We present a nominal unification algorithm that runs in O(n × 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 α-equivalent. We preserve names while using special representations of de Bruijn numbers. Operations on name handling, i.e., deciding the α-equivalence of two names and inferring a name that α-equals to a given one, are in constant time. To reduce an arbitrary unification problem to such name handlings, we preprocess the unification terms with the idea of Martelli-Montanari. |

Pages: | 8 |

Talk: | Jul 07 17:50 (Session 31S: Nominal Unification and Formalisations) |

Paper: |