Archive for the 'Nominal techniques' Category

Proof pearl: A new foundation for Nominal Isabelle

Ack!  Sorry for the severe lack of updates lately.  The blog hasn’t died (I’m in the process of moving countries).  Anyway…

By Christian Urban and Brian Huffman, from ITP 2010, available from Christian Urban’s website:

Pitts et al introduced a beautiful theory about names and binding based on the notions of permutation and support. The engineering challenge is to smoothly adapt this theory to a theorem prover environment, in our case Isabelle/HOL. We present a formalisation of this work that differs from our earlier approach in two important respects: First, instead of representing permutations as lists of pairs of atoms, we now use a more abstract representation based on functions. Second, whereas the earlier work modeled different sorts of atoms using different types, we now introduce a unified atom type that includes all sorts of atoms. Interestingly, we allow swappings, that is permutations build from two atoms, to be ill-sorted. As a result of these design changes, we can iron out inconveniences for the user, considerably simplify proofs and also drastically reduce the amount of custom ML-code. Furthermore we can extend the capabilities of Nominal Isabelle to deal with variables that carry additional information. We end up with a pleasing and formalised theory of permutations and support, on which we can build an improved and more powerful version of Nominal Isabelle.

Closed nominal rewriting and efficiently computable nominal algebra equality

By Maribel Fernandez and Murdoch J. Gabbay, from LFMTP 2010, available from Murdoch J. Gabbay’s website:

We analyse the relationship between nominal algebra and nominal rewriting, giving a new and concise presentation of equational deduction in nominal theories. With some new results, we characterise a subclass of equational theories for which nominal rewriting provides a complete procedure to check nominal algebra equality. This subclass includes specifications of lambda-calculus and first-order logic.

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.

A nominal relational model for local store

By Rasmus Mogelberg, accepted at MFPS 2010, available from Rasmus Mogelberg’s website:

Many authors have in recent work suggested using nominal sets as a framework for modelling local store because this allows for a more elementary development than the traditional presheaf models. However, when modelling the important principle of relational reasoning for local store all these models use families of relations indexed by relations on store, and thus essentially return to presheaf models on the relational level. In this paper we show how relational reasoning can also be modelled using nominal sets. Building on a model suggested by Pitts and Shinwell we construct a relational model for local store in nominal sets in which types are interpreted as relations. These relational interpretations of types capture, in a single relation for each type, the relational reasoning principle for local store which in previous models was captured using a family of relations for each type. The relational model also demonstrates how the relations constitute a model in their own right, which hopefully means that they can be used to construct better models. Using the relational model we construct a relational parametricity principle for the operation allocating local store, and we show how this implies the relational reasoning principle.

A name abstraction functor for named sets

By Vincenzo Ciancia and Ugo Montinari, from CMCS 2008, available from Vincenzo Ciancia’s website:

The problem of dening fully abstract operational models of name passing calculi has been given some elegant solutions, such as coalgebras over presheaf categories or over nominal sets. These formalisms fail to model garbage collection of unused names, hence they do not have nice properties with respects to finite state algorithms. The category of named sets, on the other hand, was designed for the purpose of supporting ecient algorithms to handle the semantics of name passing calculi. However the theory was developed in a rather ad-hoc fashion (e.g. the existence of a final coalgebra was only proved in the finite case). In this work we introduce a name abstraction functor for named sets and show that it provides a simple and effective notion of garbage collection of unused names. Along the way, we survey a number of needed results on the category of permutation algebras, an algebra-theoretic denition of nominal sets. In particular we give a formalization of the adjunction between abstraction and concretion, an example illustrating a nominal syntax alike handling of De Bruijn indexes, and an explicit functor to model the early semantics of the π -calculus in nominal sets.

Nominal domain theory for concurrency

By David Turner and Glynn Winskel, from CSL 2009, available from Glynn Winskel’s website:

This paper investigates a methodology of using FM (Fraenkel-Mostowski) sets, and the ideas of nominal set theory, to adjoin name generation to a semantic theory. By developing a domain theory for concurrency within FM sets the domain theory inherits types and operations for name generation, essentially without disturbing its original higher-order features. The original domain theory had a metalanguage HOPLA (Higher Order Process Language) and accordingly this expands to a metalanguage, Nominal HOPLA, with name generation (closely related to an earlier language new-HOPLA). Nominal HOPLA possesses an operational and denotational semantics which are related via soundness and adequacy results, again carried out within FM sets.

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.