Switch to: References

Add citations

You must login to add citations.
  1. Continuous Normalization for the Lambda-Calculus and Gödel’s T.Klaus Aehlig & Felix Joachimski - 2005 - Annals of Pure and Applied Logic 133 (1-3):39-71.
    Building on previous work by Mints, Buchholz and Schwichtenberg, a simplified version of continuous normalization for the untyped λ-calculus and Gödel’s is presented and analysed in the coalgebraic framework of non-wellfounded terms with so-called repetition constructors.The primitive recursive normalization function is uniformly continuous w.r.t. the natural metric on non-wellfounded terms. Furthermore, the number of necessary repetition constructors is locally related to the number of reduction steps needed to reach the normal form and its size.It is also shown how continuous normal (...)
    Direct download (4 more)  
    Export citation  
    Bookmark   1 citation  
  • Strong Normalization via Natural Ordinal.Daniel Durante Pereira Alves - 1999 - Dissertation,
    The main objective of this PhD Thesis is to present a method of obtaining strong normalization via natural ordinal, which is applicable to natural deduction systems and typed lambda calculus. The method includes (a) the definition of a numerical assignment that associates each derivation (or lambda term) to a natural number and (b) the proof that this assignment decreases with reductions of maximal formulas (or redex). Besides, because the numerical assignment used coincide with the length of a specific sequence of (...)
    Direct download  
    Export citation  
  • How to Assign Ordinal Numbers to Combinatory Terms with Polymorphic Types.William R. Stirton - 2012 - Archive for Mathematical Logic 51 (5-6):475-501.
    The article investigates a system of polymorphically typed combinatory logic which is equivalent to Gödel’s T. A notion of (strong) reduction is defined over terms of this system and it is proved that the class of well-formed terms is closed under both bracket abstraction and reduction. The main new result is that the number of contractions needed to reduce a term to normal form is computed by an ε 0-recursive function. The ordinal assignments used to obtain this result are also (...)
    Direct download (3 more)  
    Export citation  
    Bookmark   1 citation