\section{Single Sided Unification rules} \label{sec:ssu} \index{single sided unification}% \index{SSU}% \index{term subsumption}% For the execution of a normal Prolog clause, the goal term is unified with the head of the clause. This allows us to write facts such as below and use this relation in all four possible \jargon{modes}. This is the basis of SLD resolution that turns Prolog into a logic programming language. \begin{code} parent('Bob', 'Susan'). \end{code} \noindent In practice though, Prolog is both a logic programming language and a language for expressing computations in a near \jargon{procedural} style. The first is used to solve (notably) combinatorial problems while the latter is used for I/O, data transformation and the many non-logical operations that are involved in many applications. Many Prolog programmers experience writing procedural style Prolog as fighting non-determinism and dealing with hard to debug silent failures because no clause matches some goal. Below are two typical queries on library predicates that have a procedural nature, i.e., are \jargon{single moded}. \begin{code} ?- sum_list(a, X). false. ?- sum_list([1|T], X). T = [], X = 1 ; ERROR: Arguments are not sufficiently instantiated \end{code} \noindent The definition of \index{sum_list/2}\predref{sum_list}{2} is it appears in library(lists) is below. This implementation can be considered elegant. Note that \index{sum_list/2}\predref{sum_list}{2} has only one meaningful mode: (+,-). A general (logical) implementation would allow for a partial list or a list holding one or more variables, With a proper list that holds a single variable we can still make a sound logical implementation. In all other cases the number of solutions is infinite and even \jargon{uncountable} for a partial list, making the predicate useless as a \jargon{generator} of solutions. \begin{code} sum_list(Xs, Sum) :- sum_list(Xs, 0, Sum). sum_list([], Sum, Sum). sum_list([X|Xs], Sum0, Sum) :- Sum1 is Sum0 + X, sum_list(Xs, Sum1, Sum). \end{code} \noindent If we want to avoid the above dubious behaviour we have two options. First, we can verify that the first argument is a list before entering the recursion, changing the first clause as below. The disadvantage is that we process the list twice. \begin{code} sum_list(Xs, Sum) :- must_be(list, Xs), sum_list(Xs, 0, Sum). \end{code} \noindent Alternatively, we can rewrite the second clause to verify the list on the fly. That leads to the code below. Most likely the overhead of this alternative compared to the above is even worse in many Prolog implementations. Most people would also consider this code rather inelegant. \begin{code} sum_list(Var, _, _) :- var(Var), instantiation_error(Var). sum_list([], Sum, Sum) :- !. sum_list([X|Xs], Sum0, Sum) :- !, Sum1 is Sum0 + X, sum_list(Xs, Sum1, Sum). sum_list(NoList, _, _) :- type_error(list, NoList). \end{code} \noindent Another example is a relation \nopredref{max}{3}, expressing the maximum of two numbers. A classical textbook definition could be as below. This code has two drawbacks. First it leaves an open choice points in most Prolog implementations if \arg{X} is the largest and second it compares the two numbers twice. Some Prolog systems detect this particular case, but in general it needs two know that one test is the strict negation of the other. \begin{code} max(X,Y,X) :- X >= Y. max(X,Y,Y) :- Y > X. \end{code} \noindent As a result people use a cut and might come up with the \textbf{wrong} solution below. Consider the query \exam{?- max(5,2,2).} to see why this code is broken. \begin{code} max(X,Y,X) :- X >= Y, !. max(_,Y,Y). \end{code} \noindent A correct solution is below, \jargon{delaying} binding the output until after the cut. \begin{code} max(X,Y,M) :- X >= Y, !, M = X. max(_,Y,Y). \end{code} \noindent Some people may prefer using if-then-else as below. This is arguable the cleanest efficient solution in standard Prolog. \begin{code} max(X,Y,M) :- ( X >= Y -> M = X ; M = Y ). \end{code} \noindent As we have seen from these examples, writing procedural code in Prolog requires us to follow the two basic principles below. Both principles have been properly described in \textit{The Craft of Prolog} \cite{Keefe:90}. \begin{itemize} \item Structure every clause as \exam{Head :- Guard, !, Body}. Every clause has the cut as early as possible. \arg{Guard} can be empty. The last clause often does not need a cut. \item Avoid that the head unification binds values in the goal term. We see this may lead to undesirable results such as sum_list(L,S) binding \arg{L} to `[]` and \arg{S} to `0` as well as loss of \jargon{steadfastness}, causing max(5,2,2) to succeed. The first requires additional \index{var/1}\predref{var}{1} or \index{nonvar/1}\predref{nonvar}{1} tests. The second requires delaying unification until after the cut. \end{itemize} \href{http://picat-lang.org/}{Picat} provides the \funcref{\Sssu}{2} alternative for the Prolog \jargon{neck} (\funcref{\Sneck}{2}) to force the above practices. A Picat rule has the following shape: \begin{code} Head, Guard => Body. \end{code} \noindent This is semantically equivalent to the Prolog clause below. The \index{subsumes_term/2}\predref{subsumes_term}{2} guarantees the clause head is more \jargon{generic} than the goal term and thus unifying the two does not affect any of the arguments of the goal. This implies all output unification _must_ be done after the head unification. \begin{code} p(V1,V2,...,Vn) :- Pattern = p(A1,A2,...,An), Args = p(V1,V2,...,Vn), subsumes_term(Pattern, Args), Pattern = Args, Guard, !, Body. \end{code} \noindent SWI-Prolog as of version 8.3.19 support \funcref{\Sssu}{2} as an alternative to normal Prolog clauses. The construct comes with the following properties. \begin{itemize} \item A predicate either uses \funcref{\Sneck}{2} for all its clauses or \funcref{\Sssu}{2}. Mixing is \textbf{not} allowed and raises a permission error for a clause that does not use the same \jargon{neck} as the first clause. \item Unlike Picat, it is an error if no clause matches. \end{itemize} Given \funcref{\Sssu}{2} rules, we can rewrite \index{sum_list/2}\predref{sum_list}{2} as below. The first clause can be written using \funcref{\Sneck}{2} or \funcref{\Sssu}{2}. As the head is the most general head and there is only one clause these are fully equivalent. The \nopredref{sum_list}{3} helper needs a small modification: we need to delay the unification against \arg{Sum} to the body. The last clause is equivalent. \begin{code} sum_list(Xs, Sum) => sum_list(Xs, 0, Sum). sum_list([], Sum0, Sum) => Sum = Sum0. sum_list([X|Xs], Sum0, Sum) => Sum1 is Sum0 + X, sum_list(Xs, Sum1, Sum). \end{code} \noindent Given this definition, \exam{sum_list(L,S)} no longer matches a rule and neither does e.g., \exam{sum_list(a,S)}. Both raise an error. Currently the error is defined as below. \begin{code} existence_error(matching_rule, Head) \end{code} \noindent Should silent failure be desired if no rule matches, this is easily encoding by adding a rule at the end using the most general head and \index{fail/0}\predref{fail}{0} as body: \begin{code} sum_list(_,_,_) => fail. \end{code} \noindent \subsection{Single Sided Unification Guards} \label{sec:ssu-guard} Using the construction \exam{Head, Guard => Body}, the \arg{Guard} is executed \emph{after} the single sided head unification. If the \arg{Guard} succeeds the clause executes a cut (\predref{\Scut}{0}) and proceeds normally. There are no restrictions on the guard code. A well behaved guard is a \jargon{test}. Notably: \begin{itemize} \item Though not enforced\footnote{We do not know about an efficient way to enforce unification against head arguments}, guard code shall not instantiate variables in the \arg{Head} because this breaks the promise of SSU and may make the node non-steadfast. \item It is bad style (but again, not enforced) to have any type of side effects (output, database change, etc.) \item Typically, guard calls are \const{semidet}. Non-deterministic calls are allowed. If the guard succeeds with choicepoints these are pruned before the body is entered. \end{itemize} As a special exception, explicit unification against a variable in the head is moved into the head. See \secref{indexbody}. In the example below, the \exam{X = f(I)} is moved into the head and (thus) is executed using single sided unification. \begin{code} p(X), X = f(I), integer(I) => q(X). \end{code} \noindent \begin{quote} \textbf{Warning} Moving the guard unification into the head changes the semantics of the unification. This may be defended by the rules above that claim one should not unify against the head arguments in the guard. Future versions may use a dedicated operator to indicate that the unification may be moved into the head. \end{quote} \subsection{Consequenses of {\Sssu} single sided unification rules} \label{sec:ssu-consequences} The \funcref{\Sssu}{2} construct is handled by the low-level compiler if no \jargon{guard} is present. If a guard is present it is currently compiled into the construct below. The Picat \funcref{\Smssu}{2} \jargon{neck} operator is like \funcref{\Sssu}{2}, but does not \jargon{commit} to this rule. We are not yet sure whether or not SWI-Prolog will remain supporting \funcref{\Smssu}{2}.\footnote{\funcref{\Smssu}{2} is currently implemented but not defined as an operator.} \begin{code} Head ?=> Guard, !, Body. \end{code} \noindent The main consequence is that \index{clause/2}\predref{clause}{2} cannot distinguish between a normal clause and a \funcref{\Sssu}{2} clause. In the current implementation it operates on both without distinguishing the two. This implies e.g., \jargon{cross referencing} still works. Meta interpretation however does not work. In future versions \index{clause/2}\predref{clause}{2} may fail on these rules. As an alternative we provide \index{rule/2}\predref{rule}{2},3. \begin{description} \predicate{rule}{2}{:Head, -Rule} \nodescription \predicate{rule}{3}{:Head, -Rule, -Ref} True when \arg{Rule} is a rule/clause that implements \arg{Head}. \arg{Rule} is a complete rule term. For a normal clause this is a term \exam{Head :- Body} and for a single sided unification rule it is a term \exam{Head {\Sssu} Body}. \end{description} \subsection{SSU: Future considerations} \label{sec:ssu-future} The current implementation is a rather simple. Single sided unification is achieved doing normal head unification and backtrack if this unification bound variables in the goal term. Future versions are likely to backtrack as soon as we find a variable in the goal that needs to be unified. It is likely that in due time significant parts of the libraries will be migrated to use SSU rules, turning many silent failures on type errors into errors.