| The basic collection class in Logikus is the list. You can write a list as a pair of brackets containing a series of terms. For example, here is a list of synonyms for French roasted coffee: [dark, full, high, viennese, continental] There are many ways to write a list that unifies with this one. First, any list that contains the same number of elements will unify with this list if each term unifies with its corresponding element. For example, each of the following lists unifies with the list of synonyms: [A, B, C, D, E] [dark, full, A, B, continental] You can also describe a list in terms of its head elements and its tail, indicating the tail after a vertical bar. The tail of a list is always itself a list. For example, the following list also unifies with the list of synonyms: [A B] Unifying this structure with the synonyms unifies A with dark , and B with the list [full, high, viennese, continental]. You can specify more than one head element, separating them with commas. Consider the list [A, B C] This unifies A with dark , B with full, and C with [high, viennese, continental]. Figure 13.6 shows examples of successful and unsuccessful list unifications. (This Logikus program is in the file french.txt .) Figure 13.6. List unifications. In this example, the ok query proves itself against the ok rules, which identify themselves by number. As the output shows, only rules 1 through 5 can unify with the query.  The query in Figure 13.6 tries to prove itself by unifying with ok rules and proving them. The program first establishes a list of synonyms for French roasted coffee. The program then specifies a series of ok rules, which unify the variable N with a number and then specify a list that may unify with the given list of synonyms. The first five rules specify lists that unify with the synonyms, and the last two rules do not. The first ok rule declares ok(N, A, B) :- #(N, 1), french([A, B, C, D, E]); The ok query unifies with the head of this rule and then asks the rule's remaining structures to prove themselves. The evaluation #(N, 1) numbers the rule so that you can see which rule produces which result. The structure french([A, B, C, D, E]) unifies with the first fact of the program. The ok rule succeeds, and the query prints N = 1.0, A = dark, B = full The second ok rule is ok(N, A, B) :- #(N, 2), french([E, D, C, B, A]); This rule shows that there is nothing special about where A and B appear in the list. When the query proves itself with this rule, it prints N = 2.0, A = continental, B = viennese The third ok rule says ok(N, A, B) :- #(N, 3), french([A B]); This rule defines its list using a vertical bar. The variable A unifies with the head of the synonym list, and B unifies with the tail. The query successfully proves itself using this rule, displaying: N = 3.0, A = dark, B = [full, high, viennese, continental] The fourth ok rule declares ok(N, A, B) :- #(N, 4), french([C, D, E [A, B]]); Here, the rule uses a list that starts with three elements ( C , D , and E ) and concludes with another list. The concluding list contains exactly two elements: A and B . When this rule proves itself, C , D , and E unify with dark , full , and high . This leaves [A, B] to unify with the remainder of the synonym list, which is [viennese, continental] . This rule succeeds, and the query prints N = 4.0, A = viennese, B = continental The fifth (and final successful) rule specifies ok(N, A, B) :- #(N, 5), french([C, D, E [A B]]); This is identical to the fourth rule except in the specification of the tail list, which sets up B as the tail of a list. As before, this rule proves itself by unifying with the french rule, unifying C , D , and E as in the fourth ok rule. This leaves [A B] to unify with the remainder of the list, [viennese, continental] . Now, A unifies with the head ( viennese ) of this list, and B unifies with the tail of this list. The tail of a list is always itself a list, and in this case the tail is [continental] . After this proof succeeds, the query displays its variables as N = 5.0, A = viennese, B = [continental] The other ok rules cannot successfully prove themselves. The rule that unifies N with -1 fails because its french structure contains five terms rather than a single list. The rule that unifies N with -2 fails because its list can match only other lists that contain exactly two elements. 13.9.1 Dot Notation Internally, the logic engine stores lists as structures with a dot (" . ") as a functor and with two terms, the second of which is always a list. If you run into problems getting a list to behave as you would expect, it can help to write the list using this dot notation. For example, you can enter a fact about favorite lizards as either favs([monitor, gilaMonster, iguana]); or favs(.(monitor, .(gilaMonster, .(iguana, [])))); In the latter notation, each "dot" structure is a structure with two terms. In each case, the second term is a list, including the innermost structure whose second term is an empty list. With either of these facts in a program, you can issue a query as either favs([J, K, L]) or favs(.(J, .(K, .(L, [])))) With the fact written in either notation and with the query written in either notation, the variables J , K , and L will unify with the lizards in the fact. The bracket notation is shorter than the dot notation, but the dot notation can help illuminate how list unification works. |
