Precise Reasoning About Non-strict Functional Programs; How to Chase Bottoms, and How to Ignore Them

Precise Reasoning About Non-strict Functional Programs; How to Chase Bottoms, and How to Ignore Them
Nils Anders Danielsson
Licentiate thesis, 2005. [pdf]

Abstract

This thesis consists of two parts. Both concern reasoning about non-strict functional programming languages with partial and infinite values and lifted types, including lifted function spaces.

The first part is a case study in program verification: We have written a simple parser and a corresponding pretty-printer in Haskell. A natural aim is to prove that the programs are, in some sense, each other's inverses. The presence of partial and infinite values makes this exercise interesting. We have tackled the problem in different ways, and report on the merits of those approaches. More specifically, first a method for testing properties of programs in the presence of partial and infinite values is described. By testing before proving we avoid wasting time trying to prove statements that are not valid. Then it is proved that the programs we have written are in fact (more or less) inverses using first fixpoint induction and then the approximation lemma.

Using the proof methods described in the first part can be cumbersome. As an alternative, the second part justifies reasoning about non-total (partial) functional languages using methods seemingly only valid for total ones. Two languages are defined, one total and one partial, with identical syntax. A partial equivalence relation is then defined, the domain of which is the total subset of the partial language. It is proved that if two closed terms have the same semantics in the total language, then they have related semantics in the partial language.

Errata

Paper 1, Section 6: The third and fifth occurrences of the word "total" should be replaced by "total and finite", and the two occurrences of the text "not total" should be replaced by "partial or infinite".

Paper 2, Section 10: The last sentence in this section should be extended as follows: "(with modified preconditions: the translations of all terms have to belong to ℒ₁″)."

Nils Anders Danielsson
Last updated Thu Aug 25 13:50:35 UTC 2016.