The ζ-Semantics: A Comprehensive Semantics for Functional Programs

Article type: Research Article

Authors: Chitil, Olaf

Affiliations: Lehrstuhl für Informatik II, Aachen University of Technology, 52056 Aachen, Germany. chitil@informatik.rwth-aachen.de, http://www-i2.informatik.RWTH-Aachen.de/-chitil

Abstract: A comprehensive semantics for functional programs is presented, which generalizes the well-known call-by-value and call-by-name semantics. By permitting a separate choice between call-by value and call-by-name for every argument position of every function and parameterizing the semantics by this choice we abstract from the parameter-passing mechanism. Thus common and distinguishing features of all instances of the ζ-semantics, especially call-by-value and call-by-name semantics, are highlighted. Furthermore, a property can be validated for all instances of the ζ-semantics by a single proof. This is employed for proving the equivalence of the given denotational (fixed-point based) and two operational (reduction based) definitions of the ζ-semantics. We present and apply means for very simple proofs of equivalence with the denotational ζ-semantics for a large class of reduction-based ζ-semantics. Our basis are simple first-order constructor-based functional programs with patterns.

Keywords: functional programming language, denotational and operational semantics, call-by-value, call-by-name, strictness, pattern-matching

DOI: 10.3233/FI-1997-313404

Journal: Fundamenta Informaticae, vol. 31, no. 3-4, pp. 253-294, 1997