Typed SLD-Resolution: Dynamic Typing for Logic Programming

The three-valued logic used in this paper is the Weak Kleene logic [Kle38], later interpreted by [BB81] and [Bea16]. As in our previous work [BFC19] the third value is called wrong and represents a (dynamic) type error. In this logic, the value wrong propagates through every connective, which is a behaviour we want the type error value to have. In table 1, we describe the connectives in the logic.

The negation of logic values is defined as: $\neg true=false$, $\neg false=true$ and $\neg\emph{wrong}=\emph{wrong}$. And implication is defined as: $p-->q\equiv(\neg p)\vee q$.

Note that whenever the value wrong occurs in any connective in the logic, the result of applying that connective is wrong.

In this paper we fix the set of base types int, float, atom and string, an enumerable set of compound types $f(\sigma_{\_}1,\cdots,\sigma_{\_}n)$, where $f$ is a function symbol and $\sigma_{\_}i$ are types, and an enumerable set of functional types of the form $\sigma_{\_}1\times\cdots\times\sigma_{\_}n\rightarrow\sigma$, where $\sigma_{\_}i$ and $\sigma$ are types.

We use this specific choice of base types because they correspond to types already present, to some extent, in Prolog. Some built-in predicates already expect integers, floating point numbers, or atoms.

The alphabet of logic programming is composed of symbols from disjoint classes. For our language of terms we have an infinite set of variables Var, an infinite set of function symbols Fun, parenthesis and the comma [Apt96].

Terms are defined as follows:

• •

  a variable is a term,

• •

  if $f$ is an n-ary function symbol and $t_{\_}1,\dots,t_{\_}n$ are terms, then $f(t_{\_}1,\dots,t_{\_}n)$ is a term,

• •

  if $f$ is a function symbol of arity zero, then $f$ is a term and it is called a constant.

A ground term is a term with no variables. In the rest of the paper we assume that ground terms are assumed to be typed, meaning that each constant has associated to it a base type and for any ground compound term $f(t_{\_}1,\cdots t_{\_}n)$, the function symbol $f$ (of arity $n\geq 1$) has associated to it a functional type of the form $\sigma_{\_}1\times\cdots\times\sigma_{\_}n\rightarrow f(\sigma_{\_}1,\cdots,\sigma_{\_}n)$. Note that variables are not statically typed, but, as we will see in the forthcoming sections, type checking of the use of variables will be made dynamically through TSLD-resolution.

We now extend our language of terms to a language of programs by adding an infinite set of predicate symbols Pred and the reverse implication $\leftarrow$.

The definition of atoms, queries, clauses and programs is the usual one [Apt96]:

• •

  an atom is either a predicate symbol $p$ with arity $n$, applied to terms $t_{\_}1,\dots,t_{\_}n$, which we write as $p(t_{\_}1,\dots,t_{\_}n)$. We will represent atoms by $H,A,B$;

• •

  a query is a finite sequence of atoms, which we will represent by $Q,\bar{A},\bar{B}$;

• •

  a clause is of the form $H\leftarrow\bar{B}$, where $H$ is an atom of the form $p(t_{\_}1,\dots,t_{\_}n)$ and $\bar{B}$ is a query;

• •

  a program is a finite set of clauses, which we will represent by $P$.

The interpretation of queries and clauses is quantified. Every variable that occurs in a query is assumed to be existentially quantified and every variable that occurs in a clause is universally quantified [Apt96].

To compute in logic programming, we need a program $P$ and a query $Q$. We can interpret $P$ as being a set of statements, or rules, and $Q$ as being a question that will be answered by finding an instance $\theta(Q)$ such that $\theta(Q)$ follows from $P$. The essence of computation in logic programming is then to find such $\theta$ [Apt96].

In our setting the basic step for computation is the TSLD-derivation step. It corresponds to having a non-empty query $Q$ and selecting from $Q$ an atom $A$. If $A$ unifies with $H$, where $H\leftarrow\bar{B}$ is an input clause, we replace $A$ in $Q$ by $\bar{B}$ and apply an mgu of $A$ and $H$ to the query.

In this definition we assume that $A$ is variable disjoint with $H$. It is always possible to rename the variables in $H\leftarrow\bar{B}$ in order to achieve this, without loss of generality.

If the program is clear from the context, we speak of a TSLD-derivation of the query $Q$ and if the input clauses are irrelevant we drop the reference to them. Informally, a TSLD-derivation corresponds to iterating the process of the TSLD-derivation step. We say that a TSLD-derivation is successful if we reach the empty query, further denoted by $\square$. The composition of the mgus $\theta_{\_}1,\dots,\theta_{\_}n$ used in each TSLD-derivation step is the computed answer substitution of the query. A TSLD-derivation that reaches $false$ is called a failed derivation and a TSLD-derivation that reaches $wrong$ is called an erroneous derivation.

