>>>>>> This file contains comments interspersed with FOIL6.0 input and >>>>>> output. Comments (even blank lines) begin with >>>>>>. >>>>>> >>>>>> The first section of input identifies the types and the constants >>>>>> associated with each type. Here there are two types, X and L >>>>>> (corresponding to element and list). Individual constant names >>>>>> can be complex; remember, though, that any structure implied by >>>>>> the name is invisible to FOIL. The * in front of [] indicates >>>>>> that this is a 'theory constant' that can appear in the learned >>>>>> definition. The blank line following the last type delineates >>>>>> this section from the next. >>>>>> X: 1, 2, 3. L: [111], [112], [113], [11], [121], [122], [123], [12], [131], [132], [133], [13], [1], [211], [212], [213], [21], [221], [222], [223], [22], [231], [232], [233], [23], [2], [311], [312], [313], [31], [321], [322], [323], [32], [331], [332], [333], [33], [3], *[]. >>>>>> >>>>>> The second section defines relations by specifying the tuples of >>>>>> constants that they contain ('positive' tuples); tuples that do >>>>>> not belong in the relation can be listed explicitly or FOIL can >>>>>> determine them using the closed world assumption. Here member >>>>>> is a relation with two arguments, an element and a list. The >>>>>> pairs 1,[1] through 3,[333] are given as belonging to member >>>>>> while 1,[] through 1,[332] are noted as not belonging to member >>>>>> ('negative' tuples). >>>>>> member(X,L) 1,[1] 3,[3] 1,[11] 1,[13] 3,[13] 1,[31] 3,[31] 3,[33] 1,[111] 1,[113] 3,[113] 1,[131] 3,[131] 1,[133] 3,[133] 1,[311] 3,[311] 1,[313] 3,[313] 1,[331] 3,[331] 3,[333] ; 1,[] 1,[3] 1,[33] 1,[333] 3,[] 3,[1] 3,[11] 3,[111] 1,[2] 1,[22] 1,[23] 1,[32] 1,[222] 1,[223] 1,[232] 1,[233] 1,[322] 1,[323] 1,[332] . >>>>>> >>>>>> The input then defines another relation components with three >>>>>> arguments: a list, an element (the head of the list) and another >>>>>> list (the tail of the list). The asterisk in front of the >>>>>> relation name tells FOIL not to construct a definition for it. >>>>>> After the closing parenthesis there is a blank and the characters >>>>>> '#--/-##'. This is a 'key' (similar to that used in databases); >>>>>> to use this relation, either the value of the first argument or >>>>>> the values of both the second and third argument must be known, >>>>>> meaning that the corresponding variables in the definition must be >>>>>> bound. >>>>>> *components(L,X,L) #--/-## [1],1,[] [2],2,[] [3],3,[] [11],1,[1] [12],1,[2] [13],1,[3] [21],2,[1] [22],2,[2] [23],2,[3] [31],3,[1] [32],3,[2] [33],3,[3] [111],1,[11] [112],1,[12] [113],1,[13] [121],1,[21] [122],1,[22] [123],1,[23] [131],1,[31] [132],1,[32] [133],1,[33] [211],2,[11] [212],2,[12] [213],2,[13] [221],2,[21] [222],2,[22] [223],2,[23] [231],2,[31] [232],2,[32] [233],2,[33] [311],3,[11] [312],3,[12] [313],3,[13] [321],3,[21] [322],3,[22] [323],3,[23] [331],3,[31] [332],3,[32] [333],3,[33] . >>>>>> >>>>>> Any number of relations may be defined. The order does not matter, >>>>>> as FOIL will reorder them anyway. This section also ends with a >>>>>> blank line. >>>>>> >>>>>> The final section contains cases to test the definitions found. >>>>>> The first line names the relation to be tested, followed by test >>>>>> tuples. Each tuple ends with a colon, space, and a sign that >>>>>> indicates whether or not the tuple is supposed to satisfy the >>>>>> definition. The test parcel ends with a line containing a period; >>>>>> there can be any number of such parcels. >>>>>> member 2,[]: - 3,[121]: - 3,[23]: + 3,[232]: + . >>>>>> >>>>>> Let us now examine the output produced by FOIL for this example. >>>>>> The command used to run FOIL was 'foil6 -v3 >>>>> -v3 selects fairly verbose output. >>>>>> FOIL 6.0 [October 1993] -------- Options: verbosity level 3 Types X and L are not compatible Relation member Relation *components >>>>>> >>>>>> After reading the relations, FOIL tries to find ordering for >>>>>> the constants of types X and L. It fails to find an ordering >>>>>> for type X, but discovers one for type L -- the original >>>>>> unhelpful lexicographic order (produced by 'sort') has been >>>>>> replaced by a length ordering. >>>>>> Ordering constants of type X Checking arguments of member Checking arguments of ~member Checking arguments of components unordered Ordering constants of type L Checking arguments of member Checking arguments of ~member Checking arguments of components arguments 1,3 are consistent Finding maximal consistent set best so far components:1>3 Final order: [] [1] [2] [3] [11] [12] [13] [21] [22] [23] [31] [32] [33] [111] [112] [113] [121] [122] [123] [131] [132] [133] [211] [212] [213] [221] [222] [223] [231] [232] [233] [311] [312] [313] [321] [322] [323] [331] [332] [333] ---------- member: >>>>>> >>>>>> FOIL then commences the search for the first clause of the >>>>>> definition of member. There are initially 22 positive tuples, >>>>>> 41 tuples in all. Literals are evaluated to see the result >>>>>> of adding them to the clause. If the literal "B=[]" were >>>>>> added, the clause would be satisfied by only two of the 41 >>>>>> tuples, 0 of them being positive. The negated form of this >>>>>> literal would be satisfied by 39 of the 41 tuples, of which >>>>>> 22 would be positive. The gains for the unnegated and negated >>>>>> forms of this literal would then be 0.0 bits and 1.5 bits >>>>>> respectively. >>>>>> State (22/41, 47.5 bits available) B=[] 0[0/2] [22/39] gain 0.0,1.5 [== tried 1/1] 0.0 secs [= tried 0/0] 0.0 secs [member tried 0/0] 0.0 secs >>>>>> >>>>>> The following literal is noted as determinate ('[Det]'). >>>>>> components(B,C,D) 22[22/39] [0/2] [Det] gain 1.5,0.0 >>>>>> >>>>>> While evaluating the next literal, it becomes clear that it >>>>>> cannot be a winner. The evaluation is abandoned after >>>>>> examining 43% of the tuples. >>>>>> components(B,A,C) 10[10/10] [5/8] abandoned (43%) (pruning subsumed arguments) components(B,C,B) 0[0/0] [22/26] abandoned (63%) components(C,A,B) 8[8/11] [14/17] abandoned (68%) components(C,A,C) 0[0/0] [22/26] abandoned (63%) [components tried 5/6] 0.0 secs >>>>>> >>>>>> The literal added is the determinate literal components(B,C,D); >>>>>> under the ordering discovered for type L, variable B is now >>>>>> greater than variable D. >>>>>> Determinate literals components(B,C,D) Note B>D State (22/39, 47.5 bits available, 1 weak literal) B=[] 0[0/0] [22/39] gain 0.0,0.0 D=[] 2[2/5] [20/34] gain 0.0,1.2 [== tried 2/2] 0.0 secs A=C 14[14/14] [8/25] gain 11.2,0.0 B=D 0[0/0] [22/30] abandoned (76%) [= tried 2/2] 0.0 secs member(A,D) 16[16/16] [6/23] gain 12.8,0.0 member(C,D) 10[10/10] [10/10] abandoned (51%) member(E,D) 20[28/34] [2/13] gain 10.5,0.0 [member tried 3/3] 0.0 secs >>>>>> >>>>>> The next literal appears to introduce new variables E and F. >>>>>> However, FOIL notes that E=C and F=D, and discards the literal ('#'). >>>>>> components(B,E,F) 22[22/39] [0/0] C=E D=F [XDet] # components(B,A,E) 14[14/14] [8/25] D=E # components(B,A,B) 0[0/0] [22/28] abandoned (71%) components(B,A,D) 14[14/14] [8/25] gain 11.2,0.0 components(B,C,E) 22[22/39] [0/0] D=E [XDet] # components(B,C,B) 0[0/0] [22/28] abandoned (71%) components(B,C,D) 22[22/28] [0/0] abandoned (71%) components(B,E,B) 0[0/0] [22/29] abandoned (74%) components(B,E,D) 22[22/39] [0/0] C=E [XDet] # components(D,E,F) 20[20/25] [2/5] abandoned (76%) components(D,A,E) 10[10/10] [10/16] abandoned (66%) (pruning subsumed arguments) components(D,C,E) 8[8/8] [14/20] abandoned (71%) (pruning subsumed arguments) components(D,E,B) 0[0/0] [22/29] abandoned (74%) components(D,E,D) 0[0/0] [22/29] abandoned (74%) components(E,A,B) 8[8/10] [14/20] abandoned (76%) components(E,A,D) 22[22/39] [0/0] [Det] gain 0.0,0.0 components(E,A,E) 0[0/0] [22/26] abandoned (66%) components(E,C,B) 8[8/10] [14/17] abandoned (69%) components(E,C,D) 22[22/39] [0/0] B=E [XDet] # components(E,C,E) 0[0/0] [22/26] abandoned (66%) [components tried 20/24] 0.0 secs Determinate literals components(E,A,D) Note B>D State (22/39, 47.5 bits available, 2 weak literals) B=[] 0[0/0] [22/39] gain 0.0,0.0 D=[] 2[2/5] [20/34] gain 0.0,1.2 E=[] 0[0/0] [22/38] abandoned (97%) [== tried 3/3] 0.0 secs A=C 14[14/14] [8/25] gain 11.2,0.0 B=D 0[0/0] [22/30] abandoned (76%) B=E 14[14/14] [8/25] gain 11.2,0.0 D=E 0[0/0] [22/30] abandoned (76%) [= tried 4/4] 0.0 secs member(A,D) 16[16/16] [6/23] gain 12.8,0.0 member(C,D) 10[10/10] [10/10] abandoned (51%) member(F,D) 20[28/34] [2/13] gain 10.5,0.0 [member tried 3/3] 0.0 secs components(B,F,G) 22[22/39] [0/0] C=F D=G [XDet] # components(B,A,F) 14[14/14] [8/25] D=F # components(B,A,B) 0[0/0] [22/28] abandoned (71%) components(B,A,D) 14[14/14] [8/25] gain 11.2,0.0 components(B,A,E) 0[0/0] [22/28] abandoned (71%) components(B,C,F) 22[22/39] [0/0] D=F [XDet] # components(B,C,B) 0[0/0] [22/28] abandoned (71%) components(B,C,D) 22[22/28] [0/0] abandoned (71%) components(B,C,E) 0[0/0] [22/28] abandoned (71%) components(B,F,B) 0[0/0] [22/29] abandoned (74%) components(B,F,D) 22[22/39] [0/0] C=F [XDet] # components(B,F,E) 0[0/0] [22/29] abandoned (74%) components(D,F,G) 20[20/25] [2/5] abandoned (76%) components(D,A,F) 10[10/10] [9/15] abandoned (64%) (pruning subsumed arguments) components(D,C,F) 8[8/8] [14/20] abandoned (71%) (pruning subsumed arguments) components(D,F,B) 0[0/0] [22/29] abandoned (74%) components(D,F,D) 0[0/0] [22/29] abandoned (74%) components(D,F,E) 0[0/0] [22/29] abandoned (74%) components(E,F,G) 22[22/39] [0/0] A=F D=G [XDet] # components(E,A,F) 22[22/39] [0/0] D=F [XDet] # components(E,A,B) 0[0/0] [22/28] abandoned (71%) components(E,A,D) 22[22/28] [0/0] abandoned (71%) components(E,A,E) 0[0/0] [22/28] abandoned (71%) components(E,C,F) 14[14/14] [8/25] D=F # components(E,C,B) 0[0/0] [22/28] abandoned (71%) components(E,C,D) 14[14/14] [8/25] gain 11.2,0.0 components(E,C,E) 0[0/0] [22/28] abandoned (71%) components(E,F,B) 0[0/0] [22/29] abandoned (74%) components(E,F,D) 22[22/39] [0/0] A=F [XDet] # components(E,F,E) 0[0/0] [22/29] abandoned (74%) components(F,A,B) 8[8/10] [14/20] abandoned (76%) components(F,A,D) 22[22/39] [0/0] E=F [XDet] # components(F,A,E) 8[8/10] [14/20] abandoned (76%) components(F,A,F) 0[0/0] [22/29] abandoned (74%) components(F,C,B) 8[8/10] [14/20] abandoned (76%) components(F,C,D) 22[22/39] [0/0] B=F [XDet] # components(F,C,E) 8[8/10] [14/20] abandoned (76%) components(F,C,F) 0[0/0] [22/29] abandoned (74%) [components tried 38/44] 0.0 secs Save A=C (14,14 value 12.2) Save B=E (14,14 value 12.2) Save components(B,A,D) (14,14 value 12.2) Save components(E,C,D) (14,14 value 12.2) Best literal member(A,D) (4.6 bits) >>>>>> >>>>>> After adding literals components(E,A,D) and member(A,D), the >>>>>> clause is found to be complete. It is pruned, covered positive >>>>>> tuples removed, and the search continues. >>>>>> Initial clause (0 errs): member(A,B) :- components(B,C,D), components(E,A,D), member(A,D) QuickPrune literal components(E,A,D) Accepting quickpruned clause components(B,C,D) essential Clause 0: member(A,B) :- components(B,C,D), member(A,D) State (6/25, 24.3 bits available) B=[] 0[0/2] [6/23] gain 0.0,0.7 [== tried 1/1] 0.0 secs [= tried 0/0] 0.0 secs [member tried 0/0] 0.0 secs >>>>>> >>>>>> The apparent new variable C introduced by the next literal is >>>>>> identical to existing variable A on all positive tuples. >>>>>> It also gets the axe. >>>>>> components(B,C,D) 6[6/23] [0/2] A=+C [XDet] # components(B,A,C) 6[6/6] [0/19] [Det] gain 11.4,0.0 [components tried 2/6] 0.0 secs Best literal components(B,A,C) (4.6 bits) Clause 1: member(A,B) :- components(B,A,C) >>>>>> >>>>>> The final definition is screened and the clauses reordered >>>>>> to place the non-recursive base case ahead of the general >>>>>> recursive clause. >>>>>> Clause 1 needed for 1,[1] Clause 0 needed for 3,[13] member(A,B) :- components(B,A,C) member(A,B) :- components(B,C,D), member(A,D) Time 0.0 secs >>>>>> >>>>>> The definition is then tested on the four test cases. Horror: >>>>>> even though the definition seems fine, it gives an error on >>>>>> case 3,[232]! In order to determine by the recursive clause >>>>>> that 3 is a member of [232], it is necessary to be able to >>>>>> establish that 3 is a member of [32]. However, the tuple >>>>>> 3,[23] does not appear among the tuples known to be in the >>>>>> relation member, so 3,[232] is judged (incorrectly) to be >>>>>> false. A future release will allow the definition to be >>>>>> tested in Prolog interpretive mode, which would have produced >>>>>> the correct result for this case. >>>>>> Test relation member (+) 3,[232] Summary: 1 error in 4 trials