Simple Proofs of Characterizing Strong Normalization for Explicit Substitution Calculi

2007 ◽  
pp. 257-272 ◽  
Author(s):  
Kentaro Kikuchi
Keyword(s):  
Strong Normalization ◽  
Explicit Substitution

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.

scholarly journals Explicit substitution on the edge of strong normalization

1999 ◽  
Vol 211 (1-2) ◽  
pp. 375-395 ◽  
Author(s):  
Roel Bloo ◽  
Herman Geuvers
Keyword(s):  
Strong Normalization ◽  
Explicit Substitution

scholarly journals Weak normalization implies strong normalization in a class of non-dependent pure type systems

2001 ◽  
Vol 269 (1-2) ◽  
pp. 317-361 ◽  
Author(s):  
Gilles Barthe ◽  
John Hatcliff ◽  
Morten Heine Sørensen
Keyword(s):  
Type Systems ◽  
Strong Normalization ◽  
Pure Type ◽  
Pure Type Systems

scholarly journals Reduction in first-order logic compared with reduction in implicational logic

2007 ◽  
Vol 5 ◽  
Author(s):  
Tigran M. Galoyan
Keyword(s):  
Natural Deduction ◽  
Order Logic ◽  
First Order Logic ◽  
Strong Normalization ◽  
First Order ◽  
Reduction Sequence

In this paper we discuss strong normalization for natural deduction in the →∀-fragment of first-order logic. The method of collapsing types is used to transfer the result (concerning strong normalization) from implicational logic to first-order logic. The result is improved by a complement, which states that the length of any reduction sequence of derivation term r in first-order logic is equal to the length of the corresponding reduction sequence of its collapse term rc in implicational logic.

Sign in / Sign up

Export Citation Format

Share Document