22.07.2019
Minimal Characterization of O-notation in Algorithm Analysis, Kalle Rutanen, Theoretical Computer Science, Volume 713, pp. 31–41, February 2018.
During my thesis defence, opponent Jarkko Kari suggested to study whether the primitive properties are independent of each other. I had already noticed that one-separation and sub-composability were each independent of the other primitive properties, but for some reason I never thought about proving the same for all of the primitive properties.
In essence, showing a primitive property independent of the others requires to find a definition of O-notation which fails the property while satisfying the other primitive properties. Linear dominance then gives another definition which satisfies all the properties. The existence of such a pair of definitions proves the desired independence. Using this technique, Kari could readily give other examples of independent primitive properties. I was very excited about this; of the possibility of proving the primitive properties minimal.
As luck would have it, the candidate definitions that I had studied in the thesis were directly usable for this task. Trivial linear dominance proved one-separation independent, asymptotic linear dominance sub-composability independent, and affine dominance sub-homogeneity in independent. I was then left with the task of constructing new definitions to prove the independence of other primitive properties.
After a few days, I had obtained proofs for the independence of all primitive properties except locality. I tried to find a suitable definition to show locality independent, but did not succeed in that. This took my thoughts to my previous proof of completeness, where I was trying to prove the wrong result for many days in vain. This time I would try to prove the negative also! And sure enough, it did not take long to finish a proof which showed that locality is implied by the other primitive properties. This was very surprising to me. The proof was really fun to come by; it has to be my favourite in the whole book.
Even though locality can be proved from the other primitive properties, trying to prove things without it seems like a really bad idea. In essence, the proofs would then need to imitate the indirect way of obtaining locality. I decided to instead retain locality as a primitive property, so that primitive properties do not form a minimal axiom set. I then named the primitive properties without locality as pre-primitive properties, and showed minimality for pre-primitive properties. I think that the primitive properties make a really nice trade-off between understandability and minimality.