- Abstract:
-
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
- @InProceedings{EDI-INF-RR-0323,
- author = {
Christian Urban
and James Cheney
},
- title = {Avoiding Equivariant Unification},
- book title = {Proc. TLCA 2005},
- year = 2005,
- month = {Apr},
- url = {http://springerlink.metapress.com/app/home/contribution.asp?wasp=9cd0a2fb019c4b34be1634d5bb413579&referrer=parent&backto=issue,29,30;journal,140,2140;linkingpublicationresults,1:105633,1},
- }
|
