MLコンパイラdがMLコンパイラd'より優れていることを d ≦ d' と書く。
このとき、MLコンパイラの集合( D, ≦ )は、Edinburgh LCF MLを最小元とする完備半順序集合である。
D上の研究 f:D→D は、MLコンパイラdを使用してMLコンパイラd'を作成する。
このとき、d ≦ f(d) でなければならない。
d = f(d) である不動点dが得られたとき、かつそのときに限り、MLの研究は終了する。