Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

map.ml function join does more comparisons than needed #5171

Closed
vicuna opened this issue Oct 25, 2010 · 2 comments
Closed

map.ml function join does more comparisons than needed #5171

vicuna opened this issue Oct 25, 2010 · 2 comments
Labels

Comments

@vicuna
Copy link

vicuna commented Oct 25, 2010

Original bug ID: 5171
Reporter: bluestorm
Assigned to: @protz
Status: closed (set by @xavierleroy on 2012-09-25T18:07:21Z)
Resolution: fixed
Priority: normal
Severity: tweak
Version: 3.12.0
Fixed in version: 3.13.0+dev
Category: ~DO NOT USE (was: OCaml general)
Monitored by: @gasche mehdi pilki @ygrek @jberdine @hcarty

Bug description

I'm under the impression that the join function in Map.ml is a bit wasteful regarding the use of user-provided comparison functions :

let rec join l v d r =
  match (l, r) with
    (Empty, _) -> add v d r
  | (_, Empty) -> add v d l
  | (Node(ll, lv, ld, lr, lh), Node(rl, rv, rd, rr, rh)) ->
      if lh > rh + 2 then bal ll lv ld (join lr v d r) else
      if rh > lh + 2 then bal (join l v d rl) rv rd rr else
      create l v d r

The two base cases use the add primitive, wich itself uses the Ord.compare function to locate the right place for the key v in the tree. However, no such comparisons should be needed as we know statically that the key is (in either case) less than or bigger than all keys in the target tree.

I have experimented with the following implementation, which seems to be doing ok (but I'm not familiar with the algorithmic considerations wrt. the balanced trees) :

(* beware : those two functions assume that the added k is strictly
smaller (or bigger) than all the present keys in the tree; it
does not test for equality with the current min (or max) key.

 Indeed, they are only used during the "join" operation which
 respects this precondition.

*)
let rec add_min_binding k v = function
| Empty -> singleton k v
| Node (l, x, d, r, h) ->
bal (add_min_binding k v l) x d r

let rec add_max_binding k v = function
| Empty -> singleton k v
| Node (l, x, d, r, h) ->
bal l x d (add_max_binding k v r)

(* Same as create and bal, but no assumptions are made on the
relative heights of l and r.
*)
let rec join l v d r =
match (l, r) with
(Empty, ) -> add_min_binding v d r
| (
, Empty) -> add_max_binding v d l
| (Node(ll, lv, ld, lr, lh), Node(rl, rv, rd, rr, rh)) ->
if lh > rh + 2 then bal ll lv ld (join lr v d r) else
if rh > lh + 2 then bal (join l v d rl) rv rd rr else
create l v d r

The advantage of such a modification is that it avoids the use of the user-provided comparison function when unnecessary, which may be arbitrarily costly.

File attachments

@vicuna
Copy link
Author

vicuna commented Oct 27, 2010

Comment author: pilki

I added two modifications of the MapAVL library of coq 8.3 including the proposal, proving it correct.

@vicuna
Copy link
Author

vicuna commented Dec 23, 2011

Comment author: @protz

This has been enacted.

r11955

@vicuna vicuna closed this as completed Sep 25, 2012
@vicuna vicuna added the bug label Mar 20, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant