Certified Semantics for Relational Programming

Abstract

We present a formal study of semantics for the relational programming language miniKanren. First, we formulate a denotational semantics which corresponds to the minimal Herbrand model for definite logic programs. Second, we present operational semantics which models interleaving, the distinctive feature of miniKanren implementation, and prove its soundness and completeness w.r.t. the denotational semantics. Our development is supported by a Coq specification, from which a reference interpreter can be extracted. We also derive from our main result a certified semantics (and a reference interpreter) for SLD resolution with cut and prove its soundness.

The reported study was funded by RFBR, project number 18-01-00380.

1 Introduction

In the context of this paper, we understand “relational programming” as a puristic form of logic programming with all extra-logical features banned. Specifically, we use miniKanren as an exemplary language; miniKanren can be seen as a logical language with explicit connectives, existentials and unification, and is mutually convertible to the pure logical subset of Prolog.¹ Unlike Prolog, which relies on SLD-resolution, most miniKanren implementations use a monadic interleaving search, which is known to be complete  [15]. miniKanren is designed as a shallow DSL which may help to equip the host language with logical reasoning features. This design choice has been proven to be applicable in practice, and there are more than 100 implementations for almost 50 languages.

Although there already were attempts to define a formal semantics for miniKanren, none of them were capable of reflecting the distinctive property of miniKanren’s search—interleaving  [18]. Since this distinctive search strategy is essential for the specification of the language and its extensions, the description of almost all development on miniKanren was not based on formal semantics. The introductory book on miniKanren  [12] describes the language by means of an evolving set of examples. In a series of follow-up papers  [1, 7, 13,14,15, 30] various extensions of the language were presented with their semantics explained in terms of a Scheme implementation. We argue that this style of semantic definition is fragile and not self-sufficient since it relies on concrete implementation languages’ semantics and therefore is not stable under the host language replacement. In addition, the justification of important properties of the language and specific relational programs becomes cumbersome.

In this paper, we present a formal semantics for core miniKanren and prove some of its basic properties. First, we define denotational semantics similar to the least Herbrand model for definite logic programs  [23]; then we describe operational semantics with interleaving in terms of a labeled transition system. Finally, we prove soundness and completeness of the operational semantics w.r.t the denotational one. We support our development with a formal specification using the Coq proof assistant  [4], thus outsourcing the burden of proof checking to the automatic tool and deriving a certified reference interpreter via the extraction mechanism. As a rather straightforward extension of our main result, we also provide a certified operational semantics (and a reference interpreter) for SLD resolution with cut, a new result to our knowledge; while this step brings us out of purely relational domain, it still can be interesting on its own.

Fig. 1.

The syntax of the source language

2 The Language

In this section, we introduce the syntax of the language we use throughout the paper, describe the informal semantics, and give some examples.

The syntax of the language is shown in Fig. 1. First, we fix a set of constructors $\mathcal {C}$ with known arities and consider a set of terms $\mathcal {T}_X$ with constructors as functional symbols and variables from X. We parameterize this set with an alphabet of variables since in the semantic description we will need two kinds of variables. The first kind, syntactic variables, is denoted by $\mathcal {X}$. The second kind, semantic or logic variables, is denoted by $\mathcal {A}$. We also consider an alphabet of relational symbols $\mathcal {R}$ which are used to name relational definitions. The central syntactic category in the language is goal. In our case, there are five types of goals: unification of terms, conjunction and disjunction of goals, fresh variable introduction, and invocation of some relational definition. Thus, unification is used as a constraint, and multiple constraints can be combined using conjunction, disjunction, and recursion. The final syntactic category is a specification $\mathcal {S}$. It consists of a set of relational definitions and a top-level goal. A top-level goal represents a search procedure which returns a stream of substitutions for the free variables of the goal. The definition for a set of free variables for both terms and goals is conventional; as “ ” is the sole binding construct the definition is rather trivial. The language we defined is first-order, as goals can not be passed as parameters, returned or constructed at run time.

We now informally describe how relational search works. As we said, a goal represents a search procedure. This procedure takes a state as input and returns a stream of states; a state (among other information) contains a substitution that maps semantic variables into the terms over semantic variables. Then five types of scenarios are possible (depending on the type of the goal):

• Unification “ ” unifies terms $t_1$ and $t_2$ in the context of the substitution in the current state. If terms are unifiable, then their MGU is integrated into the substitution, and a one-element stream is returned; otherwise the result is an empty stream.

• Conjunction “ ” applies $g_1$ to the current state and then applies $g_2$ to each element of the result, concatenating the streams.

• Disjunction “ ” applies both its goals to the current state independently and then concatenates the results.

• Fresh construct “ ” allocates a new semantic variable $\alpha$, substitutes all free occurrences of x in g with $\alpha$, and runs the goal.

• Invocation “ ” finds a definition for the relational symbol $R_i^{k_i}=\lambda x_1\dots x_{k_i}\,.\,g_i$, substitutes all free occurrences of a formal parameter $x_j$ in $g_i$ with term $t_j$ (for all j) and runs the goal in the current state.

We stipulate that the top-level goal is preceded by an implicit “ ” construct, which binds all its free variables, and that the final substitutions for these variables constitute the result of the goal evaluation.

Conjunction and disjunction form a monadic  [32] interface with conjunction playing role of “ ” and disjunction the role of “ ”. In this description, we swept a lot of important details under the carpet—for example, in actual implementations the components of disjunction are not evaluated in isolation, but both disjuncts are evaluated incrementally with the control passing from one disjunct to another (interleaving)  [18]; the evaluation of some goals can be additionally deferred (via so-called “inverse-$\eta$-delay”)  [13]; instead of streams the implementation can be based on “ferns”  [8] to defer divergent computations, etc. In the following sections, we present a complete formal description of relational semantics which resolves these uncertainties in a conventional way.

As an example consider the following specification. For the sake of brevity we abbreviate immediately nested “ ” constructs into the one, writing “ ” instead of “ ”.

Here we defined² two relational symbols—“ ” and “ ”,—and specified a top-level goal “ ”. The symbol “ ” defines a relation of concatenation of lists—it takes three arguments and performs a case analysis on the first one. If the first argument is an empty list (“ ”), then the second and the third arguments are unified. Otherwise, the first argument is deconstructed into a head “ ” and a tail “ ”, and the tail is concatenated with the second argument using a recursive call to “ ” and additional variable “ ”, which represents the concatenation of “ ” and “ ”. Finally, we unify “ ” with “ ” to form a final constraint. Similarly, “ ” defines relational list reversing. The top-level goal represents a search procedure for all lists “ ”, which are stable under reversing, i.e. palindromes. Running it results in an infinite stream of substitutions:

where “$\alpha$” is a semantic variable, corresponding to “ ”, “$\beta _i$” are free semantic variables. Therefore, each substitution represents a set of all palindromes of a certain length.

3 Denotational Semantics

In this section, we present a denotational semantics for the language we defined above. We use a simple set-theoretic approach analogous to the least Herbrand model for definite logic programs  [23]. Strictly speaking, instead of developing it from scratch we could have just described the conversion of specifications into definite logic form and took their least Herbrand model. However, in that case, we would still need to define the least Herbrand model semantics for definite logic programs in a certified way. In addition, while for this concrete language the conversion to definite logic form is trivial, it may become less trivial for its extensions (with, for example, nominal constructs  [7]) which we plan to do in future.

We also must make the following observations. First, building inductive denotational semantics in a conventional way amounts to constructing a complete lattice and a monotone function and taking its least fixed point  [31]. As we deal with a first-order language with only monotonic constructs (conjunction/disjunction) these steps are trivial. Moreover, we express the semantics in Coq, where all well-formed inductive definitions already have proper semantics, which removes the necessity to justify the validity of the steps we perform. Second, the least Herbrand model is traditionally defined as the least fixed point of a transition function (defined by a logic program) which maps sets of ground atoms to sets of ground atoms. We are, however, interested in relational semantics which should map a program into n-ary relation over ground terms, where n is the number of free variables in the topmost goal. Thus, we deviate from the traditional route and describe the denotational semantics in a more specific way.

To motivate further development, we first consider the following example. Let us have the following goal:

There are three free variables, and solving the goal delivers us the following single answer:

where semantic variables $\alpha$, $\beta$ and $\gamma$ correspond to the syntactic ones “ ”, “ ”, “ ”. The goal does not put any constraints on “ ” and “ ”, so there are no bindings for “$\beta$” and “$\gamma$” in the answer. This answer can be seen as the following ternary relation over the set of all ground terms:

The order of “dimensions” is important, since each dimension corresponds to a certain free variable. Our main idea is to represent this relation as a set of total functions

$$ \mathfrak {f}:\mathcal {A}\mapsto \mathcal {D} $$

