×
Nakazawa, Koji; Naya, Hiroto

Strong reduction of combinatory calculus with streams. (English) Zbl 1326.03023

Stud. Log. 103, No. 2, 375-387 (2015).
Summary: This paper gives the strong reduction of the combinatory calculus SCL, which was introduced as a combinatory calculus corresponding to the untyped Lambda-mu calculus. It proves the confluence of the strong reduction. By the confluence, it also proves the conservativity of the extensional equality of SCL over the combinatory calculus CL, and the consistency of SCL.

MSC:

03B40 Combinatory logic and lambda calculus

Keywords:

combinatory logic; lambda-mu calculus; strong reduction; confluence
PDF BibTeX XML Cite
\textit{K. Nakazawa} and \textit{H. Naya}, Stud. Log. 103, No. 2, 375--387 (2015; Zbl 1326.03023)
Full Text: DOI

References:

[1] David R.: direct proof of the confluence of combinatory strong reduction. Theoretical Computer Science 410(42), 4204-4215 (2009) · Zbl 1187.68125
[2] Dehornoy, P. and V. van Oostrom, Z, proving confluence by monotonic single-step upperbound functions, in Logical Models of Reasoning and Computation (LMRC-08), 2008. Slides available on http://www.phil.uu.nl/oostrom/publication/talk/lmrc060508.pdf. · Zbl 1338.03017
[3] Hindley R., Seldin J.P.: Lambda-Calculus and Combinators, an Introduction. Cambridge University Press, Cambridge (2008) · Zbl 1149.03016
[4] Komori Y., Matsuda N., Yamakawa F.: A simplified proof of the church-rosser theorem. Studia Logica 102(1), 175-183 (2013) · Zbl 1338.03017
[5] Minari P.: A solution to curry and hindley’s problem on combinatory strong reduction. Archive for Mathematical Logic 48(2), 159-184 (2009) · Zbl 1172.03009
[6] Nakazawa, K. and S. Katsumata, Extensional models of untyped Lambda-mu calculus, in Fourth International Workshop on Classical Logic and Computation (CL&C’12), vol. 97 of Electric Proceedings in Theoretical Computer Science, pp. 35-47, 2012. · Zbl 1459.68071
[7] Parigot, M., λμ-Calculus: an algorithmic interpretation of classical natural deduction, in Proceedings of the International Conference on Logic Programming and Automated Reasoning (LPAR ’92), vol. 624 of Lecture Notes in Computer Science. Springer, Berlin, 1992, pp. 190-201. · Zbl 0925.03092
[8] Saurin, A., Separation with streams in the Λμ-calculus, in 20th Annual IEEE Symposium on Logic in Computer Science (LICS’ 05). IEEE Computer Society, New York, 2005, pp. 356-365.
[9] Saurin, A. Standardization and Böhm trees for Λμ-calculus, in Tenth International Symposium on Functional and Logic Programming (FLOPS 2010), vol. 6009 of Lecture Notes in Computer Science. Springer, 2010, pp. 134-149. · Zbl 1284.68137
[10] Saurin A.: Typing streams in the Λμ-calculus. ACM Transactions on Computational Logic 11, 1-34 (2010) · Zbl 1351.68065
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.