University of Oxford Logo University of OxfordDepartment of Computer Science - Home

The Generic Approximation Lemma

Graham Hutton and Jeremy Gibbons

Abstract

The approximation lemma was recently introduced as a simplification of the well-known take lemma, and is used to prove properties of programs that produce lists of values. We show how the approximation lemma, unlike the take lemma, can naturally be generalised from lists to a large class of datatypes, and present a generic approximation lemma that is parametric in the datatype to which it applies. As a useful by-product, we find that generalising the approximation lemma in this way also simplifies its proof.

Details

Journal

Information Processing Letters

Month

aug

Number

4

Pages

197–201

Volume

79

Year

2001

Links

BibTeX

Link (ps.gz)

Related pages

People

Activities