×

zbMATH — the first resource for mathematics

\(\lambda \rho\)-calculus. II. (English) Zbl 1280.03016
Summary: In Part I [Bull. Sect. Log., Univ. Łódź, Dep. Log. 31, No. 2, 65–70 (2002; Zbl 1036.03011)], the author introduced the system \(\lambda \rho\)-calculus and stated without proof that the strong normalization theorem holds. Here we introduce a lemma (Lemma 4.10) and use it to prove the strong normalization theorem. While a typed \(\lambda\)-term itself is a derivation of the natural deduction for intuitionistic implicational logic, a typed \(\lambda \rho\)-term itself is a derivation of the natural deduction for classical implicational logic. Our system is simpler than the implicational fragment of M. Parigot’s \(\lambda \mu\)-calculus (cf. [Lect. Notes Comput. Sci. 624, 190–201 (1992; Zbl 0925.03092)]).

MSC:
03B40 Combinatory logic and lambda calculus
03B05 Classical propositional logic
PDF BibTeX XML Cite
Full Text: DOI Euclid