Most of the links on this page are broken. When I click on them, they lead to a "404 not found" page.
_ is called the anonymous
variable. Multiple occurrences of _ in a single term
are not shared.myterm(A1, a2).:-:-parent(X) :- father(X, _).
Expressed as "X is a parent if X is a father of someone" . See also variable and predicate.
john is
a person.
person(john).
foo(a, b, c) is said to be a term belonging to the functor
foo/3 . foo/0 is used to refer to the atom
foo.:-:-
In Prolog, the expression a+b is exactly the same as the
canonical term +(a,b).
a+b*c as +(a, *(b,c)).?- A = B, A = a. A = B, B = a.
_ (see anonymous).
Rules for naming a variable and avoiding a warning are given in section
2.15.1.10.?- foo(a, B) = foo(A, b). A = a, B = b.
Unlike assignment (which does not exist in Prolog), unification is not directed.
?- A = b, A = c. false. ?- (A = b; true; A = c). A = b ; true ; A = c .
See also unify.
"A Prolog variable is a value that‘is not yet bound'."
That sound not correct (it would explain why var/1 is called var/1 and not unbound/1 though, but is in contradiction with all other usage of the word 'variable', in particular with the usage under "binding of a variable").
Better: A "variable" is a name (with clause scope) denoting a term or an empty cell. If it designates an empty cell, it is an unbound or uninstantiated variable, otherwise it is a bound variable, namely a variable bound to the term it denotes. The "binding state" of a variable may change from unbound to bound. Trivially:
var(X),X=1,nonvar(X)
which should really have been written
unbound(X),X=1,bound(X)
OTOH, there is a slight shift in the meaning of the word "variable" when used for a variable name in the head (where it is always unbound as it appears in unification) and in a goal (where its "bounded-ness/instantiated-ness status" changes from "fresh & unbound" to "still unbound" to "bound/partially bond" to "bound/ground").
In all these case, X is a "variable", but the meaning changes.
It is actually clearer to say that X is a variable name and denotes en empty cell ("X is an unbound variable") or a (proper? nonempty?) term. (apparently an empty cell is also a "term")
f(X) :- atomic(X),!,h0(X). % at !, we know that variable X denotes an atomic term
f(X) :- ground(X),!,h1(X). % at !, we know that variable X denotes a ground term
f(X) :- nonvar(X),!,h2(X). % at !, we know that variable X does not denote an empty cell ("is not an unbound variable")
f(X) :- var(X),!,h3(X). % at !, we know that variable X is unbound
Some adapted from
[user] prompt) is added (I suppose).See here: https://eu.swi-prolog.org/pldoc/man?section=preddesc
(1,2,3) = (1,(2,3)). Generally used as a conjunction.length(L,2). L is an unbound variable at first that is then unified with a complex term (a list of length 2) with 2 unbound values, which, when printed, appear as 2 unbound variables (i.e. their arbitrarilly chosen names are printed rather than their nonexistent content): L = [_5038, _5044].)library(yall): The closure concept used here is somewhat different from the closure concept from functional programming. The latter is a function that is always evaluated in the context that existed at function creation time. Here, a closure is a term of arity 0 =< L =< K. The term's name is the name of a predicate of arity K and the term's L arguments (where L could be 0) correspond to L leftmost arguments of said predicate. The remaining K-L arguments are left open and will be filled in by at metacall time. For example, a closure involving atom_concat/3 might be the term atom_concat(prefix). In order of increasing L, one would have increasingly more complete closures that could be passed to call/3, all giving the same result:
call(atom_concat,prefix,suffix,R).call(atom_concat(prefix),suffix,R).call(atom_concat(prefix,suffix),R).call(atom_concat(prefix,suffix,R)).choo(X) :- var(X) -> (!,debug(choo,"It's a var",[])). choo(X) :- nonvar(X) -> debug(choo,"It's not a var",[]).
my_atom == my_atom) or at the root of graphs of cells forming ground terms (f(g(a,b),c) == f(g(a,b),c)). This allows the underlying machinery to share parts of graphs representing terms. In a Prolog program, a cell, or rather, the root of graph of cells is denoted by a variable (X = f(g(a,b),c)). Thinking in terms of cells instead of terms is generally not needed unless empty cells and non-logical usage thereof enters the picture.[] on element position 2.X \== Y.: what these fresh variables denote, which are empty cells, are not the same, but X=a,Y=a,X==Y.. Empty cells are merged via unification: X \==Y, X=Y, X == Y: X and Y now designate the same empty cell. Thinking in terms of empty cells is not logical but computational and stateful in nature, and is done in the parts of the Prolog program which are doing state manipulation, for example those dealing with difference lists of open lists.freeze(X,write("Hello")),X=1. prints Hello.dif(X,Y),X=1,Y=2. succeeds but dif(X,Y),X=1,Y=1.failslibrary(check) and library(codewalk). See also library(prolog_xref) See also the Wikipedia entry on the lint program \+ stands for negation-as-failure. (i.e. Prolog program with negation)length([1,2],L), gives L=2; the 2 is the proof witness (the proof is "constructive" and doesn't just say true or false). Sometimes Prolog emits a "template proof witness" instead: length(List,2) gives List=[_,_], which is really a (most general) template for lists of length 2.1+2<4. See also: Wikipedia: Theorem, which has a glossary of related terms (Corollary etc.). That page also cites Paul Hoffman as _"It has been estimated that over a quarter of a million theorems are proved every year."_ Well, with Prolog you can prove a million theorems in a minute!p(t1,...,tn), n>=1 where p is a predicate symbol from a set P and the ti are terms from `T(F,V)`, build from a set of function symbols F and variable symbols from set of variable symbols V. The atom can also be a word of the form s = t where s,t `T(F,V)`. The set of atoms may be written `A(F,P)` (note that 0-arity predicate symbols are in principle not allowed)~ or ¬ or naf or \+. It depends on the author but generally ¬ is the strong negation.~ is the strong negation). The term Definite Clause is used to denote a clause with exactly one positive literal. Prolog programs can be viewed as a set of definite clauses in which the positive literal is the head of the rule and the negative literals constitute the body or tail of the rule. (from CACM March 1992). A Horn Clause without negative literals is called a fact H, otherwise a rule. Note that a clause without the positive literal can be interpreted as a logical constraint (not to be confused with constraint logic programming). These are not supported by Prolog (but are supported by ASP systems).arc(X,Y) ∧ path(Y,Z) ⇒ path(X,Z))` could be a part of a description of paths through a graph. (This definition has the advantage that it justifies calling A :- B,C,D a Horn clause in a logic that does not allow the equivalence A⇒B = ¬A∨B, which is intuitionistic (positive) logic, which is the logic that really applies to Prolog even though it is often said that we are dealing in classical logic)."SLD resolution can be understood procedurally as executing a nondeterministic program with procedure calls" (David Warren),
From the above, we have:
Completely different approaches at building proof systems exist: Those based on Sequent Calculus, bottom-up provers, Tableaux-based, Answer Set Programming (Stable Models) and probably others.
[] as the terminating element of the list backbone** ("list backbone" is not commonly used except by myself, but it's are pretty evocative, so I will use it here)Example of a proper list: an empty list Empty and a list of length 3 List1 and of length 2 List2.
↙"tip" List1 ------>[|] / \ 1 [|]<-------List2 / \ 2 [|] / \ ↙"fin" 3 []<----- Empty
The list Empty could also appear simply like this. There is no way to find out which of the above and the below is "really" the case from Prolog:
Empty ------>[]
2 for example, then predicates holding either of List1 or List2 will see this change). See also: duplicate_term/2 and copy_term/2.[H|T].
[].[H|T]=[1,2,3][H1,H2|T]=[1,2,3][H1,H2,H3|T]=[1,2,3] (T will not be [] - the list without the first three positions is the empty list)[H1,H2,H3,H4|T]=[1,2,3] will fail.[]. The empty list has an empty prefix.Prefix=[], Suffix=[], append(Prefix,Suffix,[]).Prefix=[], Suffix=[1,2,3], append(Prefix,Suffix,[1,2,3]).[H|T]=[1,2,3], Prefix=[H],Suffix=T, append(Prefix,Suffix,[1,2,3]).[H1,H2|T]=[1,2,3], Prefix=[H1,H2],Suffix=T, append(Prefix,Suffix,[1,2,3]).[H1,H2,H3|T]=[1,2,3], Prefix=[H1,H2,H3],Suffix=T, append(Prefix,Suffix,[1,2,3]).Newlist = [X|OldList]. If the list is seen as a stack, this is push. This is efficient.append(OldList,Tail,NewList). This is extremely expensive as it involves copying OldList. Practically never done. To borrow Perl terminology, this is shift (although Perl "shifts" at fin).OldList = [X|NewList] If the list is seen as a stack, this is pop. This is efficient.append(NewList,Tail,OldList). This is extremely expensive as it involves copying OldList into NewList. Practically never done. To borrow Perl terminology, this is unshift (although Perl "unshifts" at tip).Special case: The open list*
An open list can still grow its backbone (it can be "further instantiated") because its Fin is not set: it is "empty cell". If the there is a variable naming the Fin, say Fin, then Fin is an unbound variable, var(Fin) returns true.
An open list is transformed into a closed list by unifying that Fin with [].
A special case is the "empty open list", which is really just any unbound variable. (The future history of an unbound variable is always open, it could become anything, even the tip of a proper list).
Example of a nonempty open list:
↙"tip" List1 ------>[|] / \ 1 [|] / \ 2 [|] / \ ↙"fin" 3 <empty> <---------- Fin
An open list is simply created by: OpenList = [1,2,3|Fin].. After Fin=[] it is then a proper list.
A *difference list" (which is actually confusing terminology) is really just a "list difference": two variables which refer to two positions in a list: X=[a,b,c,d], X=[a,b|Y]. From there, you can infer the "list difference", which is the X list minus the Y list: [a,b,c] (and which in extremis can be generated with append(LDiff,Y,X).)
<--> LDiff = [a,b] X Y | | [a,b,c,d]
These two references can be packed into a term to pass them to other predicates: p(X-Y). p(X/Y). But they should not (why waste cycles?). Just use p(X,Y).
The above construction is useful when the underlying list is an "open list", where Y points to the empty cell "fin" (the write position) where new elements are appended by a producer, and X is trailing behind (the read position) where elements are consumed by a consumer. The "list difference" then is the current buffer, which is empty if X==Y, var(X), var(Y) and EOF is expressed by Y=[].
Here is another representation of the above:
X ------->[|] ^ / \ | "list difference" X-Y is a [|] | [a,b] / \ V b [|]<------------- Y / \ c [|] / \ d [] <--- list properly ends in []: proper list
When based on an open list, when the empty cell at the "backbone fin" is called Fin and takes the role of Y above and the 'X' is called 'Tip':
Tip=[a,b,c,d|Fin]
Tip ----->[|] + / \ | "list difference" Tip-Fin is a [|] | [a,b,c] / \ + b [|] / \ c ~empty cell~ <--- Fin
We can obtain an element V at the tip: Tip=[V|NewTip] and use NewTip as new Tip in the next activation:
NewTip ----> [|] + / \ | "list difference" NewTip-Fin is b [|] | [b,c] / \ + c ~empty cell~ <--- Fin
Analogous to imperative programming with pointers, Fin=[d|NewFin] grows the open list with d, and yields a fresh variable NewFin denoting the new fin, which is an empty cell.
Tip ----->[|] + / \ | "list difference" Tip-NewFin is b [|] | [b,c,d,] / \ + c [|] / \ d ~empty cell~ <--- NewFin
This can continue for some time. Mayn algorithms do not consume at the tip but just append at the fin. In any case, when we are done: Fin=[], which closes the list. Once that unification has been performed, a proper list can be found at Tip:
Tip ----->[|] + / \ | "list difference" Tip-Fin is x [|] | [x,y,z] / \ | y [|] | / \ + z [] <--- Fin after Fin=[] - there is now a proper list at Tip
or if Tip and Fin were equal when the unification is performed, in which case the "list difference" is the empty list:
Tip------> [] <----- Fin after Fin=[] - there is now a proper list at Tip
The "empty open difference list" is evidently trivially an empty cell (or two unbound variables denoting the same empty cell): Tip=Fin. It's a bit borderline. Is this really a "list"?
Tip------> ~empty cell~ <----- NewFin
It can fail or succeed of course (or throw an exception, rudely moving us back from logic-land back into programming-land), but if it succeeds:
length([a,b,c],3), When interpreted as function length(List) -> Length, length(L) is evidently surjective (in its domain), so one could say:
length([a,b,c],3) verifies/checks the length of list [a,b,c]length([a,b,c],3) verifies/checks whether list [a,b,c] is a member of the preimage of 3 (technically of the set {3}).length([a,b,c],L) computes/deduces L from [a,b,c] or maps [a,b,c] to Lappend([a,b],[c,d],X). X contains no information about the "input"append_reversible([a,b],[c,d],[X,PrefixLen]). [X,PrefixLen] contains enough information to "get back" to the input!length(L,3) yielding [a,b,c]? NOPE!length(L,3) yielding [_,_,_]. Yes!member(X,[a,b,c]) yields a, b, c in turn.append(L1,L2,[a,b,c]). yields L1 = [],L2 = [a, b, c] ; L1 = [a],L2 = [b, c] ; L1 = [a, b],L2 = [c] ; L1 = [a, b, c],L2 = []