Story of Your Lazy Function's Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy Programs

TL;DR

The paper tackles the challenge of formally reasoning about computation costs in lazy functional programs. It introduces a typed, bidirectional demand semantics that derives minimal input demands and computation costs from output demands, enabling extrinsic and modular cost analysis without heavy logics. The approach is mechanized in the Rocq Prover and validated through case studies on lazy insertion sort, lazy selection sort, and purely functional banker's and implicit queues, including proofs of amortization and persistence. A novel reverse physicist's method supports modular amortized reasoning, and the work establishes a correspondence with clairvoyant semantics to ensure soundness. Collectively, the contributions provide a rigorous framework for cost-aware reasoning in lazy languages with practical verification of non-trivial data structures.

Abstract

Lazy evaluation is a powerful tool that enables better compositionality and potentially better performance in functional programming, but it is challenging to analyze its computation cost. Existing works either require manually annotating sharing, or rely on separation logic to reason about heaps of mutable cells. In this paper, we propose a bidirectional demand semantics that allows for extrinsic reasoning about the computation cost of lazy programs without relying on special program logics. To show the effectiveness of our approach, we apply the demand semantics to a variety of case studies including insertion sort, selection sort, Okasaki's banker's queue, and the implicit queue. We formally prove that the banker's queue and the implicit queue are both amortized and persistent using the Rocq Prover (formerly known as Coq). We also propose the reverse physicist's method, a novel variant of the classical physicist's method, which enables mechanized, modular and compositional reasoning about amortization and persistence with the demand semantics.

Figures (25)

• Figure 1: The Gallina implementation of and in ANF (A-normal form) anf. For simplicity, we define these functions on lists of natural numbers (). The infix operator shown in is Gallina's "less than or equal" operator on natural numbers, which returns a boolean.
• Figure 2: The demand functions of and .
• Figure 3: An illustration of how the input demand is computed in .
• Figure 4: Syntax
• Figure 5: Typing rules.

Theorems & Definitions (9)

• lemma 1: transitivity
• lemma 2: Supremum
• lemma 3: bottom
• lemma 4: Totality
• lemma 5: monotonicity
• lemma 6: $\sqcup$-homomorphism
• theorem 1: Functional correctness
• theorem 2: Cost existence
• theorem 3: Cost minimality