Mixed Lazy/Strict Graph Semantics

Abstract. Explicitly enforcing strictness is often used by functional programmers as an important tool for making applications fit time and space efficiency requirements. Few functional programmers however, are familiar with the consequences of explicitly enforcing strictness for formal reasoning about their programs. Some “folklore ” knowledge has emerged but this is based on experience rather than on rigid proof. Up to now no formal model has been available for reasoning about enforcing strictness in denotational and operational semantics. This greatly hampered formal reasoning on mixed lazy/strict programs. This paper presents a model for formal reasoning with enforced strictness based on John Launchbury’s lazy graph semantics. Lazy graph semantics are widely considered to be essential for lazy functional programming languages. In this paper Launchbury’s semantics are extended with an explicit strict let construct. Correctness and adequacy of our mixed lazy/strict graph semantics is proven. Using these mixed semantics we formalise and prove some of the available “folklore ” knowledge. 1 Introduction an