FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
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: