Certification of Breadth-First Algorithms by Extraction

Abstract

By using pointers, breadth-first algorithms are very easy to implement efficiently in imperative languages. Implementing them with the same bounds on execution time in purely functional style can be challenging, as explained in Okasaki’s paper at ICFP 2000 that even restricts the problem to binary trees but considers numbering instead of just traversal. Okasaki’s solution is modular and factors out the problem of implementing queues (FIFOs) with worst-case constant time operations. We certify those FIFO-based breadth-first algorithms on binary trees by extracting them from fully specified Coq terms, given an axiomatic description of FIFOs. In addition, we axiomatically characterize the strict and total order on branches that captures the nature of breadth-first traversal and propose alternative characterizations of breadth-first traversal of forests. We also propose efficient certified implementations of FIFOs by extraction, either with pairs of lists (with amortized constant time operations) or triples of lazy lists (with worst-case constant time operations), thus getting from extraction certified breadth-first algorithms with the optimal bounds on execution time.

The first author got financial support by the TICAMORE joint ANR-FWF project. The second author got financial support by the COST action CA15123 EUTYPES.

A Code Correspondence

Here, we briefly describe the Coq vernacular files behind our paper that is hosted at https://github.com/DmxLarchey/BFE. Besides giving formal evidence for the more theoretical characterizations, it directly allows doing program extraction, see the README section on the given web page.

We are here presenting 24 Coq vernacular files in useful order:

• list_utils.v: One of the biggest files, all concerning list operations, list permutations, the lifting of relations to lists (Sect. 2) and segments of the natural numbers – auxiliary material with use at many places.

• wf_utils.v: The subtle tactics for measure recursion in one or two arguments with a $\mathbb {N}$-valued measure function (Sect. 2.4) – this is crucial for smooth extraction throughout the paper.

• llist.v: Some general material on coinductive lists, in particular proven finite ones (including append for those), but also the rotate operation of Okasaki [13], relevant in Sect. 7.2.

• interleave.v: The example of interleaving with three different methods in Sects. 2.3 (with existing tools—needs Coq v8.9 with package Equations) and Sect. 2.5 (with our method).

• zip.v: Zipping with a rich specification and relations with concatenation – just auxiliary material.

• sorted.v: Consequences of a list being sorted, in particular absence of duplicates in case of strict orders – auxiliary material for Sect. 3.2.

• increase.v: Small auxiliary file for full specification of breadth-first traversal (Sect. 3.3).

• bt.v: The largest file in this library, describing binary trees (Sect. 3.1), their branches and orders on those (Sect. 3.2) in relation with breadth-first traversal and structural relations on trees and forests (again Sect. 3.1).

• fifo.v: the module type for abstract FIFOs (Sect. 5.1).

• fifo_triv.v: The trivial implementation of FIFOs through lists, mentioned in Sect. 5.1.

• fifo_2lists.v: An efficient implementation that has amortized $\mathcal O(1)$ operations (see, e. g., the paper by Okasaki [13]), described in Sect. 7.1.

• fifo_3llists.v: The much more complicated FIFO implementation that is slower but has worst-case $\mathcal O(1)$ operations, invented by Okasaki [13]; see Sect. 7.2.

• bft_std.v: Breadth-first traversal naively with levels (specified with the traversal of branches in suitable order), presented in Sect. 3.3.

• bft_forest.v: Breadth-first traversal for forests of trees, paying much attention to the recursive equations that can guide the definition and/or verification (Sect. 4.1).

• bft_inj.v: Structurally equal forests with the same outcome of breadth-first traversal are equal, shown in Sect. 4.3.

• bft_fifo.v: Breadth-first traversal given an abstract FIFO, described in Sect. 5.2.

• bfn_spec_rev.v: Characterization of breadth-first numbering, see Lemma 3.

• bfn_fifo.v: The certified analogue of Okasaki’s algorithm for breadth-first numbering [14], in Sect. 5.3.

• bfn_trivial.v: Just the instance of the previous with the trivial implementation of FIFOs.

• bfn_level.v: A certified reconstruction of bfnum on page 134 (Sect. 4 and Fig. 5) of Okasaki’s article [14]. For its full specification, we allow ourselves to use breadth-first numbering obtained in bfn_trivial.v.

• bfr_fifo.v: Breadth-first reconstruction, a slightly more general task (see next file) than breadth-first numbering, presented in Sect. 5.4.

• bfr_bfn_fifo.v: Shows the claim that breadth-first numbering is an instance of breadth-first reconstruction (although they have been obtained with different induction principles).

• extraction.v: This operates extraction on-the-fly.

• benchmarks.v: Extraction towards .ml files.