Prolog unification of predicates as argument

Question

That's probably an easy one!

I have a predicate in a rule parameter. I query the rule with a fact that makes the predicate true. I'd expect SWI-Prolog to apply the predicate to the fact, infer it's truth value (true) and return accoridngly (true). But I do get false.

My facts:

key(cMaj).
key(aMin).
chord(key(X)).

My query:

?- chord(cMaj).

Because key(cMaj) is true, I would expect Prolog to make this inference and return true. I do get false. Can anybody explain why?

Answer 1

This is only an expanded version of what @mbratch wrote in his comment. But maybe it can help some too:

In Prolog, we can read chord(cMaj) to say "C Major is a chord". To find out what Prolog thinks your definition of chord/1 says, query it with a free variable:

?- chord(X).
X = key(_G1419).

Prolog reads your definition of chord/1 to be a description of a complex prolog term: "the term key(_) is a chord". This is how pattern matching with terms works. chord(X) is true so long as X is unfieid with something of the form key(_), just as list_head([Head|Tail], Head) is true if Head unifies with the first element in a list and Tail unifies with the rest.

Your definition of key/1 says that "cMaj and cMin are keys" (it is also naming terms--in this case, atoms). To get chord(cMaj) to turn out true, we need to define chord/1 such that chord(X) is true if key(X) is true:

chord(X) :- key(X).

key/1 now appears as a term to be evaluated, and X is unified with cMaj or aMin. This effectively establishes chord/1 as a synonym for key/1: they each describe the same object.