# Merging sorted lists

A good algorithm to sort lists is the merging algorithm that relies
en merging sublists that are already sorted. The structure of this
algorithm can be summarized by the following two equations
(in both cases one supposes that *a* is smaller than *b*):

merge (a :: l) (b :: l') = a :: merge l (b :: l')
merge (b :: l) (a :: l') = a :: merge (b :: l) l'

This function is not structural recursive with respect to the
the first list (because of the second equation) or with respect
to the second list (because of the first equation), but the sum of length
of lists decreases at each recursive call. Use this remark to
build an algorithm that sorts lists of elements of type *A*, working
in a functor taking a module with the following type as argument.

Module Type Comparable_data.
Parameter A : Set.
Parameter Ale : A -> A -> Prop.
Parameter Ale_dec : forall x y:A, {Ale x y}+{Ale y x}
End Comparable_data.

## Solution

Look at this file.

Going home

Yves Bertot
Last modified: Mon Mar 1 11:32:13 MET 2004