Here I'd like to show an example of runtime complexity, arising from a practical problem.
The problem is this: we want to randomly assign coworkers to get each other gifts; we do not want to assign anyone to themself.
We can do this in J, viz.
fixSelf =: ([: */ ~:) (i. @: #)
pickDerangement =: ($: ` [ @. fixSelf) @: (?~@#)
secretSanta =: ] ,: (C.~ pickDerangement)
secretSanta is a monad which will shuffle everyone:
secretSanta ('Macbeth' ; 'Duncan' ; 'Malcolm' ; 'Banquo' ; 'Macduff')
┌───────┬───────┬───────┬──────┬───────┐
│Macbeth│Duncan │Malcolm│Banquo│Macduff│
├───────┼───────┼───────┼──────┼───────┤
│Malcolm│Macduff│Macbeth│Duncan│Banquo │
└───────┴───────┴───────┴──────┴───────┘
At a high level:
-
A random permutation is selected.
-
If it contains fix-points, we go to step 1. If not, we proceed.
-
We apply the derangement to our original list, and laminate for sake of presentation.
This approach is concise and in fact efficient, but this is not immediately obvious; the worst-case performance is \(O(\infty)\) (which occurs with probability zero).
In fact, the expected performance is \(O(n)\): selecting a random permutation is \(O(n)\), and the probability that a given permutation is a derangement is nonzero for all \(n\), viz.
\(!n = \lfloor \frac{n!}{e} + \frac{1}{2} \rfloor\)
whence the steps required will follow a Bernoulli distribution with probability of success \(\approx\frac{1}{e}\) and the expected number of times we'll need to select a permutation is \(e\).
So we can't prove termination, because it doesn't terminate, but we can prove that non-termination occurs with probability zero. I think this is quite interesting, because neither Idris nor ATS handle this case, despite the fact that such scenarios occur in practice.
Point being: it's possible to come up with example algorithms that stretch the current tools of computer science, but can be handled with pencil-and-paper mathematics.