from semantic variables to ground terms. We call these functions representing functions. Thus, we may reformulate the same relation as

where we use conventional semantic brackets “$\llbracket {\bullet }\rrbracket$” to denote the semantics. For the top-level goal, we need to substitute its free syntactic variables with distinct semantic ones, calculate the semantics, and build the explicit representation for the relation as shown above. The relation, obviously, does not depend on the concrete choice of semantic variables but depends on the order in which the values of representing functions are tupled. This order can be conventionalized, which gives us a completely deterministic semantics.

Now we implement this idea. First, for a representing function

$$ \mathfrak {f} : \mathcal {A}\rightarrow \mathcal {D} $$

we introduce its homomorphic extension

$$ \overline{\mathfrak {f}}:\mathcal {T_A}\rightarrow \mathcal {D} $$

which maps terms to terms:

$$ \begin{array}{rcl} \overline{\mathfrak f}\,(\alpha ) &{} = &{} \mathfrak f\,(\alpha )\\ \overline{\mathfrak f}\,(C_i^{k_i}\,(t_1,\dots .t_{k_i})) &{} = &{} C_i^{k_i}\,(\overline{\mathfrak f}\,(t_1),\dots \overline{\mathfrak f}\,(t_{k_i})) \end{array} $$

Let us have two terms $t_1, t_2\in \mathcal {T_A}$. If there is a unifier for $t_1$ and $t_2$ then, clearly, there is a substitution $\theta$ which turns both $t_1$ and $t_2$ into the same ground term (we do not require $\theta$ to be the most general). Thus, $\theta$ maps (some) variables into ground terms, and its application to $t_{1(2)}$ is exactly $\overline{\theta }(t_{1(2)})$. This reasoning can be performed in the opposite direction: a unification $t_1\equiv t_2$ defines the set of all representing functions $\mathfrak {f}$ for which $\overline{\mathfrak {f}}(t_1)=\overline{\mathfrak {f}}(t_2)$.

We will use the conventional notions of pointwise modification of a function $f\,[x\leftarrow v]$ and substitution $g\,[t/x]$ of a free variable x with a term t in a goal (or a term) g.

For a representing function $\mathfrak {f}:\mathcal {A}\rightarrow \mathcal {D}$ and a semantic variable $\alpha$ we define the following generalization operation:

$$ \mathfrak {f}\uparrow \alpha = \{ \mathfrak {f}\,[\alpha \leftarrow d] \mid d\in \mathcal {D}\} $$

Informally, this operation generalizes a representing function into a set of representing functions in such a way that the values of these functions for a given variable cover the whole $\mathcal {D}$. We extend the generalization operation for sets of representing functions $\mathfrak {F}\subseteq \mathcal {A}\rightarrow \mathcal {D}$:

$$ \mathfrak {F}\uparrow \alpha = \bigcup _{\mathfrak {f}\in \mathfrak {F}}(\mathfrak {f}\uparrow \alpha ) $$

Now we are ready to specify the semantics for goals (see Fig. 2). We’ve already given the motivation for the semantics of unification: the condition $\overline{\mathfrak {f}}(t_1)=\overline{\mathfrak {f}}(t_2)$ gives us the set of all (otherwise unrestricted) representing functions which “equate” terms $t_1$ and $t_2$. Set union and intersection provide a conventional interpretation for disjunction and conjunction of goals. In the case of a relational invocation we unfold the definition of the corresponding relational symbol and substitute its formal parameters with actual ones.

The only non-trivial case is that of “ ”. First, we take an arbitrary semantic variable $\alpha$, not free in g, and substitute x with $\alpha$. Then we calculate the semantics of $g\,[\alpha /x]$. The interesting part is the next step: as x can not be free in “ ”, we need to generalize the result over $\alpha$ since in our model the semantics of a goal specifies a relation over its free variables. We introduce some nondeterminism by choosing arbitrary $\alpha$, but we can prove that with different choices of free variable the semantics of a goal does not change.

Lemma 1

For any goal , for any two variables $\alpha$ and $\beta$ which are not free in this goal, if $\mathfrak {f} \in \llbracket {g\,[\alpha /x]}\rrbracket$, then for any representing function $\mathfrak {f}'$, such that

• 1. $\mathfrak {f}'(\beta ) = \mathfrak {f}(\alpha )$

• 2. $\forall \gamma : \gamma \ne \alpha \wedge \gamma \ne \beta ,\; \mathfrak {f}'(\gamma ) = \mathfrak {f}(\gamma )$

it is true that $\mathfrak {f}' \in \llbracket {g\,[\beta /x]}\rrbracket$.

Fig. 2.

Denotational semantics of goals

The proof turned out to be the most cumbersome among all others in the case where g is a nested construct. In that case, we have to constructively build two representing functions (including an intermediate one for an intermediate goal) by pointwise modification. The details of this proof can be found in the extended version of the paper.³

We can prove the following important closedness condition for the semantics of a goal g.

Lemma 2 (Closedness condition)

For any goal g and two representing functions ${\mathfrak f}$ and ${\mathfrak f'}$, such that $\left. {\mathfrak f}\right| _{FV(g)} = \left. {\mathfrak f'}\right| _{FV(g)}$, it is true, that ${\mathfrak f} \in \llbracket {g}\rrbracket \Leftrightarrow {\mathfrak f'} \in \llbracket {g}\rrbracket$.

In other words, representing functions for a goal g restrict only the values of free variables of g and do not introduce any “hidden” correlations. This condition guarantees that our semantics is closed in the sense that it does not introduce artificial restrictions for the relation it defines.

4 Operational Semantics

In this section we describe the operational semantics of miniKanren, which corresponds to the known implementations with interleaving search. The semantics is given in the form of a labeled transition system (LTS)  [17]. From now on we assume the set of semantic variables to be linearly ordered ($\mathcal {A}=\{\alpha _1,\alpha _2,\dots \}$).

We introduce the notion of substitution

$$ \sigma : \mathcal {A}\rightarrow \mathcal {T_A} $$

as a (partial) mapping from semantic variables to terms over the set of semantic variables. We denote $\varSigma$ the set of all substitutions, $\mathcal {D}om\,({\sigma })$—the domain for a substitution $\sigma$, $\mathcal {VR}an\,({\sigma })=\bigcup _{\alpha \in \mathcal {D}om\,(\sigma )}\mathcal {FV}\,({\sigma \,(\alpha )})$—its range (the set of all free variables in the image).

The non-terminal states in the transition system have the following shape:

$$ S = \mathcal {G}\times \varSigma \times \mathbb {N}\mid S\oplus S \mid S \otimes \mathcal {G} $$

As we will see later, an evaluation of a goal is separated into elementary steps, and these steps are performed interchangeably for different subgoals. Thus, a state has a tree-like structure with intermediate nodes corresponding to partially-evaluated conjunctions (“$\otimes$”) or disjunctions (“$\oplus$”). A leaf in the form determines a goal in a context, where g is a goal, $\sigma$ is a substitution accumulated so far, and n is a natural number, which corresponds to a number of semantic variables used to this point. For a conjunction node, its right child is always a goal since it cannot be evaluated unless some result is provided by the left conjunct.

The full set of states also include one separate terminal state (denoted by $\diamond$), which symbolizes the end of the evaluation.

$$ \hat{S} = \diamond \mid S $$

We will operate with the well-formed states only, which are defined as follows.

Definition 1

Well-formedness condition for extended states:

• $\diamond$ is well-formed;

• is well-formed iff $\mathcal {FV}\,({g})\cup \mathcal {D}om\,({\sigma })\cup \mathcal {VR}an\,({\sigma })\subseteq \{\alpha _1,\dots ,\alpha _n\}$;

• $s_1\oplus s_2$ is well-formed iff $s_1$ and $s_2$ are well-formed;

• $s\otimes g$ is well-formed iff s is well-formed and for all leaf triplets in s it is true that $\mathcal {FV}\,({g})\subseteq \{\alpha _1,\dots ,\alpha _n\}$.

Informally the well-formedness restricts the set of states to those in which all goals use only allocated variables.

Finally, we define the set of labels:

$$ L = \circ \mid \varSigma \times \mathbb {N} $$

The label “$\circ$” is used to mark those steps which do not provide an answer; otherwise, a transition is labeled by a pair of a substitution and a number of allocated variables. The substitution is one of the answers, and the number is threaded through the derivation to keep track of allocated variables.

The transition rules are shown in Fig. 3. The first two rules specify the semantics of unification. If two terms are not unifiable under the current substitution $\sigma$ then the evaluation stops with no answer; otherwise, it stops with the most general unifier applied to a current substitution as an answer.

The next two rules describe the steps performed when disjunction or conjunction is encountered on the top level of the current goal. For disjunction, it schedules both goals (using “$\oplus$”) for evaluating in the same context as the parent state, for conjunction—schedules the left goal and postpones the right one (using “$\otimes$”).

The rule for “ ” substitutes bound syntactic variable with a newly allocated semantic one and proceeds with the goal.

The rule for relation invocation finds a corresponding definition, substitutes its formal parameters with the actual ones, and proceeds with the body.

The rest of the rules specify the steps performed during the evaluation of two remaining types of the states—conjunction and disjunction. In all cases, the left state is evaluated first. If its evaluation stops, the disjunction evaluation proceeds with the right state, propagating the label (SumStop and SumStep), and the conjunction schedules the right goal for evaluation in the context of the returned answer (ProdStopAns) or stops if there is no answer (ProdStop).

Fig. 3.

Operational semantics of interleaving search

The last four rules describe interleaving, which occurs when the evaluation of the left state suspends with some residual state (with or without an answer). In the case of disjunction the answer (if any) is propagated, and the constituents of the disjunction are swapped (SumStep, SumStepAns). In the case of conjunction, if the evaluation step in the left conjunct did not provide any answer, the evaluation is continued in the same order since there is still no information to proceed with the evaluation of the right conjunct (ProdStep); if there is some answer, then the disjunction of the right conjunct in the context of the answer and the remaining conjunction is scheduled for evaluation (ProdStepAns).

The introduced transition system is completely deterministic: there is exactly one transition from any non-terminal state. There is, however, some freedom in choosing the order of evaluation for conjunction and disjunction states. For example, instead of evaluating the left substate first, we could choose to evaluate the right one, etc. This choice reflects the inherent non-deterministic nature of search in relational (and, more generally, logical) programming. Although we could introduce this ambiguity into the semantics (by replacing specific rules for disjunctions and conjunctions evaluation with some conditions on it), we want an operational semantics that would be easy to present and easy to employ to describe existing language extensions (already described for a specific implementation of interleaving search), so we instead base the semantics on one canonical search strategy. At the same time, as long as deterministic search procedures are sound and complete, we can consider them “equivalent”.⁴

It is easy to prove that transitions preserve well-formedness of states.

Lemma 3

(Well-formedness preservation) For any transition $s \xrightarrow {l} \hat{s}$, if s is well-formed then $\hat{s}$ is also well-formed.

A derivation sequence for a certain state determines a trace—a finite or infinite sequence of answers. The trace corresponds to the stream of answers in the reference miniKanren implementations. We denote a set of answers in the trace for state $\hat{s}$ by $\mathcal {T}r_{\hat{s}}$.

We can relate sets of answers for the partially evaluated conjunction and disjunction with sets of answers for their constituents by the two following lemmas.

Lemma 4

For any non-terminal states $s_1$ and $s_2$, .

Lemma 5

For any non-terminal state s and goal g, .

These two lemmas constitute the exact conditions on definition of these operators that we will use to prove the completeness of an operational semantics.

We also can easily describe the criterion of termination for disjunctions.

Lemma 6

For any goals $g_1$ and $g_2$, substitution $\sigma$, and number n, the trace from the state is finite iff the traces from both and are finite.

These simple statements already allow us to prove two important properties of interleaving search as corollaries: the “fairness” of disjunction—the fact that the trace for disjunction contains all the answers from both streams for disjuncts—and the “commutativity” of disjunctions—the fact that swapping two disjuncts (at the top level) does not change the termination of the goal evaluation.

5 Equivalence of Semantics

Now we can relate two different kinds of semantics for miniKanren described in the previous sections and show that the results given by these two semantics are the same for any specification. This will actually say something important about the search in the language: since operational semantics describes precisely the behavior of the search and denotational semantics ignores the search and describes what we should get from a mathematical point of view, by proving their equivalence we establish the completeness of the search, which means that the search will get all answers satisfying the described specification and only those.

Fig. 4.

Denotational semantics of states

But first, we need to relate the answers produced by these two semantics as they have different forms: a trace of substitutions (along with the numbers of allocated variables) for the operational one and a set of representing functions for the denotational one. We can notice that the notion of a representing function is close to substitution, with only two differences:

• representing functions are total;

• terms in the domain of representing functions are ground.

Therefore we can easily extend (perhaps ambiguously) any substitution to a representing function by composing it with an arbitrary representing function preserving all variable dependencies in the substitution. So we can define a set of representing functions that correspond to a substitution as follows:

$$ \llbracket {\sigma }\rrbracket = \{\overline{\mathfrak f} \circ \sigma \mid \mathfrak {f}:\mathcal {A}\mapsto \mathcal {D}\} $$

And the denotational analog of operational semantics (a set of representing functions corresponding to the answers in the trace) for a given state $\hat{s}$ is then defined as the union of sets for all substitutions in the trace:

$$ \llbracket {\hat{s}}\rrbracket _{op} = \cup _{(\sigma , n) \in \mathcal {T}r_{\hat{s}}} \llbracket {\sigma }\rrbracket $$

This allows us to state theorems relating the two semantics.

Theorem 1 (Operational semantics soundness)

If indices of all free variables in a goal g are limited by some number n, then .

It can be proven by nested induction, but first, we need to generalize the statement so that the inductive hypothesis is strong enough for the inductive step. To do so, we define denotational semantics not only for goals but for arbitrary states. Note that this definition does not need to have any intuitive interpretation, it is introduced only for the proof to go smoothly. The definition of the denotational semantics for extended states is shown on Fig. 4. The generalized version of the theorem uses it.

Lemma 7 (Generalized soundness)

For any well-formed state $\hat{s}$

$$ \llbracket {\hat{s}}\rrbracket _{op} \subseteq \llbracket {\hat{s}}\rrbracket . $$

It can be proven by the induction on the number of steps in which a given answer (more accurately, the substitution that contains it) occurs in the trace. We break the proof in two parts and separately prove by induction on evidence that for every transition in our system the semantics of both the label (if there is one) and the next state are subsets of the denotational semantics for the initial state.

Lemma 8 (Soundness of the answer)

For any transition $s \xrightarrow {(\sigma , n)} \hat{s}$, $\llbracket {\sigma }\rrbracket \subseteq \llbracket {s}\rrbracket$.

Lemma 9 (Soundness of the next state)

For any transition $s \xrightarrow {l} \hat{s}$, $\llbracket {\hat{s}}\rrbracket \subseteq \llbracket {s}\rrbracket$.

It would be tempting to formulate the completeness of operational semantics as soundness with the inverted inclusion, but it does not hold in such generality. The reason for this is that the denotational semantics encodes only the dependencies between free variables of a goal, which is reflected by the closedness condition, while the operational semantics may also contain dependencies between semantic variables allocated in constructs. Therefore we formulate completeness with representing functions restricted on the semantic variables allocated in the beginning (which includes all free variables of a goal). This does not compromise our promise to prove the completeness of the search as miniKanren returns substitutions only for queried variables, which are allocated in the beginning.

Theorem 2 (Operational semantics completeness)

If the indices of all free variables in a goal g are limited by some number n, then

Similarly to the soundness, this can be proven by nested induction, but the generalization is required. This time it is enough to generalize it from goals to states of the shape . We also need to introduce one more auxiliary semantics—step-indexed denotational semantics (denoted by $\llbracket {\bullet }\rrbracket ^i$). It is an implementation of the well-known approach  [2] of indexing typing or semantic logical relations by a number of permitted evaluation steps to allow inductive reasoning on it. In our case, $\llbracket {g}\rrbracket ^i$ includes only those representing functions that one can get after no more than i unfoldings of relational calls.

The step-indexed denotational semantics is an approximation of the conventional denotational semantics; it is clear that any answer in conventional denotational semantics will also be in step-indexed denotational semantics for some number of steps.

Lemma 10

$\llbracket {g}\rrbracket \subseteq \cup _i \llbracket {g}\rrbracket ^i$

Now the generalized version of the completeness theorem is as follows.

Lemma 11 (Generalized completeness)

For any set of relational definitions, for any number of unfoldings i, for any well-formed state ,

The proof is by the induction on number of unfoldings i. The induction step is proven by structural induction on goal g. We use Lemmas 4 and 5 for evaluation of a disjunction and a conjunction respectively, and Lemma 1 in the case of fresh variable introduction to move from an arbitrary semantic variable in denotational semantics to the next allocated fresh variable. The details of this proof may be found in the extended version of the paper.

6 Specification in Coq

We certified all the definitions and propositions from the previous sections using the Coq proof assistant.⁵ The Coq specification for the most part closely follows the formal descriptions we gave by means of inductive definitions (and inductively defined propositions in particular) and structural induction in proofs. The detailed description of the specification, including code snippets, is provided in the extended version of the paper, and in this section we address only some non-trivial parts of it and some design choices.

The language formalized in Coq has a few non-essential simplifications for the sake of convenience. Specifically, we restrict the arities of all constructors to be either zero or two and require all relations to have exactly one argument. These restrictions do not make the language less expressive in any way since we can always represent a sequence of terms as a list using constructors and .

In our formalization of the language we use higher-order abstract syntax  [27] for variable binding, therefore we work explicitly only with semantic variables. We preferred it to the first-order syntax because it gives us the ability to use substitution and the induction principle provided by Coq. On the other hand, we need to explicitly specify a requirement on the syntax representation, which is trivially fulfilled in the first-order case: all bindings have to be “consistent”, i.e. if we instantiate a higher-order construct with different semantic variables the results will be the same up to some renaming (provided that both those variables are not free in the body of the binder). Another requirement we have to specify explicitly (independent of HOAS/FOAS dichotomy) is a requirement that the definitions of relations do not contain unbound semantic variables.

To formalize the operational semantics in Coq we first need to define all preliminary notions from unification theory  [3] which our semantics uses. In particular, we need to implement the notion of the most general unifier (MGU). As it is well-known  [25] all standard recursive algorithms for calculating MGU are not decreasing on argument terms, so we can’t define them as simple recursive functions in Coq due to the termination check failure. The standard approach to tackle this problem is to define the function through well-founded recursion. We use a distinctive version of this approach, which is more convenient for our purposes: we define MGU as a proposition (for which there is no termination requirement in Coq) with a dedicated structurally-recursive function for one step of unification, and then we use a well-founded induction to prove the existence of a corresponding result for any arguments and defining properties of MGU. For this well-founded induction, we use the number of distinct free variables in argument terms as a well-founded order on pairs of terms.

In the operational semantics, to define traces as (possibly) infinite sequences of transitions we use the standard approach in Coq—coinductively defined streams. Operating with them requires a number of well-known tricks, described by Chlipala  [9], to be applied, such as the use of a separate coinductive definition of equality on streams.

The final proofs of soundness and completeness of operational semantics are relatively small, but the large amount of work is hidden in the proofs of auxiliary facts that they use (including lemmas from the previous sections and some technical machinery for handling representing functions).

7 Applications

In this section, we consider some applications of the framework and results, described in the previous sections.

7.1 Correctness of Transformations

One important immediate corollary of the equivalence theorems we have proven is the justification of correctness for certain program transformations. The completeness of interleaving search guarantees the correctness of any transformation that preserves the denotational semantics, for example:

• changing the order of constituents in conjunctions and disjunctions;

• distributing conjunctions over disjunctions and vice versa, for example, normalizing goals info CNF or DNF;

• moving fresh variable introduction upwards/downwards, for example, transforming any relation into a top-level fresh construct with a freshless body.

Note that this way we can guarantee only the preservation of results as sets of ground terms; the other aspects of program behavior, such as termination, may be affected by some of these transformations.⁶

One of the applications for these transformations is a conversion from/to Prolog. As both languages use essentially the same fragment of first-order logic, their programs are mutually convertible. The conversion from Prolog to miniKanren is simpler as the latter admits a richer syntax of goals. The inverse conversion involves the transformation into a DNF and splitting the disjunction into a number of separate clauses. This transformation, in particular, makes it possible to reuse our approach to describe the semantics of Prolog as well. In the following sections we briefly address this problem.

7.2 SLD Semantics

The conventional Prolog SLD search differs from the interleaving one in just one aspect—it does not perform interleaving. Thus, changing just two rules in the operational semantics converts interleaving search into the depth-first one:

With this definition we can almost completely reuse the mechanized proof of soundness (with minor changes); the completeness, however, can no longer be proven (as it does not hold anymore).

7.3 Cut

Dealing with the “cut” construct is known to be a cornerstone feature in the study of operational semantics for Prolog. It turned out that in our case the semantics of “cut” can be expressed naturally (but a bit verbosely). Unlike SLD-resolution, it does not amount to an incremental change in semantics description. It also would work only for programs directly converted from Prolog specifications.

The key observation in dealing with the “cut” in our setting is that a state in our semantics, in fact, encodes the whole current search tree (including all backtracking possibilities). This opens the opportunity to organize proper “navigation” through the tree to reflect the effect of “cut”. The details of the semantic description can be found in the extended version of the paper.

For this semantics, we can repeat the proof of soundness w.r.t. to the denotational semantics. There is, however, a little subtlety with our construction: we cannot formally prove that our semantics indeed encodes the conventional meaning of “cut” (since we do not have other semantics of “cut” to compare with). Nevertheless, we can demonstrate a plausible behavior using the extracted reference interpreter.

7.4 Reference Interpreters

Using the Coq extraction mechanism, we extracted two reference interpreters from our definitions and theorems: one for conventional miniKanren with interleaving search and another one for SLD search with cut. These interpreters can be used to practically investigate the behavior of specifications in unclear, complex, or corner cases. Our experience has shown that these interpreters demonstrate the expected behavior in all cases.

8 Related Work

The study of formal semantics for logic programming languages, particularly Prolog, is a well-established research domain. Early works  [10, 16] addressed the computational aspects of both pure Prolog and its extension with the cut construct. Recently, the application of certified/mechanized approaches came into focus as well. In particular, in one work  [21] the equivalence of a few differently defined semantics for pure Prolog is proven, and in another work  [20] a denotational semantics for Prolog with cut is presented; both works provide Coq-mechanized proofs. It is interesting that the former one also advocates the use of higher-order abstract syntax. We are not aware of any prior work on certified semantics for Prolog which contributed a correct-by-construction interpreter. Our certified description of SLD resolution with cut can be considered as a certified semantics for Prolog modulo occurs check in unification (which Prolog does not have by default).

The implementation of first-order unification in dependently typed languages constitutes a well-known challenge with a number of known solutions. The major difficulty comes from the non-structural recursivity of conventional unification algorithms, which requires to provide a witness for convergence. The standard approach is to define a generally-recursive function and a well-founded order for its arguments. This route is taken in a number of works  [5, 19, 26, 28], where the descriptions of unification algorithms are given in Coq, LCF and Alf. The well-founded used there is lexicographically ordered tuples, containing the information about the number of different free variables and the sizes of the arguments. We implement a similar approach, but we separate the test for the non-matching case into a dedicated function. Thus, we make a recursive call only when the current substitution extension is guaranteed, which allows us to use the number of different free variables as the well-founded order. An alternative approach suggested by McBride  [25] gives a structurally recursive definition of the unification algorithm; this is achieved by indexing the arguments with the numbers of their free variables.

The use of higher-order abstract syntax (HOAS) for dealing with language constructs in Coq was addressed in early work  [11], where it was employed to describe the lambda calculus. The inconsistency phenomenon of HOAS representation, mentioned in Sect. 6, is called there “exotic terms” there and is handled using a dedicated inductive predicate “ ”. The predicate has a non-trivial implementation based on subtle observations on the behavior of bindings. Our case, however, is much simpler: there is not much variety in “exotic terms” (for example, we do not have reductions in terms), and our consistency predicate can be considered as a limited version of “ ” for a more limited language.

The study of formal semantics for miniKanren is not a completely novel venture. Previously, a nondeterministic small-step semantics was described  [24], as well as a big-step semantics for a finite number of answers  [29]; neither uses proof mechanization and in both works the interleaving is not addressed.

The work of Kumar  [22] can be considered as our direct predecessor. It also introduces both denotational and operational semantics and presents a HOL-certified proof for the soundness of the latter w.r.t. the former. The denotational semantics resembles ours but considers only queries with a single free variable (we do not see this restriction as important). On the other hand, the operational semantics is non-deterministic, which makes it impossible to express interleaving and extract the interpreter in a direct way. In addition, a specific form of “executable semantics” is introduced, but its connection to the other two is not established. Finally, no completeness result is presented. We consider our completeness proof as an essential improvement.

The most important property of interleaving search—completeness—was postulated in the introductory paper  [18], and is delivered by all major implementations. Hemann et al.  [15] give a proof of completeness for a specific implementation of miniKanren; however, the completeness is understood there as preservation of all answers during the interleaving of answer streams, i.e. in a more narrow sense than in our work since no relation to denotational semantics is established.

9 Conclusion and Future Work

In this paper, we presented a certified formal semantics for core miniKanren and proved some of its basic properties (including interleaving search completeness, disjunction fairness and commutativity), which are believed to hold in existing implementations. We also derived a semantics for conventional SLD resolution with cut and extracted two certified reference interpreters. We consider our work as the initial setup for the future development of miniKanren semantics.

The language we considered here lacks many important features, which are already introduced and employed in many implementations. Integrating these extensions—in the first hand, disequality constraints,—into the semantics looks a natural direction for future work. We are also going to address the problems of proving some properties of relational programs (equivalence, refutational completeness, etc.).