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 suﬃciently 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 veriﬁed. In this way the amount of program code which must be veriﬁed by hand in order to complete the proof is reduced, increasing conﬁdence in the result.