Why the constant 'undefined'? Logics of partial terms for strict and non-strict functional programming languages

Abstract

In this article we explain two different operational interpretations of functional programs by two different logics. The programs are simply typed λ-terms with pairs, projections, if-then-else and least fixed point recursion. A logic for call-by-value evaluation and a logic for call-by-name evaluation are obtained as as extensions of a system which we call the basic logic of partial terms (BPT). This logic is suitable to prove properties of programs that are valid under both strict and non-strict evaluation. We use methods from denotational semantics to show that the two extensions of BPT are adequate for call-by-value and call-by-name evaluation. Neither the programs nor the logics contain the constant 'undefined'.