Library Subsumption
Parberry's results
Definition direct_subsumption (n:nat) (C C':comparator_network) :=
forall s:bin_seq n, In s (outputs C n) ->
In s (outputs C' n).
Theorem Parberry : forall n C C' N, channels n C -> direct_subsumption n C C' ->
sorting_network n (C'++N) -> sorting_network n (C++N).
Bundala & Závodný's results
Definition subsumption (n:nat) (C C':comparator_network)
(P:permut) (HP:permutation n P) :=
forall s:bin_seq n, In s (outputs C n) ->
In (apply_perm P s) (outputs C' n).
Theorem BZ : forall n P HP C C' N, standard n C -> subsumption n C C' P HP ->
sorting_network n (C'++N) ->
sorting_network n (standardize (C ++ apply_perm_to_net P N)).
Lemma subsumption_dec_1 : forall n C C' P HP,
{subsumption n C C' P HP} + {~subsumption n C C' P HP}.
Optimized algorithm for subsumption
Definition bin_seq_compare (n:nat) (b b':bin_seq n) : comparison.
Defined.
Lemma eq_BS_compare : forall n b b', bin_seq_compare n b b' = Eq -> b = b'.
Lemma BS_compare_eq : forall n b, bin_seq_compare n b b = Eq.
Lemma BS_compare_trans : forall n b b' b'', bin_seq_compare n b b' = Lt -> bin_seq_compare n b' b'' = Lt ->
bin_seq_compare n b b'' = Lt.
Lemma BS_compare_sym_Gt : forall n b b', bin_seq_compare n b b' = Gt -> bin_seq_compare n b' b = Lt.
Definition opt_outputs C n := list_to_BTree _ (bin_seq_compare _) (outputs C n).
Definition subsumption_opt (n:nat) (C C':comparator_network)
(P:permut) (HP:permutation n P) :=
forall s:bin_seq n, BT_In s (opt_outputs C n) ->
BT_In (apply_perm P s) (opt_outputs C' n).
Lemma subsumption_opt_to : forall n C C' P HP, subsumption_opt n C C' P HP -> subsumption n C C' P HP.
Lemma subsumption_to_opt : forall n C C' P HP, subsumption n C C' P HP -> subsumption_opt n C C' P HP.
Lemma subsumption_opt_dec : forall n C C' P HP,
{subsumption_opt n C C' P HP} + {~subsumption_opt n C C' P HP}.
Lemma subsumption_dec : forall n C C' P HP,
{subsumption n C C' P HP} + {~subsumption n C C' P HP}.