Suppose I want to sort a list of natural numbers by constructing a binary search tree and then going through it in an inorder traversal, and I write an insertion function that takes the existing partially constructed binary search tree and returns a new one with the next value in the list inserted.

Is there any way to tell Coq to do this "in place" in a way that it doesn't end up copying the tree n times in succession? I don't care about the intermediary search trees and I'm fine with them being overwritten or made inaccessible, I want Coq to modify the existing leaves of the tree.

it sounds like what you want is mutability of data, which Coq as a pure language doesn't support. Your best bet might be to use a framework like CFML, which represents mutable computations indirectly in Coq, and allows you to reason about them using separation logic

Note that each copying should only affect one path, which in the average case is logarithmic in the number of elements.

Yes, but that depends on the input distribution so it might or might not help, unless you implement a balanced tree in Coq — which is definitely possible.

Karl Palmskog said:

it sounds like what you want is mutability of data, which Coq as a pure language doesn't support. Your best bet might be to use a framework like CFML, which represents mutable computations indirectly in Coq, and allows you to reason about them using separation logic

Yes I had worried the answer would be something like that. Thank you for the reference. I am just generally looking for advice on implementing data structures in a performant way with reasonable performance.

James Wood said:

Note that each copying should only affect one path, which in the average case is logarithmic in the number of elements.

Ah, great point, I hadn't thought of that.

Okasaki's *Purely Functional Data Structures* I think is still the standard reference.

Indeed. https://cstheory.stackexchange.com/a/1550/989 lists updates in the field since that book, but I agree with James.

Last updated: Jun 24 2024 at 13:02 UTC