Avoiding Equivariance in Alpha-Prolog

αProlog is a logic programming language which is well-suited for rapid prototyping of type systems and operational semantics of typed λ-calculi and many other languages involving bound names. In αProlog, the nominal unification algorithm of Urban, Pitts and Gabbay is used instead of first-order unification. However, although α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 αProlog programs we studied run correctly without equivariant unification. In this paper, we give several examples of α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.

• Type: Conference
• Year: 2005
• Where: TLCA
• Authors: Christian Urban, James Cheney
• Keywords: Equivariant Unification, Nominal Logic, Nominal Unification, Theoretical Computer Science, TLCA 2005