Proving Lazy Folklore with Mixed Lazy/Strict Semantics
Abstract
Explicit enforcement of strictness is used by functional programmers for many different purposes. Few functional programmers, however, are aware that explicitly enforcing strictness has serious consequences for (formal) reasoning about their programs. Some vague “folklore” knowledge has emerged concerning the correspondence between lazy and strict evaluation but this is based on experience rather than on rigid proof. This paper employs a model for formal reasoning with enforced strictness based on John Launchbury’s lazy graph semantics. In this model Launchbury’s semantics are extended with an explicit strict let construct. Examples are given of the use of these semantics in formal proofs. We formally prove some “folklore” properties that are often used in informal reasoning by programmers.
Full text