In a TSLD-derivation, at each TSLD-derivation step we have several choices. We choose an atom from the query, a clause from the program, and a mgu. It is proven in [Apt96] that the choice of mgu does not affect the success or failure of an SLD-derivation, as long as the resulting mgu is idempotent. Since for TSLD-derivations the successes are the same as the ones in a corresponding SLD-derivation, then the result still holds for TSLD.

The selection rule, i.e, how we choose the selected atom in the considered query, does not influence the success of a TSLD-derivation either [Apt96], however if you stopped as soon as unification returns false, it could prevent us from detecting a type error, in a later atom. Let us show this in the following example.

In fact, as the comma stands for conjunction, and since $wrong\wedge false=false\wedge wrong=wrong$, we have to continue even if typed unification outputs $false$ in a step, and check if we ever reach the value $wrong$. In general, for any selection rule $S$ we can construct a query $Q$ such that it is necessary to continue when typed unification outputs $false$ for some atom in $Q$. Therefore, when we reach the value $false$ in a TSLD-derivation step, we continue applying steps until either we obtain a value $wrong$ from typed unification or we have no more atoms to select. In this last case, we can safely say that we reached $false$. This guarantees independence of the selection rule. For the following example we use the selection rule that always chooses the leftmost atom in a query, which is the selection rule of Prolog.

Note that when we get to $false$ for a typed unification in a TSLD-derivation, we can only output $false$ or $wrong$, so either way it is not a successful derivation.

The selected clause from the program is another choice point we have at each TSLD-derivation step. We will discuss the impact of this choice in the next section.

When we want to find a successful TSLD-derivation for a query, we need to consider the entire search space, which consists of all possible derivations, choosing all possible clauses for a selected atom. We are considering a fixed selection rule here, so the only thing that changes between derivations is the selected clause. We say that a clause $H\leftarrow\bar{B}$ is applicable to an atom $A$ if $H$ and $A$ have the same predicate symbol with the same arity.

Prolog uses the leftmost selection rule, where one always selects the leftmost atom in the query, and since the selection rule does not change the success of a TSLD-derivation we will use this selection rule in the rest of the paper.

We will present two auxiliary definitions which are needed to clearly define the notion of a type error in a program.

The blamed clause is a clause in the program which causes a type error. A similar notion was first defined for functional programming languages with the blame calculus [WF09].

Note that if a program does not have a type error, then there is no blamed clause in the TSLD-tree. Also note that the order of the atoms in the generic query may change the place where we use the blamed clause, but it will not change the fact that there exists one or not.

Intuitively, having a type error in the program means that somewhere in the program we will perform typed unification between two terms that do not have the same type.

Consider a generic query $Q=A,\bar{A}$, where $A=p(X_{\_}1,\dots,X_{\_}n)$. For some derivation, after one step, we will have $\theta(\bar{B},\bar{A})$, where $H\leftarrow\bar{B}$ is a clause in $P$ and $\theta$ is a unifier of $A$ and $H$. Since $\theta$, or any other idempotent mgu of $A$ and $H$, is a renaming of $\{X_{\_}1\mapsto t_{\_}1,\dots,X_{\_}n\mapsto t_{\_}n\}$, where $H=p(t_{\_}1,\dots,t_{\_}n)$, and since the variables $X_{\_}1,\dots,X_{\_}n$ do not occur in $\bar{B}$ because the clause is variable disjoint from the query by definition, nor do they occur in $\bar{A}$, by the definition of the generic query, then $\theta(\bar{B},\bar{A})=\bar{B},\bar{A}$. The argument holds for any other atom in $\bar{A}$. Thus whenever the selected atom belongs to the original query $Q$ the result is never $wrong$ and the mgu can be ignored.

After selecting the blamed clause $c$, every TSLD-derivation is such that $Q_{\_}0\implies\dots\implies Q_{\_}n\implies\emph{wrong}$. Thus, at step $Q_{\_}n$, the selected atom comes from the program and every mgu applied up to this point is from substitutions arising from the program itself and not the query. Therefore, the type error was in the program.

If there is no type error in the program $P$ but the TSLD-tree is finitely erroneous, then that error must have occurred in a unification between terms from the query and the program. We then say that the type error is in the query.

Let $U$ be a non-empty set of semantic values, which we will call the universe. We assume that the universe is divided into domains such that each ground type is mapped to a non-empty domain. Thus, $U$ is divided into domains as follows: $U=Int+Float+Atom+String+A_{\_}1+\dots+A_{\_}n+F+Bool+W$, where $Int$ is the domain of integer numbers, $Float$ is the domain of floating point numbers, $Atom$ is the domain of non-numeric constants, $String$ is the domain of strings, $A_{\_}i$ are domains for trees, where each domain has trees whose root is the same functor symbol and its n-children belong to n domains and $F$ is the domain of functions. Moreover, we define $Bool$ as the domain containing $true$ and $false$, and $W$ as the domain with the single value $wrong$, corresponding to a run-time error. We will call $Int$, $Float$, $Atom$, and $String$ the base domains, and $A_{\_}1,\dots,A_{\_}n$ the tree domains. In particular, we can see that constants are separated into several predefined base domains, one for each base type, while complex terms, i.e. trees, are separated into domains depending on the principal function symbol (root) and the n-tuple inside the parenthesis (n-children).

Every constant of type $T$ is associated with a semantic value in one of the base domains, $Int$, $Float$, $Atom$, or $String$, corresponding to $T$. Every function symbol $f$ of arity $n$ in our language is associated with a mapping $f_{\_}U$ from any n-tuple of base or tree domains $\delta_{\_}1\times\dots\times\delta_{\_}n$ to the domain $F(\delta_{\_}1,\dots,\delta_{\_}n)$, which is the domain of trees whose root is $f$ and the n-children are in the domains $\delta_{\_}i$.

To define the semantic value for terms, we will first have to define states. States, $\Sigma$, are mappings from variables into values of the universe. We also define a function $domain$ that when applied to a semantic value returns the domain it belongs to. The semantic value of a term is defined as follows:

An interpretation associates every predicate symbol $p$ with a function $p_{\_}U$ in $F$, such that the output of the function $p_{\_}U$ is the domain $Bool$ and the input is a union of tuples of domains. For each tuple that is in its domain, the function $p_{\_}U$ either returns $true$ or $false$. We will use $|[~{}|]_{\_}{I,\Sigma}$ to denote the semantics of an expression $E$, which can be an atom, a query, or a clause, in an interpretation $I$, and define it as follows:

The term language and their semantic values are fixed, thus each interpretation $I$ is determined by the interpretation of the predicate symbols. Interpretations differ from each other only in the functions $p_{\_}U$ they associate to each predicate $p$ defined in $P$. We now define a context as a set $\Delta$ of pairs of the form $X:D$, where $X$ is a variable that occurs only once in the set, and $D$ is a domain. We say that $\Sigma$ complies with $\Delta$ if every binding $X:v$ in $\Sigma$ is such that $(X:D)\in\Delta$ and $v\in D$. An interpretation $I$ is a model of $E$ in the context $\Delta$ iff for every state $\Sigma$ that complies with $\Delta$, $|[E|]_{\_}{I,\Sigma}=true$. We will denote this as $\Delta\models|[E|]_{\_}I$. Given a program $P$, we say that an interpretation $I$ is a model of $P$ in context $\Delta$ if $I$ is a model of every clause in $P$ in context $\Delta$. Here we assume, without loss of generality, that all clauses are variable disjoint with each other. If two expressions $E_{\_}1$ and $E_{\_}2$ are such that every model of $E_{\_}1$ in a context $\Delta$ is also a model of $E_{\_}2$ in the context $\Delta$, then we say that $E_{\_}2$ is a semantic consequence of $E_{\_}1$ and represent this by $E_{\_}1\models E_{\_}2$. Suppose two interpretations $I_{\_}1$ and $I_{\_}2$ are models of program $P$ in some context $\Delta$. Suppose, in particular, that for some predicate $p$ of $P$ the associated function is $p_{\_}{U1}$ for $I_{\_}1$ and $p_{\_}{U2}$ for $I_{\_}2$. Let us call $T_{\_}i$ the set of tuples of terms for which $p_{\_}{Ui}$ outputs $true$, and $F_{\_}i$ to the set of tuples of terms for which $p_{\_}{Ui}$ outputs $false$. We say that $I_{\_}1$ is smaller than $I_{\_}2$ if $T_{\_}1\subseteq T_{\_}2$ and, if $T_{\_}1=T_{\_}2$, then $F_{\_}1\subseteq F2$. We say that a model $I$ of $P$ in context $\Delta$ is minimal if for every other model $I\prime$ of $P$ in context $\Delta$, $I$ is smaller than $I\prime$.

To calculate the set of accepted tuples for a given interpretation we will use the immediate consequence operator $T_{\_}P$. The $T_{\_}P$ operator is traditionally used in the logic programming literature to iteratively calculate the minimal model of a logic program as presented in [vEK76, Apt96, Llo84].

Since for us interpretations for predicates are typed, $T_{\_}P\uparrow\omega(\emptyset)$ does not generate an interpretation by itself. Instead it generates a set of atoms $S$. Then we say that any interpretation $I$ derived from $S$ is such that for all predicates $p$ occurring in $S$, $I(p)::(D_{\_}{(1,1)}\times\dots\times D_{\_}{(1,n)})\cup\dots\cup(D_{\_}{(k,1)},\dots,D_{\_}{(k,n)})\to Bool$, where for all $i$ there is at least one atom $p(v_{\_}1,\dots,v_{\_}n)\in S$ such that $v_{\_}1\in D_{\_}{(i,1)},\dots,v_{\_}n\in D_{\_}{(i,n)}$. Note that these interpretations may not be models of $P$ using our new definition of a model. We are now able to define the notion of ill-typed program.