Constraint Logic Programming:
A Programming Approach to Teaching the Semantics of Logic

James J. Lu

Department of Computer Science
Bucknell University
Lewisburg, PA 17837. U.S.A.
jameslu@bucknell.edu

Abstract

The problem of teaching the notion of logical consequence is discussed, and a solution proposed. The essential idea is to make concrete the abstract notion of interpretation through computer programs. Constraint Logic Programming appears to meet this idea nicely. This material is based upon work supported by the NSF under Grant CCR9225037.

Introduction

This paper analyzes a major conceptual difficulty students have in learning logic in general, and in learning the semantics of logic programming in particular. The difficulty is in understanding the notion of logical consequence (i.e. entailment). We show how Constraint Logic Programming (CLP) [JL87], a recent extension to classical logic programming, can be used to overcome this difficulty especially for undergraduate computer science students who possess some intuition regarding computation and programming. To simplify our discussion, we focus on entailment in the context of Horn-clause logic programming. However, we believe the ideas presented here can be more generally applied to make the semantical foundation of mathematical logic more accessible to undergraduate students.

The context in which the thoughts described here originated is in the teaching of the undergraduate programming languages course. Typically, the topics in the course are divided among state-based (procedural and object-oriented), function-based (functional), and relation-based language paradigms (logic). In the last case, an attempt is made to illustrate the declarative nature of programming in logic, i.e. to illustrate the correspondence between the declarative semantics of logic programming and its operational counterpart.

Logic Programming and Logical Consequence

Hence, a proper introduction to logic programming requires an understanding of logic. In particular, as computing in logic programming corresponds to determining logical consequence, some coverage of interpretation, satisfiability, and theoremhood is crucial in setting the semantical basis for discussion [Llo88].

To communicate these ideas, the first notion that must be understood is interpretation. A common way to illustrate the idea is to first write down a specific formula, say p(f(a)), and to discuss a number of possible interpretations. For instance, take the domain D to be the natural numbers, and assign to p the relation odd, to f the function successor, and to a the value 1. Under this interpretation, p(f(a)) is a formula that is not satisfied. On the other hand, an interpretation which assigns p to even while assigning f and a as before will satisfy p(f(a)). Yet another interpretation may consider an entirely different domain. For example, take the domain to be the set of names of people in a family, and a, f and p may be interpreted respectively as 'adam', 'father', and 'tall'.

Though a discussion of the sort above is intuitively clear for small examples, many students find it difficult to separate the syntax of the formula from its semantics. Certainly, for a large number of students, mathematical logic is the first topic of study for which they must learn to detach a sequence of symbols from any consideration of meaning a priori. Hence for more complex cases, the idea of interpretations over arbitrary domains is quickly lost. Even at the propositional level, where the notion of interpretations is more easily seen through the use of truth tables, logical consequence -- truth with respect to all models of a theory -- rarely holds any intuition.

The problem is therefore twofold. Students first of all must accept the idea that the semantics of a formula can be divorced from its syntax, on top of that they need to consider a concept defined based on interpretations over all possible domains which includes numerous non-standard interpretations; i.e. the non-intended interpretations of the Lowenheim-Skolem Theorem.

Without the firm semantical grounding, the operational aspects of Horn-clause logic programming, as seen through resolution and unification ([Rob65]), are reduced to meaningless syntactic exercises. Students either perform these computations without any semantical context, or they continue to see the symbols of the formulas as having some inherent, uncontrovertible meaning. In the latter case, students are continually surprised by when, for example, Prolog does not respond positively to the query p(3) from the given axiom p(1 + 2).

An Analysis

In one sense, the problem is simply a matter of presentation. The traditional exposition of logic in logic texts promotes a deductive style of learning | a style that is less suitable for most students than the inductive style [WO93]. Suppose we consider for a moment that the two parts of logic, the syntax and the semantics, to be two axes of a plane (the logic plane). Then a traditional style of presentation cuts this plane in the direction parallel with the semantic axis since, as discussed in the previous section, we typically fix a formula and examine the possible interpretations that may be given for that formula. Again, students find such a discussion difficult to grasp since by varying the interpretations of a formula, they are forced to detach the symbols of the formulas from what they perceive as the ``obvious'' interpretation.

Suppose instead, we slice the logic plane in the direction parallel with the syntactic axis, thus fixing an interpretation while considering the meaning of various formulas within that interpretation. This allows students to take advantage of any intuition they might possess regarding a specific domain (e.g. the real numbers, the integers), and moreover the symbols of the formulas can serve as reminders of the ``intended'' underlying interpretation. Indeed, this is the perspective supported by Constraint Logic Programming (CLP).

In CLP, Horn clauses are augmented with constraints, and are called constraint clauses. Formally, the syntax of a constraint clause is a first order formula, but with the semantics defined over a fixed interpretation. Hence, given the structure < N,< ,+ > where N is the natural numbers and the interpretation that maps + to the addition operator, the constraint clauses

1. odd(1).
2. odd(X + 2) < -- odd(X).
define the set of all odd number in N. The key is that in these two formulas, the symbols 1, 2, + have fixed meanings within the chosen structure < N,< ,+ >. Based on the fixed interpretation, CLP uses the idea of constraint solving to determine the truth and the falsity of a formula with respect to the given program. The basic operational details are illustrated in the following resolution deduction for answering whether 3 is odd; odd(3).
3. < -- odd(3) Initial Query
4. < -- (3 = X + 2) /\ odd(X) Resolving (3) and (2)
5. < -- (3 = X + 2) /\ (1 = X) Resolving (4) and (1)

At each step of a deduction, an atom is selected from the current goal and matched with the conclusion of an implication in the given program. Matching the atom odd(3) in the initial query with the conclusion odd(X + 2) of clause (2) yields the subquery odd(X) along with the constraint 3 = X + 2. As the constraint has a solution within the structure < N, < , + >, the deduction continues. In the second step, the atom odd(X) is matched against the atom odd(1) in clause (1), thus producing the resolvent (3 = X + 2) /\ (X = 1). As the statement holds in the structure < N, < , + >, the deduction succeeds.

The point here is that the above deduction makes sense to students simply because we are interpreting the above program under the intended interpretation, namely < N, < , + >. As a consequence, the symbols 1, 2, 3 denote what they ``should'' denote, and the operator + behaves in the way that it ``should'' behave.

