Proving 50-Year-Old Sorting Networks Optimal: Part 1

Proving 50-Year-Old Sorting Networks Optimal: Part 1
jix.one

I was struck by this paragraph, towards the end (edited to remove copying artifacts):

>> 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.

This is almost precisely the definition of subsumption between first-order clauses, defined by Gordon Plotkin's thesis (a foundational piece of work in Inductive Logic Programming, ILP) from 1971 [1]. A more modern definition is as follows:

Let C, D be two clauses (considered as sets of literals interpreted as a disjunction). C ≼ D (read "C subsumes D") iff there exists a substitution θ of the variables in C such that Cθ ⊆ D.

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 optimisation.

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 "general relativity" -and that is defined as E = mc² to boot.

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 "subsumes" from "subset".

I looked briefly for the original definition of "subsumption" in the context of sorting networks, but could only find a definition in the 2014 Codish et al. paper cited in the article ("Sorting Networks: to the End and Back Again"):

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.

Not only does this definition use the same notation as Plotkin'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.

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 least general generalisation of two clauses, which is a unique object that can be constructed without a search. Without an expensive 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 :)

I'm still intrigued by the similarities of definitions and notations between the two fields. Anyone knows where they come from?

____________________

[1] https://era.ed.ac.uk/handle/1842/6656

If you track this down, note it's an ancient text, type-written with symbols added in by hand and difficult to read. I'm still not done with it. There's two shorter papers that get right to the point:

A note on inductive generalisation:

https://www.semanticscholar.org/paper/A-Note-on-Inductive-Ge...

A further note on inductive generalisation:

https://www.semanticscholar.org/paper/A-Further-Note-on-Indu...

Codish et al. have a background in SAT solving, which is somewhat related to logic programming. In SAT solving subsumption of clauses usually doesn't involve any substitutions. That's the notion of subsumption I was familiar with before reading Codish et al. Given that, extending subsumption to handle the symmetries inherent in the problem felt like a natural extension as it maintains all the relevant properties, but I also wouldn't be surprised if this was inspired by ILP.