## 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
```