Call-by-value, call-by-name and the logic of values

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.