sort_inversions[N: posnat, T: TYPE, <= : (total_order?[T]) ]: THEORY %---------------------------------------------------------------------------- % inversions, i.e., index pairs i < j such that A(i) > A(j) % are witnessses that array A is not sorted. % transposition of adjacent elements A(j) > A(j+1) decrease % the number of inversions. This is the basis of bubble sort. % % Author: Alfons Geser, National Institute of Aerospace, 2003 %----------------------------------------------------------------------------
A : VAR [below(N) -> T]
inv : VAR finite_set[index_pair]
i,j,k: VAR below(N)
x : VAR T
% to discharge the TCC for inversions
finite_inversions: LEMMA
is_finite[index_pair]({(i, j) | i < j & NOT A(i) <= A(j)})
% the set of inversions, i.e, of index pairs (i,j) such that % A(i) and A(j) are not in sorted order
inversions(A): finite_set[index_pair] =
{(i,j) | i < j & NOT A(i) <= A(j)}
pi: VAR permutation
% to discharge the TCC for ap(pi,inv) below
finite_ap: LEMMA
is_finite[index_pair](LAMBDA (i, j): inv(pi(i), pi(j)))
% apply a permutation pi to a set of index pairs
ap(pi,inv): finite_set[index_pair] = LAMBDA (i,j): inv(pi(i),pi(j))
% applying a permutation does not change the number of index pairs
card_ap: LEMMA
card[index_pair](ap(pi,inv)) = card[index_pair](inv)
inversions_transpose: LEMMA
j < N-1 & NOT A(j) <= A(j+1) =>
inversions(A o transpose(j,j+1)) =
ap(transpose(j,j+1),remove((j,j+1),inversions(A)))
% main results: % 1) if (j,j+1) is an inversion then exchanging j with j+1 decreases % the number of inversions by one % 2) if there are no inversions then A is sorted % 3) if there are inversions then there are inversions of the form (j,j+1)
card_inversions_transpose: THEOREM
j < N-1 & NOT A(j) <= A(j+1) =>
card(inversions(A)) = 1 + card(inversions(A o transpose(j,j+1)))
successive_inversion_lem: LEMMA
(EXISTS i: i < i+d & i+d < N & NOT A(i) <= A(i+d)) =>
(EXISTS j: j < N-1 & NOT A(j) <= A(j+1))
successive_inversion_exists: THEOREM NOT sorted?(A) => EXISTS j: j < N-1 & NOT A(j) <= A(j+1)
END sort_inversions
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.0Bemerkung:
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
