Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Avoiding Equivariant Unification
Authors: Christian Urban ; James Cheney
Date:Apr 2005
Publication Title:Proc. TLCA 2005
Publication Type:Conference Paper
alphaProlog is a logic programming language which is well-suited for rapid prototyping of type systems and operational semantics of typed lambda-calculi and many other languages involving bound names. In alphaProlog, the nominal unification algorithm of Urban, Pitts and Gabbay is used instead of first-order unification. However, although alphaProlog can be viewed as Horn-clause logic programming in Pitts nominal logic, proof search using nominal unification is incomplete in nominal logic. Because of nominal logics equivariance principle, complete proof search would require solving NP-hard equivariant unification problems. Nevertheless, the alphaProlog programs we studied run correctly without equivariant unification. In this paper, we give several examples of alphaProlog programs that do not require equivariant unification, develop a test for identifying such programs, and prove the correctness of this test via a proof-theoretic argument.
Links To Paper
springer official version
Bibtex format
author = { Christian Urban and James Cheney },
title = {Avoiding Equivariant Unification},
book title = {Proc. TLCA 2005},
year = 2005,
month = {Apr},
url = {,29,30;journal,140,2140;linkingpublicationresults,1:105633,1},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh