Unifying Hindsight and Foresight: Lazy Cost Analysis as Functional Logic Programming

Clairvoyance semantics and demand semantics are both pure and time-cost equivalent to lazy evaluation, offering alternatives to the stateful natural semantics of lazy evaluation for analyzing computation cost. Unfortunately, clairvoyance semantics is simple but hard to execute, and demand semantics is executable but complicated. In this paper, we propose a novel approach for unifying these two semantics using functional logic programming. We propose (1)~a logical clairvoyance translation, which translates lazy functional programs to functional logic programs where the computation cost is reified, and (2)~a logical demand translation, which is a simple extension to the logical clairvoyance translation. We prove that these two translations correctly implement clairvoyance and demand semantics respectively using Agda. We also conduct case studies on examples including insertion sort and Okasaki’s banker’s queue using Curry/KiCS2 to show how these translations can be used in practice.