# 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 allithere is somejÎ1..mwith kj= ?i

andsubtype(Sj, Ti)

elsefalse.

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) returnstrue, then . Thus, to establish the second claim, it suffices to show thatsubtype(S, T) must always returnsomething-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 > |