The combination of non-determinism and sorting is mostly associated with permutation sort, a sorting algorithm that is not very useful for sorting and has an awful running time.
In this paper we look at the combination of non-determinism and sorting in a different light: given a sorting function, we apply it to a non-deterministic predicate to gain a function that enumerates permutations of the input list. We get to the bottom of necessary properties of the sorting algorithms and predicates in play as well as discuss variations of the modelled non-determinism.
On top of that, we formulate and prove a theorem stating that no matter which sorting function we use, the corresponding permutation
function enumerates all permutations of the input list. We use free theorems, which are derived from the type of a function
alone, to prove the statement.
Mon 19 SepDisplayed time zone: Osaka, Sapporo, Tokyo change
17:00 - 18:15 | |||
17:00 25mTalk | Compact Bit Encoding Schemes for Simply-Typed Lambda-Terms Research Papers Kotaro Takeda University of Tokyo, Japan, Naoki Kobayashi University of Tokyo, Japan, Kazuya Yaguchi Tohoku University, Japan, Ayumi Shinohara Tohoku University, Japan DOI | ||
17:25 25mTalk | Queueing and Glueing for Optimal Partitioning (Functional Pearl) Research Papers Shin-Cheng Mu Academia Sinica, Taiwan, Yu-Hsi Chiang National Taiwan University, Taiwan, Yu-Han Lyu Dartmouth College, USA DOI | ||
17:50 25mTalk | All Sorts of Permutations (Functional Pearl) Research Papers Jan Christiansen Flensburg University of Applied Sciences, Germany, Nikita Danilenko University of Kiel, Germany, Sandra Dylus University of Kiel, Germany DOI | ||