scholarly journals A λ-calculus with explicit weakening and explicit substitution

2001 ◽  
Vol 11 (1) ◽  
pp. 169-206 ◽  
Author(s):  
RENÉ DAVID ◽  
BRUNO GUILLAUME
Keyword(s):  
Strong Normalization ◽  
Explicit Substitution ◽  
Explicit Substitutions ◽  
De Bruijn ◽  
De Bruijn Indices

Since Melliès showed that λσ (a calculus of explicit substitutions) does not preserve the strong normalization of the β-reduction, it has become a challenge to find a calculus satisfying the following properties: step-by-step simulation of the β-reduction, confluence on terms with metavariables, strong normalization of the calculus of substitutions and preservation of the strong normalization of the λ-calculus. We present here such a calculus. The main novelty of this calculus (given with de Bruijn indices) is the use of labels that represent updating functions and correspond to explicit weakening. A typed version is also presented.

Pure type systems with explicit substitutions

2015 ◽  
Vol 25 ◽  
Author(s):  
DANIEL FRIDLENDER ◽  
MIGUEL PAGANO
Keyword(s):  
Type Systems ◽  
Pure Type ◽  
Explicit Substitution ◽  
Explicit Substitutions ◽  
Pure Type Systems ◽  
De Bruijn ◽  
New Formulation ◽  
De Bruijn Indices ◽  
Meta Theory

AbstractWe introduce a new formulation of pure type systems (PTSs) with explicit substitution and de Bruijn indices and formally prove some of its meta-theory. Using techniques based on Normalisation by Evaluation, we prove that untyped conversion can be typed for predicative PTSs. Although this equivalence was settled by Siles and Herbelin for the conventional presentation of PTSs, we strongly conjecture that our proof method can also be applied to PTSs with η.

THE SOUNDNESS OF EXPLICIT SUBSTITUTION WITH NAMELESS VARIABLES

1998 ◽  
Vol 09 (03) ◽  
pp. 321-349
Author(s):  
FAIROUZ KAMAREDDINE
Keyword(s):  
Classical Calculus ◽  
Explicit Substitution ◽  
De Bruijn ◽  
De Bruijn Indices

We show the soundness of a λ-calculus ℬ where de Bruijn indices are used, substitution is explicit, and reduction is step-wise. This is done by interpreting ℬ in the classical calculus where the explicit substitution becomes implicit and de Bruijn indices become named variables. This is the first flat semantics of explicit substitution and step-wise reduction and the first clear account of exactly when α-reduction is needed.

scholarly journals Proof nets and explicit substitutions

2003 ◽  
Vol 13 (3) ◽  
pp. 409-450 ◽  
Author(s):  
ROBERTO DI COSMO ◽  
DELIA KESNER ◽  
EMMANUEL POLONOVSKI
Keyword(s):  
Equivalence Relation ◽  
Simulation Technique ◽  
Cut Elimination ◽  
Complex Mechanism ◽  
Explicit Substitutions ◽  
Proof Nets ◽  
De Bruijn ◽  
The One ◽  
De Bruijn Indices

We refine the simulation technique introduced in Di Cosmo and Kesner (1997) to show strong normalisation of $\l$-calculi with explicit substitutions via termination of cut elimination in proof nets (Girard 1987). We first propose a notion of equivalence relation for proof nets that extends the one in Di Cosmo and Guerrini (1999), and show that cut elimination modulo this equivalence relation is terminating. We then show strong normalisation of the typed version of the $\ll$-calculus with de Bruijn indices (a calculus with full composition defined in David and Guillaume (1999)) using a translation from typed $\ll$ to proof nets. Finally, we propose a version of typed $\ll$ with named variables, which helps to give a better understanding of the complex mechanism of the explicit weakening notation introduced in the $\ll$-calculus with de Bruijn indices (David and Guillaume 1999).

Explicit substitution calculi with de Bruijn indices and intersection type systems

2014 ◽  
Vol 23 (2) ◽  
pp. 295-340 ◽  
Author(s):  
D. L. Ventura ◽  
F. Kamareddine ◽  
M. Ayala-Rincon
Keyword(s):  
Type Systems ◽  
Explicit Substitution ◽  
De Bruijn ◽  
De Bruijn Indices

Cut rules and explicit substitutions

2001 ◽  
Vol 11 (1) ◽  
pp. 131-168 ◽  
Author(s):  
RENÉ VESTERGAARD ◽  
JOE WELLS
Keyword(s):  
Order Term ◽  
Term Rewriting ◽  
Cut Elimination ◽  
Cut Rule ◽  
Logical Deduction ◽  
Rewriting Systems ◽  
Explicit Substitution ◽  
Explicit Substitutions ◽  
Rewrite Rules ◽  
De Bruijn Indices

