Formal derivation of greedy algorithms from relational specifications: a tutorial

Yu-Hsi Chiang, Shin-Cheng Mu. Journal of Logical and Algebraic Methods in Programming, in press.
[Paper(doi:10.1016/j.jlamp.2015.12.003) | Code]

Many programming tasks can be specified as optimisation problems in which a relation is used to generate all possible solutions, from which we wish to choose an optimal one. A relational operator “shrink”, developed by José N. Oliveira, is particularly suitable for constructing greedy algorithms from such specifications. Meanwhile, it has become standard in many sub-fields in programming language that proofs must be machine-verified. This tutorial leads the readers through the development of algebraic derivations of three greedy algorithms, one fold-based and two unfold-based, using AoPA, a library designed for machine-verified relational program calculation.

Leave a Reply

Your email address will not be published. Required fields are marked *

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>