Abstract Interpretation Using Laziness: Proving Conway's Lost Cosmological Theorem

The paper describes an abstract interpretation technique based on lazy functional programming, and applies it to the proof of Conway’s Lost Cosmological Theorem, a combinatorial proposition analogous to the four color theorem or Kepler’s conjecture, which essentially states that a certain predicate holds of all lists of integers from 1 to 4. The technique makes use of the semantics of Haskell in the following way: evaluating a predicate on a partial lazy list to True proves that the predicate would evaluate to True on any list extending the partial list. In this way proving a property of all lists can be reduced to evaluating the property on sufficiently many partial lists, which cover the set of all lists. The proof is completed by proving the correctness of the code implementing the predicate by hand. The oracle that chooses a covering set of partial lists need not be verified. In this way the amount of program code which must be verified by hand in order to complete the proof is reduced, increasing confidence in the result.