Wiki Agenda Contact Version française

Same fringe

``Same fringe'' is a famous problem. Given two binary search trees, we must decide whether they contain the same elements (more details here).

The solution presented here uses two zippers, to traverse both trees simultaneously. Each zipper corresponds to the left spine of a tree, as a bottom-up list.


Authors: Jean-Christophe Filliâtre

Topics: Trees

Tools: Why3

see also the index (by topic, by tool, by reference, by year)


(*
  ``Same fringe'' is a famous problem.
  Given two binary search trees, you must decide whether they contain the
  same elements. See for instance http://www.c2.com/cgi/wiki?SameFringeProblem
*)

module SameFringe

  use int.Int
  use list.List
  use list.Length
  use list.Append

  (* binary trees with elements at the nodes *)

  type elt

  val eq (x y: elt) : bool ensures { result <-> x=y }

  type tree =
    | Empty
    | Node tree elt tree

  function elements (t : tree) : list elt = match t with
    | Empty -> Nil
    | Node l x r -> elements l ++ Cons x (elements r)
  end

  (* the left spine of a tree, as a bottom-up list *)

  type enum =
    | Done
    | Next elt tree enum

  function enum_elements (e : enum) : list elt = match e with
    | Done -> Nil
    | Next x r e -> Cons x (elements r ++ enum_elements e)
  end

  (* the enum of a tree [t], prepended to a given enum [e] *)

  let rec enum t e variant { t }
    ensures { enum_elements result = elements t ++ enum_elements e }
  = match t with
    | Empty -> e
    | Node l x r -> enum l (Next x r e)
    end

  let rec eq_enum e1 e2 variant { length (enum_elements e1) }
    ensures { result=True <-> enum_elements e1 = enum_elements e2 }
  = match e1, e2 with
    | Done, Done ->
        True
    | Next x1 r1 e1, Next x2 r2 e2 ->
        eq x1 x2 && eq_enum (enum r1 e1) (enum r2 e2)
    | _ ->
        False
    end

  let same_fringe t1 t2
    ensures { result=True <-> elements t1 = elements t2 }
  = eq_enum (enum t1 Done) (enum t2 Done)

  let test1 () = enum Empty Done
  let test2 () = eq_enum Done Done
  let test3 () = same_fringe Empty Empty

  val constant a : elt
  val constant b : elt

  let leaf x = Node Empty x Empty

  let test4 () = same_fringe (Node (leaf a) b Empty) (Node Empty a (leaf b))
  let test5 () = same_fringe (Node (leaf a) b Empty) (Node Empty b (leaf a))

  exception BenchFailure

  let bench () raises { BenchFailure -> true } =
    if not (test4 ()) then raise BenchFailure

end

module Test

  use int.Int
  clone SameFringe with type elt = int

  let test1 () = enum Empty Done
  let test2 () = eq_enum Done Done
  let test3 () = same_fringe Empty Empty

  constant a : int = 1
  constant b : int = 2

  let leaf x = Node Empty x Empty

  let test4 () = same_fringe (Node (leaf a) b Empty) (Node Empty a (leaf b))
  let test5 () = same_fringe (Node (leaf a) b Empty) (Node Empty b (leaf a))

end

download ZIP archive