Proving 50-Year-Old Sorting Networks Optimal: Part 1
Nice piece of work, if a bit esoteric (or maybe that&#x27;s the best part!).<p>I was struck by this paragraph, towards the end (edited to remove copying
artifacts):<p>&gt;&gt; This is not quite yet the full approach used by Codish et al. Instead of
using set inclusion to compare output sets, they define a relation called
subsumption. Remember that above, where we introduced sorting networks, we noted
that unconditional exchanges do not count towards the networks size as we can
always rearrange the network to eliminate them. Therefore for two candidate
sorting network prefixes A and B for which there is a sequence of unconditional
exchanges X such that outputs(AX)⊆ outputs(B), the same extension argument can
be made to show that outputs(AXS) ⊆ outputs(BS) for any suffix S. In this case A
subsumes B, and again there is no need to keep the candidate B around, as for
any sorting network BS, the network AXS will also be a sorting network of the
same size. Note that any sequence of unconditional exchanges corresponds to a
permutation and vice versa, so effectively this exploits symmetry under
permutation.<p>This is almost precisely the definition of subsumption between first-order
clauses, defined by Gordon Plotkin&#x27;s thesis (a foundational piece of work in
Inductive Logic Programming, ILP) from 1971 [1]. A more modern definition is as
follows:<p><i>Let C, D be two clauses (considered as sets of literals interpreted as a
disjunction). C ≼ D (read &quot;C subsumes D&quot;) iff there exists a substitution θ of
the variables in C such that Cθ ⊆ D.</i><p>This is a central result in ILP and logic programming also because it turns out
that if C ≼ D, then C |= D, read C entails D, or D is true whenever (in any
interpretation where) C is true. This is a generalisation relation that can be
exploited to prune a search space for logic programs that must entail a set of
positive examples and not entail a set of negative examples. These mathematics
of generalisation are the foundation of one of the main branches of ILP and set
ILP apart from machine learning approaches that are based on <i>optimisation</i>.<p>To make an analogy, reading the above paragraph from the article was, for me, as
surprising as I would imagine it would be for a phycisist reading an article on
sorting algorithms and finding that there is a computer science concept called
&quot;general relativity&quot; -and that is defined as E = mc² to boot.<p>So I was curious to see if the sorting network concept and the logic programming
concept are connected in some way, other than the obvious derivation of
&quot;subsumes&quot; from &quot;subset&quot;.<p>I looked briefly for the original definition of &quot;subsumption&quot; in the context of
sorting networks, but could only find a definition in the 2014 Codish et al.
paper cited in the article (&quot;Sorting Networks: to the End and Back Again&quot;):<p><i>The second notion involves permutations. Given two comparator networks C and C′
on n channels, we say that C subsumes C′, denoted C ≼ C′, if π(outputs(C)) ⊆
outputs(C′) for some permutation π of {1,...,n}. In this situation, if C′ can be
extended to a sorting network, then so can C (within the same size or depth),
which allows C′ to be removed from the search space.</i><p>Not only does this definition use the same notation as Plotkin&#x27;s subsumption,
where A ≼ B is read as _A_ subsumes B (and not, as it may come more natural, the
other way around) but the relation is also used to prune a search space. In cross-applied ILP
parlance, we would speak of a refinement operator that replaces C with its
specialisations.<p>It is interesting to note that while much work in ILP has used the subsumption
relation to prune a search space (or order it, or bind it, etc) Plotkin himself
proposed instead to construct the <i>least general generalisation</i> of two clauses,
which is a unique object that can be constructed without a search. Without an
<i>expensive</i> search. I now wonder if this approach can be applied to sorting
networks. But, I only wonder a little. After all, this is not my field :)<p>I&#x27;m still intrigued by the similarities of definitions and notations between the
two fields. Anyone knows where they come from?<p>____________________<p>[1] <a href="https:&#x2F;&#x2F;era.ed.ac.uk&#x2F;handle&#x2F;1842&#x2F;6656" rel="nofollow">https:&#x2F;&#x2F;era.ed.ac.uk&#x2F;handle&#x2F;1842&#x2F;6656</a><p>If you track this down, note it&#x27;s an ancient text, type-written with symbols
added in by hand and difficult to read. I&#x27;m still not done with it. There&#x27;s two
shorter papers that get right to the point:<p><i>A note on inductive generalisation</i>:<p><a href="https:&#x2F;&#x2F;www.semanticscholar.org&#x2F;paper&#x2F;A-Note-on-Inductive-Generalization-Plotkin&#x2F;aeb91d9afd98334eece191b8d3ce3239d4f91d71" rel="nofollow">https:&#x2F;&#x2F;www.semanticscholar.org&#x2F;paper&#x2F;A-Note-on-Inductive-Ge...</a><p><i>A further note on inductive generalisation</i>:<p><a href="https:&#x2F;&#x2F;www.semanticscholar.org&#x2F;paper&#x2F;A-Further-Note-on-Inductive-Generalization-Plotkin&#x2F;8a4101f8811b4cea9e212ca384834379126d58ed" rel="nofollow">https:&#x2F;&#x2F;www.semanticscholar.org&#x2F;paper&#x2F;A-Further-Note-on-Indu...</a>