text:
# First-order Logic as a Constraint Programming Language

## 1 Introduction

By the celebrated result of Turing first-order logic is undecidable. In particular, the question of determining for an interpretation whether a first-order formula is satisfiable and finding a satisfying substitution if it is, is undecidable. Still, for many formulas this question can be answered in a straightforward way. Take for instance the following simple formula interpreted over the standard interpretation for arithmetics:

$$y<zy=1z=2$$
(1)
It is easy to see that it is satisfied by the substitution $`\{y/\mathrm{𝟏},z/\mathrm{𝟐}\}`$. Similarly, it is easy to see that the formula

$$\neg (x=1)x=0$$
(2)
is satisfied by the substitution $`\{x/\mathrm{𝟎}\}`$.

The question is whether we can capture this concept of “straightforwardness” in a natural way. Our first attempt to answer this question was given in Apt and Bezem  by providing a natural operational semantics for first-order logic which is independent of the underlying interpretation for it. It captures the computation process as a search for a satisfying substitution for the formula in question. Because the problem of finding such a substitution is in general undecidable, we introduced in it the possibility of a partial answers in the form of a special $`\mathrm{𝐞𝐫𝐫𝐨𝐫}`$ state indicating a run-time error. In Apt  we slightly extend this approach by explaining how more general equalities can be handled and formulate it in the form of a denotational semantics for first-order logic. Unfortunately, both semantics are too weak to deal properly with formulas (1) and (2): for both of them the $`\mathrm{𝐞𝐫𝐫𝐨𝐫}`$ state is generated.

In this paper we try to overcome these limitations by providing a computational interpretation of first-order logic in the spirit of constraint programming. According to this view the computation process takes place on two levels. At one level we have the usual program execution. At the other level, in the “background” inaccessible to the user, an automatic maintenance of the constraint store takes place. The problem we tackle is undecidable, so we introduce the possibility of partial answers. They are modeled now by a non-empty constraint store or the $`\mathrm{𝐞𝐫𝐫𝐨𝐫}`$ state.

The automatic maintenance of the constraint store is modeled by a parametric *infer* operation that acts on states. The idea of an abstract *infer* operation is due to Jaffar and Maher . Here we consider it in presence of arbitrary first-order formulas. Because of this generality we can obtain various sound realizations of the constraint store management by appropriately instantiating *infer*. The correctness of this approach is formalized in the form of an appropriate soundness result. To establish it we need to assume some properties of the *infer* operation. They are formulated as five “healthiness” conditions.

To illustrate the benefits of this view of first-order logic and to show the scope of the soundness result, we discuss several ways of instantiating the infer parameter to specific constraint management policies. Examples include admission of a constraint store consisting of arbitrary first-order formulas, restriction to a constraint store consisting only of atomic constraints, and restriction to a constraint store consisting only of arbitrary first-order positive formulas. We can also discuss in this framework in a uniform way unification, an algorithm for solving equations and disequations over the Herbrand algebra, and Gaussian elimination in presence of arithmetic constraints.

On the more practical side, these considerations lead to specific implementation proposals of the constraint store in presence of block declarations and conditionals, here modeled, respectively, by means of existential quantification and of negation, conjunction and disjunction.

To clarify these issues we return to formula (1). If we do not admit a constraint store, as in the semantics of  and , its evaluation yields the $`\mathrm{𝐞𝐫𝐫𝐨𝐫}`$ state, since we cannot evaluate $`y<z`$ without knowing the values for $`y`$ and $`z`$. But if we do allow atomic constraints in the store, we can postpone the evaluation of $`y<z`$ and the evaluation yields the substitution $`\{y/\mathrm{𝟏},z/\mathrm{𝟐}\}`$.

Next, let us reconsider formula (2). If only atomic formulas are allowed as constraints, the evaluation of this formula yields the $`\mathrm{𝐞𝐫𝐫𝐨𝐫}`$ state, since we can neither evaluate $`\neg (x=1)`$ nor add this formula to the constraint store. If, however, negated formulas are allowed in the constraint store the substitution $`\{x/\mathrm{𝟎}\}`$ is an answer. The soundness theorem states that each computed substitution satisfies the evaluated formula.

The question of providing an appropriate semantics for first-order logic in the spirit of constraint programming could be approached by taking for a formula $`\varphi (\overline{x})`$ a clause $`p(\overline{x})\varphi (\overline{x})`$, where $`p`$ is a new relational symbol and by applying to it a transformation in the style of Lloyd and Topor . The outcome would be a constraint logic program that uses negation. After clarifying how to deal properly with negation this could yield a rather indirect answer to the question we study. In contrast, our approach, expressed in the form of a denotational semantics, is much more direct and conceptually transparent: the meaning of each formula is expressed directly in terms of the meaning of its constituents and it is parametrized in a simple way by the *infer* operation.

The rest of the paper is organized as follows. In Section 2 we introduce the infer operation and discuss in detail the requirements we impose on it. The main difficulty has to do with the appropriate treatment of existential variables. In Section 3 we define our denotational semantics. Next, in Section 4 we show that the proposed semantics subsumes the denotational semantics provided in . Then in Section 5 we discuss various increasingly powerful forms of constraint store management, each modeled by means of a particular infer operation. Finally, in Section 6 we discuss related work.

## 2 Towards the denotational semantics

Below we work our way towards our proposal for the denotational semantics in several steps, first introducing the basic semantic ingredients, then discussing the crucial conditions on the infer parameter and finally presenting the denotational semantics for first order logic with infer parameter. In the next section we will then state the soundness result for the semantics. The proof details are referred to the appendix. We discuss several ways of instantiating the infer parameter to show the scope of the soundness result. In the final section we review the goals and results and look ahead to further developments.

### Preliminaries

Let’s assume that an algebra $`𝒥`$ is given over which we want to perform computations. The basic ingredient of the semantic universe will be the set of states, states. States come in two kinds. First we have an error state, which remains unanalyzed. All other states consist of two components: one component is a constraint store $`𝒞`$, the other a substitution $`\theta `$. Such a state is then written $`𝒞;\theta `$. As always, a substitution $`\theta `$ is a mapping from variables to terms. It assigns a term $`x\theta `$ to each variable $`x`$, but there are only finitely many variables for which $`xx\theta `$. These variables form $`dom(\theta )`$, the domain of $`\theta `$. The application of a substitution $`\theta `$ to a term $`t`$, written $`t\theta `$, is defined as usual. We denote the empty substitution by $`ϵ`$.

A constraint store $`𝒞`$, is simply a finite set of formulas of first order logic. In many applications there are extra requirements on the syntactic form of a constraint store, but for now we keep things as general as possible. $``$ is a special formula which is always false.

Throughout the paper we try to limit the number of brackets and braces as much as possible. In particular, for a finite set $`\{A_1,\mathrm{},A_n\}`$ we will often write $`A_1,\mathrm{},A_n`$. Also, we write $`\text{infer}𝒞;\theta `$ instead of $`\text{infer}(𝒞;\theta )`$, etc.

### The treatment of local variables: dropping things

An important ingredient of the set up is the $`\mathrm{𝐷𝑅𝑂𝑃}_u`$ mapping on states. It is the way we deal with local variables. This works in two steps: first we define the substitution DROP$`{}_{u}{}^{}(\theta )`$ for each variable $`u`$ and substitution $`\theta `$, as in :

| $`u\mathrm{𝐷𝑅𝑂𝑃}_u(\theta )`$ $`=u`$ |
| --- |
| $`x\mathrm{𝐷𝑅𝑂𝑃}_u(\theta )`$ $`=x\theta `$ for all other variables $`x`$ |

So, $`\mathrm{𝐷𝑅𝑂𝑃}_u`$ makes the current value of $`u`$ disappear, thus capturing the idea of a local variable to the substitutions. But we also have another component in states: the constraint store. Dropping $`u`$ from such a set of formulas compares to existential quantification over $`u`$. There is one little extra point to take care of, however: in a state $`𝒞;\eta `$ the information that $`\eta `$ provides about the value of $`u`$ is implicitly available to $`𝒞`$. Therefore, we perform the quantification $`u`$ only after adding the information about the value of $`u`$ explicitly to $`𝒞`$. Also the values $`y\eta `$ in which $`u`$ appears have to be kept in mind. We take the conjunction of the equations $`y=y\eta `$ for all such variables $`y`$ and write it as $`𝐲=𝐲\eta `$. This leads us to the following formula that takes care of the local variables in $`𝒞`$.

> $`u(u=u\eta 𝐲=𝐲\eta 𝒞)`$

Note that this formula depends both on $`u`$ and $`\eta `$. So, we cannot define a dropu-mapping on constraint stores alone: we have to know $`\eta `$ as well.

This formula expresses the information we are after in a uniform way, but in ‘borderline cases’ the syntactic format is awkward. For example, if $`𝒞=\mathrm{}`$, we get a trivial existential quantification over the first two conjuncts. This existential quantifier is semantically harmless, but specific constraint propagation formalisms simply do not work on existentially quantified formulas. Therefore we rather adopt a format in which the quantifier only appears if it is really necessary.

This is done in two steps: first, the quantification over $`u`$ only matters for the formulas in $`𝒞`$ in which $`u`$ actually occurs. We make this explicit in the definition by distinguishing $`𝒞(u)`$, the subset of $`𝒞`$ that contains exactly the formulas with the free variable $`u`$. In the formula we use for the dropu-mapping we can then always take $`𝒞𝒞(u)`$ outside the scope of the quantifier. This gives:

> $`𝒞𝒞(u),u(u=u\eta 𝐲=𝐲\eta 𝒞(u))`$

Finally, in the special case $`𝒞(u)=\mathrm{}`$, we leave out the existentially quantified formula altogether.

For the error-state we simply set: $`\text{drop}_u\text{error}=\text{error}`$. To summarize, the mapping $`\text{drop}_u`$ is defined on states by the following cases:

| $`\text{drop}_u𝒞;\eta `$ | $`=`$ | $`𝒞;\text{DROP}_u(\eta )`$ | if $`𝒞(u)=\mathrm{}`$ |
| --- | --- | --- | --- |
| $`\text{drop}_u𝒞;\eta `$ | $`=`$ | $`u(u=u\eta 𝐲=𝐲\eta 𝒞(u)),`$ |  |
|  |  | $`𝒞𝒞(u);\text{DROP}_u(\eta )`$ | if $`𝒞(u)\mathrm{}`$ |
| $`\text{drop}_u\text{error}`$ | $`=`$ | error |  |
|  |  |  |  |

### Conditions on infer

Another important ingredient of the framework is the infer mapping. infer maps a state to a set of states. The infer mapping is the basic notion of computation in the semantics: we do not specify what happens ‘within’ the infer mapping. This makes the set up extremely general: the infer steps can consist of calls to a constraint solver, like a unification algorithm or an algorithm for solving linear equations over reals, calls to a constraint propagation algorithm, or other atomic computation steps. Several instances of the infer mapping will be discussed in more detail later on.

We can almost get away with complete generality regarding infer. To make sure that the formalism respects first order logic, we have to make a few modest requirements. Let us write $`𝒞;\theta _𝒥\varphi `$ for $`𝒞\theta _𝒥\varphi \theta `$. In particular $`\mathrm{};\theta _𝒥\varphi `$ iff $`_𝒥\varphi \theta `$. Then the restrictions that we need in the soundness proof below, read as follows:

if $`𝒞^{};\theta ^{}\text{infer}𝒞;\theta `$, then $`𝒞;\theta _𝒥\varphi `$ iff $`𝒞^{};\theta ^{}_𝒥\varphi `$

if $`𝒞^{};\theta ^{}\text{infer}𝒞;\theta `$, then also $`𝒞_v^{};\theta _v^{}\text{infer}𝒞;\theta `$,

where $`𝒞_v^{};\theta _v^{}`$ is obtained from $`𝒞^{};\theta ^{}`$ by replacing all occurrences of $`u`$ by $`v`$ for a variable $`u`$ that is fresh w.r.t. $`𝒞;\theta `$ and a variable $`v`$ that is fresh w.r.t. both $`𝒞;\theta `$ and $`𝒞^{};\theta ^{}`$

if $`\text{infer}𝒞;\theta =\mathrm{}`$, then $`𝒞;\theta _𝒥`$

$`\text{infer}\text{error}=\{\text{error}\}`$

$`\text{infer}\mathrm{};\theta =\{\mathrm{};\theta \}`$

So, the infer mapping should respect logical equivalence, i.e., the state $`𝒞^{};\theta ^{}`$ that we reach starting from $`𝒞;\theta `$, should still make the same formulas true. Furthermore, the infer mapping should not be sensitive to the choice of fresh variables: if infer works for $`u`$, it should also work for an alternative fresh variable $`v`$. Finally, infer should respect falsity and the error state.111The Identity requirement is not necessary for the proof of the soundness theorem, but it seems too natural to leave it out. Renaming is used only in the proof of the Preservation/Persistence Lemma in the case of the existential formula. When we talk about the consistency of states, we are dealing with a three way distinction. We say that a state $`\sigma `$ is: $`𝒥`$-consistent, if $`\sigma \text{error}`$ and $`\sigma \vDash ̸_𝒥`$; $`𝒥`$-inconsistent, if $`\sigma \text{error}`$ and $`\sigma _𝒥`$; error, if $`\sigma =\text{error}`$. For a set of states $`\mathrm{\Sigma }\text{states}`$ we then distinguish: $`\text{cons}_𝒥(\mathrm{\Sigma })`$ $`=\{\sigma \mathrm{\Sigma }:\sigma \text{ is }𝒥\text{-consistent}\}`$ and $`\text{cons}_𝒥^+(\mathrm{\Sigma })`$ $`=\{\sigma \mathrm{\Sigma }:\sigma \text{ is not }𝒥\text{-inconsistent}\}`$. Usually it is clear to which $`𝒥`$ we refer and we omit $`𝒥`$ from the notation.

## 3 Denotational semantics

We now define a denotational semantics for first order logic in which the infer mapping is a parameter. The parameter can be set to give the semantics from Apt , for example, but many other settings are available, as we will see below. This way we obtain general results, that apply uniformly to various forms of constraint store management.

We define the mapping $`[[\varphi ]]:\text{states}\text{states}`$, using postfix notation.222We also sneak in the notation: $`\mathrm{\Sigma }[[\varphi ]]`$ for $`_{\sigma \mathrm{\Sigma }}\{\sigma [[\varphi ]]\}`$.

| $`𝒞;\theta [[A]]`$ | $`=\text{infer}𝒞,A;\theta `$ for an atomic formula $`A`$ |
| --- | --- |
| $`𝒞;\theta [[\varphi _1\varphi _2]]`$ | $`=𝒞;\theta [[\varphi _1]]𝒞;\theta [[\varphi _2]]`$ |
| $`𝒞;\theta [[\varphi _1\varphi _2]]`$ | $`=(𝒞;\theta [[\varphi _1]])[[\varphi _2]]`$ |
| $`𝒞;\theta [[\neg \varphi ]]`$ | $`=\{\begin{array}{cc}\text{infer}𝒞;\theta \hfill & \text{if }\text{ }\text{cons}^+(𝒞;\theta [[\varphi ]])=\mathrm{}\hfill \\ \mathrm{}\hfill & \text{if }𝒞^{};\theta ^{}\text{cons}(𝒞;\theta [[\varphi ]])\text{ }\text{ for}\hfill \\ & \text{some }𝒞^{};\theta ^{}\text{ equivalent to }𝒞;\theta \hfill \\ \text{infer}𝒞,\neg \varphi ;\theta \hfill & \text{otherwise}\hfill \end{array}`$ |
| $`𝒞;\theta [[x\varphi ]]`$ | $`=_\sigma \{\text{infer}\text{drop}_u(\sigma )\}`$ where, for some fresh $`u`$, |
|  | $`\sigma `$ ranges over $`\text{cons}^+(𝒞;\theta [[\varphi \{x/u\}]])`$ |
| $`\text{error}[[\varphi ]]`$ | $`=\{\text{error}\}`$  for all $`\varphi `$ |

The definition relies heavily on the notation that was introduced before. But it is still quite easy to see what goes on. The atomic formulas are handled by means of the infer mapping. Then, disjunction is interpreted as nondeterministic choice, and conjunction as sequential composition. For existential quantification we use the $`\text{drop}_u`$ mapping (for a fresh variable $`u`$). The error clause says that there is no recovery from error. In the case for negation, three contingencies are present: first, the case where $`\varphi `$ is inconsistent. Then we continue with the input state $`𝒞;\theta `$. Secondly, the case where $`\varphi `$ is already true in (a state equivalent to) the input state. Then we conclude that $`\neg \varphi `$ yields inconsistence, i.e., we get $`\mathrm{}`$. Finally, we add $`\neg \varphi `$ to the constraint store $`𝒞`$ if it is impossible at this point to reach a decision about the status of $`\neg \varphi `$.

Next we show that the denotational semantics with the infer parameter is sound. This amounts to two things: 1. successful computations of $`\varphi `$ result in states in which $`\varphi `$ holds; 2. if no successful computation of $`\varphi `$ exists, $`\varphi `$ is false in the initial state.

###### Theorem 3.1 (Soundness)

Let $`𝒞;\theta `$ and $`\varphi `$ be given. Then we have:

1. If $`𝒞^{};\theta ^{}𝒞;\theta [[\varphi ]]`$, then $`𝒞^{};\theta ^{}_𝒥\varphi `$
2. If $`\text{cons}^+(𝒞;\theta [[\varphi ]])=\mathrm{}`$ , then $`𝒞;\theta _𝒥\neg \varphi `$.

The proof of the theorem is by a simultaneous induction on the structure of the formula $`\varphi `$. In the proof we need a preservation/persistence result, that we give as a separate lemma.

###### Lemma 1 (Preservation/Persistence)

1. If $`𝒞;\theta _𝒥\varphi _1`$ and $`𝒞^{};\theta ^{}𝒞;\theta [[\varphi _2]]`$, then $`𝒞^{};\theta ^{}_𝒥\varphi _1`$ (validity)
2. If $`𝒞\theta `$ and $`(\varphi _1\varphi _2)\theta `$ are mutually consistent (in $`𝒥`$) and

$`𝒞^{};\theta ^{}\text{cons}(𝒞;\theta [[\varphi _2]])`$,

then $`𝒞^{}\theta ^{}`$ and $`(\varphi _1\varphi _2)\theta ^{}`$ are mutually consistent (in $`𝒥`$). (consistency)

The lemma says that computations of $`[[\varphi _2]]`$ will not disturb the status of $`[[\varphi _1]]`$: the computation preserves validity and consistency. The proof of the lemma is by a simultaneous induction on the structure of $`\varphi _2`$. Some proof details are given in the appendix. Here we continue by considering several instantiations of the general format.

## 4 Modeling the denotational semantics of Apt

We start our analysis by recalling the semantics provided in . The idea of this semantics is to provide a uniform computational meaning for the first-order formulas independent of the underlying interpretation and without a constraint store. This yields a limited way of processing formulas in the sense that occasionally an error may arise. After we have reintroduced this semantics we shall discuss a number of its extensions, all involving a specific constraint store management. So, let us recall the relevant definitions.

###### Definition 1

Assume a language of terms $`L`$ and an algebra $`𝒥`$ for it.

* Consider a term of $`L`$ in which we replace some of the variables by the elements of the domain $`D`$. We call the resulting object a generalized term.
* Given a generalized term $`t`$ we define its $`𝒥`$-evaluation as follows. Each ground term of $`s`$ of $`L`$ evaluates to a unique value in $`𝒥`$. Given a generalized term $`t`$ replace each maximal ground subterm of $`t`$ by its value in $`𝒥`$. We call the resulting generalized term a $`𝒥`$-term and denote it by $`[[t]]_𝒥`$.
* By a $`𝒥`$-substitution we mean a finite mapping from variables to $`𝒥`$-terms which assigns to each variable $`x`$ in its domain a $`𝒥`$-term different from $`x`$. We write it as $`\{x_1/h_1,\mathrm{},x_n/h_n\}`$. We define the notion of an application of a $`𝒥`$-substitution $`\theta `$ to a generalized term $`t`$ in the standard way and denote it by $`t\theta `$.
* A composition of two $`𝒥`$-substitutions $`\theta `$ and $`\eta `$, written as $`\theta \eta `$, is defined as the unique $`𝒥`$-substitution $`\gamma `$ such that for each variable $`x`$

$$x\gamma =[[(x\theta )\eta ]]_𝒥.$$

The $`𝒥`$-substitutions generalize both the usual substitutions and the valuations, which assign domain values to variables. After these introductory definitions we recall the semantics $`[[]]`$ of an equation between two generalized terms (so a fortiori, between two terms). Here and elsewhere we do not indicate the dependency of the semantics on the underlying interpretation or algebra.

