×

Avoiding equivariance in Alpha-Prolog. (English) Zbl 1114.68027

Urzyczyn, Paweł (ed.), Typed lambda calculi and applications. 7th international conference, TLCA 2005, Nara, Japan, April 21–23, 2005. Proceedings. Berlin: Springer (ISBN 3-540-25593-1/pbk). Lecture Notes in Computer Science 3461, 401-416 (2005).
Summary: \(\alpha\)Prolog 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 \(\alpha\)Prolog, the nominal unification algorithm of Urban, Pitts and Gabbay is used instead of first-order unification. However, although \(\alpha\)Prolog 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 logic’s equivariance principle, complete proof search would require solving NP-hard equivariant unification problems. Nevertheless, the \(\alpha\)Prolog programs we studied run correctly without equivariant unification. In this paper, we give several examples of \(\alpha\)Prolog 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.
For the entire collection see [Zbl 1070.03001].

MSC:

68N17 Logic programming
68N18 Functional programming and lambda calculus
PDFBibTeX XMLCite
Full Text: DOI