Abstract
We introduce two logics for partiality, a call-by-value logic and a call-by-name logic. Both logics are variants of the logic of partial terms, an extension of the first-order predicate calculus by a definedness predicate. In our logics, however, quantifiers may only be instantiated to value terms and not to arbitrary, defined terms as in the logic of partial terms. We show that the call-by-value logic is computationally adequate for call-by-value evaluation, whereas the call-by-name logic has the same property for call-by-name evaluation. In order to relate the call-by-value logic to partial combinatory logic, we introduce a new lambda abstraction for terms of partial combinatory logic which has better properties than the one used previously.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Z. M. Ariola, M. Felleisen, J. Maraist, M. Odersky, and P. Wadler. A call-by-need lambda calculus. In Proceedings of the ACM Symposium on Principles of Programming Languages (POPL '95), pages 233–246. ACM Press, 1995.
M. J. Beeson. Foundations of Constructive Mathematics. Springer-Verlag, 1985.
W. Clinger and J. A. Rees. The revised4 report on the algorithmic language Scheme. ACM LISP Pointers, 4(3), 1991.
S. Feferman. A language and axioms for explicit mathematics. In J. N. Crossley, editor, Algebra and Logic, pages 87–139, Berlin, 1975. Springer-Verlag, Lecture Notes in Mathematics 450.
S. Feferman. Polymorphic typed lambda-calculi in a type-free axiomatic framework. In W. Sieg, editor, Logic and Computation, volume 106 of Contemporary Mathematics, pages 101–136, Providence, Rhode Island, 1990. American Mathematical Society.
S. Feferman. Definedness. Technical report, Department of Mathematics, Stanford University, 1995.
P. Hudlak, S. Peyton Jones, and P. Wadler. Report on the programming language Haskell, a non-strict purely functional language. ACM SIGPLAN Notices, 27(5), 1992.
R. Milner, M. Tofte, and R. Harper. The definition of Standard ML. The MIT Press, 1990.
G. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1:125–159, 1975.
A. Sabry and P. Wadler. A reflection on call-by-value. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP '96), pages 13–24, Philadelphia, Pennsylvania, 1996. ACM Press.
R. F. Stärk. Why the constant undefined? Logics of partial and undefined terms for strict and non-strict functional programming languages. Technical Report 96-11, Institute of Informatics, University of Fribourg, Switzerland, 1996.
T. Strahm. Partial applicative theories and explicit substitutions. J. of Logic and Computation, 6(1):55–77, 1996.
A. S. Troelstra and D. van Dalen. Constructivism in Mathematics: an Introduction. North-Hollland, Amsterdam, 1988.
D. A. Turner. An overview of Miranda. ACM SIGPLAN Notices, 21(12):158–166, 1986.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Stärk, R.F. (1997). Call-by-Value, call-by-name and the logic of values. In: van Dalen, D., Bezem, M. (eds) Computer Science Logic. CSL 1996. Lecture Notes in Computer Science, vol 1258. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63172-0_54
Download citation
DOI: https://doi.org/10.1007/3-540-63172-0_54
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63172-9
Online ISBN: 978-3-540-69201-0
eBook Packages: Springer Book Archive