Archive for the 'de Bruijn indices' Category

Hybrid: A Defintional Two Level Approach to Reasoning with Higher-Order Abstract Syntax

By Amy Felty and Alberto Monigliano, accepted in the Journal of Automated Reasoning 2010, available from Amy Felty’s website:

Combining higher-order abstract syntax and (co)-induction in a logical framework is well known to be problematic. We describe the theory and the practice of a tool called Hybrid, within Isabelle/HOL and Coq, which aims to address many of these difficulties. It allows object logics to be represented using higher-order abstract syntax, and reasoned about using tactical theorem proving and principles of (co)induction. Moreover, it is definitional, which guarantees consistency within a classical type theory. The idea is to have a de Bruijn representation of λ-terms providing a definitional layer that allows the user to represent object languages using higher-order abstract syntax, while offering tools for reasoning about them at the higher level. In this paper we describe how to use Hybrid in a multi-level reasoning fashion, similar in spirit to other systems such as Twelf and Abella. By explicitly referencing provability in a middle layer called a specification logic, we solve the problem of reasoning by (co)induction in the presence of non-stratifiable hypothetical judgments, which allow very elegant and succinct specifications of object logic inference rules. We first demonstrate the method on a simple example, formally proving type soundness (subject reduction) for a fragment of a pure functional language, using a minimal intuitionistic logic as the specification logic. We then prove an analogous result for a continuation-machine presentation of the operational semantics of the same language, encoded this time in an ordered linear logic that serves as the specification layer. This example demonstrates the ease with which we can incorporate new specification logics, and also illustrates a significantly more complex object logic whose encoding is elegantly expressed using features of the new specification logic.

Advertisements

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 dening 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 ecient 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 finite 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 denition 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.

CINNI: A generic calculus of explicit substitutions and its application to lambda-, sigma- and pi-calculi

By Mark Oliver Stehr, from WRLA 2000, available from Mark Oliver Stehr’s website:

We approach the general problem of representing higher-order languages, that are usually equipped with special variable binding constructs, in a less specialized first-order framework such as membership equational logic and the corresponding version of rewriting logic. The solution we propose is based on CINNI, a new calculus of explicit substitutions that makes use of a term representation that contains both the standard named notation and de Bruijn’s indexed notation as special subcases. The calculus is parametric in the syntax of the object language, which allows us to apply it to different object languages such as λ-calculus, Abadi and Cardelli’s object calculus (ς-calculus) and Milner’s calculus of communicating mobile processes (π-calculus). As a practical result we obtain executable formal representations of these object languages in Maude with a representational distance close to zero.

Unembedding domain specific languages

By Robert Atkey, Sam Lindley and Jeremy Yallop, from ACM SIGPLAN Haskell Symposium 2009, available from Robert Atkey’s website:

Higher-order abstract syntax provides a convenient way of embedding domain-specific languages, but is awkward to analyse and manipulate directly.

We explore the boundaries of higher-order abstract syntax. Our key tool is the unembedding of embedded terms as de Bruijn terms, enabling intensional analysis. As part of our solution we present techniques for separating the definition of an embedded program from its interpretation, giving modular extensions of the embedded language, and different ways to encode the types of the embedded language.

Associated slides are available here, a video is available here, and Haskell code is available here.

De Bruijn notation as a nested datatype

By Richard Bird and Ross Paterson, in the Journal of Functional Programming, available from Ross Paterson’s website:

de Bruijn notation is a coding of lambda terms in which each occurrence of a bound variable x is replaced by a natural number, indicating the `distance’ from the occurrence to the abstraction that introduced x. One might suppose that in any datatype for representing de Bruijn terms, the distance restriction on numbers would have to maintained as an explicit datatype invariant. However, by using a nested (or non-regular) datatype, we can define a representation in which all terms are well-formed, so that the invariant is enforced automatically by the type system.

Programming with nested types is only a little more difficult than programming with regular types, provided we stick to well-established structuring techniques. These involve expressing inductively defined functions in terms of an appropriate fold function for the type, and using fusion laws to establish their properties. In particular, the definition of lambda abstraction and beta reduction is particularly simple, and the proof of their associated properties is entirely mechanical.

Associated Haskell files are here.

Proof pearl: de Bruijn terms really do work

By Michael Norrish and Rene Vestergaard, from TPHOLs 2007, available from Michael Norrish’s website:

Placing our result in a web of related mechanised results, we give a direct proof that the de Bruijn λ-calculus (a la Huet, Nipkow and Shankar) is isomorphic to an α-quotiented λ-calculus. In order to establish the link, we introduce an “index-carrying” abstraction mechanism over de Bruijn terms, and consider it alongside a simplified substitution mechanism. Relating the new notions to those of the α-quotiented and the proper
de Bruijn formalisms draws on techniques from the theory of nominal sets.

Slides from a related presentation are available here.

Bridging de Bruijn indices and variable names in explicit substitutions calculi

By Fairouz Kamareddine and Alejandro Rios, in the Logic Journal of the Interest Group in Pure and Applied Logic, available from Fairouz Kamareddine’s website:

Calculi of explicit substitutions have almost always been presented using de Bruijn indices with the aim of avoiding alpha-conversion and being as close to machines as possible. De Bruijn indices however, though very suitable for the machine, are difficult to human users. This is the reason for a renewed interest in systems of explicit substitutions using variable names. We believe that the study of these systems should not develop without being well-tied to existing work on explicit substitutions. The aim of this paper is to establish a bridge between explicit substitutions using de Bruijn indices and using variable names and to do so, we provide the lambda-t-calculus: a lambda-calculus a la de Bruijn which can be translated into a lambda-calculus with explicit substitutions written with variables names. We present explicitly this translation and use it to obtain preservation of strong normalisation for lambda-t. Moreover, we show several properties of lambda-t, including confluence on closed terms and e#ciency to simulate beta-reduction. Furthermore, lambda-t is a good example of a calculus written in the lambda-s-style (cf. [19]) that possesses the updating mechanism of the calculi a la lambda-sigma.