Using one the two previous lemmas the algorithmic rules

If we add the type Bool, how do these properties change?

This brings us to the definition of the algorithmic subtype relation.

We say that the algorithmic rules are sound because every statement that can be derived from algorithmic rules can also be derived from the declarative rules (the algorithmic rules do not prove anything new), and complete because every statement that can be derived from the declarative rules can also be derived from the algorithmic rules (the algorithmic rules prove everything that could be proved before).

16.1.5 Proposition [Soundness and Completeness]

then subtype(T1, S1) ∧subtype(S2, T2)
else if S = {kj:SjjÎ1..m} and T = {?i:TiiÎ1..n}
then {?iiÎ1..n} ⊆ {kjjÎ1..m}
∧for all i there is some jÎ1..m with kj = ?i
and subtype(Sj, Ti)
else false.

A concrete realization of this algorithm in ML appears in Chapter 17.

Proof: The first claim is easy to check (by a straightforward induction on a derivation of ). Conversely,

it is also easy to check that, if subtype(S, T) returns true, then . Thus, to establish the second claim, it suffices to show that subtype(S, T) must always return something-i.e., that it cannot diverge. This we can do by observing that the sum of the sizes of the input pair S and T is always strictly larger than the sum of the sizes of the arguments to any recursive call that that algorithm makes. Since this sum is always positive, an infinite sequence of recursive calls is not possible.

	< Free Open Study >