We introduce a method to associate calculi of proof terms and rewrite rules with cut elimination procedures for logical deduction systems (i.e., Gentzen-style sequent calculi) in the case of intuitionistic logic. We illustrate this method using two different versions of the cut rule for a variant of the intuitionistic fragment of Kleene's logical deduction system G3.Our systems are in fact calculi of explicit substitution, where the cut rule introduces an explicit substitution and the left-→ rule introduces a binding of the result of a function application. Cut propagation steps of cut elimination correspond to propagation of explicit substitutions, and propagation of weakening (to eliminate it) corresponds to propagation of index-updating operations. We prove various subject reduction, termination, and confluence properties for our calculi.Our calculi improve on some earlier calculi for logical deduction systems in a number of ways. By using de Bruijn indices, our calculi qualify as first-order term rewriting systems (TRS's), allowing us to use correctly certain results for TRS's about termination. Unlike in some other calculi, each of our calculi has only one cut rule and we do not need unusual features of sequents.We show that the substitution and index-updating mechanisms of our calculi work the same way as the substitution and index-updating mechanisms of Kamareddine and Ríos' λs and λt, two well-known systems of explicit substitution for the standard λ-calculus. By a change in the format of sequents, we obtain similar results for a known λ-calculus with variables and explicit substitutions, Rose's λbxgc.

scholarly journals Distribution of Variables in Lambda-Terms with Restrictions on De Bruijn Indices and De Bruijn Levels

10.37236/8579 ◽  
2019 ◽  
Vol 26 (4) ◽  
Author(s):  
Bernhard Gittenberger ◽  
Isabella Larcher
Keyword(s):  
The Other ◽  
Bounded Number ◽  
Mean And Variance ◽  
De Bruijn ◽  
De Bruijn Indices ◽  
Strange Phenomenon ◽  
Normally Distributed

We consider two special subclasses of lambda-terms that are restricted by a bound on the number of abstractions between a variable and its binding lambda, the so-called De-Bruijn index, or by a bound on the nesting levels of abstractions, i.e., the number of De Bruijn levels, respectively. We show that the total number of variables is asymptotically normally distributed for both subclasses of lambda-terms with mean and variance asymptotically equal to $Cn$ and $\tilde{C}n$, respectively, where the constants $C$ and $\tilde{C}$ depend on the bound that has been imposed. For the class of lambda-terms with bounded De Bruijn index we derive closed formulas for the constant. For the other class of lambda-terms that we consider, namely lambda-terms with a bounded number of De Bruijn levels, we show quantitative and distributional results on the number of variables, as well as abstractions and applications, in the different De Bruijn levels and thereby exhibit a so-called "unary profile" that attains a very interesting shape.  Our results give a combinatorial explanation of an earlier discovered strange phenomenon exhibited by the counting sequence of this particular class of lambda-terms. 

scholarly journals A unified treatment of syntax with binders

2012 ◽  
Vol 22 (4-5) ◽  
pp. 614-704 ◽  
Author(s):  
NICOLAS POUILLARD ◽  
FRANÇOIS POTTIER
Keyword(s):  
Natural Number ◽  
Data Structures ◽  
Transformation Function ◽  
Natural Numbers ◽  
Programming Error ◽  
Free Variables ◽  
De Bruijn ◽  
Abstract Interface ◽  
Representation Techniques ◽  
De Bruijn Indices

AbstractAtoms and de Bruijn indices are two well-known representation techniques for data structures that involve names and binders. However, using either technique, it is all too easy to make a programming error that causes one name to be used where another was intended. We propose an abstract interface to names and binders that rules out many of these errors. This interface is implemented as a library in Agda. It allows defining and manipulating term representations in nominal style and in de Bruijn style. The programmer is not forced to choose between these styles: on the contrary, the library allows using both styles in the same program, if desired. Whereas indexing the types of names and terms with a natural number is a well-known technique to better control the use of de Bruijn indices, we index types with worlds. Worlds are at the same time more precise and more abstract than natural numbers. Via logical relations and parametricity, we are able to demonstrate in what sense our library is safe, and to obtain theorems for free about world-polymorphic functions. For instance, we prove that a world-polymorphic term transformation function must commute with any renaming of the free variables. The proof is entirely carried out in Agda.

Sign in / Sign up

Export Citation Format

Share Document