Next: , Up: Introduction to declarative programming   [Contents]


3.1.1 Declarative semantics

Mercury clauses say things that are true about the function or predicate being defined. To illustrate we will use an example from the previous chapter. (Note that, here and below, some declarations would need to be added to make this compile.)

length([]) = 0.
length([_ | Xs]) = 1 + length(Xs).

Both of these clauses are facts about the function length/1. The first simply states that the length of an empty list is zero. The second is a little more complicated because it involves variables, but it states that no matter what expressions we substitute for the variables ‘Xs’ and ‘_’, the length of ‘[_ | Xs]’ will be one greater than the length of ‘Xs’. In other words, the length of a non-empty list is one greater than the length of its tail.

These two statements are true according to our intuitive idea of length. Furthermore, we can see that the clauses cover every possible list, since every list is either empty or non-empty, and every non-empty list has a tail that is also a list. Perhaps surpisingly, this is enough to conclude that our implementation of list length is correct, at least as far as arguments and return values are concerned.

As another example, the following clauses define a predicate named append/3, which is intended to be true if the third argument is the list that results from appending the first and second arguments. (Equivalently, we could say that it is possible to split the list in the third argument to produce the first and second arguments.)

append([], Bs, Bs).
append([X | As], Bs, [X | Cs]) :-
    append(As, Bs, Cs).

The first clause is a fact that states if you append the empty list and any other list, the result will be the same as that other list. The second clause is a rule; these are taken as logical implications in which the body implies the head (i.e. ‘:-’ is interpreted as reverse implication). So this is stating that, for any substitution, if ‘Cs’ is the result of appending ‘As’ and ‘Bs’, then ‘[X | Cs]’ is the result of appending ‘[X | As]’ and ‘Bs’.

Again, both clauses are true according to the intended interpretation, which is defined as all of the propositions about the functions and predicates in the program that the programmer intends to be true. And the definition is complete, meaning that for every proposition that is intended to be true there is either a fact that covers it, or a rule whose head covers it and (under the same substitution) whose body is intended to be true. Thus we can conclude in a similar way to above that our code is correct.

The declarative semantics of a Mercury program is defined as all of the propositions that can be inferred to be true from the clauses of the program (with some additional “axioms” that are not important right now). If the program is producing incorrect output, this is saying that there is a difference between the declarative semantics and the intended interpretation. From the above discussion, there must be some clause that is false in the intended interpretation, or some definition that is incomplete.

This is the advantage of declarative programming. Despite the semantics being relatively simple—you only need to know about which propositions are true and which are false, and not how the program actually executes—it is still effective in reasoning about your program, even so far as to be able to localize a bug observed in the output down to individual clauses or definitions.

Not every question can be answered by the declarative semantics. It doesn’t tell us how the program executes, so it can’t tell us whether our program will terminate, for example, or what its computational complexity is. For that we need an operational semantics, which is the subject of the next section.


Next: , Up: Introduction to declarative programming   [Contents]