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).

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 η.

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.

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 Parametric Matroid of Rough Set

2015 ◽  
Vol 23 (06) ◽  
pp. 893-908 ◽  
Author(s):  
Yanfang Liu ◽  
Hong Zhao ◽  
William Zhu
Keyword(s):  
Rough Set ◽  
Equivalence Relation ◽  
Rough Sets ◽  
Rough Set Theory ◽  
Attribute Reduction ◽  
Independent Set ◽  
Approximation Operator ◽  
Approximation Number ◽  
Lower Approximation ◽  
The One

Rough set is mainly concerned with the approximations of objects through an equivalence relation on a universe. Matroid is a generalization of linear algebra and graph theory. Recently, a matroidal structure of rough sets is established and applied to the problem of attribute reduction which is an important application of rough set theory. In this paper, we propose a new matroidal structure of rough sets and call it a parametric matroid. On the one hand, for an equivalence relation on a universe, a parametric set family, with any subset of the universe as its parameter, is defined through the lower approximation operator. This parametric set family is proved to satisfy the independent set axiom of matroids, therefore a matroid is generated, and we call it a parametric matroid of the rough set. Through the lower approximation operator, three equivalent representations of the parametric set family are obtained. Moreover, the parametric matroid of the rough set is proved to be the direct sum of a partition-circuit matroid and a free matroid. On the other hand, partition-circuit matroids are well studied through the lower approximation number, and then we use it to investigate the parametric matroid of the rough set. Several characteristics of the parametric matroid of the rough set, such as independent sets, bases, circuits, the rank function and the closure operator, are expressed by the lower approximation number.

scholarly journals Quotienting the delay monad by weak bisimilarity

2017 ◽  
Vol 29 (1) ◽  
pp. 67-92 ◽  
Author(s):  
JAMES CHAPMAN ◽  
TARMO UUSTALU ◽  
NICCOLÒ VELTRI
Keyword(s):  
Computer Science ◽  
Equivalence Relation ◽  
Type Theory ◽  
Partial Functions ◽  
Homotopy Type Theory ◽  
Inductive Type ◽  
Alternative Approach ◽  
The One ◽  
Axiom Of Countable Choice

The delay datatype was introduced by Capretta (Logical Methods in Computer Science, 1(2), article 1, 2005) as a means to deal with partial functions (as in computability theory) in Martin-Löf type theory. The delay datatype is a monad. It is often desirable to consider two delayed computations equal, if they terminate with equal values, whenever one of them terminates. The equivalence relation underlying this identification is called weak bisimilarity. In type theory, one commonly replaces quotients with setoids. In this approach, the delay datatype quotiented by weak bisimilarity is still a monad–a constructive alternative to the maybe monad. In this paper, we consider the alternative approach of Hofmann (Extensional Constructs in Intensional Type Theory, Springer, London, 1997) of extending type theory with inductive-like quotient types. In this setting, it is difficult to define the intended monad multiplication for the quotiented datatype. We give a solution where we postulate some principles, crucially proposition extensionality and the (semi-classical) axiom of countable choice. With the aid of these principles, we also prove that the quotiented delay datatype delivers free ω-complete pointed partial orders (ωcppos).Altenkirch et al. (Lecture Notes in Computer Science, vol. 10203, Springer, Heidelberg, 534–549, 2017) demonstrated that, in homotopy type theory, a certain higher inductive–inductive type is the free ωcppo on a type X essentially by definition; this allowed them to obtain a monad of free ωcppos without recourse to a choice principle. We notice that, by a similar construction, a simpler ordinary higher inductive type gives the free countably complete join semilattice on the unit type 1. This type suffices for constructing a monad, which is isomorphic to the one of Altenkirch et al. We have fully formalized our results in the Agda dependently typed programming language.

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 Principal Typings in a Restricted Intersection Type System for Beta Normal Forms with De Bruijn Indices

2010 ◽  
Vol 15 ◽  
pp. 69-82 ◽  
Author(s):  
Daniel Ventura ◽  
Mauricio Ayala-Rincón ◽  
Fairouz Kamareddine
Keyword(s):  
Normal Forms ◽  
Type System ◽  
De Bruijn ◽  
De Bruijn Indices
Sign in / Sign up

Export Citation Format

Share Document