CODEWITHSUNDEEP
prolog
Eric Zinda
Eric Zinda

Reputation: 877

Prolog single-variable query returns an error. Why?

I've created a simple Prolog program (using GNU Prolog v1.4.4) with a single fact:

sunny.

When I run the following query:

sunny.

I get:

yes

As I'd expect. When I run this query:

X.

I get:

uncaught exception: error(instantiation_error,top_level/0)

when I expected to get:

X = sunny

Anyone know why?

Upvotes: 4

Views: 365

Answers (1)

lambda.xy.x
lambda.xy.x

Reputation: 4998

Prolog is based on first-order logic but X is a second order logic query (the variable stands for a rule head / fact, not only a term): you ask "which predicates can be derived?" or in other words "which formulas are true?". Second order logic is so expressive that we lose many nice properties of first-order logic (*). That's why a second order variable must be sufficiently instantiated to know which rule to try at the time it is called (that's what the error message means). For instance the queries

?- X=member(A,[1,2,3]), X.

and

?- member(A,[1,2,3]).

still allow Prolog to try the definition of the member predicate (in fact the two definitions are equivalent) but

?- X, X=member(A,[1,2,3]).

will throw an exception because at the time X should be derived, we don't know that it's supposed to become the predicate member(A,[1,2,3]).

Your case is much simpler though: you can wrap sunny as a term into a predicate such that Prolog knows which rules to try. The facts

weather(sunny).
weather(rainy).

define the predicate weather such that now we only have a first-order variable as argument in our query:

?- weather(X).
X = sunny ;
X = rainy.

Now that we are talking about the term level, everything works as you expected.

(*) Although the problem of finding out if a formula is valid is undecidable in both cases, in first order logic at least all true formulas can be eventually derived but if a formula is false, the search might not terminate (i.e. first-order logic is semi-decidable). For second order logic there are formulas that can neither be proved not disproved. What is worse is that we cannot even tell if a second-order formula belongs to this category.

Upvotes: 6

Related Questions