In general, we are interested in two properties of logic meta-interpreters for normal programs.
If an answer produced by npl has free variables in it then the correctness of such an answer means that each grounding of those variables produces an evident answer for the goal.
Example. Consider the normal program
We could have originally given a (more complicated) definition for an evident answer substitution that allowed free variables.
Meta-interpreters like npl can be counted on as having evidentiary correctness because these meta-interpreters are designed to actually construct the required clause trees.
Exercise 1. Argue informally, using careful inspection of the source code for npl, that if and when npl has finished computing an answer it has actually constructed a bonafide clause tree and therefore computed an evident answer (provided free variables in npl's answers are considered appropriately, as mentioned above). The specification to inspect is that given previously for ctie (the clause tree inference engine), which was designed to grow these trees incrementally.
Notice carefully that evidentiary soundness is different than the usual concept of logical soundness, which would require that the answers computed should be logical consequences of the program. Logical soundness of the meta-interpreter is a concept that would really only make sense if the normal program is known to be consistent.
Exercise 2. Show that evidentiary correctness implies logical soundness. Give some sample programs to show that evidentiary correctness is a strictly stronger condition than logical soundness. What kind of programs do these examples have to be?
The second important property for a normal logic meta-interpreter is called evidentiary completeness. There are varying degrees of evidentiary completness. As an acceptor (Yes/No) algorithm the meta-interpreter should say Yes when given a ground normal goal G for which there exists a closed clause tree rooted at G; and otherwise the meta-interpreter should answer No. For the npl meta-interpreter this means that the Prolog goal npl(G) would yield yes in the former case, No in the latter.
As an answer generator, varying degrees of completeness would result depending on how many answers the meta-interpreter would give for normal goals with variables. The best that one can hope for is that the meta-interpreter would find all possible values for the variables in the goal.
A normal program is recursive if the collection of contrapositive clauses contra(P) is recursive.
Exercise 3. Give a formal definition of a recursive normal program, with all of the details. This takes some careful formulation even though the concept is fairly straightforward. (Hint: You know what a recursive Prolog program is, even though it has not be formally defined in the tutorial!)
Exercise 4. Show, using a variety of examples of nonrecursive normal programs, that npl can generate all possible answers, but that, even when it does, it still might generate many repeated answers. Use Prolog goals like ?- bagof(answer_list, npl(G), S) where answer_list is a list of the variables in G; e.g., if G is p(X,Y) then answer_list would be [X,Y].
However, normal programs with recursion can cause uncontrolled looping, and consequent nonterminating behavior for the meta-interpreter.
Here is a simple normal program that can give npl a lot of trouble. The student should follow along by trying all of the sample executions.
Example P3. Suppose that we have a little road map with towns a,b and c, and connecting roads 1,2, and 3.
"f6_3_1 =120 =106>
Suppose that roads connecting towns are either ok to travel or not. Consider the normal program connects(a,b,1). connects(b,a,1). connects(b,c,2). connects(c,b,2). connects(a,c,3). connects(c,a,3). ok(1) | ok(2). ok(3). go(X,Y) :- connects(X,Y,R), ok(R). go(X,Z) :- connects(X,Y,R), ok(R), go(Y,Z). Read the 7th clause as intending to say that at least one of road 1 or road 2 is ok. The 9th and 10th clause give a familiar looking declaration for being able to go from one town to another. Load P3 into npl and try some goals... ?- [npl]. ... ?- know('p3.npl'). %%% The file holding P3 ?- why(go(a,b)). |-- go(a, b) |-- connects(a, b, 1) |-- true |-- ok(1) |-- ~ ok(2) |-- ~ go(c, b) |-- ~ go(a, b) |-- ancestor resolution |-- connects(a, c, 3) |-- true |-- ok(3) |-- true |-- connects(c, b, 2) |-- true ?- why(go(b,a)). ... The second goal given will not terminate. The npl meta-interpreter trys to match goals left-to-right (like Prolog). An examination of contra(P3) will help indicate why. In particular, note that the contrapositive ~go(A, B) :- ~go(C, B), connects(C, A, D), ok(D). is left-recursive (without first binding C). Also, the contrapositive ~ok(A) :- ~go(B, C), connects(B, D, A), go(D, C). introduces new variables in the body that would not have been bound in the head.
Exercise 5. Draw a diagram to trace how npl tries to construct a clause tree having root go(b,a). (Prolog's trace may be of some help.) Try to show how the left-recursiveness and the late binding cause looping.
As example P3 shows, it is easy to create simple, interesting normal programs for which npl, or any similar meta-interpreter, will be computationally incomplete: That is, the meta-interpreter will not be able to confirm or generate all possible evident answers. Various methods can be used to pry out answers, such as grounding and reordering of goals, as illustrated for P3.
One can modify contra(P3) to try to aleviate the problems that we have mentioned. To save a file for contra(P3), use the following ... ?- [npl]. ... ?- know('p3.npl'). Yes ?- tell('p3.c'), show, told. ... The last goal will write the clauses in contra(P3) to the file 'p3.c', where we have used extension 'c' to indicate "contrapositives.
Now edit the file p3.c to effect the following changes ... %% p3.cg %%%% for grounding %%%%% town(a). town(b). town(c). %%%%%%%%%%%%%%%%%%%%%%%%% connects(a, b, 1). connects(b, a, 1). connects(b, c, 2). connects(c, b, 2). connects(a, c, 3). connects(c, a, 3). ok(1) :- ~ok(2). ok(2) :- ~ok(1). ok(3). go(A, B) :- connects(A, B, C), ok(C). go(A, B) :- connects(A, C, D), ok(D), go(C, B). ~connects(A, B, C) :- ~go(A, B), ok(C). ~ok(A) :- connects(B, C, A), %% reordered body ~go(B, C). ~connects(A, B, C) :- ~go(A, D), ok(C), go(B, D). ~ok(A) :- connects(B, D, A), %% reordered town(C), %% grounding added ~go(B, C), go(D, C). ~go(A, B) :- connects(C, A, D), %% reordered ~go(C, B), ok(D). The edit changes have been highlighted in red. Save this file as p3.crg, the 'r' for reordering and the 'g' for "grounding.
Note that we have informally introduced two static proof strategies. They are "staticbecause one simply modifies the normal program given to the meta-interpreter rather than
Bhopal news
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100