In reading a paper in this paragraph on page 22 (section 1.1.1. The logical variable) it reads
A variable represents any data object. Initially the value of the variable is unknown, but it may become known by instantiation. A variable may be instantiated only once, i.e. it is single-assignment. Variables may be bound to other variables. When a variable is instantiated to a value, this value is seen by all the variables bound to it.
I never thought about there being a difference between the two words (bound or instantiated) but in reading the paragraph there clearly is a difference.
So when noting such in Prolog should the distinction be made?
The main reason I am asking is that in writing answers I always use the word bound for either, I am thinking I should be more accurate in my terminology.
This sentence [from the cited paper] is not ideal phrasing. Consider as an example:
?- V = a(_), V = a(1).
V = a(1).
Prolog is not a single assignment language. Is a language where terms can only be further instantiated when unified. Of course, the implicit context in that paragraph is to distinguish from procedural languages, hence the the word “assignment”, which makes the sentence fair. We can also argue that, in the second goal above, V no longer references a variable but a compound term, a(_). Anyway, words are fun and being trapped at home with no biking for two weeks is driving me crazy. The end.
I’m not really aware of binding and instantiation being different terms. It does make some sense though. Binding to a value (i.e., not a variable) creates and instance of the original term, making instantiation a good term. Binding two variables may or may not create an instance in this sense. For example, if we simply to A=B with nothing else happening we do no instantiate anything. On the other hand, x(A,A) is an instance of x(A,B) and thus also binding variables can instantiate terms.
I’ve always used the terms interchangeable and think I will keep doing so if there are no stronger arguments.
Personally, if I want to be formal, I avoid the term “binding” and use “unification” instead. As far as I have seen, “binding” is Prolog-specific while “unification” is a generally accepted logic programming term that also has a very clear definition (in Robinson’s unification algorithm).
I wasn’t always like that. In the past I was a care-free child that would happily use “binding”, “unification” and “instantiation” interchangeably. But then some of my work fell to the hands of savage reviewers who brutally slaughtered my careless use of vague terminology and I have never been the same since.
Moreover, a reminder that, in this challenging times, everything should be coded using negation in order to respect social distancing for terms and variables!