Matthew R. Lakin - Constraint solving in non-permutative nominal abstract syntax

lmcs:995 - Logical Methods in Computer Science, August 25, 2011, Volume 7, Issue 3 - https://doi.org/10.2168/LMCS-7(3:6)2011
Constraint solving in non-permutative nominal abstract syntaxArticle

Authors: Matthew R. Lakin

    Nominal abstract syntax is a popular first-order technique for encoding, and reasoning about, abstract syntax involving binders. Many of its applications involve constraint solving. The most commonly used constraint solving algorithm over nominal abstract syntax is the Urban-Pitts-Gabbay nominal unification algorithm, which is well-behaved, has a well-developed theory and is applicable in many cases. However, certain problems require a constraint solver which respects the equivariance property of nominal logic, such as Cheney's equivariant unification algorithm. This is more powerful but is more complicated and computationally hard. In this paper we present a novel algorithm for solving constraints over a simple variant of nominal abstract syntax which we call non-permutative. This constraint problem has similar complexity to equivariant unification but without many of the additional complications of the equivariant unification term language. We prove our algorithm correct, paying particular attention to issues of termination, and present an explicit translation of name-name equivariant unification problems into non-permutative constraints.


    Volume: Volume 7, Issue 3
    Published on: August 25, 2011
    Imported on: January 3, 2011
    Keywords: Computer Science - Programming Languages,D.3.1, D.3.3

    2 Documents citing this article

    Consultation statistics

    This page has been seen 1391 times.
    This article's PDF has been downloaded 280 times.