Repository navigation
Static optimality for splay trees - #22
berendsohn wants to merge 15 commits into
Conversation
|
@AntoineduFresne, can you review this PR? |
Fixed typos and syntax/formatting (done with an LLM), added the new files to AlgoLib.lean, made BSTAPI.staticCost a wrapper around the Tree version, removed unused code and simplified a few proofs. FnLb_of_Fintype_of_FnPos is now FnLb_of_Finite_of_FnPos and takes [Finite α].
AntoineduFresne
left a comment
AntoineduFresne
left a comment
There was a problem hiding this comment.
Thanks a lot for this, really nice work! I've gone through BSTAPI.lean and Weighted.lean so far, and I'll review StaticOptimality.lean and the smaller changes (BinaryTree, Basic, Complexity) later.
I pushed a cleanup commit on top of yours (unused code, typos, formatting and a few small simplifications; details in the commit message), so please pull before you continue. One API change to be aware of: FnLb_of_Fintype_of_FnPos is now FnLb_of_Finite_of_FnPos and takes [Finite α].
For the part I reviewed, there's only one thing, please add the usual copyright header (with you under Authors) to Weighted.lean and StaticOptimality.lean.
Also there are other alternative definition (that doesn't use the forallquantifier) for FnLbOne w and FnNonneg w which are just 1 ≤ w and 0 ≤ w altough FnPos has no such notation (0 < w isn't pointwise positivity). But this is irrelevant from my side I guess.
About your question on duplication. I believe that it is fine for this PR for now. it seems that the unweighted analysis is just the case w = 1. You can maybe do a follow-up that derives Complexity.lean from Weighted.lean, which might hopefully remove the need for Weighted to import Complexity.
I went through the rest of the files. For syntax and spelling cleanups, I allowed myself to commit it directly (only spacing, blank lines... line breaks (100-character limit)) (this concerns StaticOptimality.lean and the new lemmas in BinaryTree.lean)
I renamed your new lemmas to follow the Mathlib naming conventions, i.e. nonnil_of_mem -> ne_nil_of_mem nil_of_toKeyList_empty -> eq_nil_of_toKeyList_eq_nil num_nodes_from_toKeyList -> num_nodes_eq_length_toKeyList Dir.applyChild_ne_nil_of_ne_nil -> applyChild_ne_nil_of_ne_nil (applyChild is not in the Dir namespace) and updated the places where they are used. I used AI to help me with this.
…ad of handling each case separately.
…rom this library or Mathlib) or shorter the proofs directly by providing the term.
…omplexity.lean, so instead of making it public I used Mathlib's Real.logb_le_logb_of_le directly, that way the PR doesn't need to touch Complexity.lean. I also merged splay_tree_static_optimality' into splay_tree_static_optimality: the private version only existed to take IsBST s as an extra assumption, but that follows from hkeys and IsBST init in one line, so the same statement doesn't need to be written twice. Feel free to revert if you prefer it your way.
…andling each case separately.
…just intro the lets from the statement instead of writing them out again, φ_zigzig and φ_zigzag had a let c that was never used, and in φ_mirror the subtrees were named the other way round (r for the left one), so I swapped them. I also shortened size_mul_weight and search_path_len_right a bit.
…' doesn't need the cases on m (nothing below uses the split), and splay_tree_static_optimality doesn't need by_cases init = nil, since each access already gives init ≠ nil. The rest of both proofs is unchanged, just one indentation level less.
…t several times: rank_eq_logb_size in Weighted (rank is just log₂ of the size, also for nil since log₂ 0 = 0 in Mathlib), which shortens rank_le_of_size_le, rank_eq_of_toKeyList_eq and rank_mirror, and size_eq_mul_size in StaticOptimality (if two weight functions differ by a constant factor on the keys of a tree, so do the sizes), which replaces the list induction that staticWeight_size_left and staticWeight_size_right each did separately.
… at h and assumption steps can be done with a single simpa ... using h, so I used that in both places.
…:= ... and simp only [reassemble_cons]; push_cast, so I moved them once above the split_ifs.
AntoineduFresne
left a comment
AntoineduFresne
left a comment
There was a problem hiding this comment.
Hi Benjamin,
I took the liberty of pushing a few small simplifications to your branch, I hope that's okay. I split them into several commits, one per kind of change (formatting, lemma names, shorter proofs, two small helper lemmas, ...), so it should be easy to look at them one by one and revert anything you don't like.
I also noticed two other things that might work, but I'm not sure and didn't look into them further, so feel free to ignore them:
- In
splay_total_weighted_cost', I wonder if the three inductions (hbst',hcont'andhsize) could come from a single one showing that splaying doesn't change the key list (toKeyList_splay), maybe withIsBST_of_toKeyList_eq,mem_iff_mem_toKeyListandsize_from_toKeyList. - In
staticWeight_size_left, if I'm not mistaken the exponents.num_nodes - l.num_nodes - 1is justr.num_nodes(andl.num_nodesinstaticWeight_size_right). Maybe stating them with the natural power3 ^ r.num_nodeswould make therpowcomputations instaticWeight_size_self_uba bit simpler.
Apart from that, it looks good to me as far as I can tell. I'm seeing Sorrachai on Monday, so I'll ask him what he thinks, and then hopefully we can approve it soon. Thanks again for the PR!
|
Thanks! I'm happy with the changes you made, the simplifications are very nice. Thanks for the informative commit messages.
Done. I also added you since you made some changes. I'll also look into your two proposals, but I'm quite busy this month so it may take some time. |
Okay, this was easy actually. |
This branch has not been deployed
3 participants
A proof of static optimality for splay trees: for any sufficiently long sequence of access operations, splay trees perform as well as any static tree (up to a constant factor).
This includes a variant of Sleator and Tarjan's classical access lemma.
For the static optimality proof, I used the method outlined by David Eppstein here, which circumvents the need to work with entropy.
Some more notes:.
log ncomplexity bound (or rather from the cslib pull request); it was mostly a matter of transforming the analysis from unweighted to weighted. Parts of the original analysis are now special cases of the new analysis. Not sure how much duplication is desired.Weighted.leanneeds to importComplexityandCorrectness; this could be remedied by some reorganization.log w(T)/w(T_x), wherew(T)is the total weight of the tree andw(T_x)is the weight of the subtree rooted at the accessed nodex. I proved instead the weakerlog w(T)/w(x). This is because even stating the strong variant seemed to require some new definitions regarding rooted subtrees, and because the weaker variant is almost always sufficient in my experience.O(n²), instead of the originalO(n log n)(wherenis the number of nodes, not accesses). This is because of the method I used.I'm new to lean and this is my very first project, so all feedback is appreciated.