DTC

In the following tutorial, we learn how to verify the correctness of the type of the append predicate.

Append

We start with the definition of the append predicate.

    append ([], L, L).
    append ([X|Xs], Y, [X|Zs]) :-
        append (Xs, Y, Zs).

This code will be first preprocessed to the following form:

    append (tuple3 (nil, L, L)).
    append (tuple3 (cons (X, Xs), Y, cons (X, Zs))) :-
        append (tuple3 (Xs, Y, Zs)).

This is due to the fact that the typechecker accepts only unary predicates and that brackets are merely syntactic sugar used to denote list constructors: cons and nil. The preprocessor understands more extensions and is described in detail in the reference manual.

Interface

Since prolog operates exclusively on terms, there is no place for type annotations in the source file. Thus, the annotations have to be stored in a separate file with a .pi extension. The annotation for the append predicate is very simple:

    append : ain -> aout.

This simply says that the typechecker should look into the type definitions and find appropriate states: "ain" and "aout".

Type Definitions

Now we need to define the input and output types of the append predicate. First, we need to define which terms should be recognized as lists:

    nil is list.
    cons (top, list) is list.

As you can see in the example above, we say that nil should be recognized as list and cons(x,y) should also be recognized as list if x has been recognized to be anything (top is a special symbol to denote everything) and y has been recognized as list. Now it's time to uncover the type of our predicate.

    tuple3 (list, list, top) is ain.
    tuple3 (list, list, list) is aout.

Our claim is: whenever we feed append with two lists and something else, and the program terminates, we get three lists as a result.

Verification

In order to verify that this type is correct, simply save the examples in files: append.pl, append.pi and typedefs.td and run the typechecker like this:

    $ dtc typedefs.td append
    Preprocessing append.pl...done.
    Reading type definitions from typedefs.td...done.
    Parsing /tmp/dtc-DrH1Yk.pl...done.
    Parsing /tmp/dtc-DrH1Yk.pi...done.
    Checking types...ok.

Determinism

As we know, append is not only used to append two lists:

    append ([1, 2, 3], [4, 5, 6], X)

but also to split a list into two parts:

    append (X, Y, [1, 2, 3, 4, 5, 6])

And there comes one of the features of our typechecker: it accepts nondeterministic types too.

    tuple3 (list, list, top) is ain.
    tuple3 (top, top, list) is ain.
    tuple3 (list, list, list) is aout.

In the example above we say: no matter whether you give two lists to append, or one list to split, you always end up with three lists. And since this type is valid, the typechecker will accept it.

Counterexamples

Nondeterminism lets us define even more sophisticated types, like for example this one:

    cons (top, olist) is olist.
    cons (one, list) is olist.
    zero is one.

The example above defines the type of the list with at least one zero. We can now try to prove that append preserves the minimum-one-element property.

    tuple3 (olist, list, top) is ain.
    tuple3 (list, olist, top) is ain.
    tuple3 (list, list, olist) is aout.

This says: if one of the arguments contains at least one zero, the resulting list will contain at least one zero as well. Although the reasoning is true, the typechecker will fail:

    $ dtc typedefs.td append
    Preprocessing append.pl...done.
    Reading type definitions from typedefs.td...done.
    Parsing /tmp/dtc-CB5wPC.pl...done.
    Parsing /tmp/dtc-CB5wPC.pi...done.
    Checking types...invalid.
    
    Typechecking failed for the clause:
    in_append (tuple3 (V_Xs, V_Y, V_Zs)) <-- \
        in_append (tuple3 (cons (V_X, V_Xs), V_Y, cons (V_X, V_Zs)))
    
    With the following counterexample:
    V_Xs = nil
    V_Y = nil
    V_X = zero
    V_Zs = cons (zero, nil)

The typechecker was actually trying to prove that whenever you pass the correct term to the predicate, it will pass a correct term further, which does not have to be true in order for the type to be correct. As an example consider the following call:

    append([zero],[],Z).

The bottommost recursive call to the append predicate will get two empty lists as arguments, which violates the type correctness.

Notice that the type checker always produces a respective counterexample that violates type correctness, which eases program debugging.