Reduction rules for intuitionistic \(\lambda\rho\)-calculus. (English) Zbl 1378.03012

Summary: The third author gave a natural deduction style proof system called the \(\lambda\rho\)-calculus for implicational fragment of classical logic in [Tsukuba J. Math. 37, No. 2, 307–320 (2013; Zbl 1280.03016)]. In [Intuitionistic fragment of the \(\lambda\mu\)-calculus. Techn. Rep., Tokyo Institute of Technology (2015); “Intuitionistic tree sequent calculus and intuitionistic \(\lambda\rho\)-calculus”, Post-proceedings of the RIMS Workshop “Proof Theory, Computability Theory and Related Issues” (to appear)], the fourth author gave a natural subsystem “intuitionistic \(\lambda\rho\)-calculus” of the \(\lambda\rho\)-calculus, and showed the system corresponds to intuitionistic logic. The proof is given with tree sequent calculus (Kripke models), but is complicated. In this paper, we introduce some reduction rules for the \(\lambda\rho\)-calculus, and give a simple and purely syntactical proof to the theorem by use of the reduction. In addition, we show that we can give a computation model with rich expressive power with our system.


03B40 Combinatory logic and lambda calculus
03B20 Subsystems of classical logic (including intuitionistic logic)
03F03 Proof theory in general (including proof-theoretic semantics)


Zbl 1280.03016
Full Text: DOI


[1] Andou, Y., A system of \({{λ}{μ}}\)-calculus proper to the implicational fragment of classical natural deduction with one conclusion, in RIMS Kokyuroku 976, 1997. · Zbl 0925.03097
[2] Cirstea, H. F.; Germain, K. C., A \({{ρ}}\)-calculus of explicit constraint application, Electronic Notes in Theoretical Computer Science, 117, 51-67, (2005) · Zbl 1272.68172
[3] Griffin, T. G., A formulae-as-type notion of control, in Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages 1989, 47-58.
[4] Hindley, J. R., and J. P. Seldin, Lambda-Calculus and Combinators: An Introduction, Cambridge University Press, Cambridge, 2008. · Zbl 1149.03016
[5] Howard, W. A., The formulae-as-types notion of construction, in To H. B. Curry: Essays on Combinatory Logic, Lambda-Calculus, and Formalism 1980, 479-490. · Zbl 0895.03011
[6] Kobayashi, S., Monad as modality, Theoretical Computer Science, 175, 29-74, (1997) · Zbl 0895.03011
[7] Komori, Y.; Matsuda, N.; Yamakawa, F., A simplified proof of the church-rosser theorem, Studia Logica, 102, 175-183, (2014) · Zbl 1338.03017
[8] Komori, Y., \({{λ}{ρ}}\)-calculus II, Tsukuba Journal of Mathematics, 37, 307-320, (2013) · Zbl 1280.03016
[9] Miyamoto, K., and A. Igarashi, A modal foundation for secure information flow, in Proceedings of the Workshop on Foundations of Computer Security 2004, 187-203. · Zbl 1338.03017
[10] Matsuda, N., Intuitionistic fragment of the \({{λ}{μ}}\)-calculus, Technical Report, Tokyo Institute of Technology C-282, 2015.
[11] Matsuda, N., Intuitionistic tree sequent calculus and intuitionistic lambda-rho-calculus, in Post-proceedings of the RIMS Workshop “Proof Theory, Computability Theory and Related Issues”, to appear.
[12] Nakano, H., A \({{ρ}}\)-calculus of explicit constraint application, Logic, Language and Computation 61-72, 1994.
[13] Nakano, H., The non-deterministic catch and throw mechanism and its subject reduction property, in Proceedings of Logic, Language and Computation 1992, 82-89.
[14] Parigot, M., \({{λ}{μ}}\)-calculus: an algorithmic interpretation of classical natural deduction, in Proceedings of Logic programming and automated reasoning 1992, 190-201. · Zbl 0925.03092
[15] Sørensen M. H., Urzyczyn P.: Lectures on the Curry-Howard Isomorphism, Elsevier, Amsterdam, (2006) · Zbl 1183.03004
[16] Szabo, M. E., The Collected Papers of Gerhard Gentzen, North-Holland, Amsterdam, 1969. · Zbl 0209.30001
[17] Yamagata, Y., Strong normalization of second order symmetric lambda-mu calculus, Theoretical Aspects of Computer Software 459-467, 2001.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.