Sort
Module
signature SORT
structure Sort
:> SORT
This module defines functions for testing orderedness of lists, inserting elements into ordered lists, merging ordered lists, and sorting lists, as well as the total ordering type on which they are based.
In the following specifications, if xs
and yz
are lists, then:
xs
is a permuation of ys
iff xs
can be formed by reordering the elements of ys
;
xs
is a sub-permutation of ys
iff xs
can be formed from ys
by first removing some (possibly none) of the elements of ys
, and then reordering the remaining elements.
[2, 1, 3, 1]
is a permutation of [1, 3, 2, 1]
, and [6, 5, 4, 1]
is a sub-permutation of [1, 4, 5, 2, 6, 4]
.
type 'a total_ordering = 'a * 'a -> order
val equal : 'a total_ordering -> 'a * 'a -> bool
val less : 'a total_ordering -> 'a * 'a -> bool
val lessEqual : 'a total_ordering -> 'a * 'a -> bool
val sorted : bool * 'a total_ordering -> 'a list -> bool
val insert : bool * 'a total_ordering -> 'a * 'a list -> 'a list
val merge : bool * 'a total_ordering -> 'a list * 'a list -> 'a list
val sort : bool * 'a total_ordering -> 'a list -> 'a list
type 'a total_ordering = 'a * 'a -> order
cmp
(for "compare") of type 'a total_ordering
must satisfy the following formulas, for all values x
, y
and z
of type 'a
:
cmp(x, y) = EQUAL
iff x
and y
are indistinguishable;
cmp(x, y) = LESS
iff cmp(y, x) = GREATER
;
cmp(x, y) = LESS
and cmp(y, z) = LESS
, then cmp(x, z) = LESS
.
cmp(x, x)
;
cmp(x, y) = EQUAL
iff cmp(y, x) = EQUAL
;
cmp(x, y) = EQUAL
and cmp(y, z) = EQUAL
, then cmp(x, z) = EQUAL
;
cmp(x, y) = EQUAL
and cmp(y, z) = LESS
, then cmp(x, z) = LESS
;
cmp(x, y) = LESS
and cmp(y, z) = EQUAL
, then cmp(x, z) = LESS
.
equal cmp (x, y)
cmp(x, y) = EQUAL
.
less cmp (x, y)
cmp(x, y) = LESS
.
lessEqual cmp (x, y)
cmp(x, y)
returns LESS
or EQUAL
.
sorted (true, cmp) xs
lessEqual cmp (ListAux.sub(xs, i),
ListAux.sub(xs, i + 1))
, for all 1 <= i <= length xs - 1
.
sorted (false, cmp) xs
less cmp (ListAux.sub(xs, i),
ListAux.sub(xs, i + 1))
, for all 1 <= i <= length xs - 1
.
insert (true, cmp) (x, ys)
sorted (true, cmp) ys
, then insert
returns a permutation zs
of x :: ys
such that sorted (true, cmp) zs
.
insert (false, cmp) (x, ys)
sorted (false, cmp) ys
, then insert
returns a sub-permutation zs
off x :: ys
such that sorted (false, cmp) zs
and, for all elements w
of x :: ys
, there is an element z
of zs
such that equal cmp (w, z)
.
merge (true, cmp) (xs, ys)
sorted (true, cmp) xs
and sorted (true, cmp) ys
, then merge
returns a permuation zs
of xs @ ys
such that sorted (true, cmp) zs
.
merge (false, cmp) (xs, ys)
sorted (false, cmp) xs
and sorted (false, cmp) ys
, then merge
returns a sub-permutation zs
of xs @ ys
such that sorted (false, cmp) zs
and, for all elements w
of xs @ ys
, there is an element z
of zs
such that equal
cmp (w, z)
.
sort (true, cmp) xs
ys
of xs
such that sorted (true, cmp) ys
.
sort (false, cmp) xs
ys
of xs
such that sorted (false, cmp) ys
and, for all elements x
of xs
, there is an element y
of ys
such that equal cmp (x, y)
.
sort (dups, cmp) xs
begins by checking whether sorted (dups, cmp) xs
, in a computation taking at most length xs - 1
calls to cmp
. If sorted
returns true
, then xs
is returned. Otherwise, xs
is sorted using merge sort.
Forlan Version 4.12
Copyright © 2019 Alley Stoughton