$`\begin{array}{ccc}[[s=t]](\theta )\hfill & :=\hfill & \{\begin{array}{cc}\{\theta \{s\theta /[[t\theta ]]_𝒥\}\}\hfill & \text{if }s\theta \text{ is a variable that does not occur in }t\theta \text{,}\hfill \\ \{\theta \{t\theta /[[s\theta ]]_𝒥\}\}\hfill & \text{if }t\theta \text{ is a variable that does not occur in }s\theta \hfill \\ & \text{and }s\theta \text{ is not a variable,}\hfill \\ \{\theta \}\hfill & \text{if }[[s\theta ]]_𝒥\text{ and }[[t\theta ]]_𝒥\text{ are identical,}\hfill \\ \mathrm{}\hfill & \text{if }s\theta \text{ and }t\theta \text{ are ground and }[[s\theta ]]_𝒥[[t\theta ]]_𝒥\text{,}\hfill \\ \{\text{error}\}\hfill & \text{otherwise.}\hfill \end{array}\hfill \end{array}`$
Consider now an interpretation $``$ based on an algebra $`𝒥`$. Given an atomic formula $`p(t_1,\mathrm{},t_n)`$ different from $`s=t`$ and a $`𝒥`$-substitution $`\theta `$ we denote by $`p_{}`$ the interpretation of $`p`$ in $``$. We say that

* $`p(t_1,\mathrm{},t_n)\theta `$ is true if $`p(t_1,\mathrm{},t_n)\theta `$ is ground and $`([[t_1\theta ]]_𝒥,\mathrm{},[[t_n\theta ]]_𝒥)p_{}`$,
* $`p(t_1,\mathrm{},t_n)\theta `$ is false if $`p(t_1,\mathrm{},t_n)\theta `$ is ground and $`([[t_1\theta ]]_𝒥,\mathrm{},[[t_n\theta ]]_𝒥)p_{}`$.

To deal with the existential quantification we use the $`DROP_x`$ operation defined in Section 2, extended in the standard way to the subsets of $`Subs\{error\}`$. Now $`[[]]`$ is defined by structural induction as follows. $`A`$ is here an atomic formula different from $`s=t`$.

* $`[[A]](\theta ):=\{\begin{array}{cc}\{\theta \}\hfill & \text{if }A\theta \text{ is true,}\hfill \\ \mathrm{}\hfill & \text{if }A\theta \text{ is false,}\hfill \\ \{\text{error}\}\hfill & \text{otherwise, that is if }A\theta \text{ is not ground,}\hfill \end{array}`$
* $`[[\varphi _1\varphi _2]](\theta ):=[[\varphi _2]]([[\varphi _1]](\theta ))`$,
* $`[[\varphi _1\varphi _2]](\theta ):=[[\varphi _1]](\theta )[[\varphi _2]](\theta )`$,
* $`[[\neg \varphi ]](\theta ):=\{\begin{array}{cc}\{\theta \}\hfill & \text{if }[[\varphi ]](\theta )=\mathrm{}\text{,}\hfill \\ \mathrm{}\hfill & \text{if }\theta [[\varphi ]](\theta )\text{,}\hfill \\ \{\text{error}\}\hfill & \text{otherwise,}\hfill \end{array}`$
* $`[[x\varphi ]](\theta ):=DROP_u([[\varphi \{x/u\}]](\theta ))`$, where $`u`$ is a fresh variable.

The following example clarifies the way we interpret atoms and conjunction.

###### Example 1

Assume the standard algebra for the language of arithmetic with the set of integers as domain. We denote its elements by $`\mathrm{},\mathrm{𝟐},\mathrm{𝟏},\mathrm{𝟎},\mathrm{𝟏},\mathrm{𝟐},\mathrm{}`$. Each constant $`i`$ evaluates to the element i. We then have

1. $`[[y=z1z=x+2]](\{x/\mathrm{𝟏}\})=[[z=x+2]](\{x/\mathrm{𝟏},y/z\mathrm{𝟏}\})=`$

$`\{\{x/\mathrm{𝟏},y/\mathrm{𝟐},z/\mathrm{𝟑}\}\},`$
2. $`[[y=1z=1y1=z1]](\epsilon )=\{\{y/\mathrm{𝟏},z/\mathrm{𝟏}\}\},`$
3. $`[[y=1z=2y<z]](\epsilon )=\{\{y/\mathrm{𝟏},z/\mathrm{𝟐}\}\},`$
4. $`[[x=0\neg (x=1)]](\epsilon )=\{\{x/\mathrm{𝟎}\}\},`$
5. $`[[y1=z1y=1z=1]](\epsilon )=\{\text{error}\},`$
6. $`[[y<zy=1z=2]](\epsilon )=\{\text{error}\},`$
7. $`[[\neg (x=1)x=0]](\epsilon )=\{\text{error}\}.`$

So in this semantics the conjunction is not commutative and consequently it is important in which order the formulas are processed. This semantics is a special case of the semantics provided in Section 3. It is obtained by using the following infer relation:

* $`\text{infer}A;\theta :=\{\mathrm{};\eta :\eta [[A]](\theta )\}`$ for an atomic formula $`A`$, where we identify $`\mathrm{};\text{error}`$ with error,
* $`\text{infer}𝒞;\theta :=\{\text{error}\}`$ for all other states $`𝒞;\theta `$.

The relevant ‘embedding’ theorem is the following one.

###### Theorem 4.1 (Embedding)

* $`\eta [[\varphi ]](\theta )`$ iff $`\mathrm{};\eta \mathrm{};\theta [[\varphi ]]`$.
* $`\text{error}[[\varphi ]](\theta )`$ iff $`\text{error}\mathrm{};\eta [[\varphi ]]`$.

## 5 Specific constraint store managements

We now illustrate the generality of our approach by presenting various increasingly powerful forms of constraint store management. Each of them is obtained by a particular propagation step that works on special states and is executed whenever and as-long-as it can be applied. aux is our name for the maximal repetition of the step.333Note that maximal repetition of one step is just one strategy for constraint management. Already Jaffar and Maher  mention other options, distinguishing for example, quick-checking, progressive and ideal CPL systems. Of course, our set up can also accommodate such variations. So, aux is a procedure on special states that is the least fixed point of $`\text{aux}=\text{step}\text{aux}`$. Then we can define the infer mapping as follows:

| $`\text{infer}\mathrm{𝐞𝐫𝐫𝐨𝐫}`$ | $`=\{\mathrm{𝐞𝐫𝐫𝐨𝐫}\}`$ |
| --- | --- |
| $`\text{infer}\mathrm{};\theta `$ | $`=\{\mathrm{};\theta \}`$ |
| $`\text{infer}𝒞;\theta `$ | $`=\text{aux}𝒞;\theta `$ for a special state $`𝒞;\theta `$ |
| $`\text{infer}𝒞;\theta `$ | $`=\{\mathrm{𝐞𝐫𝐫𝐨𝐫}\}`$ otherwise |

Now the examples are obtained by a specification of the special states and the step procedure. In each case it is then straightforward to check that the adopted definition of infer satisfies the conditions we put on it in Section 2. Consequently, in each case the Soundness Theorem holds. Informally, in each case we provide a sound constraint store management.

### Equations as active constraints

Below, following Jaffar and Maher , we make a distinction between *active* and *passive* constraints. In our framework active constraints are the ones that are capable of changing the values of the variables, while the passive ones boil down to formulas that become tests after an appropriate instantiation.

As an example how active constraints can be modeled using the presented semantics consider unification as a way of solving equality constraints. To model it we choose as the underlying algebra the Herbrand algebra, the universe of which consists of the set of all ground terms of the language $`L`$.

The constraint stores of special states only contain equations. The equations are active, and each step consists of unification, whenever possible. So, we put:

$$\text{step}\mathrm{};\theta :=\mathrm{}$$

