Planning for an Efficient Implementation of
Hypothetical Bousi$\sim$Prolog

A basic hypothetical propositional logic transition system is first defined, to determine the operational semantics of the language.

Let $\Pi$ be a program. Let $E$ be a set of tuples $\langle G,\Pi\rangle$ (goal, program), each representing a state of a computation. Let $\stackrel{{\scriptstyle\!\!\!\;}}{{{\Rightarrow}_{\mbox{\tiny HPSLD}}}}\subseteq(E\times E)$ be the transition relation as now defined in Definition 2.1. A successful inference sequence for a given state is a sequence ending in the state $\langle\square,\Pi\rangle$, where $\square$ represents the empty clause.

The following simple program, adapted from [Bonner (1994)], illustrates this definition.

This definition of hypothetical propositional resolution can be neatly implemented in Prolog with a meta-interpreter keeping track of the current program, which can be augmented as needed by the embedded implication. Proposals of other logic systems [Bonner (1994), Lopez and Pimentel (1999)] also suggest this kind of implementation (passing the program as an argument). The solving of an embedded implication can be implemented in a meta-interpreter with the clause: $solve((R\Rightarrow\phi),\Pi)\leftarrow solve(\phi,[R|\Pi])$ (cf. Appendix A). But passing the program as an argument in Prolog requires that its data structure be built in the heap, a costly operation. Another alternative is to use the dynamic database to assert the program rules. In contrast to other Prolog implementations, SWI-Prolog does not differentiate between compiling and asserting, producing a similar code for both operations which, in particular, retains multi-argument and deep indexing. In this way, accessing data in dynamic memory is typically faster than in the heap, even using techniques such as Key-Value associations implemented as a balanced binary tree (AVL tree).

A first approach to dealing with the embedded implication is to consult the program as a normal Prolog program with a definition for the embedded implication with the operator $\Rightarrow$: $(X\Rightarrow Y)\leftarrow assertz(X)\land call(Y)\land retract(X).$ Thus, it is possible to answer goal $\leftarrow p$ for program {$p\leftarrow q\Rightarrow q$}: solving $p$ amounts to asserting $q$ and subsequently solving goal $\leftarrow q$. When $q$ has been proved, the assumption is retracted. However, this approach is not correct because alternatives can be lost. Consider the program {$p\leftarrow(q\leftarrow r)\Rightarrow q$, $r$, $r$}. Clearly, there should be two answers for goal $p$ but, after solving $q$ for the first answer, the hypothesis is retracted, so that further answers are lost.

Simply removing the retraction does not fix the issue because the hypothesis would then be beyond the scope of the implication. For example, in the program {$p\leftarrow(q\Rightarrow q)\land q$}, the goal $\leftarrow p$ would succeed when it should fail because the second call to $q$ is outside the scope of the embedded implication. Instead, a plausible approach is to attach each hypothesis to the program context it belongs to, and allow its selection only in that context, which is the technique explained in the next section.

Rule 2 in Definition 2.1 constructs a proof for the consequent $A$ in the context of $\Pi\cup\{R\}$, where $\Pi$ is the current program and $R$ is the antecedent of the embedded implication (hypothesis). Thus, each assumption builds a new program which can be understood as a program context for the proof of a consequent.

Because embedded implication queries can be nested, $R_{1}\Rightarrow R_{2}\Rightarrow\ldots R_{n}\Rightarrow A$, also hypothetical contexts can be chained $\Pi_{0}\subseteq\Pi_{1}\subseteq\Pi_{2}\subseteq\ldots\subseteq\Pi_{n}$, where $\Pi_{i+1}=\Pi_{i}\cup\{R_{i+1}\}$. Hypothetical contexts are partially ordered by the set inclusion relation $\subseteq$. For pragmatic reasons, contexts can be identified by a sequence of unique symbols, one for each new context in the inference sequence. For the chain of contexts $\Pi_{0}\subseteq\Pi_{1}\subseteq\Pi_{2}\subseteq\ldots\subseteq\Pi_{n}$, the sequence of symbols $i_{1}\ldots i_{j}$, $1\leq j\leq n$, identifies the context $\Pi_{j}$, where $\Pi_{0}$ stands for the initial user program (for which the empty sequence is assumed as its context identifier).

More formally, given a (possibly total ordered) set of indexes $I$, a context $\Pi_{j}$ can be identified by a univocal sequence of indexes $s_{j}=i_{1}\ldots i_{j}$, $1\leq j\leq n$, called a context identifier, and alternatively denoted by $\Pi_{s_{j}}$. For a context $\Pi_{s}$, with context identifier $s$, and an embedded implication query $R\Rightarrow A$, a new context $\Pi_{s.i}$ is built, where the context identifier $s.i$ is the concatenation of a fresh index $i\in I$ to the sequence $s$. The initial user program $\Pi_{0}$ is denoted by $\Pi_{\epsilon}$, where $\epsilon$ is the empty sequence.

The set of context identifiers $S$ is a prefix-ordered set, where the prefix relation $\preceq$ on $S$ is defined as follows: for two context identifiers $s_{1}$ and $s_{2}$, $s_{1}\preceq s_{2}$ if and only if $s_{1}$ is a prefix of $s_{2}$; that is, there exists a sequence of indexes $s$ such that $s_{2}=s_{1}.s$. The prefix relation is reflexive ($(\forall s\in S)~{}s\preceq s$), anti-symmetric ($(\forall s_{1},s_{2}\in S)s_{1}\preceq s_{2}\wedge s_{2}\preceq s_{1}\to s_{1}=s_{2}$), transitive ($(\forall s_{1},s_{2},s_{3}\in S)s_{1}\preceq s_{2}\wedge s_{2}\preceq s_{3}\to s_{1}\preceq s_{3}$) and downward total ($(\forall s_{1},s_{2},s_{3}\in S)~{}s1\preceq s_{3}\wedge s_{2}\preceq s_{3}\to(s1\preceq s_{2}\vee s_{2}\preceq s_{1})$) [Cuijpers (2013)]. The first three properties classify a prefix order as a partial order. Only the downward totality is special, meaning that, although the future evolution of a computation may be branching, from a given point of execution, the past is always totally ordered. In our framework, where the set of sequences has a minimum element (the empty sequence $\epsilon$), the evolution of a computation can be abstracted by a tree structure, where the branches are sequences representing a context identifier and each prefix in the sequence, a previous context identifier. By construction, for all context identifiers $s_{1}$ and $s_{2}$, if $s_{1}\preceq s_{2}$ then $\Pi_{s_{1}}\subseteq\Pi_{s_{2}}$.

As contexts are sets of rules, each rule can be identified as belonging to a context by the identifier of its program context. Thus, a context identifier can be associated with a rule.

In the framework of hypothetical reasoning, a rule only can be selected for solving if it is within the scope of the current context. Alternatively, we often say that $R$, with context identifier $s_{j}$, is included in (or belongs to) the context $\Pi_{s_{k}}$, because $\Pi_{s_{j}}\subseteq\Pi_{s_{k}}$ when $s_{j}\preceq s_{k}$. Thus, from a context $\Pi_{s_{k}}$ it is possible to access all rules whose context identifier $s_{j}$ is a prefix of $s_{k}$.

Hypothetical propositional SLD resolution can be efficiently implemented by translating hypothetical propositional programs into Prolog in a such a way as to mimic this operational semantics. This translation is based on, first, providing a context identifier for each rule (either a user-program rule or the hypothesis in an embedded implication); and, second, transmitting the current context for which the rule is selected during inferencing. Each hypothesis receives a new index symbol (an integer for simplicity) which is added to the current context identifier sequence to form the identifier of the new context. This sequence can be implemented as a reversed integer list.

In contrast to the basic implementations in Section 2, user programs and hypotheses must be translated by adding the new arguments for the rule and current context identifiers:

Definition 2.4 deserves some comment. Firstly, variables (e.g., $S^{R}$ or $S^{C}$) denote context identifiers, which may be unknown at translation time. In general, $S^{R}$ (or $S^{H}$) denotes the context to which a rule $R$ (or $H$) belongs, while $S^{C}$ (or $S^{C^{\prime}}$) denotes the current context in which the rule will be selected for solving or the goal will be solved.

Since an embedded implication $H\Rightarrow G$ generates a new context $S^{H}=S^{C}.I$, the corresponding hypothetical rule $H$ will be annotated with $S^{H}$, which will be the current context in which the goal G will be solved. It is not possible to set the actual index $I$ in the sequence $S^{H}$ for the embedded implication until solving-time (also, depending on the goal, not all contexts will be needed). Actually solving an embedded implication will bind the elements in the sequence representing the context. As $chk(\epsilon,S^{C})$ always holds, it can be omitted in the translation. The following example illustrates Definition 2.4 for a simple program rule:

Solving the embedded implication can be implemented as follows:

Considering $\stackrel{{\scriptstyle\!\!\!\;}}{{{\Rightarrow}_{\mbox{\tiny SLD}}}}\subseteq(E\times E)$ as the transition relation for propositional SLD resolution of a program $\Pi$, where $E$ is a set of states formed by tuples $\langle G,\theta,\Pi\rangle$ (goal, substitution, program), the following can be stated:

See the proof of Proposition 3.6 in the predicate logic case, of which this is a particular case.

Definition 2.1 can be extended to the non-propositional case by dealing with substitutions, which then become part of the notion of computation state. Let $E$ be a set of tuples $\langle G,\sigma,\Pi\rangle$ (goal, substitution, program), each representing a state of a computation. Let $\stackrel{{\scriptstyle\!\!\!\;}}{{{\Rightarrow}_{\mbox{\tiny HSLD}}}}\subseteq(E\times E)$ be the transition relation as defined in Definition 3.1 below. A successful inference sequence for a given state is a sequence ending in the state $\langle\square,\sigma^{\prime},\Pi\rangle$.

As in the propositional case, HSLD can be implemented as a meta-interpreter, and Definition 2.4 can easily be extended to the predicate logic case by using predicates instead of propositions:

The following example illustrates Definition 3.2 for a simple program that will be used in several places hereafter:

$\blacksquare$

Despite the two solutions above for solving the embedded implication by means of a meta-interpreter and program translation, our goal is to add this kind of implication to Bousi$\sim$Prolog, which requires complex rule transformations.

This raises two problems: First, in contrast to the solution in Definition 3.2, a more involved translation is required before asserting hypotheses. This first issue suggests avoiding program compilations at run-time by translating hypotheses at compile-time, but this leads to the second problem: When asserting a rule, all variables become universally quantified by default, but this is no longer true in the context of an embedded implication. Thus, it will be necessary to take account of substitutions in assumptions. Taking the logic system shown in Section 2.3 as a starting point, the following sections will cover these two issues.

One possible approach to addressing the first problem is to translate and assert clauses at compile-time, so that a program does not need any translation at run-time. Although this involves all hypotheses in the program being translated and asserted, it is highly likely that the memory thus speculatively used will return a pay-off in terms of run-time gains.

Since it is not known how many times a given embedded implication will be selected for solving, some sort of registration is needed at run-time. First, the hypothesis can be translated and asserted at run-time and, whenever the embedded implication is selected for solving at run-time, the corresponding hypothesis is registered for the current context. Each registration will correspond to one alternative of the hypothesis and can be represented by an entry in a new dynamic predicate $reg$/2: one argument for the rule reference and another for the context in which it was registered.

Therefore, registering a rule $R$ for a new context needs a univocal reference $I^{R}$ to the rule. A new argument must thus be added to any predicate containing its reference, which can be achieved with a predicate similar to $get\_ci$ (Definition 2.5). Definition 2.4 must be modified to add this argument to head clauses and to translate the embedded implication with the reference to the translated hypothesis. In addition to the call to the $chk$/2 predicate, each body rule must include a call to $reg$/2 to retrieve, by backtracking, as many alternatives of the hypothesis as were registered in the course of the solving process.

In turn, solving the embedded implication needs to perform this registration of the hypothesis for the current context $S^{C}$ augmented with this hypothesis. Then, the embedded implication is added, with two new arguments: the new element in the context identifier sequence $I^{C}$ and the current context $S^{C}$, meaning it is no longer a binary operator: $\Rightarrow(I^{R},G,I^{C},S^{C})\leftarrow get\_ci(I^{C})\land assertz(reg(I^{R},S^{C}.I^{C}))\land call(G)$

The following examples informally illustrate the proposed translation (which will be formalised in Definition 3.5) and the behaviour of the translated program. From here on, context identifiers will be represented as reversed lists of unique indexes.

An advantage of this approach with respect to that given in Section 2.3 is that assumptions via recursion require only one translated rule in the memory, rather than needing as many translated rules as assumptions. The following program illustrates this:

$\Pi=\{p(0),p(N)\leftarrow N>0\land N_{1}~{}is~{}N-1\land(q\Rightarrow p(N_{1}))\}$

There is only one translated rule for $q$ (the same as in the previous example) and as many entries in $reg$/2 as $N$ in the goal $\leftarrow p(N)$.

An assertion with free variables is a problem in this approach because it is translated at compile-time and the actual substitution is not known before solving-time.

Compared to the approach in Section 2.3 (and extended to the predicate logic case in Definition 3.2), where each assumption is asserted at run-time, now an assumption is asserted at compile-time without any trace of its actual substitution, which can lead to losing bindings for the shared variables between the hypothesis and its rule. The following program illustrates this issue:

Moreover, variable sharing is also a problem. Let us consider the following example:

Substitutions must therefore be passed when solving an embedded implication by using its hypothesis: Each rule will contain an extra argument containing the list of shared variables. In addition, the list of shared variables will be added to the rule registration in the context of the embedded implication so that, at solving-time, the translated implication can map the current substitution to these variables. Finally, each rule body in the translation will include a call to the $reg$ predicate extended with an argument containing these shared variables, making it possible to transmit variable bindings at run-time. This is formalised in the next subsection.

Satisfying the requirements set out above, we define rule registration as follows:

Then, the implementation of embedded implication solving, as introduced for the propositional case in Definition 2.5, is adapted as follows:

Considering what must be added to the translation (precompiling with registering, and variable sharing), rule and goal translation are defined as follows:

Considering $\stackrel{{\scriptstyle\!\!\!\;}}{{{\Rightarrow}_{\mbox{\tiny SLD}}}}\subseteq(E\times E)$ as the transition relation for SLD resolution of a program $\Pi$, where the space state $E$ is a set of tuples $\langle G,\theta,\Pi\rangle$ (goal, substitution, program), the following can be stated:

Appendix A contains a performance analysis and Appendix B the proof of this proposition.

It is first convenient to review some concepts before extending BPL to include hypothetical reasoning.

BPL, among other features, incorporates a unification algorithm based on proximity relations. A proximity relation is a binary fuzzy relation $\mathscr{R}:U\times U\longrightarrow[0,1]$ on a universe $U$ satisfying, for any $e,e_{1},e_{2},e_{3}\in U$, the reflexive ($\mathscr{R}(e,e)=1$) and symmetric ($\mathscr{R}(e_{1},e_{2})=\mathscr{R}(e_{2},e_{1})$)) properties. If in addition it has the $\triangle$-transitive property ($\mathscr{R}(e_{1},e_{3})\geq\mathscr{R}(e_{1},e_{2})\mbox{\footnotesize$\triangle$}\mathscr{R}(e_{2},e_{3})$), where the operator $\triangle$ is an arbitrary t-norm, it is called a similarity relation. A proximity relation allows two symbols in a program to be weakly related. Given a binary fuzzy relation $\mathscr{R}$ and a value $\lambda$, the $\lambda$-cut $\mathscr{R}_{\lambda}=\{\langle x,y\rangle\mid\mathscr{R}(x,y)\geq\lambda\}$. By abuse of language, the value $\lambda$ is also called $\lambda$-cut (or cut value), which can be understood as a user-defined threshold intended to prune answers for a minimum degree of confidence.

A weak unification of terms builds upon the notion of weak unifier of level $\lambda$ for two expressions $\mathscr{E}_{1}$ and $\mathscr{E}_{2}$ with respect to $\mathscr{R}$ (or $\lambda$-unifier): a substitution $\theta$ such that $\mathscr{R}(\mathscr{E}_{1}\theta,\mathscr{E}_{2}\theta)\geq\lambda$, which is the unification degree of $\mathscr{E}_{1}$ and $\mathscr{E}_{2}$ with respect to $\theta$ and $\mathscr{R}$. There are several weak unification algorithms [Julián-Iranzo and Sáenz-Pérez (2021)] based on this notion and on the proximity-based unification relation $\Rightarrow$, which defines a transition system (based on [Martelli and Montanari (1982)]). This relation, applied to a set of unification problems $\{\mathscr{E}_{i}\approx\mathscr{E}^{\prime}_{i}|1\leq i\leq n\}$ can yield either a successful or a failed sequence of transition steps. In the first case, both a successful substitution and a unification degree are obtained (detailed in, e.g., [Julián-Iranzo and Sáenz-Pérez (2021)]). The weak most general unifier (wmgu) $\theta$ between two expressions, denoted by ${\sf\small wmgu}_{\mathscr{R}}^{\lambda}(\mathscr{E}_{1},\mathscr{E}_{2})$, is defined as a $\lambda$-unifier of $\mathscr{E}_{1}$ and $\mathscr{E}_{2}$ such that there is no other $\lambda$-unifier $\sigma$ which is more general than $\theta$. That is, there exists a substitution $\delta$ such that, for any variable $x$ in ${\mathscr{D}}om(\sigma)\cup{\mathscr{D}}om(\theta)$, $\mathscr{R}(x\sigma,x\theta\delta)\geq\lambda$. Although, unlike in the classical case, the wmgu is not unique, the weak unification algorithm computes a representative wmgu with approximation degree greater than or equal to any other wmgu.

To combine WSLD and hypothetical reasoning, it is necessary to augment the notion of computation state by adding to it the context of the computation (i.e., the current program).

Let $E$ be a set of tuples $\langle G,\Pi,\theta,\alpha\rangle$ (goal, program, substitution, approximation degree), each representing a state of a computation. Let $\stackrel{{\scriptstyle\!\!\!\;}}{{{\Rightarrow}_{\mbox{\tiny HWSLD}}}}\subseteq(E\times E)$ be the transition relation as defined below in Definition 4.1. A successful inference sequence for a given state is a sequence ending in the state $\langle\square,\Pi,\theta^{\prime},\alpha^{\prime}\rangle$ for some substitution $\theta^{\prime}$ and approximation degree $\alpha^{\prime}$, where $\square$ represents an empty clause.

An operational semantics can be defined for expanded programs by means of a transition system with a set $E$ of states (goal, program, substitution, degree), adding a new inference rule to the tackling of assumptions: