0005171: map.ml function `join` does more comparisons than needed

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0005171

OCaml

OCaml general

public

2010-10-25 16:47

2012-09-25 20:07

Reporter

bluestorm

Assigned To

protz

Priority

normal

Severity

tweak

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

3.12.0

Target Version

Fixed in Version

3.13.0+dev

Summary

0005171: map.ml function `join` does more comparisons than needed

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.

Tags

No tags attached.

Attached Files

FMapAVL.v [^] (67,717 bytes) 2010-10-27 12:34

FMapFullAVL.v [^] (25,209 bytes) 2010-10-27 12:34

Relationships

Notes
(0005691) pilki (reporter) 2010-10-27 12:35	I added two modifications of the MapAVL library of coq 8.3 including the proposal, proving it correct.

(0006525) protz (manager) 2011-12-23 21:55	This has been enacted. r11955

Issue History
Date Modified	Username	Field	Change
2010-10-25 16:47	bluestorm	New Issue
2010-10-27 12:34	pilki	File Added: FMapAVL.v
2010-10-27 12:34	pilki	File Added: FMapFullAVL.v
2010-10-27 12:35	pilki	Note Added: 0005691
2011-05-20 15:01	doligez	Status	new => acknowledged
2011-12-23 21:55	protz	Note Added: 0006525
2011-12-23 21:55	protz	Status	acknowledged => resolved
2011-12-23 21:55	protz	Fixed in Version	=> 3.13.0+dev
2011-12-23 21:55	protz	Resolution	open => fixed
2011-12-23 21:55	protz	Assigned To	=> protz
2012-09-25 20:07	xleroy	Status	resolved => closed