Generically, the computational mechanism of CLP contains a resolution component for generating new queries based on selections of atoms from queries and clauses from the given program (see Figure 1). In addition, there is a constraint solving component which tests for the solvability of the constraint part within each query of the deduction. In the above example, the constraint solver Sigma in Figure 1 must interpret the symbols +, < and 0..9 faithfully in order to implement the necessary algorithms for solving arithmetic constraints.

                   Xi0,Q0    C1
                     |       /
                     |      /
                     |     /
                     |    /
                     |   /
                   Xi1,Q1    C2
                     |       /
   Constraint        |      /          Resolution
   Solver            |     /
   Sigma             |    /
                     |   /
                   Xi2,Q2  
                     .
                     .
                     .
              Xi{n-1},Q{n-1}  Cn  
                     |       /
                     |      /
                     |     /
                     |    /
                     |   /
                   Xin,Qn


                  Figure 1
       (The Xi's represent constraints)

How Does This Help

The purpose of our discussion is to develop means to convey to students the notions of interpretation and logical consequence in classical logic programming more effectively. Particularly for computer science students, we hope to utilize their computational background in this endeavor. So far, we examined an extension of classical logic programming, namely CLP, where by fixing attention to consequence with respect to a single interpretation, the set of answerable queries is a superset of the set of answerable queries in classical logic programming. In the example program odd from the previous section, odd(3) is not classically entailed since there are interpretations in which each clause in the program holds while the query odd(3) does not. The question is, how can this weaker view of consequence help students to understand the classical consequence relation?

The important observation is that as a computer implementation of a language, the constraint solver Sigma which underlies the CLP computation of Figure 1, in effect, makes explicit the structure over which any given CLP program is interpreted. The constraint solver Sigma can be regarded as a function (or a subprogram) of the overall CLP interpreter. As such, it provides a ``concrete'' representation of the abstract notion of an interpretation since within Sigma, explicit references to the operation + will appear whenever the symbol + occurs in the given CLP program.

Now without changing the syntax of the program odd, suppose we replace the constraint solver Sigma with a different constraint solver, say Sigma0, which interprets the symbols 0..9, +, and < differently. Then clearly, odd defines a very different relation than the ``intended'' one, and in particular, odd(3) may no longer be satisfied under the new interpretation. Certainly, students with experience in computer programming should have little difficulty in understanding this. It is akin to the replacement of a function (or procedure) in a program with a different function whose input-output behavior differs from the original function. Naturally, the behavior of the overall program will change accordingly.

Finally, after examinations of several non-standard interpretations of the same program odd through several constraint solvers, the classical notion of entailment (i.e. truth in all models of the program) may be introduced simply by the removal of the constraint solver Sigma. Equivalently, we may speak in terms of replacing Sigma with an unspecified constraint solver Sigma'. While initially, soundness of a deduction is measured against the fixed interpretation given by the constraint solver Sigma, soundness in the presence of an unspecified constraint solver can only be guaranteed by allowing for constraints to be solved syntactically.

With respect to the example odd, 3 = X + 1 is not solvable syntactically since no substitution for X will yield an expression for X + 1 that is syntactically identical to 3. Similarly, X = 3 + 1 is only solved under the condition that X is substituted with the expression 3 + 1. Through this requirement, any conclusion thus derived must be sound regardless of what Sigma' turns out to be. In other words, the computational counterpart of the notion of logical consequence is simply that the only allowable deductions are those that are sound with respect to arbitrary constraint solvers.

A Teaching Tool

In a sense, what we are proposing here is a substitute. That is, our suggested way of thinking encourages an association of interpretations with computer programs. Specifically, an interpretation relates symbols in a set of logical formulas to functions, or more generally, modules, that are defined within computer programs. A useful tool to further facilitate the teaching of this idea is a "hybrid programming language" that combines logic and algorithmic programming. A program written in this language has two parts: a set of logical formulas L (typically clauses) and a set of functions F (with associated data structures) written in some conventional imperative or functional language. The clauses define relations using base relations as well as functions in F. Executions of the functions in F are invoked during deductions over the clauses in L. Most importantly, the programmer must specify, for each constant and function symbols occurring in L, a corresponding denotation either in F or as a language built-in. Figure 2 shows an example of how such a program might appear. A feature that will be provided is the ability to not associate a symbol with any existing functions or type. Such symbols are uninterpreted and are handled syntactically as in ordinary logic programming.

Although the high-level, declarative semantics of this hybrid language can be given by the theory of CLP, the language also raises a number of interesting theoretical and practical programming languages issues such as scoping rules, encapsulation, type checking, and run-time representations. Should these issues be resolved, we believe the language will provide an invaluable logic-teaching tool.

           F                       | Association  |       L
    -------------------------------|--------------|------------------------
    function f1(x:integer):integer;| succ with f1 | p1(X) < -- q(succ(X),1).
    begin                          |              | 
      . . .                        | max with f2  | q(X,Y,max(X,Y)).
    end;                           |              | 
                                   | 1 is integer | q(X,Y,Z) < - ...
                                   |              |
    function f2(x,y:integer):integer;             |
    begin                          |              |
      . . .                        |              |
    end;                           |              |

                          Figure 2

Conclusion

Whenever the following question is posed to students,

"Give an example of an unsatisfiable formula."
it invariably brings out answers of the following sorts from students.
American_president(Clinton)
Course_grade(John,A)
Equal(Plus(1,1),2)
These mistakes suggest a misunderstanding regarding the role of symbols in logic, and in particular what it means to interpret them in a certain way.

We have argued that CLP provides a concrete realization of the abstract notion of interpretation through the use of constraint solving. A CLP-deduction is easier for students to grasp than classical resolution deduction since it is grounded more in ``real-world'' intuition. As a byproduct, students can also better learn the notion of classical logical consequence since it is possible to take advantage of their familiarity with computer programming.

References