Email Gateway (Jan 25 2026 at 15:45): Email Gateway (Jan 25 2026 at 15:45):From: Tobias Nipkow <nipkow@in.tum.de>
Swap Distance
Manuel Eberl
Given two lists that are permutations of one another, the swap distance (also
known as the Kendall tau distance) is the minimum number of swap operations of
adjacent elements required to make the two lists the same.
Equivalently, the swap distance of two finite linear orders and is the number of
disagreements of the two orders, i.e. of pairs such that and .
This article defines these two notions of swap distance as well as their
equivalence under the obvious isomorphism between lists and linear orders given
by interpreting a list as a ranking of elements in descending order.
An efficient O(n log n) algorithm to compute the swap distance is also provided
via the connection to the number of inversions of a list, for which an efficient
algorithm is already available in the AFP.
https://www.isa-afp.org/entries/Swap_Distance.html
Linear orders as rankings
Manuel Eberl
This entry formalises the obvious isomorphism between finite linear orders and
lists, where the list in question is interpreted as a ranking, i.e. it lists the
elements in descending order without repetition.
It also provides an executable algorithm to compute topological sortings, i.e.
all rankings whose linear orders are extensions of a given relation.
https://www.isa-afp.org/entries/Rankings.html
The Impossibility of Strategyproof Rank Aggregation
Manuel Eberl and Patrick Lederer
In Social Choice Theory, a social welfare function (SWF) is a function that
takes a collection of individual preferences on some set of alternatives and
returns an aggregated preference relation.
More formally: Consider finite sets of agents N = {1,...,n} and alternatives A =
{x1,...,xm}. The input of an SWF is an n-tuple of rankings (i.e. linear orders)
of A, and its output is a ranking of A as well.
Various desirable properties on SWFs can be defined:
Anonymity: The SWF is invariant under permutation of the agents.
Unanimity: If all voters prefer x over y, then x is preferred over y in the
output ranking as well.
Majority consistency: If there exists a ranking x1,...,xm such that for every i
< j, the alternative xi is preferred over xj by more than half of the agents,
that ranking must be returned.
Kemeny strategyproofness: Strategic voting is not possible for a single agent,
i.e. no agent can achieve a result more aligned with their own preferences by
lying about them.
This entry contains two impossibility results for SWFs with alternatives and agents:
There exists no anonymous, unanimous, and Kemeny-strategyproof SWF for m >=
5 and n even or for m = 4 and n a multiple of 4.
There exists no majority-consistent and Kemeny-strategyproof SWF for m = 4
and n >= 3 or m >= 4 and n : {9,11,13,15} Un {17,...}.
For some of the base cases, SAT solving is used by letting specialised
automation prove a large number of clauses, translating to the DIMACS format,
and importing a proof pre-generated by an external SAT solver using Lammich's
GRAT format.
https://www.isa-afp.org/entries/SWF_Impossibility.html
Enjoy 3 times!
Last updated: Jan 31 2026 at 12:53 UTC