Gagallium

This small interlude post is not about Coq nor CFML: I present a data structure from Okasaki’s Purely functional data structures, implemented in OCaml.

It comes as a preliminary explanation for an incoming formalization of it in CFML (see next post), including an complexity analysis!

In a recent paper, Arthur Charguéraud and François Pottier present a formal proof of an OCaml implementation of Tarjan’s union-find algorithm. The proof covers two aspects: first, functional correctness (“the algorithm is correct”), but also asymptotic complexity. For example, one of the results of the paper is that the link function runs in $O(α(n))$ elementary steps, $α$ being the inverse of the Ackermann function.

Actually, the complexity results of the paper are not presented using the “big-O” notation, commonly used in asymptotic complexity proofs: the various constants are explicit and manipulated through the proof.

In these blog posts (current, interlude and final), I’ll describe a tentative extension of CFML, the Coq library François and Arthur used for their proof. Its goal is to enable asymptotic reasoning, big-O notations and such to be used to prove complexity of programs.