Stream: Coq users

Topic: How to prevent unnecessary copying?


view this post on Zulip Patrick Nicodemus (Apr 30 2022 at 18:59):

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.

view this post on Zulip Karl Palmskog (Apr 30 2022 at 19:50):

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

view this post on Zulip James Wood (Apr 30 2022 at 19:53):

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

view this post on Zulip Paolo Giarrusso (Apr 30 2022 at 20:07):

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.

view this post on Zulip Patrick Nicodemus (Apr 30 2022 at 20:14):

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.

view this post on Zulip Patrick Nicodemus (Apr 30 2022 at 20:14):

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.

view this post on Zulip James Wood (Apr 30 2022 at 20:19):

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

view this post on Zulip Paolo Giarrusso (Apr 30 2022 at 20:48):

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


Last updated: Feb 01 2023 at 13:03 UTC