Free Variable in Prolog

Question

Can anyone explain the concept of free variables in Prolog. Is it similar to anonymous variables ? Or is there a difference. Also could be great if an example is given to explain.

Answer 1

tl;dr: free is a notion to distinguish universally bound (free in clause notation) from existentially bound variables in setof/3, bagof/3, etc. - some people use free to mean "currently not instantiated" and some use it to denote an output argument that's meant to be instantiated by the predicate but that's not how the standard uses it.

long version: I will quote the Prolog standard on the definition:

7.1.1.4 Free variables set of a term The free variables set, FVt of a term T with respect to a term v is a set of variables defined as the set difference of the variable set (7.1.1.1) of T and BV where BV is a set of variables defined as the union of the variable set of v and the existential variables set (7.1.1.3) of T.

where they explicitly note:

The concept of a free variables set is required when defining bagof/3 (8.10.2) and setof/3 (8.10.3).

Perhaps as a background: in logic, a free variable is one that is not bound by a quantifier (e.g. x is bound and y is free in ∀x p(x,y) ). A (pure) prolog clause head(X) :- goal1(X), goal2(X). can be read as the logical formula ∀X goal1(X) ∧ goal2(X) → head(X). In practice, as long as we use fresh variables whenever we try to unify a goal with a clause, we can just disregard the universal quantifiers. So for our purposes we can treat X in the clause above as free.

This is all and well until meta-predicates come in: say we are interested in the set of first elements in a list of tuples:

?- setof(X, member(X-Y, [1-2, 2-2, 1-3]), Xs).
Y = 2,
Xs = [1, 2] ;
Y = 3,
Xs = [1].

But we get two solutions: the ones where Y=2 and those where Y=3. What I'd actually want to say is: there exists some Y such that X-Y is a member of the list. The Prolog notation for this pattern is to write Var^Term:

?- setof(X, Y^member(X-Y, [1-2, 2-2, 1-3]), Xs).
Xs = [1, 2].

In the first example, both X and Y are free, in the second example X is free and Y is bound.

If we write this as a formula we get setof(X, ∃Y member(X-Y, [1-2, 2-3, 1-3]), Xs) which is not a first order formula anymore (there is an equivalent first order one but this is where the name meta predicate comes in). Now the problem is that the Var^Term notation is purely syntactical - internally there is only one type of variable. But when we describe the behaviour of setof and friends we need to distinguish between free and existentially bound variables. So unless you are using metapredicates, all of your variables can be considered as free (1).

The Learning Prolog link provided by @Reema Q Khan is a bit fuzzy in its use of free. Just looking at the syntax, X is free in X=5, X is 2 + 3. But when we run this query, as soon as we get to the second goal, X has been instantiated to 5 so we are actually running the query 5 is 2 + 3 (2). What is meant in that context is that we expect is/3 to unify its first argument (often called "output" argument). To make sure this always succeeds we would pass a variable here (even though it's perfectly fine not to do it). The text tries to describe this expectation as "free variable" (3).

(1) ok, formally, anything that looks like Var^Term considers Var existentially bound but without meta-predicates this doesn't matter. (2) I believe there is a clash in notation that some texts use "X is bound to 5" here, which might increase the confusion. (3) What the should say is that they expect that the argument has not been instantiated yet but even that does not capture the semantics correctly - Paulo Moura already gave the initial ground example 5 is 3 + 2.

Answer 2

Maybe this can help. (If I have prepared it, I might as well post it! Still hard to read, needs simplification.)

In fact, you need to distinguish whether you talk about the syntax of the program or whether you talk about the runtime state of the program.

The word "variable" takes on slightly different meanings in both cases. In common usage, one does not make a distinction, and the understanding this fluent usage provides is good enough. But for beginners, this may be a hurdle.

In logic, the word "variable" has the meaning of "a symbol selected from the set of variable symbols", and it stands for the possibly infinite set of terms it may take on while fulfilling any constraints given by the logical formulae it participates in. This is not the "variable" used in reasoning about an actual programs.