Archive for the 'Explicit substitutions' Category

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.

Higher-order unification via explicit substitutions

By Gilles Dowek, Therese Hardin and Claude Kirchner, from Information and Computation, available from ScienceDirect:

Higher order unification is equational unification for βη-conversion. But it is not first order equational  unification, as substitution has to avoid capture. Thus, the methods for equational unification (such as narrowing) built upon grafting (i.e., substitution without renaming) cannot be used for higher order unification, which needs specific algorithms. Our goal in this paper is to reduce higher order unification to first order equational unification in a suitable theory. This is achieved by replacing substitution by grafting, but this replacement is not straightforward as it raises two major problems. First, some unification problems have solutions with grafting but no solution with substitution. Then equational unification algorithms rest upon the fact that grafting and reduction commute. But grafting and βη-reduction do not commute in λ-calculus and reducing an equation may change the set of its solutions. This difficulty comes from the interaction between the substitutions initiated by βη-reduction and the ones initiated by the unification process. Two kinds of variables are involved: those of βη-conversion and those of unification. So, we need to set up a calculus which distinguishes between these two kinds of variables and such that reduction and grafting commute. For this purpose, the application of a substitution of a reduction variable to a unification one must be delayed until this variable is instantiated. Such a separation and delay are provided by a calculus of explicit substitutions. Unification in such a calculus can be performed by well-known algorithms such as narrowing, but we present a specialised algorithm for greater efficiency. At last we show how to relate unification in λ-calculus and in a calculus with explicit substitutions. Thus, we come up with a new higher order unification algorithm which eliminates some burdens of the previous algorithms, in particular the functional handling of scopes. Huet’s algorithm can be seen as a specific strategy for our algorithm, since each of its steps can be decomposed into elementary ones, leading to a more atomic description of the unification process. Also, solved forms in λ-calculus can easily be computed from solved forms in λσ-calculus.

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.