Technical reports

Fixed point promotion: taking the induction out of automated induction

William Sonnex

March 2017, 170 pages

This technical report is based on a dissertation submitted September 2015 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Trinity College.

DOI: 10.48456/tr-905

Abstract

This thesis describes the implementation of Elea: the first automated theorem prover for properties of observational approximation between terms in a functional programming language. A term approximates another if no program context can tell them apart, except that the approximating term can be less defined than the approximated term. Elea can prove terms equivalent by proving approximation in both directions.

The language Elea proves approximations over is pure, call-by-name, and with non-strict data-types, a subset of the Haskell language. In a test set of established properties from the literature, Elea performs comparably well to the current state of the art in automated equivalence proof, but where these provers assume all terms are total, Elea does not.

Elea uses a novel method to prove approximations, fixed-point promotion, a method which does not suffer from some of the weaknesses of cyclic proof techniques such as induction or coinduction. Fixed-point promotion utilises an unfold-fold style term rewriting system, similar to supercompilation, which uses multiple novel term rewriting steps in order to simulate the lemma discovery techniques of automated cyclic provers.

Elea is proven sound using denotational semantics, including a novel method for verifying an unfold-fold style rewrite, a method I have called truncation fusion.

Full text

PDF (0.9 MB)

BibTeX record

@TechReport{UCAM-CL-TR-905,
  author =	 {Sonnex, William},
  title = 	 {{Fixed point promotion: taking the induction out of
         	   automated induction}},
  year = 	 2017,
  month = 	 mar,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-905.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-905},
  number = 	 {UCAM-CL-TR-905}
}