Archive for the 'alphaProlog' Category

Relating nominal and higher-order abstract syntax specifications

By Andrew Gacek, from PPDP 2010, available from Andrew Gacek’s website:

Nominal abstract syntax and higher-order abstract syntax provide a means for describing binding structure which is higher-level than traditional techniques. These approaches have spawned two different communities which have developed along similar lines but with subtle differences that make them difficult to relate. The nominal abstract syntax community has devices like names, freshness, name-abstractions with variable capture, and the new-quantifier, whereas the higher-order abstract syntax community has devices like lambda-binders, lambda conversion, raising, and the nabla-quantifier. This paper aims to unify these communities and provide a concrete correspondence between their different devices. In particular, we develop a semantics-preserving translation from alpha-Prolog, a nominal abstract syntax based logic programming language, to G-, a higher-order abstract syntax based logic programming language. We also discuss higher-order judgments, a common and powerful tool for specifications with higher-order abstract syntax, and we show how these can be incorporated into G-. This establishes G- as a language with the power of higher-order abstract syntax, the fine-grained variable control of nominal specifications, and the desirable properties of higher-order judgments.


Equivariant unification

By James Cheney, from RTA 2005, available from James Cheney’s website:

Nominal logic is a variant of first-order logic with special facilities for reasoning about names and binding based on the underlying concepts of swapping and freshness. It serves as the basis of logic programming and term rewriting techniques that provide similar advantages to, but remain simpler than, higher-order logic programming or term rewriting systems. Previous work on nominal rewriting and logic programming has relied on nominal unification, that is, unification up to equality in nominal logic. However, because of nominal logic’s equivariance property, these applications require a stronger form of unification, which we call equivariant unification. Unfortunately, equivariant unification and matching are NP-hard decision problems. This paper presents an algorithm for equivariant unification that produces a complete set of finitely many solutions, as well as NP decision procedure and a version that enumerates solutions one at a time. In addition, we present a polynomial time algorithm for swapping-free equivariant matching, that is, for matching problems in which the swapping operation does not appear.

alphaKanren: A fresh name in nominal logic programming

By William E. Bird and Daniel P. Friedman, from WSFP 2007, available from William E. Bird’s website:

We present αKanren, an embedding of nominal logic programming in Scheme. αKanren is inspired by αProlog and MLSOS, and allows programmers to easily write interpreters, type inferencers, and other programs that must reason about scope and binding. αKanren subsumes the functionality, syntax, and implementation of miniKanren, itself an embedding of logic programming in Scheme. We present the complete implementation of αKanren, written in portable R 5 RS Scheme. In addition to the implementation, we provide introductions to miniKanren and αKanren, and several example programs, including a type inferencer for the simply typed λ-calculus.

Scheme source files can be found here.

alpha Prolog: A logic programming language with names, binding and alpha-equivalence

By James Cheney and Christian Urban, from ICLP2004, available from the alphaProlog website:

There are two well-known approaches to programming with names, binding, and alpha-equivalence up to consistent renaming: representing names and bindings as concrete identifiers in a first-order language (such as Prolog), or encoding names and bindings as variables and abstractions in a higher-order language (such as Lambda-Prolog). However, both approaches have drawbacks: the former often involves stateful name-generation and requires manual definitions for alpha-equivalence and capture-avoiding substitution, and the latter is semantically very complicated, so reasoning about programs written using either approach can be very difficult.

Gabbay and Pitts have developed a new approach to encoding abstract syntax with binding based on primitive operations of name-swapping and freshness. This paper presents alphaProlog, a logic programming language that uses this approach, along with several illustrative example programs and an operational semantics.

Example programs, and more, are available from the alphaProlog website.