Normalization without reducibility

Annals of Pure and Applied Logic 107 (1-3):121-130 (2000)
  Copy   BIBTEX

Abstract

In [gallier], general results (due to Coppo, Dezani and Veneri) relating properties of pure lambda terms and their typability in some systems with conjunctive types are proved in a uniform way by using the reducibility method.This paper gives a very short proof of the same results (actually, one of them is a bit stronger) using purely arithmetical methods

Categories

Keywords

Reprint years

2001

DOI

10.1016/s0168-0072(00)00030-0

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,497

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Strong Enumeration Reducibilities.Roland Sh Omanadze & Andrea Sorbi - 2006 - Archive for Mathematical Logic 45 (7):869-912.
Some general results about proof normalization.Marc Aiguier & Delphine Longuet - 2010 - Logica Universalis 4 (1):1-29.
A semantical proof of the strong normalization theorem for full propositional classical natural deduction.Karim Nour & Khelifa Saber - 2006 - Archive for Mathematical Logic 45 (3):357-364.
On Nondeterminism, Enumeration Reducibility and Polynomial Bounds.Kate Copestake - 1997 - Mathematical Logic Quarterly 43 (3):287-310.
A New Reducibility between Turing‐ and wtt‐Reducibility.Sui Yuefei - 1994 - Mathematical Logic Quarterly 40 (1):106-110.
A characterization of the Δ⁰₂ hyperhyperimmune sets.Roland Sh Omanadze & Andrea Sorbi - 2008 - Journal of Symbolic Logic 73 (4):1407-1415.
On the logic of reducibility: Axioms and examples. [REVIEW]Karl-Georg Niebergall - 2000 - Erkenntnis 53 (1-2):27-61.
A short proof of the strong normalization of classical natural deduction with disjunction.René David & Karim Nour - 2003 - Journal of Symbolic Logic 68 (4):1277-1288.
Bounded enumeration reducibility and its degree structure.Daniele Marsibilio & Andrea Sorbi - 2012 - Archive for Mathematical Logic 51 (1-2):163-186.
Strong Normalization and Typability with Intersection Types.Silvia Ghilezan - 1996 - Notre Dame Journal of Formal Logic 37 (1):44-52.
Bounds in the Turing reducibility of functions.Karol Habart & K. Habart - 1992 - Mathematical Logic Quarterly 38 (1):423-430.
Supervenience and reducibility: An odd couple.Ausonio Marras - 1994 - Philosophical Quarterly 44 (171):215-222.
Supervenience, necessary coextensions, and reducibility.John Bacon - 1986 - Philosophical Studies 49 (March):163-76.

Analytics

Added to PP
2013-12-22

Downloads
15 (#953,911)

6 months
7 (#441,920)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

A domain model characterising strong normalisation.Ulrich Berger - 2008 - Annals of Pure and Applied Logic 156 (1):39-50.

Add more citations

References found in this work

Functional Characters of Solvable Terms.M. Coppo, M. Dezani-Ciancaglini & B. Venneri - 1981 - Mathematical Logic Quarterly 27 (2‐6):45-58.
Functional Characters of Solvable Terms.M. Coppo, M. Dezani-Ciancaglini & B. Venneri - 1981 - Mathematical Logic Quarterly 27 (2-6):45-58.
Typing untyped λ-terms, or reducibility strikes again!Jean Gallier - 1998 - Annals of Pure and Applied Logic 91 (2-3):231-270.
A new type assignment for λ-terms.M. Coppo & M. Dezani-Ciancaglini - 1978 - Archive for Mathematical Logic 19 (1):139-156.

Add more references