$$\text{step}𝒞,s=t;\theta :=\{\begin{array}{cc}\{𝒞;\theta \eta \}\hfill & \text{if }\eta \text{ is an mgu of }s\theta \text{ and }t\theta \text{,}\hfill \\ \mathrm{}\hfill & \text{if }s\theta \text{ and }t\theta \text{ are not unifiable.}\hfill \end{array}$$

Other specific forms of active constraints can be modeled in our framework in an equally straightforward way.

### Atoms as passive constraints

The drawback of the semantics defined in the previous section is that it yields $`\mathrm{𝐞𝐫𝐫𝐨𝐫}`$ when a wrong order of conjuncts is accidentally chosen. A possible remedy is to use atoms as passive constraints, i.e., to move the atoms that currently evaluate to $`\mathrm{𝐞𝐫𝐫𝐨𝐫}`$ to the constraint store instead.

For the handling of passive constraints we include a split procedure on special states to isolate the passive constraints: $`\text{split}𝒞;\theta =𝒞_p,𝒞_a;\theta `$, where $`𝒞_p`$ is a list of the constraints that are passive when evaluated by $`\theta `$ and $`𝒞_a`$ is a list of the constraints that are active when evaluated by $`\theta `$. When this is done, we perform a step on the active constraints. Next we re-group the constraints to reconsider the active-passive split in the new state. So, the step we perform in the auxiliary procedure is a composed action: $`\text{aux}=\text{splitstep}\text{splitstep}`$ and $`\text{splitstep}=\text{split}\text{step}`$.444We ignore various implementation details regarding the particular choice of an active constraint and the distinction between lists and sets.

In the current example we set the split procedure as indicated: we regard the atoms that would evaluate to $`\mathrm{𝐞𝐫𝐫𝐨𝐫}`$ passive. Then the step works as follows:

| $`\text{step}𝒞_p;\theta `$ | $`=\{𝒞_p;\theta \}`$ | if no active constraints occur |
| --- | --- | --- |
| $`\text{step}𝒞_p,𝒞_a,s=t;\theta `$ | $`=\{𝒞_p,𝒞_a;\theta \eta \}`$ | if $`\eta `$ is an mgu of $`s\theta ,t\theta `$ |
| $`\text{step}𝒞_p,𝒞_a,s=t;\theta `$ | $`=\mathrm{}`$ | if $`s\theta ,t\theta `$ cannot be unified |
| $`\text{step}𝒞_p,𝒞_a,A;\theta `$ | $`=\{𝒞_p,𝒞_a;\theta \}`$ | if $`A\theta `$ is true |
| $`\text{step}𝒞_p,𝒞_a,A;\theta `$ | $`=\mathrm{}`$ | if $`A\theta `$ is false |

Then the $`\text{splitstep}:=\text{split}\text{step}`$ combines the two actions and aux repeats the splitstep until no more active constraints are left to remove. Reconsider now the formulas from items (5) and (6) of Example 1. We now have

> $`\mathrm{};\epsilon [[y1=z1y=1z=1]]=`$
>
> $`y1=z1;\epsilon [[y=1z=1]]=`$ $`\{\mathrm{};\{y/\mathrm{𝟏},z/\mathrm{𝟏}\}\}`$

and

> $`\mathrm{};\epsilon [[y<zy=1z=2]]=y<z;\epsilon [[y=1z=2]]=`$
>
> $`\{\mathrm{};\{y/\mathrm{𝟏},z/\mathrm{𝟐}\}\}.`$

This shows the difference brought in by this infer procedure. However, in the case of the formula from item (7), we still have

$$\mathrm{};\epsilon [[\neg (x=1)x=0]]=\{\mathrm{𝐞𝐫𝐫𝐨𝐫}\}.$$

### Equations as active and passive constraints

In general, equations can be both active and passive constraints. For example, linear equations over reals can be active and non-linear ones passive. To model computation in their presence we choose as the underlying algebra the standard algebra for the language of arithmetic with the set of real numbers as the domain. The special states are the ones that just have equations in the constraint store. Next, we use a split procedure that regards the linear equations as active and the non-linear ones as passive. Using standard arithmetic operations each linear equation can be rewritten into one of the following forms:

| $``$ | $`0=0`$, |
| --- | --- |
| $``$ | $`r=0`$, where $`r`$ is a non-zero real, and |
| $``$ | $`x=u`$, where $`x\mathrm{𝑉𝑎𝑟}`$ and $`u`$ a linear expression not containing $`x`$. |

This leads to the following definition of the propagation step:

> $`\text{step}𝒞_p,\mathrm{};\theta :=\{𝒞_p;\theta \}`$

> $`\text{step}𝒞_p,𝒞_a,s=t;\theta :=\{\begin{array}{cc}𝒞_p,𝒞_a;\theta \hfill & s\theta =t\theta \text{ rewrites to }0=0\text{,}\hfill \\ \mathrm{}\hfill & s\theta =t\theta \text{ rewrites to }r=0\text{,}\hfill \\ & \text{where }r\text{ is a non-zero real,}\hfill \\ 𝒞_p,𝒞_a;\theta \{x/u\}\hfill & s\theta =t\theta \text{ rewrites to }x=u\text{,}\hfill \end{array}`$

The last clause models in effect the Gaussian elimination step, now in presence of linear and non-linear equations.

### Negative literals as passive constraints

The infer methods introduced above allowed only atoms in the constraint store of special states, that is to say an occurrence of non-atomic formulas in the constraint store leads to an immediate error. Let us extend the infer method to allow for negative literals in the constraint store of special states. Now we can easily modify the definitions from ”Atoms as passive constraints”: we regard states with finite sets of literals as special states and regard the literals that would evaluate to $`\mathrm{𝐞𝐫𝐫𝐨𝐫}`$ as passive. Then the definition of the step is obtained by having a literal $`L`$ instead of an atom $`A`$. Now, in the case of the formula from item (7) of Example 1 we have

> $`\mathrm{};\epsilon [[\neg (x=1)x=0]]=\neg (x=1);\epsilon [[x=0]]=`$
>
> $`\text{step}\neg (x=1);\{x/\mathrm{𝟎}\}=\{\mathrm{};\{x/\mathrm{𝟎}\}\}.`$

### Equality and disequality constraints

We continue the previous example for the case of an arbitrary language of terms together with equality and disequality constraints.555We ignore the notational distinction between the disequation $`st`$ and the negation $`\neg (s=t)`$ for the moment. We adapt the definition by having as active constraints all equations as well as those disequations that are ground or of the form $`t\theta t\theta `$. The split of $`𝒞;\theta `$ now produces $`𝒞_p,𝒞_a;\theta `$ with $`𝒞_p=s_1t_1,\mathrm{},s_nt_n`$, a list of all the disequations $`s_it_i𝒞`$ for which $`(s_it_i)\theta `$ is not ground and not of the form $`tt`$. The definition of the step then is:

| $`\text{step}𝒞_p;\theta `$ | $`=\{𝒞_p;\theta \}`$ | if no active constraints occur |
| --- | --- | --- |
| $`\text{step}𝒞_p,𝒞_a,s=t;\theta `$ | $`=\{𝒞_p,𝒞_a;\theta \eta \}`$ | if $`\eta `$ is an mgu of $`s\theta ,t\theta `$ |
| $`\text{step}𝒞_p,𝒞_a,s=t;\theta `$ | $`=\mathrm{}`$ | if $`s\theta ,t\theta `$ cannot be unified |
| $`\text{step}𝒞_p,𝒞_a,st;\theta `$ | $`=\{𝒞_p,𝒞_a;\theta \}`$ | if $`s\theta t\theta `$ is true |
| $`\text{step}𝒞_p,𝒞_a,st;\theta `$ | $`=\mathrm{}`$ | if $`s\theta t\theta `$ is false |

Then we get, for example

> $`\mathrm{};\epsilon [[f(x)f(y)g(x,b)=g(a,y)]]=`$
>
> $`\text{step}f(x)f(y);\{x/a,y/b\}=\{\mathrm{};\{x/a,y/b\}\}`$.

In general, if no $`\mathrm{𝐞𝐫𝐫𝐨𝐫}`$ occurs, we can expect $`\mathrm{},ϵ[[\varphi ]]`$ to contain special states from which all active constraints are removed, i.e., states of the form $`𝒞;\theta `$ where $`𝒞`$ is a list of inequations $`st`$ such that $`s\theta t\theta `$ is passive. It follows from the independence of inequations of  that over an infinite Herbrand Universe such a constraint store is consistent, i.e., has a grounding solution $`\eta `$. For such an $`\eta `$ we can then conclude: $`s_i\theta t_i\theta `$ (for each $`1in`$) and $`\varphi \theta \eta `$.

The grounding solution $`\eta `$ can not be built up during the computation of $`[[\varphi ]]`$. This is clear from the example $`xyx=c`$. If we make the choice $`\{x/d,x/c\}`$ as a grounding solution for $`xy`$ too soon, we are no longer able to deal with $`x=c`$ later on. Hence we can benefit from the independence of inequations only after the computation of $`[[xyx=c]]`$ has been completed.

### Existential formulas as passive constraints

At this point only literals are allowed in the constraint store. We can easily extend the current store management to one in which also existential formulas are allowed in the constraint store. To this end we need some quantifier elimination procedure elim that is able to deal with at least some form of existential quantification. Then we can have $`\text{step}:=\text{elim}`$.

### Arbitrary formulas as passive constraints

The previous constraint store management can be extended by allowing arbitrary formulas in the constraint store. This makes sense as soon as we have some decision procedure solve that is able to deal with at least some type of negative formulas. Then we can have $`\text{step}:=\text{solve}`$.

## 6 Rationale and Related Work

As clarified in Section 4 the soundness result established here generalizes the appropriate result provided in . The drawback of this semantics was that it yielded error as answer for several clearly satisfiable formulas, like the ones considered in the introduction.

Our interest in a semantics that models constraint management in a sound way stems from our attempts to add constraints to the programming language Alma-0 of Apt et al. . Alma-0 extends imperative programming by features that support declarative programming. This language allows us to interpret the formulas of first-order logic (without universal quantification) as executable programs. In Apt and Schaerf  we proposed to extend Alma-0 by constraints but found that this led to situations in which the customary interpretation of the conditionals by means of the implication is unsound.

Using the above considerations we can provide a simple sound interpretation of the IF B THEN S ELSE T END statement. Namely, it is sufficient to interpret it in logic as $`(BS)(\neg BT)`$, written in the Alma-0 syntax as EITHER B; S ORELSE (NOT B); T END. This interpretation requires that negative literals, here NOT B, are used as passive constraints. On the implementation level backtracking is then needed but the above interpretation can be reduced to the customary implementation of IF B THEN S ELSE T END if the condition B evaluates to true or false irrespectively of the constraint store.

As already mentioned in the introduction the modelling of the constraint store maintenance by means of an abstract infer mechanism is due to Jaffar and Maher . In their framework the computation mechanism of constraint logic programming is modeled, so local variables (modeled by existential variables) and negation are absent but recursion is considered. Additionally, only conjunctions of atomic formulas are allowed as constraints.

In  several semantics for constraint logic programming are compared. In this paper a mapping solv is used that allows for inconsistency checks during the computation. solv can vary with the intended application, just like our infer parameter, but, unlike infer, it cannot model arbitrary constraint propagation steps. In fact, in  the constraint propagation steps take place only at the end of each the computation.

An alternative approach to model the essentials of constraint programming is provided by the concurrent constraint programming (ccp) approach pioneered by Saraswat  and Saraswat, Rinard and Panangaden . In this scheme the programs can also be considered as formulas with the difference that the atomic tell and ask operations are present and that the parallel composition connective is present. The idea captured by this model is that the processes interact by means of a constraint system using the tell and ask operations. The constraint system is a set of constraints equipped with the entailment operation.

The ccp programs can be written in a logical way by dropping the “tell” context around a constraint and by interpreting the ask($`c`$) statement as the implication $`c`$. However, in spite of this logical view of ccp programs it is not clear how to interpret them as first-order formulas with the customary semantics. In Fages, Ruet and Soliman  a logical semantics of ccp programs is given by interpreting them in intuitionistic linear logic. Both the denotational semantics for this language and the correctness (in the assertional style) of ccp programs were considered in a number of papers, see, e.g., de Boer et al.  and de Boer et al. . How to add to this framework in a sound way negation was studied in Palamidessi, de Boer and Pierro . By the nature of this approach the study of the constraint store management captured here by means of the infer mechanism is absent in this framework.

## Acknowledgement

We thank Catuscia Palamidessi for helpful discussion on the subject of ccp programs.

## Appendix: the proofs

In this appendix we give proof details of the Soundness Theorem and Preservation/Persistence Lemma. Both proofs are by simultaneous inductions on the structure of the formula. We focus on the existential quantification cases, which are the most subtle. We use the notation $`_𝒥\varphi [\overline{a}]`$ to indicate the assignment of values $`\overline{a}`$ to (at least) the free variables in $`\varphi `$. In the case of the lemma it will be convenient to standardize this as follows: we are concerned with $`𝒞\theta `$ and $`\varphi _i\theta `$ (for $`i=1,2`$) and denote the values for the free variables shared by the $`\varphi _i\theta `$ by $`\overline{d}`$. Then we use the values $`\overline{c}`$ for the remaining free variables in $`\varphi _1\theta `$ and $`\overline{e}`$ for the remaining free variables in $`\varphi _2\theta `$. Finally, we denote the values of the remaining free variables in $`𝒞\theta `$ by $`\overline{b}`$. So, we will mostly use blocks of the form $`[\overline{b},\overline{c},\overline{d},\overline{e}]`$.

Proof of Preservation/Persistence Lemma 1:

$``$ atoms: In the atomic case $`\varphi _2=A`$ for some atom $`A`$ and $`𝒞^{\prime \prime };\theta ^{\prime \prime }\text{infer}𝒞,A;\theta `$. Straightforward application of property (1) does the trick.

$``$ disjunction: In this case $`\varphi _2=(\psi _1\psi _2)`$ and $`𝒞^{\prime \prime };\theta ^{\prime \prime }𝒞;\theta [[\psi _i]]`$ for some $`i=1,2`$. In this situation the inductive hypotheses apply straightforwardly.

$``$ conjunction: In this case $`\varphi _2=(\psi _1\psi _2)`$ and $`𝒞^{\prime \prime };\theta ^{\prime \prime }𝒞^{};\theta ^{}[[\psi _2]]`$ for some

$`𝒞^{};\theta ^{}𝒞;\theta [[\psi _1]]`$. Now two applications of the inductive hypothesis are required. For preservation of validity this is straightforward. For preservation of consistency it works as follows: by assumption $`_𝒥(𝒞\theta ,(\varphi _1(\psi _1\psi _2))\theta )[\overline{b},\overline{c},\overline{d},\overline{e}]`$. So, $`_𝒥(𝒞\theta ,(\varphi _1\psi _1)\theta )[\overline{b},\overline{c_1},\overline{d_1},\overline{e_1}]`$, restricting the $`\overline{d}`$ and $`\overline{e}`$ to the relevant variables and moving some of the $`\overline{d}`$ values to $`\overline{c_1}`$. By induction hypothesis we get $`_𝒥(𝒞^{}\theta ^{},(\varphi _1\psi _1)\theta ^{})[\overline{b_1^{}},\overline{c_1^{}},\overline{d_1^{}},\overline{e_1^{}}]`$. Next the induction hypothesis (for $`\varphi _1\psi _1`$ and $`\psi _2`$) provides $`_𝒥(𝒞^{\prime \prime }\theta ^{\prime \prime },((\varphi _1\psi _1)\psi _2)\theta ^{\prime \prime })[\overline{b^{\prime \prime }},\overline{c^{\prime \prime }},\overline{d^{\prime \prime }},\overline{e^{\prime \prime }}]`$, as required.

$``$ negation: In this case $`\varphi _2=\neg \psi `$. We have to distinguish cases

* $`\varphi _2`$ is ’true’: $`𝒞^{\prime \prime };\theta ^{\prime \prime }\text{infer}𝒞;\theta `$ (and $`\text{cons}^+(𝒞;\theta [[\psi ]])=\mathrm{}`$. ) Now property (1) gives the results.
* $`\varphi _2`$ is ’false’: in this case $`𝒞;\theta [[\varphi _2]]=\mathrm{}`$ and both (i) and (ii) are void.
* ’otherwise’: we get $`𝒞^{\prime \prime };\theta ^{\prime \prime }\text{infer}𝒞,\neg \psi ;\theta `$. The results follow from first order logic and property (1).

$``$ existential quantification: Now $`\varphi _2=x\psi `$ for some $`x`$, $`\psi `$. So, consider $`\text{infer}\text{drop}_u𝒞^{};\eta `$ for some consistent $`𝒞^{};\eta 𝒞;\theta [[\psi \{x/u\}]]`$ ($`u`$ fresh). By property (1) it suffices to consider $`\text{drop}_u𝒞^{};\eta =`$ $`(𝒞^{}𝒞^{}(u,𝐲)),u(u=u\eta 𝐲=𝐲\eta 𝒞^{}(u,𝐲));\text{DROP}_u(\eta )`$. We call $`\mathrm{𝐷𝑅𝑂𝑃}_{u,𝐲}(\eta )=\theta ^{\prime \prime }`$.

1. By assumption $`𝒞;\theta _𝒥\varphi _1`$. By induction hypothesis $`𝒞^{};\eta _𝒥\varphi _1`$. From this $`(u=u\eta 𝒞^{})\text{DROP}_u(\eta )_𝒥(u=u\eta \varphi _1)\text{DROP}_u(\eta )`$. So, $`(u=u\eta 𝒞^{})\text{DROP}_u(\eta )_𝒥\varphi _1\text{DROP}_u(\eta )`$. Repeating this for the $`𝐲`$, we get $`(u=u\eta 𝐲=𝐲\eta 𝒞^{})\theta ^{\prime \prime }_𝒥\varphi _1\theta ^{\prime \prime }`$. By (2) we may assume that this holds for some $`u`$ that does not occur in $`\varphi _1\theta ^{\prime \prime }`$. Hence the implicit overall universal quantification over $`u`$ can be replaced by an existential quantification over $`u`$ on the left hand side of the sequent. This gives

> $`((𝒞^{}𝒞^{}(u,𝐲))u(u=u\eta 𝐲=𝐲\eta 𝒞^{}(u,𝐲)))\theta ^{\prime \prime }_𝒥\varphi _1\theta ^{\prime \prime }`$.

Now we can safely re-instantiate the values of the variables in y to obtain the same for $`\mathrm{𝐷𝑅𝑂𝑃}_u(\eta )=\theta ^{\prime \prime }\{𝐲/𝐲\eta \}`$

> $`((𝒞^{}𝒞^{}(u,𝐲))u(u=u\eta 𝐲=𝐲\eta 𝒞^{}(u,𝐲)))\text{DROP}_u(\eta )_𝒥\varphi _1\text{DROP}_u(\eta )`$.
2. The assumption gives $`_𝒥(𝒞\theta ,(\varphi _1x\psi ))\theta )[\overline{b},\overline{c},\overline{d},\overline{e}]`$. From the induction hypothesis we obtain $`_𝒥(𝒞^{}\eta ,(\varphi _1\psi \{x/u\})\eta )[\overline{b^{}},\overline{c^{}},\overline{d^{}},\overline{e^{}},f]`$ where $`f`$ is the value of $`u`$. From this we conclude $`_𝒥(𝒞^{}\eta ,(\varphi _1x\psi )\eta )[\overline{b^{}},\overline{c^{}},\overline{d^{}},\overline{e^{}},f]`$. So, we can be sure that suitable values for all the variables in $`𝒞^{}`$ and $`(\varphi _1x\psi )`$ are available, if we use the values in the block $`[\overline{b^{}},\overline{c^{}},\overline{d^{}},\overline{e^{}},f]`$ and the substitution $`\eta `$ as a middle man. But then we can also assign these values directly to the variable $`u`$, eliminating the middle man $`\eta `$. This way we get values $`[\overline{b^{\prime \prime }},\overline{c^{\prime \prime }},\overline{d^{\prime \prime }},\overline{e^{\prime \prime }}]`$ such that $`_𝒥(((𝒞^{}𝒞^{}(u,𝐲))u=u\eta 𝐲=𝐲\eta 𝒞^{}(u,𝐲))\text{DROP}_u(\eta ),`$ $`(\varphi _1x\psi )\text{DROP}_u(\eta ))[\overline{b^{\prime \prime }},\overline{c^{\prime \prime }},\overline{d^{\prime \prime }},\overline{e^{\prime \prime }}]`$. From this the consistency of $`\text{drop}_u𝒞^{};\eta `$ and $`(\varphi _1x\psi )\text{DROP}_u(\eta )`$ is clear. $`\mathrm{}`$

Proof of Soundness Theorem 1:

$``$ atoms: In case $`\varphi `$ is an atomic formula $`A`$, $`𝒞;\theta [[\varphi ]]=\text{infer}𝒞,A;\theta `$. Now straightforward applications of property (1) and (3) give the result.

$``$ disjunction: In case $`\varphi `$ is a disjunction, $`\varphi _1\varphi _2`$ say, $`𝒞;\theta [[\varphi ]]=𝒞;\theta [[\varphi _1]]𝒞;\theta [[\varphi _2]]`$. The induction hypotheses apply immediately.

$``$ conjunction: In case $`\varphi `$ is a conjunction, $`\varphi _1\varphi _2`$ say, $`𝒞^{\prime \prime };\theta ^{\prime \prime }𝒞;\theta [[\varphi ]]`$ iff $`𝒞^{\prime \prime };\theta ^{\prime \prime }𝒞^{};\theta ^{}[[\varphi _2]]`$ for some $`𝒞^{};\theta ^{}𝒞;\theta [[\varphi _1]]`$. Part 1. of the theorem is a straightforward consequence of the induction hypothesis and persistence. For part 2 we add some details. We have: if $`𝒞^{};\theta ^{}𝒞;\theta [[\varphi _1]]`$ is consistent, then $`𝒞^{};\theta ^{}[[\varphi _2]]`$ only contains inconsistent states. From this we may conclude by induction hypothesis that for each $`𝒞^{};\theta ^{}\text{cons}(𝒞;\theta [[\varphi _1]])`$

$$𝒞^{};\theta ^{}_𝒥\neg \varphi _2.$$
(5)
Now assume that for some666Notation for assignment of values as in the lemma. $`[\overline{b},\overline{c},\overline{d},\overline{e}]`$, $`_𝒥(𝒞\theta \varphi _1\theta \varphi _2\theta )[b,c,d,e]`$ and that we have a $`𝒞^{};\theta ^{}\text{cons}(𝒞;\theta [[\varphi _1]])`$. Then persistence (2) tells us that the consistency is preserved, i.e., there are $`[\overline{b^{}},\overline{c^{}},\overline{d^{}},\overline{e^{}}]`$ such that $`_𝒥(𝒞^{}\theta ^{}\varphi _1\theta ^{}\varphi _2\theta ^{})[\overline{b^{}},\overline{c^{}},\overline{d^{}},\overline{e^{}}]`$. But this contradicts the statement (5). So, for no $`[\overline{b},\overline{c},\overline{d},\overline{e}]`$, $`_𝒥(𝒞\theta \varphi _1\theta \varphi _2\theta )[\overline{b},\overline{c},\overline{d},\overline{e}]`$, which is as required.

$``$ negation: In case of a negation $`\neg \varphi `$, there are three situations to consider

* $`𝒞^{};\theta ^{}\text{infer}𝒞;\theta `$ and $`\text{cons}^+(𝒞;\theta [[\varphi ]])=\mathrm{}`$. Now case (1) of the theorem follows from the induction hypothesis for case (2) and equivalence condition (1). Case (2) follows from conditions (1) and (3).
* $`𝒞;\theta [[\neg \varphi ]]=\mathrm{}`$ and there is some $`𝒞^{};\theta ^{}\text{cons}(𝒞;\theta [[\varphi ]])`$, which is equivalent to $`𝒞;\theta `$. Now case (1) is satisfied trivially and case (2) follows from the induction hypothesis for (1) and condition (1) on infer.
* $`𝒞;\theta [[\neg \varphi ]]=\text{infer}𝒞,\neg \varphi ;\theta `$. Let $`𝒞^{};\theta ^{}\text{infer}𝒞,\neg \varphi ;\theta `$ be given. Now case (1) follows from condition (1) and case two relies on conditions (1) and (3).

$``$ existential quantification: In case of an existential quantification $`x\varphi `$, we have to consider $`𝒞^{\prime \prime };\theta ^{\prime \prime }\text{infer}\text{drop}_u𝒞^{};\eta `$, for $`𝒞^{};\eta \text{cons}(𝒞;\theta [[\varphi \{x/u\}]])`$ (some fresh $`u`$). Call $`\text{DROP}_{u,𝐲}(\eta )=\theta ^{}`$. Below we use a crucial fact about first order logic: if $`x`$ is not free in $`\chi `$, then $`x(\psi \chi )((x\psi )\chi )`$.

1. By induction hypothesis $`𝒞^{};\eta _𝒥\varphi \{x/u\}`$. By first order logic

$`(𝒞^{}𝒞^{}(u,𝐲))\eta _𝒥(𝒞^{}(u,𝐲)\varphi \{x/u\})\eta `$. From this we conclude that $`(𝒞^{}𝒞^{}(u,𝐲))\eta _𝒥(𝒞^{}(u,𝐲)x\varphi )\eta `$. $`(𝒞^{}𝒞^{}(u,𝐲))`$ does not contain $`u`$ or $`𝐲`$, so: $`(𝒞^{}𝒞^{}(u,𝐲))\theta ^{}_𝒥(𝒞^{}(u,𝐲)u=u\eta 𝐲=𝐲\eta x\varphi )\theta ^{}`$. As $`u`$ does not occur in $`(x\varphi )\theta ^{}`$, we can apply the crucial fact to get

$`(𝒞^{}𝒞^{}(u,𝐲))\theta ^{}u(𝒞^{}(u,𝐲)u=u\eta 𝐲=𝐲\eta )\theta ^{}_𝒥(x\varphi )\theta ^{}`$. Now we can make $`\theta ^{}`$ more specific by re-instantiating the values $`𝐲\eta `$ for the variables in $`𝐲`$. This suffices (by (1)).
2. In this case there is no fresh $`u`$ which produces a $`𝒞^{};\eta \text{cons}(𝒞;\theta [[\varphi \{x/u\}]])`$. The induction hypothesis then gives $`𝒞;\theta _𝒥(\neg \varphi \{x/u\})`$ (for all fresh $`u`$), from which $`𝒞;\theta _𝒥(x\varphi )`$ (as $`u`$ is fresh w.r.t. $`\theta `$). $`\mathrm{}`$


format: text

text:
# 𝑍𝛼-expansion for self-energy radiative corrections to parity nonconservation in atoms

## A

The calculations performed use the following algebraic relations

$`\gamma _5=0,\gamma _\mu \gamma _5=a_\mu ,\gamma _\mu \gamma _\nu \gamma _5=(p_\mu a_\nu p_\nu a_\mu ),`$ (A1)
$`\gamma _\mu \gamma _\nu \gamma _\lambda \gamma _5=(a_\mu g_{\nu \lambda }a_\nu g_{\mu \lambda }+a_\lambda g_{\mu \nu })iϵ_{\mu \nu \lambda \rho }a^\rho ,`$ (A2)
where the $`X\mathrm{T}r(X\mathrm{})`$, and conventional integrals

$`{\displaystyle \frac{d^4q}{(q^2+2qsM^2)^n}}`$ $`=`$ $`{\displaystyle \frac{(1)^ni\pi ^2c_n}{(M^2+s^2)^{n2}}},n>2,`$ (A3)
$`{\displaystyle \frac{q^\mu d^4q}{(q^2+2qsM^2)^n}}`$ $`=`$ $`{\displaystyle \frac{(1)^{n1}i\pi ^2c_ns^\mu }{(M^2+s^2)^{n2}}},n>2,`$ (A4)
$`{\displaystyle \frac{q^\mu q^\nu d^4q}{(q^2+2qsM^2)^3}}`$ $`=`$ $`{\displaystyle \frac{i\pi ^2}{2}}\left[{\displaystyle \frac{s^\mu s^\nu }{M^2+s^2}}{\displaystyle \frac{1}{2}}g^{\mu \nu }\left(\mathrm{ln}{\displaystyle \frac{\mathrm{\Lambda }^2}{M^2+s^2}}{\displaystyle \frac{3}{2}}\right)\right],`$ (A5)
$`{\displaystyle \frac{q^\mu q^\nu q^\lambda d^4q}{(q^2+2qsM^2)^n}}`$ $`=`$ $`{\displaystyle \frac{(1)^ni\pi ^2c_n}{(M^2+s^2)^{n3}}}\left[{\displaystyle \frac{s^\mu s^\nu s^\lambda }{M^2+s^2}}+{\displaystyle \frac{g^{\mu \nu }s^\lambda +g^{\mu \lambda }s^\nu +g^{\nu \lambda }s^\mu }{2(n3)}}\right],n>3,`$ (A6)
where $`c_n=1/[(n1)(n2)]`$, $`M`$ is a scalar, $`s`$ is a four-vector, $`qs(qs)`$, and $`\mathrm{\Lambda }`$ is the ultraviolet cut-off.


text:
# Pattern formation in colloidal mixtures under external driving fields

## 1 Introduction

When brought into nonequilibrium, physical systems may spontaneously exhibit many different kinds of pattern formation (for recent reviews see Refs. ) which are much richer than the traditional phase transitions in equilibrium systems. While the latter are by now well-understood by microscopic theories and simulations , full microscopic theories operating on a particle-resolved level for nonequilibrium situations still represent a major challenge. In this paper we study a “microscopic” system designed to model binary colloidal suspensions in an external field which is an off-lattice version  of a diffusive system in an external driving field. Colloidal dispersions indeed represent excellent model systems which can be brought into nonequilibrium  via external fields in a controlled way  and can be studied experimentally with a real-space resolution of an interparticle distance . Another complementary realization of a driven diffusive off-lattice systems is pedestrian motion in pedestrian zones .

In our model, we consider an equimolar binary mixture of so-called $`A`$ and $`B`$ particles. The particles are identical as far as their mutual interaction is concerned which we model via a Yukawa pair potential having charged colloidal dispersions in mind. The $`A`$ and $`B`$ particles, however, respond differently to the external field applied: $`A`$ particles feel an external force $`\stackrel{}{F}^{(A)}`$ while $`B`$-particles are driven by a different force $`\stackrel{}{F}^{(B)}`$. Completely overdamped Brownian dynamics (with hydrodynamic interactions neglected) are assumed  for the colloidal motion. The case of parallel forces where $`\stackrel{}{F}^{(A)}=\stackrel{}{F}^{(B)}`$ was investigated recently by computer simulation by us and G. Hoffmann  via nonequilibrium Brownian dynamics computer simulations in the case where the field-free thermodynamic equilibrium state was a mixed fluid. As a result, above a critical strength of the external force, the system exhibits a transition towards lane formation. The lanes comprise bundles of particles of the same kind ($`A`$ or $`B`$) and are parallel to the driving field. This nonequilibrium phase separation results from a slip-stream effect caused or transported by the interparticle interactions. The critical force can be theoretically estimated by setting the external force to a typical interaction force resulting from a pairwise potential $`V(r)`$ between the particles. Experimental evidence for such an instability has been accumulated in sedimentation dynamics of bidisperse suspensions .

In this paper, we generalize the set-up previously studied in Ref.  into the following two directions: First, we study the case where the two external forces $`\stackrel{}{F}^{(A)}`$ and $`\stackrel{}{F}^{(B)}`$ are not parallel. Second, we study - for parallel forces - the case where the equilibrium field-free state is crystalline. For non-parallel forces, lane formation does also occur. The direction of the lanes, however, is tilted with respect to the driving fields. In more details lanes are directed along the difference vector $`\stackrel{}{F}^{(B)}\stackrel{}{F}^{(A)}`$ of the two external forces. For a randomly occupied crystal, on the other hand, a two-stage transition shows up: first, above a threshold, the external fields melts the solid mechanically. Upon increasing the external field strength further, a reentrant freezing transition is discovered. The resulting crystalline structure involves completely demixed $`A`$\- and $`B`$ solids sliding against each other similar to the fluid lane formation.

The paper is organized as follows: In section 2, we define the model used and describe briefly our simulation technique. Results for non-parallel external forces are presented in section 3. The solid-fluid-solid reentrant behavior is discussed in section 4. Conclusion are given in section 5. In particular, we discuss a possible verification of our predictions in experiments.

## 2 The model

In our model , we consider a symmetric binary colloidal mixture comprising $`2N`$ Brownian colloidal particles in $`d=2`$ spatial dimensions. Half of them are particles of type $`A`$, the other half is of type $`B`$ with partial number densities $`\rho _A=\rho _B=\rho /2`$. The colloidal suspension is held at fixed temperature $`T`$ via the bath of microscopic solvent particles. Two colloidal particles are interacting via an effective Yukawa pair potential

$$V(r)=V_0\sigma \mathrm{exp}\left[\kappa (r\sigma )/\sigma \right]/r,$$
(1)
where $`r`$ is the center-to-center separation, $`V_0`$ is an energy scale and $`\sigma `$ is the particle diameter as a length scale. This is a valid model for charge-stabilized suspensions confined to two dimensions .

The dynamics of the colloids is overdamped Brownian motion. The friction constant $`\xi =3\pi \eta \sigma `$ (with $`\eta `$ denoting the shear viscosity of the solvent) is assumed to be the same for both $`A`$ and $`B`$ particles. The constant external force acting on the $`i`$th particle, $`\stackrel{}{F}_i`$, is different for the both constituents of the binary mixture. It is $`\stackrel{}{F}_i=\stackrel{}{F}^{(A)}`$ for $`A`$ particles and $`\stackrel{}{F}_i=\stackrel{}{F}^{(B)}`$ for $`B`$ particles.

The stochastic Langevin equations for the colloidal trajectories $`\stackrel{}{r}_i(t)`$ $`(i=1,\mathrm{},2N)`$ read as

$$\xi \frac{d\stackrel{}{r}_i}{dt}=\stackrel{}{}_{\stackrel{}{r}_i}\underset{ji}{}V(\stackrel{}{r}_i\stackrel{}{r}_j)+\stackrel{}{F}_i+\stackrel{}{F}_i^{(\mathrm{R})}(t).$$
(2)
The right-hand-side includes all forces acting onto the colloidal particles, namely the force resulting from inter-particle interactions, the external constant force, and the random forces $`\stackrel{}{F}_i^{(\mathrm{R})}`$ describing the collisions of the solvent molecules with the $`i`$th colloidal particle. The latter are Gaussian random numbers with zero mean, $`\overline{\stackrel{}{F}_i^{(\mathrm{R})}}=0`$, and variance

$$\overline{(\stackrel{}{F}_i^{(\mathrm{R})})_\alpha (t)(\stackrel{}{F}_j^{(\mathrm{R})})_\beta (t^{})}=2k_BT\xi \delta _{\alpha \beta }\delta _{ij}\delta (tt^{}).$$
(3)
The subscripts $`\alpha `$ and $`\beta `$ stand for the two Cartesian components and $`k_BT`$ is the thermal energy. In the absence of an external field, the model reduces to a two-dimensional Brownian Yukawa fluid in equilibrium which has been extensively investigated as far as structural and dynamical equilibrium correlations and freezing transitions are concerned .

We solve the Langevin equations of motion by Brownian dynamics simulations  using a finite time-step and the technique of Ermak . We observed the system running into a steady-state after a transient relaxation. We put $`N=250`$ $`A`$ and $`N=250`$ $`B`$ particles into a square cell of length $`\mathrm{}`$ with periodic boundary conditions. The total colloidal number density is $`\rho =2N/\mathrm{}^2`$. The typical size of the time-step was $`0.003\tau _\mathrm{B}`$, where $`\tau _B=\xi \sigma ^2/V_0`$ is a suitable Brownian timescale. We simulated typically $`2\times 10^4`$ time steps which corresponds to a simulation time of $`60\tau _B`$. After an initial relaxation period of $`20\tau _B`$, statistics was gathered in the steady state.

## 3 Non-parallel external forces

### 3.1 General argument for tilted lane formation

Let us first recapitulate what is know for parallel external forces $`\stackrel{}{F}^{(A)}`$ and $`\stackrel{}{F}^{(B)}`$: in Ref. , it was shown that lane formation occurs involving either $`A`$ or $`B`$ particles which are sliding against each other in the field direction. In the lane involving $`A`$ particles only, all these particle are drifting with an global velocity $`\stackrel{}{F}^{(A)}/\xi `$ while opposite regions which involve $`B`$ particles are streaming with the overall velocity $`\stackrel{}{F}^{(B)}/\xi `$. By subtracting the overall velocity using a Galilei transformation one readily sees that within the completely separated lanes, equilibrium Boltzmann statistics is realized. The system just separates into two different equilibrium states which are drifting relative to each other. Physically, the formation of lanes is generated by collisions of $`A`$ against $`B`$ particles pushed by the external force which dynamically separates $`A`$ and $`B`$ particles until completely demixed lanes are formed. A similar lane formation for sheared granular matter was found via molecular dynamics simulation in . The formation of lanes is a sharp first-order non-equilibrium phase transition occurring if the external field difference $`|\stackrel{}{F}^{(A)}\stackrel{}{F}^{(B)}|`$ exceeds a critical value. A Galilei transformation also proves that only the relative velocity of $`A`$ and $`B`$ regions is relevant. Hence, without loss of generality, it is sufficient to study the special case $`\stackrel{}{F}^{(A)}=\stackrel{}{F}^{(B)}`$.

For non-parallel external forces, the collisions between $`A`$ and $`B`$ particles are not any longer central and the phase separated structure will be different, in general. In order to get insight into the location of an interface between two completely demixed regions involving $`A`$ and $`B`$ particles only, we first do a simple continuum argument: consider a (one-dimensional) interface between an $`A`$ and $`B`$ region with a direction described by a two-dimensional vector $`\stackrel{}{d}`$, see Fig. 1. The full interface position can be parameterized by a set of vectors

$`\stackrel{}{r}(s)=\stackrel{}{R}_0+s\stackrel{}{d},`$ (4)
where $`s`$ is a real parameter and $`\stackrel{}{R}_0`$ is a vector describing a point on the interface. After a time $`\mathrm{\Delta }t`$, the $`A`$ particles have moved on average a distance $`\stackrel{}{F}^{(A)}\mathrm{\Delta }t/\xi `$, while the $`B`$ particles have been displaced by a distance $`\stackrel{}{F}^{(B)}\mathrm{\Delta }t/\xi `$. Neglecting any collisions, the $`A`$ particles near the interface will move towards a new interface which is described by the set of vectors

$`\stackrel{}{r}^{(A)}(s)=\stackrel{}{R}_0+s\stackrel{}{d}+\stackrel{}{F}^{(A)}\mathrm{\Delta }t/\xi ,`$ (5)
while the $`B`$ particles near the interface will drift to

$`\stackrel{}{r}^{(B)}(s^{})=\stackrel{}{R}_0+s^{}\stackrel{}{d}+\stackrel{}{F}^{(B)}\mathrm{\Delta }t/\xi `$ (6)
with another real parameter $`s^{}`$. The interface can only be stable if these two interfaces coincide. In case they do not, there is either empty space which will be filled by neighboring particles or $`A`$ and $`B`$ particles will collide which will destroy the interface as well. Hence, the stability criterion is that for any $`s`$ there is an $`s^{}`$ such that $`\stackrel{}{r}^{(A)}(s)=\stackrel{}{r}^{(B)}(s^{})`$ which simply yields the condition

$`\stackrel{}{d}={\displaystyle \frac{\mathrm{\Delta }t}{\xi (ss^{})}}[\stackrel{}{F}^{(B)}\stackrel{}{F}^{(A)}].`$ (7)
This implies that for an interface to be stable, its direction has to be collinear with the force difference

$`\mathrm{\Delta }\stackrel{}{F}=\stackrel{}{F}^{(B)}\stackrel{}{F}^{(A)}.`$ (8)
Hence, the angle $`\alpha `$ describing the interface orientation (see Fig. 1) is

$`\alpha =\mathrm{arcsin}{\displaystyle \frac{\mathrm{\Delta }\stackrel{}{F}\stackrel{}{F}^{(B)}}{|\mathrm{\Delta }\stackrel{}{F}||\stackrel{}{F}^{(B)}|}}.`$ (9)
Clearly, contrarily to the case of parallel forces, the interface position will move in space. The interface velocity $`v_I`$ normal to its position can be calculated as

$`v_I={\displaystyle \frac{|\stackrel{}{F}^{(A)}\times \stackrel{}{F}^{(B)}|}{\xi |\mathrm{\Delta }\stackrel{}{F}|}}.`$ (10)
Obviously, the same argument can be repeated with exchanged roles of $`A`$ and $`B`$ showing that stable parallel lanes with the direction $`\mathrm{\Delta }\stackrel{}{F}`$ are expected with move with the interface velocity $`v_I`$ given by Eq. (10). Furthermore, the same argument applied for a small $`\mathrm{\Delta }t`$ shows that a curved interface is unstable such that a stable interface has to be straight.

Let us finally discuss two special cases: first returning to parallel forces, indeed the interface direction is parallel to the field direction, the angle $`\alpha `$ is $`\pi /2`$, and the interface velocity vanishes as follows directly from Eq. (10). Second the case of perpendicular forces deserves some particular attention. Here the angle $`\alpha `$ is

$`\alpha =\mathrm{arctan}{\displaystyle \frac{|\stackrel{}{F}^{(B)}|}{|\stackrel{}{F}^{(A)}|}}`$ (11)
and the interface velocity can be expressed as

$`v_I={\displaystyle \frac{|\stackrel{}{F}^{(A)}||\stackrel{}{F}^{(B)}|}{\xi |\mathrm{\Delta }\stackrel{}{F}|}}.`$ (12)
Obviously, this general argument is only a necessary condition for a stable $`AB`$ interface. An alternative is a mixed situation with no interface at all driven by entropy. In analogy to the parallel case we anticipate that a critical strength of $`\mathrm{\Delta }\stackrel{}{F}`$ is needed to build stable lanes. This will now be investigated by computer simulation and simple theory in more detail.

### 3.2 Computer simulation results

In our simulation we assume - without loss of generality - the direction of $`\stackrel{}{F}^{(B)}`$ along the $`y`$ axis of the simulation box. The model parameters are fixed to $`\rho \sigma ^2=1.0`$, $`\kappa =4.0`$, and $`V_0=2.5k_BT`$. Simulation snapshots for different external field strengths are shown in Fig. 2(a)-(d).

In Fig. 2(a), no field is applied and a homogeneous completely mixed state is visible. In Fig. 2(b), on the other hand, the external forces are parallel: $`\stackrel{}{F}^{(A)}=\stackrel{}{F}^{(B)}`$. The magnitude $`|\stackrel{}{F}^{(A)}\stackrel{}{F}^{(B)}|`$ is beyond the critical strength  such that lane formation parallel to the field shows up. Nonparallel forces with perpendicular directions are investigated in Figs. 2 (c) and (d). One observes formation of tilted lanes which are indeed in the direction of the force difference vector as expected from our general argument. In following the configurations as a function of time we verified the simple formula of the interface velocity $`v_I`$ as given in Eq. (10).

In a next step, we study perpendicular forces keeping their ratio $`q=|\stackrel{}{F}^{(A)}|/|\stackrel{}{F}^{(B)}|`$ fixed but increasing their magnitude. For small forces the system stays demixed. In increasing the strength of both fields, we have calculated suitable order parameters which are sensitive to tilted lane formation. These are immediate generalizations of those used in Ref. . The order parameter exhibits a sharp jump indicating the critical field strength of the force difference vector upon which tilted lane formation is achieved. There is a clear hysteresis loop if the force is reduced again such that the non-equilibrium phase transition towards tilted lane formation is of first order. The critical value $`\mathrm{\Delta }F_c`$ of the force difference $`|\mathrm{\Delta }\stackrel{}{F}|`$ is shown versus the ratio $`q=|\stackrel{}{F}^{(A)}|/|\stackrel{}{F}^{(B)}|`$ in Fig. 3. We shall compare these data to a simple theoretical prediction in the next subsection.

A careful remark is in order for small positive $`q`$. The periodic boundary conditions used in the simulation corresponds to a toroidal topology shown in Fig. 4. If $`q`$ is getting small the boundary conditions enforce a multiple winding around the torus such that finite size effects are expected to be significant. Therefore we have not shown simulation data for small $`q`$ in Fig. 2.

### 3.3 Theory

We are aiming at a rough theoretical estimation of the boundaries of the demixing transition with constant external fields $`\stackrel{}{F}^{(A)}`$ and $`\stackrel{}{F}^{(B)}`$. This was already put forward in Ref.  for parallel forces and is generalized here to the general case of non-parallel forces.

Consider first a central collision between an $`A`$ and $`B`$ particle pair, see Fig. 5. Transforming the trajectories onto one with a fixed common center of mass of the two particles, one realizes that the collision is effectively driven by half of the force difference, $`\frac{1}{2}(\stackrel{}{F}^{(A)}\stackrel{}{F}^{(B)})=\frac{1}{2}\mathrm{\Delta }\stackrel{}{F}`$ for $`A`$ particles and $`\frac{1}{2}(\stackrel{}{F}^{(B)}\stackrel{}{F}^{(A)})=\frac{1}{2}\mathrm{\Delta }\stackrel{}{F}`$ for $`B`$ particles. A transition towards patterned lanes is expected if $`|\mathrm{\Delta }\stackrel{}{F}|/2`$ is larger than a typical average force between $`A`$ and $`B`$ particles, and lane formation is induced. The latter force depends both on density and on the external fields themselves. We estimate a typical average force between two opposite particles by considering different “effective” interparticle spacings. The first typical interparticle spacing is set by the density alone, $`a=\rho ^{1/2}`$. Including fluctuations in the interparticle distance induced by a finite temperature results in a further smaller effective average distance $`\stackrel{~}{a}`$ as obtained by setting a typical interparticle energy equal to $`V(a)+k_BT`$. Hence $`\stackrel{~}{a}=V^1\left[V(a)+k_BT\right]`$ where $`V^1`$ is the inverse function of the interaction potential $`V(r)`$. Finally the presence of the external fields enforces an even smaller averaged distance $`a^{}`$ between two colliding opposite particles.

We estimate this minimum distance $`a^{}`$ by adding the net force per colliding particle $`\mathrm{\Delta }F/2`$ to the force at distance $`\stackrel{~}{a}`$ via

$`a^{}=F^1\left[\mathrm{\Delta }F/2+F(\stackrel{~}{a})\right],`$ (13)
where $`F^1`$ is the inverse function of $`F(r)=\frac{d}{dr}V(r)`$. In general, an $`AB`$ particle pair will not collide directly along $`\mathrm{\Delta }\stackrel{}{F}/2`$ such that the actual average distance is between $`a^{}`$ and $`\stackrel{~}{a}`$. Hence the averaged force $`\overline{f}`$ between an $`A`$ and a $`B`$ particle is roughly

$`\overline{f}={\displaystyle \frac{1}{\stackrel{~}{a}a^{}}}[V(a^{})V(\stackrel{~}{a})].`$ (14)
The critical force difference $`\mathrm{\Delta }F_\mathrm{c}`$ is reached when it becomes of the order of the mean force $`\overline{f}`$,

$`\mathrm{\Delta }F_\mathrm{c}=2\lambda \overline{f}.`$ (15)
$`\lambda =2`$ is a dimensionless prefactor which is determined by an optimal fit to all simulation results for parallel forces .

The basic prediction of this simple theory is that the only essential parameter governing tilted lane formation is the magnitude $`|\mathrm{\Delta }\stackrel{}{F}|`$. This prediction can be tested by simulation. In fact, in Fig. 3, the critical value of $`|\mathrm{\Delta }\stackrel{}{F}|`$ is shown for different ratios $`q=|\stackrel{}{F}^{(A)}|/|\stackrel{}{F}^{(B)}|`$. Were the theory correct, all the simulation data should fall on a horizontal line independent of $`q`$. As can be deduced from Fig. 3, this is indeed confirmed. Furthermore, the actual magnitude predicted from the theory is in line with the simulation data. Note that - as far as the non-parallel case is concerned - there is no fit parameter involved. The global fit parameter $`\lambda `$ is solely adjusted to the case of parallel forces.

### 3.4 Three-dimensional model

The model and all methods and arguments can readily be generalized to three spatial dimensions. Similar conclusions hold for the formation of tilted lanes. We have also performed computer simulations in a cubic box in three dimensions and observed tilted lane formation. Results are presented in Fig. 6: tilted lane formation is clearly visible in the plane spanned by the two forces $`\stackrel{}{F}^{(A)}`$ and $`\stackrel{}{F}^{(B)}`$, see Fig. 6 (a). Perpendicular to the direction $`\mathrm{\Delta }\stackrel{}{F}`$ of the lanes, the system shows a structure reminiscent of two-dimensional spinodal decomposition, see Fig. 6 (b). The parameters are for these snapshots $`\kappa =4.0`$, $`V_0=2.5k_BT`$ and $`\rho \sigma ^3=1`$. In conclusion, this shows that pattern formation is a general effect which is independent of the dimensionality of the model.

## 4 Reentrant freezing for a driven Brownian crystal

In this section we focus on a Brownian crystal which is driven by an external field. To this end, the external fields acting onto $`A`$ and $`B`$ particles are parallel ($`\stackrel{}{F}^{(A)}=\stackrel{}{F}^{(B)}=f\stackrel{}{e}_y`$) but in contrast to Ref.  the field-free equilibrium initial state is a triangular crystal. The case of a fluid field-free configuration is easier as rotational symmetry with respect to the direction of the external field applied is ensured. This is no longer true for a crystal where one has to specify the field direction with respect to the crystalline orientation resulting in an anisotropy which reflects the crystalline symmetry. Clearly, in the absence of any external field, $`A`$ and $`B`$ particles are indistinguishable; hence the equilibrium state is randomly occupied triangular crystal. In the other limit of very strong fields, one expects again phase separation into completely demixed $`A`$ and $`B`$ regions. Once they are demixed, they follow Boltzmann statistics. Consequently the equilibrium state is a pure $`A`$ (or $`B`$) crystal of the same lattice than the original (field free) one. What is less clear intuitively is how the system transforms from the first randomly occupied crystal into the demixed crystal if the field is turned continuously on. At least two scenarios are conceivable: either the system retains the underlying solid lattice but particle exchange hopping processes generated by the external field demix the crystalline state or the crystal first melts mechanically via the external field and then crystallizes again. In our simulations we almost exclusively observed the latter scenario.

In order to detect a triangular crystalline order we define a suitable crystallinity order parameter $`\mathrm{\Psi }_6`$ that probes sixfold symmetry around a given particle via

$`\mathrm{\Psi }_6=\left|{\displaystyle \frac{1}{12N}}{\displaystyle \underset{j=1}{\overset{2N}{}}}{\displaystyle \underset{<k>}{}}e^{6\mathrm{i}\varphi _{jk}}\right|.`$ (16)
Here the $`k`$-sum includes the six nearest neighbors of the given particle and the $`j`$-sum extends over $`2N`$ particles in the simulation box. The large angular brackets indicate a time average. $`\varphi _{jk}`$ is the polar angle of the interparticle distance vector with respect to a fixed reference frame. For ideal sixfold symmetry, i.e., for a perfect triangular crystal, $`\mathrm{\Psi }_6=1`$. Thermal fluctuations cause deviations from this ideal case but a value of $`\mathrm{\Psi }_6>0.8`$  is conveniently taken to be conclusive evidence for a triangular crystal.

In Fig. 7 we plot $`\mathrm{\Psi }_6`$ versus the difference external force $`f^{}=|\stackrel{}{F}^{(B)}|\sigma /k_BT`$ for fixed parameters $`\kappa =4.0,V_0=15.0k_BT`$, and $`\rho \sigma ^2=1`$.

The direction of the force is (11)-direction of the triangular crystal. Note that in contrast to the parameters used in section 3, the interactions energy is much larger to ensure that the equilibrium field-free state is crystalline. Indeed the crystallinity order parameter in the field-free case is around $`\mathrm{\Psi }_6=0.87`$. Upon increasing the external field strength to $`f^{}10`$, the crystallinity order parameter sharply drops down and stays to values close to zero indicating a melting of the crystal induced by the external field. This melting process is mainly caused by a mechanical stress induced by the external field with respect to $`AB`$ particle pairs. As the field is getting larger ($`f^{}200`$), the order parameter $`\mathrm{\Psi }_6`$ increases again to values close to 0.7. This is accompanied with lane formation as indicated by a drastic increase of another order parameter $`\varphi `$ defined in Ref.  which is sensitive to lane formation. The whole scenario is illustrated also by simulation snapshots shown in Fig. 8. While Fig. 8 (a) corresponds to a field-free randomly mixed crystal, Fig. 8 (b) and (c) are in the molten state while Fig. 8 (d) represents a refrozen demixed crystal sliding against each other. In Fig. 8 (b) and (c) worm like structures along the fields occur as a precursor to lanes formed by solids. Consequently we have shown evidence for a reentrant freezing behavior generated by external fields in non-equilibrium. A qualitative similar situation occurs for colloidal solids in linear shear flow . A continuous increase of the shear rate can lead to shear-melting and subsequent recrystallization into a different solid structure . A similar effect is shear thinning and subsequent shear thickening as observed in colloidal fluids for increasing shear rates .

## 5 Conclusions

To summarize: we have generalized earlier studies of non-equilibrium pattern formation in continuum driven diffusive mixtures to non-parallel external fields and crystalline states. As main results we found tilted lanes along the force difference vector which are wandering with a constant interface velocity provided the external force difference is large enough. Furthermore, a solid melts and refreezes if the magnitude of an external field is increased.

Let us remark on possibilities of non-equilibrium lane formation in more complicated systems: first, our system studied was completely symmetric involving the same partial densities and the same particle-particle interactions. For experimental realizations  this will not be fulfilled in general. However, the basic physics of lane formation will not change. Secondly, if ternary and further multicomponent mixture beyond binary ones are considered, we expect cascades of lane formation transitions involving the different particles species as the external field is increased.

We finally comment on possible experimental realizations of our model: There are different fields where the pattern formation we predicted within our model can be verified, namely in colloidal dynamics and in pedestrian motion. Binary colloidal mixtures indeed can be driven by constant external forces. Important examples for parallel forces are sedimentation where the external force is gravity  or electrokinetic motion of charged colloids  where the external force is an electric field. Both the fluid and crystalline field-free state can be studied. A recent realization with mixed crystals can be found in . One possible drawback is the hydrodynamic backflow  caused by strong hydrodynamic interactions  which were neglected in our model. An overall backflow can be avoided by a time dependent oscillatory field (e.g. AC electric field) which leads qualitatively to the same lane formation if its frequency is small enough . We further think that the long-ranged hydrodynamic flow around a driven colloidal particle will favor lane formation, i.e. the critical field strength needed to generate lane formation is expected to be lower than with hydrodynamic interactions neglected. Colloids can also be exposed to external laser-optical and magnetic filed  which generate external forces in a controlled way coupling to the dielectricity (resp. the magnetic permeability) of the colloidal material. Nonparallel external forces in colloidal mixtures can be realized by crossing two external fields e.g. gravity with electric, laser-optical with electric, laser-optical with magnetic etc. The two species of a colloidal mixture will in general respond differently to the two external fields such that the resulting total external force will be different in direction.

A different realization is dynamics of pedestrians in pedestrian zones and in lecture halls. Similar off-lattice models involving Brownian particles have been used to simulate the collective behavior of pedestrians  including escape panic . Our setup of perpendicular external fields is realized by two crossing pedestrian lanes in which pedestrians are only moving in one direction. Based on our results, we would expect tilted lane formation provided the density of the pedestrians is high enough. Finally it would be interesting to extend phenomenological hydrodynamical theories which predict lane formation for parallel forces via an instability  to the case of tilted forces. Work along these lines is in progress.

## Acknowledgments

It is with great pleasure that we dedicate this paper to J. P. Hansen on the occasion of his 60th birthday. We thank T. Palberg, J. Chakrabarti, J. Sherwood, V. Popkov and E. Allahyarov for helpful remarks. Financial support from the DFG (Sonderforschungsbereich 237) is gratefully acknowledged.

## References