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.