Avoiding Equivariance in Alpha-Prolog

8 years 11 months ago
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.
Christian Urban, James Cheney
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where TLCA
Authors Christian Urban, James Cheney
Comments (0)