text:
# The (Lazy) Functional Side of Logic Programming

## 1 Introduction

The possibility of translating logic programs into functional ones has long been a subject of investigation. Among the different proposals \[Mar94, Mar95, GW92, RKS98, Red84, vR97\]. Such systems are usually devised for one of the following purposes: for proving program properties, for providing better insight on the relation between functional and logic languages, or – to a minor extent – for improving program performance.

Common to all the approaches mentioned is that the original logic program, in order to be translated, needs to be *well-moded* and this has led to the common understanding that these programs can be considered to be the “functional part” of logic programs. This is confirmed by the following statement in \[Mar95\]: “$`\mathrm{}`$ the class of functionally moded (well-moded and simply moded) programs can be rightly considered *the* functional core of logic programs”.

Well-moded programs have, among other features, a straightforward left-to-right dataflow model (see \[AE93, AM94\]) and prohibit the use of *logical variables* to their full potential such as in complex logical data structures like difference-lists. As a consequence of this it is now widely accepted that “complex” logical variables, the possibility of a dynamic selection rule, and general properties of non-well-moded programs are exclusive features of logic programs.

This is not quite right. At least, not to the extent that one is brought to think.

In this paper we show, among other things, that logical structures such as difference lists have a natural counterpart in *lazy* functional programs; i.e. that most programs using difference-lists are functional in nature. This shows immediately that many common non-well-moded programs are functional in nature and that well-modedness is thus not a necessary attribute of those logic programs behaving functionally. We do this by employing a straightforward – literal – translation of moded logic programs into Haskell, a lazy functional language.

Furthermore, we use the same translation system to show that some programs requiring a dynamic scheduling mechanism are also intrinsically functional.

Summarizing, in this paper we readdress the old question of what features are exclusive to the logic programming paradigm and demonstrate that the current circumscription is unreasonably restrictive.

## 2 Preliminaries

Due to space constraints we omit preliminaries and assume that the reader is acquainted with the terminology and the main results of logic programming theory (see \[Apt90, Llo87\]). In this paper we use over-lined characters to indicate (a possibly empty) sequence of objects, so $`\overline{t}`$ can denote a sequence $`t_1,\mathrm{},t_n`$ of terms, $`\overline{x}`$ a sequence of variables and $`\overline{𝙰}`$ a sequence of atoms (i.e. a query). To avoid confusion with built-in symbols, we use $``$ to indicate syntactic equivalence.

In what follows we study logic programs executed by means of the LD-resolution, which consists of the SLD-resolution combined with the leftmost selection rule. An SLD-derivation in which the leftmost selection rule is used is called an LD-derivation.

### 2.1 Modes for Logic Programs

This section is partially borrowed from \[AE93\], we refer to the appendix and to \[AM94\] for further information over well-moded logic programs.

###### Definition 2.1

Consider an $`n`$-ary relation symbol $`𝚙`$. By a *mode* for $`𝚙`$ we mean a function $`𝚖_𝚙`$ from $`\{1,\mathrm{},n\}`$ to the set $`\{\mathrm{𝙸𝚗},\mathrm{𝙾𝚞𝚝}\}`$. If $`𝚖_𝚙(𝚒)=\text{In}`$, we call $`i`$ an *input position* of $`p`$ and if $`𝚖_𝚙(𝚒)=\text{Out}`$, we call $`i`$ an *output position* of $`𝚙`$ (both w.r.t. $`𝚖_𝚙`$). $`\mathrm{}`$

An $`n`$-ary relation $`𝚙`$ with a mode $`𝚖_𝚙`$ will be denoted by $`𝚙(𝚖_𝚙(\mathrm{𝟷}),\mathrm{},𝚖_𝚙(𝚗)).`$ For example, for programs member and append we typically have the following listings and modes:

| mode member(In, In). |
| --- |
| member(El, \[El|\_\]). |
| member(El, \[\_|Rest\]) $``$member(El, Rest). |
| mode append(In, In, Out). |
| append(\[ \], \_, \[ \]). |
| append(\[H|Tail\], List, \[H|Tail’\]) $``$append(Tail, List, Tail’). |

Modes indicate how the arguments of a relation should be used. We assume that to each relation symbol is associated a unique mode. Multiple modes can be obtained by simply renaming the relations.

In presence of modes, we require the programs and the queries to be somehow naturally *consistent* wrt them. Before we introduce the notion of consistency we have to provide some further notation. When writing an atom as $`𝚙(\overline{𝚞},\overline{𝚟})`$ we now assume that $`\overline{𝚞}`$ is a sequence of terms filling in the input positions of $`𝚙`$ and $`\overline{𝚟}`$ is a sequence of terms filling in the output positions. Thus, for notational simplicity, we assume that the input positions come first.

Let us call *producing* the input position of the head and the output positions of the body atoms, and *consuming* the other positions of a clause, we have the following definition

###### Definition 2.2 (Consistent)

A clause (query) is *consistent* iff every variable occurs in at least one producing position. $`\mathrm{}`$

The last LP notion we need is the one of *plain* program. Here and in the sequel, a set of terms is called *linear* if every variable occurs at most once in it. In other words, a sat of terms is linear iff no variable has two distinct occurrences in any of the terms and no two terms have a variable in common.

###### Definition 2.3 (Plain)

A clause $`𝚙_\mathrm{𝟶}(\overline{𝚜}_\mathrm{𝟶},\overline{𝚝}_{𝚗+\mathrm{𝟷}})𝚙_\mathrm{𝟷}(\overline{𝚜}_\mathrm{𝟷},\overline{𝚝}_\mathrm{𝟷}),\mathrm{},𝚙_𝚗(\overline{𝚜}_𝚗,\overline{𝚝}_𝚗)`$ is called *plain* if

1. $`\overline{𝚝}_1,\mathrm{},\overline{𝚝}_n`$ is a linear family of variables;
2. $`\overline{𝚜}_0`$ is linear.

A query $`\overline{𝚀}`$ is called *plain* iff the clause $`𝚚\overline{𝚀}`$ is, where q is any (dummy) atom of zero arity.

A program is called *plain* if every clause of it is. $`\mathrm{}`$

Thus a plain program is a program in which producing positions are filled in by variables and in which a variable occurs in at most one producing position.

Condition (i) is similar to, though less restrictive, than the one of simply moded programs as defined in \[AE93\] (as we do not impose an ordering constraint).

Our translation requires programs to be consistent and plain. This is far less restrictive than well-modedness plus simple-modedness, and as we shall see allows us to capture a broader segment of functional behaviour found in logic programs. Indeed, it is now perhaps *too* lenient, but suffices for the goals of this paper to broaden the characterization of logic programs. Regarding the (non) restrictiveness of the concepts of plain and consistent programs, we have the following:

###### Remark 2.4

It is important to realize that most programs are plain111this assertion is substantiated by the fact that most programs are simply moded, as shown by “mini-survey” at the end of \[AE93\]., and that non plain programs can naturally be transformed into equivalent plain ones, virtually all consistent programs are either plain or safely translatable into a plain form. This is also practically demonstrated by the fact that the language Mercury employs a pre-processing phase in which all programs are translated into a *superheterogeneous* form (which is very similar to the form of plain programs). Concerning (ii), we can always transform a consistent program $`𝙿`$ into an equivalent consistent program $`𝙿^{}`$ which satisfies it. For instance, for the member program defined above, we can transform its first clause into member(El, \[Head|Rest\]) $``$El == Head. It is also worth noticing that append is already input-linear. $`\mathrm{}`$

### 2.2 Haskell Programs

Our translation system maps logic programs into lazy functional programs, which are written in (a subset of) Haskell \[HPW92\]. The subset we use includes the proposed extension of *pattern guards* \[Pey97\], which we describe below.

The programs we are going to generate are built as sets of *equations*, each of the following form:

| f s1 $`\mathrm{}`$ sj | $`|`$ guard1,1, $`\mathrm{}`$, guard1,j | = result1 |
| --- | --- | --- |
|  | $`\mathrm{}`$ |
|  | $`|`$ guardn,1, $`\mathrm{}`$, guardn,m | = resultn,1 |
|  | $`|`$ otherwise | = resultn+1 |

where f is a function symbol, s1 $`\mathrm{}`$ sj are *parameters* and $`\mathrm{𝗀𝗎𝖺𝗋𝖽}_{𝗑,𝗒},\mathrm{𝗈𝗍𝗁𝖾𝗋𝗐𝗂𝗌𝖾}`$ are *guard qualifiers*. The ‘$`|`$’ introduces a guard, and the ‘,’ acts as a logical conjunctive. Pattern matching may take place on the parameters. Without pattern guards, the guard qualifiers would have to be boolean expressions; that is, we would only return $`\mathrm{𝗋𝖾𝗌𝗎𝗅𝗍}_\mathrm{𝟣}`$ if the associated guards $`\mathrm{𝗀𝗎𝖺𝗋𝖽}_{\mathrm{𝟣},\mathrm{𝟣}}\mathrm{}\mathrm{𝗀𝗎𝖺𝗋𝖽}_{\mathrm{𝟣},𝗃}`$ all evaluate to true. The semantics of Haskell dictates that definitions and guards are tried in sequential order.

The situation with pattern guards is somewhat different. In fact, *patterns guards* can also contain *let-expressions* (which are defined as usual) and *pattern-matching expressions* which are expressions of the form pattern $``$term, and whose semantics is the following: if term matches with pattern then the variables in pattern are appropriately instantiated, and the pattern-matching guard returns true, otherwise it return false. Consider:

| f z | $`|`$ let x = g z |
| --- | --- |
|  | , \[y\] $``$x |
|  | , y $``$ 10 | = (True,1) |
|  | $`|`$ otherwise | = (False,0) |

Here, the tuple (True,1) will only be returned if the two qualifiers in the first guard succeed. That is, 1) the argument x can be pattern matched to a list of one element (denoted by \[y\], which also binds y to this element), and 2) the boolean condition y $``$ 10 is true. In all this, the value of $`𝗑`$ is determined by $`𝗀𝗓`$. If any of these fail, then the second guard is tried. In this case, the special guard otherwise will be tried, which always succeeds. A let qualifier can also be introduce recursive bindings; this will become clear in the sequel. A more detailed example is presented in Appendix B.

As explained below, we need to capture the fact that a predicate might succeed (possibly returning a computed answer substitution), or fail. To do so, we introduce a new datatype $`\mathrm{𝖱𝖾𝗌𝗎𝗅𝗍}`$ in our Haskell programs by:

| data Result $`\alpha `$ = Suc $`\alpha `$ $`|`$ Fail |  |
| --- | --- |

That is, the datatype $`\mathrm{𝖱𝖾𝗌𝗎𝗅𝗍}`$ has two constructors, $`\mathrm{𝖥𝖺𝗂𝗅}`$ and $`\mathrm{𝖲𝗎𝖼}`$, the latter of which can be applied to some term.

Note that the Haskell programs which we generate are not the obvious programs that a functional programmer would write – this is not the intention. They do, however, do what the logic programmer intended. All of the programs given in this paper can be compiled by any Haskell compiler supporting pattern guards.

We also want to mention that despite the fact that pattern guards are an important feature of our translation, we could do without them – at the price of less elegant translation. A Haskell compiler will usually regard these as syntactic sugar anyway, and compile them into more basic primitives already found in Haskell. This implies that all the statements we are going to give in the sequel are true regardless of the availability of a pattern guard construct in the target language.

## 3 A Translation System

In logic programming, queries can succeed, loop or fail. This third possibility is of crucial importance, since it is often used as a control mechanism. As an example, one can consider the following programming scheme:

Where test verifies that the value produced by generate is appropriate, and failure and backtracking take care of the ill-formed terms. Another common scheme is the following one:

| p(X) $``$test\_a, X = 1. |
| --- |
| p(X) $``$test\_b, X = 2. |

Where test\_a and test\_b model a typical case statement, and the selection of the right branch is done via the failure and backtracking mechanism.

Nevertheless, relations which are “not supposed to fail” are quite common in logic programming. We say that a relation is “not supposed to fail” if – when called in a “correct” way – produces at least one answer. Examples of such relations are sort, flatten and append, (this latter, for calls of the form $`\mathrm{𝚊𝚙𝚙𝚎𝚗𝚍}(𝚕_\mathrm{𝟷},𝚕_\mathrm{𝟸},𝚇)`$, where $`𝚕_\mathrm{𝟷}`$ and $`𝚕_\mathrm{𝟸}`$ are lists, and $`𝚇`$ is a new variable will always produce one answer).

The ubiquity of predicates which are not supposed to fail is confirmed by the fact that Mercury requires the programmer to specify for each relation symbol, whether it might fail or not. This information is then used to generate optimized code.

We do the same thing for our translation, and from now on we assume that the set of predicate symbols is partitioned into two disjoint sets, namely

predicates, which, when called, are expected to produce at least one answer (such as append), and

predicates, which when called are allowed to report no answer, i.e., to fail immediately or succeed (such as member and $`<`$).

Thus, we have the following definition.

###### Definition 3.1

A *partitioning* is a map from the set of predicate symbols into the set $`\{\text{test},\text{non-test}\}`$.

Let $`𝙿`$ be a program and $`𝒬`$ be a set of queries, we say that $`𝙿`$ is *correct* wrt. $`𝒬`$ iff for every $`\overline{𝙰}𝒬`$ every, time that a non-test atom $`𝙱`$ is selected in a LD-derivation of $`\overline{𝙰}`$ in $`𝙿`$ then $`𝙱`$ has at least one successful LD-derivation. $`\mathrm{}`$

Thus every program is correct wrt. the trivial partitioning in which all predicates are *test*. Checking correctness is orthogonal to the purposes of this paper, but we should mention that it can be done either using abstract interpretation \[DLGH97\] or on modes and types \[PR97\]; also Mercury employs a system based on modes and types in order to check that the programs are consistent (modulo non-termination) wrt. the partitioning provided by the programmer.

The partition into test and non-test predicates exposes the implicit failure mechanism present in logic programs. Our translation will transform non-test predicates as ordinary functions, but transform test predicates by returning something of the type Result$`\alpha `$, allowing us to indicate failure. Essentially if a function fails in the logic programming sense, then a value of $`\mathrm{𝖥𝖺𝗂𝗅}`$ will be returned. Each “value” returned from a test predicate is only every used in a function if it is successfully matched against $`\mathrm{𝖲𝗎𝖼𝖼}𝖺`$ indicating that no failure occurred(it was not $`\mathrm{𝖥𝖺𝗂𝗅}`$). The combination of plain programs with a partition makes it easy to identify the logic programs that can be mapped to functions, and which functions to enhance by mimicking the implicit failure mechanism. Now, let $`𝚙`$ be a predicate symbol with mode

$$𝚙(\stackrel{i}{\stackrel{}{\mathrm{𝙸𝚗},\mathrm{},\mathrm{𝙸𝚗}}},\stackrel{j}{\stackrel{}{\mathrm{𝙾𝚞𝚝},\mathrm{},\mathrm{𝙾𝚞𝚝}}})$$

Then $`𝚙`$ can naturally be translated into a function of type

$$\begin{array}{cc}𝗉:𝖳_\mathrm{𝟣}\times \mathrm{}\times 𝖳_𝗂(𝖲_\mathrm{𝟣}\times \mathrm{}\times 𝖲_𝗃)\hfill & \text{if }𝚙\text{ is a }\text{non-test}\text{ predicate}\hfill \\ 𝗉:𝖳_\mathrm{𝟣}\times \mathrm{}\times 𝖳_𝗂\mathrm{𝖱𝖾𝗌𝗎𝗅𝗍}(𝖲_\mathrm{𝟣}\times \mathrm{}\times 𝖲_𝗃)\hfill & \text{if }𝚙\text{ is a }\text{test}\text{ predicate}\hfill \end{array}$$

Where $`𝖳_𝗂`$ and $`𝖲_𝗂`$ are appropriate Haskell types. Here we will not bother further with the type that the translated predicate has: the Haskell compiler will be able to infer it autonomously; what it is important to see is that the Haskell counterpart of p is a function which maps a tuple with $`i`$ elements into a tuple containing $`j`$ elements, possibly embedded in the $`\mathrm{𝖱𝖾𝗍𝗎𝗋𝗇}`$ datatype depending on whether p is a non-test predicate or not. We shall employ the value $`\mathrm{𝖥𝖺𝗂𝗅}`$ to denote the functional counterpart of failure222Confusingly, if a test predicate returns no values then we will return $`\mathrm{𝖲𝗎𝖼}()`$, where $`()`$ looks like an empty tuple but which is in actual fact the only element in the unit type..

### 3.1 The Translation

Our translation method requires the program to be translated to be *consistent* and *plain*. Of these conditions, *consistency* is the only crucial one, in fact as stated in Remark 2.4 it is (virtually) always possible to transform a consistent program into an equivalent program which is plain; moreover, most programs are plain already.

Now, we can transform the logic program into a Haskell one via a simple syntactic transformation. First, we have to translate variables, terms and predicate symbols; this is done in a straightforward way: one just has to respect the syntactic conventions of the two languages (uppercase and lowercases, and built-in predicates). Of course, predicate symbols are transformed into non-constructor function symbols. In the sequel we use sans-serif characters for Haskell constructs and typewriter font for logic programming ones, for instance, $`𝗍,𝗌`$ denote the Haskell counterpart of the LP terms $`𝚝,𝚜`$.

###### Definition 3.2 (Translation)

Let $`𝙿`$ be a logic program, and
$`\begin{array}{cccccccc}𝚙(\overline{𝚝}_\mathrm{𝟷},\overline{𝚜}_\mathrm{𝟷})\hfill & & 𝚙_{\mathrm{𝟷},\mathrm{𝟷}}(\overline{𝚒}_{\mathrm{𝟷},\mathrm{𝟷}},\overline{𝚘}_{\mathrm{𝟷},\mathrm{𝟷}}),\mathrm{},𝚙_{\mathrm{𝟷},𝚔_\mathrm{𝟷}}(\overline{𝚒}_{\mathrm{𝟷},𝚔_\mathrm{𝟷}},\overline{𝚘}_{\mathrm{𝟷},𝚔_\mathrm{𝟷}}),𝚚_{\mathrm{𝟷},\mathrm{𝟷}}(\overline{𝚞}_{\mathrm{𝟷},\mathrm{𝟷}},\overline{𝚟}_{\mathrm{𝟷},\mathrm{𝟷}}),\mathrm{},𝚚_{\mathrm{𝟷},𝚕_\mathrm{𝟷}}(\overline{𝚞}_{\mathrm{𝟷},𝚕_\mathrm{𝟷}},\overline{𝚟}_{\mathrm{𝟷},𝚕_\mathrm{𝟷}}).& & & & & \\ & \mathrm{}& & & & & & \\ 𝚙(\overline{𝚝}_𝚗,\overline{𝚜}_𝚗)\hfill & & 𝚙_{𝚗,\mathrm{𝟷}}(\overline{𝚒}_{𝚗,\mathrm{𝟷}},\overline{𝚘}_{𝚗,\mathrm{𝟷}}),\mathrm{},𝚙_{𝚗,𝚔_𝚗}(\overline{𝚒}_{𝚗,𝚔_𝚗},\overline{𝚘}_{𝚗,𝚔_𝚗}),𝚚_{𝚗,\mathrm{𝟷}}(\overline{𝚞}_{𝚗,\mathrm{𝟷}},\overline{𝚟}_{𝚗,\mathrm{𝟷}}),\mathrm{},𝚚_{𝚗,𝚕_𝚗}(\overline{𝚞}_{𝚗,𝚕_𝚗},\overline{𝚟}_{𝚗,𝚕_𝚗}).& & & & & \end{array}`$
be the set of clauses of $`𝙿`$ defining predicate p, where the predicates $`𝚙_{𝚒,𝚓}`$ are test predicates and the predicates $`𝚚_{𝚒,𝚓}`$ are the non-test ones. Here we assume that the clauses had been renamed apart, i.e., that they share no variables.

* If $`𝚙`$ is a *test* predicate, then the *translation* of the above section into Haskell is the following script (for the moment the underlined parts have to be treated as if the underline wasn’t there):

| p ($`\overline{𝗑}`$) | $`|`$ | ($`\overline{𝗍}`$1) $``$($`\overline{𝗑}`$), |
| --- | --- | --- |
|  |  | Suc ($`\overline{𝗈}`$1,1) $``$p1,1($`\overline{𝗂}`$1,1), |
|  |  | $`\mathrm{}`$ |
|  |  | Suc($`\overline{𝗈}`$$`_{1,k_1}`$) $``$p$`_{1,k_1}`$($`\overline{𝗂}`$$`_{1,k_1}`$), |
|  |  | let ($`\overline{𝗏}`$1,1) = q1,1($`\overline{𝗎}`$1,1), |
|  |  | $`\mathrm{}`$ |
|  |  | let ($`\overline{𝗏}`$$`_{1,l_1}`$) = q$`_{1,l_1}`$($`\overline{𝗎}`$$`_{1,l_1}`$) |  |
|  |  |  | = Suc($`\overline{𝗌}`$1) |
|  | $`|`$ | ($`\overline{𝗍}`$2) $``$($`\overline{𝗑}`$), |
|  |  | $`\mathrm{}`$ |
|  |  |  | = Suc($`\overline{𝗌}`$2) |
|  | $`\mathrm{}`$ |
|  | $`|`$ otherwise = Fail |

If one of the clauses of the above section is a unit clause, (i.e. $`𝚙(\overline{𝚝},\overline{𝚜}_𝚓).`$) or if its body contains no test predicates then the corresponding line has the trivial guard True.

Note that sequences may be empty, so if the predicate had no output positions, then $`\overline{𝗌}`$ would be the term $`()`$.
* If $`𝚙`$ is a *non-test* predicate, then translation of the above section corresponds to the above script *after removal* of the underlined parts; namely we have to eliminate from it the otherwise statement and the Suc’s from the return values. $`\mathrm{}`$

Clearly, list constructions and built-in predicates need to be handled separately, in particular, a test predicate of the form $`\overline{𝚝}==\overline{𝚜}`$ will be transformed to the term which returns either $`\mathrm{𝖲𝗎𝖼}()`$ on success and $`\mathrm{𝖥𝖺𝗂𝗅}`$ on failure. We will abuse the notation and also call this function $`==`$.

###### Example 3.3

Let us now consider the program append. It is already plain, so, assuming append to be non-test predicate, its translation is:

| append (x1,x2) | $`|`$ | (\[ \], list) $``$(x1, x2) |
| --- | --- | --- |
|  |  |  | = list |
|  | $`|`$ | ((x:xs), list) $``$(x1, x2) |
|  | , | let tail’ = append (xs, list) |
|  |  |  | = x:tail’ |

Notice that nothing prohibits us from declaring append as a *test* predicate, if we do so we, the result of the translation is:

| append (x1,x2) | $`|`$ | (\[ \], list) $``$(x1, x2) |
| --- | --- | --- |
|  |  |  | = Suc list |
|  | $`|`$ | ((x:xs), list) $``$(x1, x2) |
|  | , | Suc tail’ $``$append (xs, list) |
|  |  |  | = Suc (x:tail’) |
|  | $`|`$ | otherwise = Fail |

In practice, the first program is more efficient than the second one (though, this can differ per compiler), and it is more lazy than the second one. This is further explained in the following *aside*.

###### Remark 3.4

The adopted partitioning has a natural influence on the strictness of the resulting Haskell code. Consider the differences in the above translations of append: if append is declared as non-test then its translation will contain a let-expression in the guard

let tail’ = append (xs, list) (1)

while if it is declared as test then, in its place, we will find the guard

Suc tail’ $``$append (xs, list) (2)

Now, while (1) is a let expression whose bound expression will only be invoked if (and to the extent that) the value of tail’ is demanded, the second is a guard, which has to be satisfied in order for the function it appears in to return a value. Indeed, in (2) the term append (xs,list) will always be reduced until it is completely computed, i.e. until it either reaches either “success” or “failure”. In this sense (2) is strict, while (1) is lazy.

This behaviour is quite natural if one considers the following: since test atoms might fail, we cannot trust their partial answers until we have computed whether they’ll succeed or not. This implies that they always have to be fully “computed”, therefore forcing a strict computation. On the other hand non-test predicates are guaranteed to eventually succeed, so their computation might be stopped at the moment that we have reached a partial result which is “sufficient for our purposes”. Therefore the non-test predicates naturally fit the lazy model of computation. $`\mathrm{}`$

## 4 Logic Programs in a Lazy Functional Language

We are at last in a position to demonstrate our thesis that the set of logic programs considered as functional needs to be expanded. As issues, we consider logic variables, dynamic scheduling and backtracking in turn.

The dynamics of some of the programs we are going to present in this section is unavoidably rather complex, we apologize for the inconvenience and ask the reader to resort to patience and understanding.

### 4.1 Logical Variables vs. Lazy Evaluation

*Logical variables* are one of the peculiarities of logic programming. Most of the time, they are used in a standard way, that is just as variables in an imperative language – this is the case for instance when the program is well-moded. Nevertheless there are many important situations in which logical variables are exploited in all their power. A typical such case is in the presence of *difference structures* such as *difference lists*.

Here we show that even when used in a truly “logical” way, logical variables are in many cases not an exclusive feature of logic programs.

The following Polish Flag Problem example (incidentally, a simplified version of Dijkstra’s Dutch Flag Problem), reads as follows: given a list of objects which are either red or white, rearrange it in such a way that the red elements appear first and the white ones appear after them. The following program is inspired by \[O’K90, page 117\], we have replaced “$``$” by “,”, thus splitting a position filled in by a difference-list into two positions. Because of this change in some relations, additional arguments are introduced.

| polish(InList, RedWhites) $``$ |
| --- |
|  | distribute(InList, RedWhites, Whites, Whites,\[ \]). |
| distribute(\[ \], Reds, Reds, Whites, Whites). |
| distribute(\[X|Xs\], \[X|Reds0\], Reds, Whites0, Whites) $``$red(X), |
|  | distribute(Xs, Reds0, Reds, Whites0, Whites). |
| distribute(\[X|Xs\], Reds0, Reds, \[X|Whites0\], Whites) $``$white(X), |
|  | distribute(Xs, Reds0, Reds, Whites0, Whites). |
| mode polish(In, Out): non-test. |
| mode distribute(In, Out, In, Out, In): non-test. |

Where we assume that predicates red and white are appropriately defined elsewhere in the program and have mode red(In): test. This program is plain and consistent, and by translating it we obtain

| polish inlist | $`|`$ | t $``$inlist, |
| --- | --- | --- |
|  |  | let (redwhites, whites) = distribute(t, whites, \[ \]) |
|  |  |  | = redwhites |
| distribute(is, rstail, wstail) | $`|`$ | (\[ \],rs,ws) $``$(is,rstail,wstail) |
|  |  | = (rs, ws) |
|  | $`|`$ | (x:xs,rs,ws) $``$(is,rstail,wstail) |
|  | , | let (rshead, wshead) = distribute(xs, rs, ws) |
|  | , | Suc () $``$red x |
|  |  |  | = (x:rshead, wshead) |
|  | $`|`$ | (x:xs,rs,ws) $``$(is,rstail,wstail) |
|  | , | let (rshead, wshead) = distribute(xs, rs, ws) |
|  | , | Suc () $``$white x |
|  |  |  | = (rshead, x:wshead) |

Where red and white are again defined elsewhere in the program. This program runs perfectly well. Notice that the definition of polish employs a *circular data structure*: in fact the variable whites appears both on the left hand side and on the right hand side of the expression $`\mathrm{𝗅𝖾𝗍}(\mathrm{𝗋𝖾𝖽𝗐𝗁𝗂𝗍𝖾𝗌},\mathrm{𝗐𝗁𝗂𝗍𝖾𝗌})=\mathrm{𝖽𝗂𝗌𝗍𝗋𝗂𝖻𝗎𝗍𝖾}(𝗍,\mathrm{𝗐𝗁𝗂𝗍𝖾𝗌},[])`$, in the guard.

Circular data structures were first advocated by Bird \[Bir84\] in order to avoid multiple traversal of data structures, and since then have become a standard tool of *lazy* functional languages. It is worth remarking that the above program (and most other programs employing circular structures) would not function properly if we had used a *strict* functional language.

It is important to notice that the original logic program employs logical variables in a highly non-trivial way. This is confirmed by the fact that the program is not well-moded.

The fact that a program using difference-lists actually presents a functional behaviour is not incidental. Consider an atom containing a difference-list $`\mathrm{}𝚙(𝚝\backslash 𝚜)`$ (for the sake of simplicity, we assume that it does not have any other argument), as above, we split this position in two, and obtain $`\mathrm{}𝚙(𝚝\backslash 𝚜)`$. Now, the whole idea of having difference lists, is that when a computation starting in (an instance of) $`\mathrm{}𝚙(𝚝\backslash 𝚜)`$ will succeed, it will report a computed answer substitution (c.a.s.) $`\theta `$ such that $`𝚜\theta `$ is (“points to”) the tail of $`𝚝\theta `$. This implies that for all $`\sigma `$ if $`𝚜\theta \sigma `$ is ground, then $`𝚝\theta \sigma `$ is ground as well. Typically, after $`\mathrm{}𝚙(𝚝\backslash 𝚜)`$ has succeeded with c.a.s. $`\theta `$, $`𝚜\theta `$ will eventually be unified with a ground (classical) list (or with the head of another difference-list, in which case the reasoning continues by considering the tail of this second difference-structure). After this unification has taken place, $`𝚝\theta `$ is going to be a classical list, which can be employed as normal. In this sense we have that $`𝚝`$ depends on $`𝚜`$, therefore $`𝚝`$ has to be considered output and $`𝚜`$ input, and the above atom should be translated into let s = p(t); the only problem is that $`𝚜`$ is an input in disguise, in the sense that when $`𝚙(𝚝,𝚜)`$ is called, $`𝚜`$ is typically not (yet) ground (in other words, it is not yet known). However, this is hardly a problem when we consider *lazy* functional languages (at the same time, it is the reason why programs with difference lists cannot be easily translated into a strict functional language).

One could argue that the above reasoning could be completely reversed, starting by saying that “$`\mathrm{}`$ for all $`\sigma `$ if $`𝚝\theta \sigma `$ is ground, then $`𝚜\theta \sigma `$ is ground as well, $`\mathrm{}`$, thus if $`𝚝\theta `$ is unified to a ground list, then $`𝚜\theta `$ will become a ground list, and this shows that $`𝚜`$ depends on $`𝚝`$, and that therefore the above atom should be translated into s = p(t)” (which would fail to function). This is in principle true (dependencies in LP are always bidirectional), however, this property is never used, indeed it cannot be used in practice for the following simple reason: after succeeding with c.a.s. $`\theta `$, we typically have that $`𝚝\theta [𝚊_\mathrm{𝟷},𝚊_\mathrm{𝟸},\mathrm{},𝚊_𝚔|𝚇]`$ and that $`𝚜\theta 𝚇`$. Now, while it is always possible to unify $`𝚜\theta `$ with any ground list $`𝚕`$, trying to do this with $`𝚝\theta `$ will almost certainly lead to failure (unless $`[𝚊_\mathrm{𝟷},𝚊_\mathrm{𝟸},\mathrm{},𝚊_𝚔]`$ is a prefix of $`𝚕`$). Therefore difference-lists are virtually always employed in a *directional* fashion.

Another example of a program using logical variables which can be safely translated into Haskell is given in the following section. Of course, one can find an example of a program using difference-lists which would not work in Haskell; actually, counterexamples are extremely easy to contrive: variables in LP are always adirectional, and if one fully exploits this will always obtain a program which has no functioning functional counterpart. We don’t want to deny this, on the contrary: here we are interested in how programs are *usually* used, and in pointing out that some standard methodologies which are normally considered as applicable only to LP, are actually not so.

Of course not all programs using logical variables are translated correctly: typical such examples are the programs which incrementally fill in a data structures such as in the *eight queen* example and in the SEQUENCE example in Appendix C (these programs use unification in a crucial way, and this is confirmed by the fact that they are not *consistent*). Other examples are circular programs such as the following one

| p(X) $``$eq(X, X). |
| --- |
| eq(X, X). |

moded as follows: p(In:Ground):non-test and eq(Out:Ground, Out:Ground):non-test. This program is circular in a non-well-founded way, and this, when translated, yields a program which is not *productive*.

We can safely conclude that difference lists have a natural counterpart in the circular structures of lazy functional programming.

### 4.2 Dynamic scheduling vs. Lazy Evaluation

Another prominent property of logic programming is the possibility of having a dynamic selection rule, possibly guided by appropriate *delay declarations*. Let us consider the following example, which, given the list Xs of integer values, del\_max(Xs,Zs) produces the list Zs by deleting all the occurrences of its maximum element.

|  | del\_max(Xs, Zs) $``$find\_max\_and\_del(Xs, Max, Zs, Max). |
| --- | --- |
| % | find\_max\_and\_del(InList,El,OutList,Max) |
| % |  | Max is the maximum element of the list InList, and |
| % |  | OutList is obtained from Inlist by deleting all the occurrences of  El from it |
|  | find\_max\_and\_del(\[ \], \_, \[ \], 0). |
|  | find\_max\_and\_del(\[X | Xs\], El, Ys, Max) $``$ |
|  |  | find\_max\_and\_del(Xs, El, Zs, Max’), |
|  |  | sup(X, Max’, Max), |
|  |  | del\_if\_first(\[X | Zs\], El, Ys). |
|  | del\_if\_first(\[EL | Zs\], El, Zs). |
|  | del\_if\_first(\[X | Zs\], El, \[X|Zs\]) $``$X $``$ El. |
|  | mode del\_max(In:List\[Int\], Out:List\[Int\]): non-test. |
|  | mode find\_max\_and\_del(In:List\[Int\],In:Int,Out:List\[Int\],Out:Int):non-test. |
|  | mode sup(In:Int, In:Int, Out:Int): non-test. % defined in the obvious way |
|  | mode del\_if\_first(In:List\[Int\], In:Int, Out:List\[Int\]): non-test. |

It is worth noticing that the program uses logical variables in a nontrivial way. This is confirmed by the fact that it is not well-moded. Specifically, the variable Max in the first clause is used as an asynchronous communication channel between processes, as the atom find\_max\_and\_del(Xs, Max, Max, Zs) uses Max as input value that it has to produce itself.

Furthermore, the program requires an appropriate *dynamic scheduling*. In fact, when run with a standard left-to-right selection rule, the query del\_max(ts, Zs) ($`\mathrm{𝚝𝚜}`$ being a list of natural numbers) leads to a run-time error (or to an incorrect answer), and, provided that we fix this problem, to a very inefficient computation.

The first problem (concerning the runtime error) is due to the fact that the computation will soon a goal of the form del\_if\_first(ts, El, Zs), where ns $`(=[𝚗|\mathrm{𝚗𝚜}^{}])`$ is a non-empty list of integers, and El and Zs are distinct variables. At that point the interpreter will proceed and might reach the call $`𝚗\mathrm{𝙴𝚕}`$, which – being El a variable – will flounder333In practice, the behaviour of the interpreters in these situations are different, this depends on the non-logical behaviour of the built-ins of PROLOG and on whether we employ == in order to make the program plain and $`\backslash `$== in order to implement $``$. For instance in Eclipse and SWI-Prolog the call n == El fails, and a subsequent call n $`\backslash `$== El succeeds (!) in Eclipse by returning the empty c.a.s. and in SWI-prolog by instantiating El to an apparently random numeric value. Of course, this behaviours lead to solutions which are almost always incorrect.. In other words, this program cannot be run with the normal leftmost selection rule.

The second problem (concerning program’s inefficiency) is due to the fact that the query del\_max(Xs, Zs) could return the list $`\mathrm{𝚉𝚜}`$ in linear time (scanning $`\mathrm{𝚇𝚜}`$ only once), however, it is easy to see that if we employ any fixed selection rule, the program has to go through a remarkable amount of backtracking, which makes it run in quadratic time on the length of the input list444Informally, the reason is that the interpreter will run into some calls of the form $`\mathrm{𝚍𝚎𝚕}\mathrm{\_}\mathrm{𝚒𝚏}\mathrm{\_}\mathrm{𝚏𝚒𝚛𝚜𝚝}(\mathrm{},\mathrm{𝙴𝚕},\mathrm{𝚉𝚜})`$, where $`\mathrm{𝙴𝚕}`$ is still a variable. For this reason $`\mathrm{𝚍𝚎𝚕}\mathrm{\_}\mathrm{𝚒𝚏}\mathrm{\_}\mathrm{𝚏𝚒𝚛𝚜𝚝}(\mathrm{},\mathrm{𝙴𝚕},\mathrm{𝚉𝚜})`$ will take a guess and delete an element which will usually turn out not to be the correct one, and this will eventually produce backtracking. Since the number of needed backtracking steps is linear in the size of the input list, this decreases the performance of the program from linear to quadratic time. In order to avoid this problem, we have to make sure that an atom of the form $`\mathrm{𝚍𝚎𝚕}\mathrm{\_}\mathrm{𝚒𝚏}\mathrm{\_}\mathrm{𝚏𝚒𝚛𝚜𝚝}(\mathrm{\_},\mathrm{𝙴𝚕},\mathrm{\_})`$ will be selected in the derivation only when $`\mathrm{𝙴𝚕}`$ will be instantiated to a ground term. We can do this by employing the above delay declarations..

Both problems can be solved by employing a *dynamic selection rule* and by prohibiting the selection of certain atoms until their arguments are sufficiently instantiated using for instance the following *delay declarations* \[Nai82\]:

| delay sup(X, Y, \_) until ground(X) $``$ ground(Y). |
| --- |
| delay $``$(X,Y) until ground(X) $``$ ground(Y). |
| delay del\_if\_first(\[X|Xs\], El, \_) until ground(X) $``$ ground(El) |

For instance, the first declaration will suspend any call to sup(t, s, v). until t and s are ground terms. Delay declarations have become an important standard control tool and are implemented in various versions of Prolog (for instance in Sixtus Prolog and in Eclipse \[WV93\]) and in the language Gödel \[HL94\].

Now, let us for a moment not bother about the delay declarations and translate this program into Haskell. We obtain the following script.

| del\_max as | $`|`$ | xs $``$as |
| --- | --- | --- |
|  | , | let (zs, maxel) = find\_max\_and\_del (xs,maxel) |
|  |  |  | = zs |
| find\_max\_and\_del (x1,x2) | $`|`$ | (\[ \], el) $``$(x1, x2) |
|  |  |  | = (\[ \], 0) |
|  | $`|`$ | (x:xs, el) $``$(x1,x2) |
|  | , | let (zs, maxel’) = find\_max\_and\_del (xs,el) |
|  | , | let maxel = max x maxel’ |
|  | , | let ys = del\_if\_first (x:zs, el) |
|  |  |  | = (ys, maxel) |
| del\_if\_first (x1, x2) | $`|`$ | (\[ \], el) $``$(x1, x2) |
|  |  |  | = \[ \] |
|  | $`|`$ | (x:xs, el) $``$(x1,x2) |
|  | , | x == el |
|  |  |  | = zs |
|  | $`|`$ | (x:xs, el) $``$(x1,x2) |
|  | , | x /= el |
|  |  |  | = x:zs |

This program works fine, and his runtime complexity is linear in the size of the input. We can therefore state that the lazy computational mechanism compensates for the lack of control over dynamic scheduling, without which the above logic program could not be run or would have a quadratic complexity.

Thus although the mechanism of lazy evaluation and delay declarations are quite different (actually, they are the opposite: the call-by-need mechanism determines which term *has* to be reduced, while delay declarations determine which atoms *should not* be resolved), they often accomplish the same thing.

The fact that lazy evaluation here plays a crucial role is confirmed by the fact that, if we had declared all predicates to be test predicates (thus forcing strictness, as explained in the Remark 3.4) the translated program would not function properly.

Thus again we are in presence of a program exploiting logical variables in a complex way which nevertheless has a natural translation into Haskell.

### 4.3 Backtracking and Nondeterminism

Another outstanding feature of logic programs is their backtracking mechanism, which virtually implements a *don’t know* nondeterministic system.

In the light of the above examples, we believe that nondeterminism is by far the most important and the mostly used peculiar feature of the logic programming paradigm. We don’t want to challenge this, on the contrary. At the same time, it is important for us to show to which extent a (lazy) functional program can mimic a logic program which uses backtracking.

Consider the following program.

| backtracker(X) :- producer\_a(Y), picky\_modifier(Y,X). |
| --- |
| backtracker(X) :- producer\_b(Y), picky\_modifier(Y,X). |
| producer\_a("a"). |
| producer\_b("b"). |
| picky\_modifier("b", "c"). |

The adopted mode and partitioning is

| backtracker(Out) : non-test |
| --- |
| producer\_a(Out) : non-test ( and the same for  producer\_b ) |
| picky\_modifier(In, Out) : test |

Its translation is the following:

| backtracker | $`|`$ | let y = producer\_a |
| --- | --- | --- |
|  | , | Suc x $``$picky\_modifier y |
|  |  |  | = x |
|  | $`|`$ | let y = producer\_b |
|  | , | Suc x $``$picky\_modifier y |
|  |  |  | = x |
| producer\_a = ”a” |
| producer\_b = ”b” |
| picky\_modifier x | $`|`$ | x == ”b” |
|  |  |  | = Suc ”c” |
|  | $`|`$ | otherwise = Fail |

The Haskell translation is able to report all the correct answers, even though in LP for the query $`\mathrm{𝚋𝚊𝚌𝚔𝚝𝚛𝚊𝚌𝚔𝚎𝚛}(𝚇)`$ in order to return the answer X = "a", the interpreter has to go through some backtracking. Notice in fact that the above logic program is not deterministic.

Consider now the following program scheme:

It is immediate to translate it and to check that if generate has more than one solution then the translation does not behave as the logic program does: while the query :- p(X) succeeds provided that one of the solutions of generate(X) satisfies test(X), the Haskell translation manages to report one answer only so in the unlikely case that the first solution founded by generate(X) satisfies test(X); in all other cases $`𝗉`$ reduces to $`\mathrm{𝖥𝖺𝗂𝗅}`$.

The key factor for the translation to work correctly we need to avoid logic programs in which consistent queries might originate SLD trees with more than one successful (sub-) branch. There exists techniques based on list-comprehension in order to translate logic programs into functional programs in such a way that the resulting program will (eventually, lazily) report the list of all the answers that the initial logic program would. In those cases, however, one can clearly not talk of a *literal* translation, which is the starting point of our research (programs able to return more than one answer are in our opinion intrinsically logic programs, and therefore do not belong to our target).

To be precise, a non-deterministic logic program can be safely translated onto Haskell provided it is *input discriminative*, as defined as follows:

###### Definition 4.1 (Input Discriminative)

Let $`𝙿`$ be a program, $`M_𝙿`$ be its least Herbrand model, and

| p1($`\overline{𝚒}`$1, $`\overline{𝚘}`$1) | $``$$`\overline{\mathrm{𝚝𝚎𝚜𝚝}}`$1, $`\overline{\mathrm{𝚛𝚎𝚜𝚝}}`$1. |
| --- | --- |
|  | $`\mathrm{}`$ |
| pn($`\overline{𝚒}`$n, $`\overline{𝚘}`$n) $``$$`\overline{\mathrm{𝚝𝚎𝚜𝚝}}`$n, $`\overline{\mathrm{𝚛𝚎𝚜𝚝}}`$n. |

Be the complete set of the rules of $`𝙿`$ (where the conjunction $`\overline{\mathrm{𝚝𝚎𝚜𝚝}}`$i contains only test predicates and $`\overline{\mathrm{𝚛𝚎𝚜𝚝}}`$i contains only non-test predicates). We say that $`𝙿`$ is *input discriminative* if for each $`jk[1,n]`$, such that $`𝚙_j=𝚙_k`$ we have that

* for each ground $`\theta `$ such that $`\overline{𝚒}_j\theta =\overline{𝚒}_k\theta `$ we have that $`M_𝙿\neg (\overline{\mathrm{𝚝𝚎𝚜𝚝}}_j\theta \overline{\mathrm{𝚝𝚎𝚜𝚝}}_k\theta )`$. $`\mathrm{}`$

It is worth noticing that this concept of input discriminative program is rather less restrictive than the concept of *deterministic* program, and that input-discrimitative programs might still require non-trivial (non-shallow, see \[SS86, Ch. 6\]) backtracking. We could say that these programs admit some *shallow nondeterminism*.

Summarizing, there is a point to be remarked, that – strictly speaking – the Haskell translation of a program can *always* mimic the backtracking taking place in the original logic program. What the Haskell translation can*not* do is report multiple answers.

#### Failure, Nondeterminism and Related Work

The feature of logic programs of being able of reporting more than answer, and how this is handled in the different translation systems is a topic which deserves a separate discussion.

Regarding this issue, the literature on papers presenting a translation from logic to functional programs can be divided in two main groups.

On one side we find papers which are not concerned with the nondeterminism (or the backtracking) mechanism of logic languages \[Mar94, GW92, RKS98, vR97\], these papers are usually mainly concerned in providing a transformation system which allows one to prove program properties such as termination of the original logic program. For this reason they focus on obtaining a translation which maps only the non-failing computations correctly. In these papers the failure and backtracking mechanism are disregarded during the translation.

On the other side, we find \[Mar95, Red84\], in which the authors propose a translation in which the full (PROLOG-like) computational mechanism is preserved, including the possibility of having multiple answer for the same query and the possibility of failure. This is achieved by letting a query return the *list* of computed answer substitutions, where the empty list corresponds to the failing case, in the same way advocated by Wadler \[Wad85\]. The lazy computational mechanism then takes care of computing only those answers which are necessary, and backtracking is faithfully rendered by a standard list-comprehension schema.

The translation system we have employed lies somewhere in the middle between those two methods. Our goal was to take also failure into account, yet retaining a literal translation system, in which the computational mechanism of the resulting functional program is as similar as possible to the one of the original logic program.

Of course we can only correctly translate programs which do not return more than one answer for the same query (at the same time, it is important to notice that these programs don’t have to be deterministic; for instance member is nondeterministic).

In our opinion, the possibility of returning more than one answer is to be considered a *peculiar* one of the LP paradigm, and the fact that it can be emulated by functional programs does not obliterate our position.

## 5 Conclusions

The goal of our research was to investigate to which extent some features considered peculiar of the logic programming paradigm are really so. For this purpose we have devised a simple – literal – system which enabled us to translate logic programs into the lazy functional language Haskell.

It is known (see also \[Mar94, GW92, RKS98, vR97\]) that *if we restrict our attention to non-failing, non-backtracking computation* then well-moded simply moded programs have a natural counterpart in a functional language. The properties of being well-moded and simply moded indicates a manner of use of variables in logic programming which is undoubtedly “functional”. To this statement we want to add that well- and simply moded programs can be considered as *strictly* functional, as they can be safely translated into a *strict* functional language.

In this paper we have shown that in a *lazy* functional language, this picture broadens significantly, and some of the features that were – in the light of the results above – commonly considered as exclusive of the logic programming paradigm, can be naturally found in a lazy functional language such as Haskell.

In particular, we have shown that the use of complex logical variables in data structures such as difference lists (or such as in program in del\_max) find a natural counterpart in the circular structures \[Bir84\] of lazy functional programs. These structures that were commonly considered as “structurally logical” are thus not so. We can then attempt a rough classification of logic programs according to the level of complexity at which they employs their variables (backtracking and nondeterminism is not considered here). We then have the following division.

1. *Strictly Functional* programs which use variables in a standard (imperative-like) way. These are characterized by being *well-moded* (or by being so after permutation of the clause’s body atoms).
2. *Lazy Functional* programs which admit a safe translation into Haskell: i.e. programs which can be translated into Haskell (via the syntactic translation) and whose operational behaviour is isomorphic to the one of their functional counterpart.
3. *Intrinsically Logical* programs which do not admit a safe translation into Haskell with our translation scheme.

This raises the interesting question of how large is the class of intrinsically logical programs. Without pretending to be able to characterize extensively this limit, it is interesting to notice that programs which are plain and consistent and which either admit a Layered Mode \[EG96\], or are S-well-typed programs \[BM97\] are safely translatable into Haskell (modulo the possibility of backtracking, which is discussed in the sequel). As argued in \[EG96\], we believe that these programs actually encompass the majority of actual programs which use logical variables in a non-elementary way. We think that a classification and understanding of these levels might be useful both to enhance the performance of logic languages (as already done to some extent in the language Mercury) and to prove more precise program properties.

Furthermore, we have also addressed another logical feature: the possibility of dynamic scheduling. In theory in LP *any* atom is selectable as all selection rules yield the same successful derivations. In practice this does not work, and adopting a random selection rule would in the best case yield to an explosion of the search space; for this reason PROLOG uses a fixed left-to-right selection rule, a feature which is either explicitly or implicitly always exploited by the programmers. However, some programs (like delmax above, or concurrent-like programs) are not correct under a fixed search rule. In these cases the “right” selection strategy is enforced by the use of appropriate delay declarations (d.d.), which serve to indicate which atoms in a query should not be resolved. The implementation of d.d. is rather costly, as atoms are continuously being suspended and forced. Here we have seen one example in which the lazy evaluation mechanism of Haskell achieves the same effect of the use of d.d.. As we have pointed out, call-by-need can be regarded as a dynamic selection strategy, which is however based on an principle opposite to the one of d.d. in the sense that call-by need determines which term has to be reduced, while delay declarations determine which atoms should *not* be resolved. A naturally arising question here is whether it is possible to implement in logic programming languages a selection rule which is “driven” by a call-by-need mechanism, instead of “restricted” by the use of delay declarations. This could possibly lead to reduction of the suspension overhead and thus to performance improvements. The difficulty in implementing such a search rule lies in the fact that in LP it is not clear which output values depend on which input values (actually, it is not clear what is input and what it is output to start with), so in order to implement such an intelligent selection strategy, one would need some sophisticated analysis tools which might either be based on abstract interpretation (with tools similar to the ones of \[CDG93\]), or on refined versions of modes such as the ones described in \[BM97, EG96\]. Other works related to this subjects are \[LK92, EvR98\].

We have also discussed the fact that logic programs allow backtracking. We have seen that – strictly speaking – backtracking computations can be easily mimicked by the functional language by an appropriate use of the guards; what cannot be (easily) mimicked in Haskell is the possibility of returning multiple answers, at least not unless one uses additional constructs such as the list-of-successes method \[Wad85\]. An interesting research direction might be to define appropriate monadic structures (such as those in \[Wad92\]) to capture the failure or success and returning of multiple arguments. This would broaden the set of logical programs which we can capture with our simple translation scheme, without adding signifant complexity to it.

In conclusion, we have demonstrated with a simple, literal translation scheme that several features considered as belonging specifically to logic programming are found naturally in lazy functional programming, dismissing the folklore that the functional core of logic programming is contained in the set of well- and simple moded programs.

## Appendix A Well-Moded Programs

The following concept is essentially due to Dembinski and Maluszynski \[DM85\]; we use here an elegant formulation due to Rosenblueth \[Ros91\].

###### Definition A.1

A clause $`𝚙_\mathrm{𝟶}(\overline{𝚝}_\mathrm{𝟶},\overline{𝚜}_{𝚗+\mathrm{𝟷}})𝚙_\mathrm{𝟷}(\overline{𝚜}_\mathrm{𝟷},\overline{𝚝}_\mathrm{𝟷}),\mathrm{},𝚙_𝚗(\overline{𝚜}_𝚗,\overline{𝚝}_𝚗)`$ is called *well-moded* if for $`i[1,n+1]`$

$$\mathrm{𝑉𝑎𝑟}(\overline{𝚜}_𝚒)\underset{𝚓=\mathrm{𝟶}}{\overset{𝚒\mathrm{𝟷}}{}}\mathrm{𝑉𝑎𝑟}(\overline{𝚝}_𝚓).$$

A query $`\overline{𝙰}`$ is called *well-moded* iff the clause $`𝚚\overline{𝙰}`$ is, where $`𝚚`$ is any (dummy) atom of zero arity.

A program is called *well-moded* if every clause of it is. $`\mathrm{}`$

It is important to notice that the first atom of a well-moded goal is ground in its input positions and a variant of a well-moded clause is well-moded. Furthermore, the notion of of well-modedness, is “persistent”, as shown by the following Lemma. Recall that a LD-resolvent is a resolvent in which the leftmost atom per the query is the selected one, and that an LD-derivation is a derivation obtained employing the leftmost selection rule,

###### Lemma A.2

An LD-resolvent of a well-moded goal and a well-moded clause that is variable-disjoint with it, is well-moded. $`\mathrm{}`$

The next result is originally due to Dembinski and Maluszynski and follows directly from the definition of well-moded program.

###### Corollary A.3

Let $`𝙿`$ and $`\overline{𝙰}`$ be well-moded, and let $`\xi `$ be an LD-derivation of $`\overline{𝙰}`$ in $`𝙿`$. All atoms selected in $`\xi `$ contain ground terms in their input positions. $`\mathrm{}`$

That is, in presence of well-moded programs and queries, if we use a left-to-right computation schema we are sure that every time that we select an atom, the “value” of his input arguments has already been fully computed. This shows that well-moded programs have a straightforward left-to-right data-flow.

Under certain conditions well-moded programs are also *unification-free*. To show this, we need a definition first. The following notion was first defined in \[AE93\].

###### Definition A.4

A clause $`𝚙_\mathrm{𝟶}(\overline{𝚜}_\mathrm{𝟶},\overline{𝚝}_{𝚗+\mathrm{𝟷}})𝚙_\mathrm{𝟷}(\overline{𝚜}_\mathrm{𝟷},\overline{𝚝}_\mathrm{𝟷}),\mathrm{},𝚙_𝚗(\overline{𝚜}_𝚗,\overline{𝚝}_𝚗)`$ is called *simply moded* if if $`\overline{𝚝}_\mathrm{𝟷},\mathrm{},\overline{𝚝}_𝚗`$ is a linear family of variables and for $`i[1,n]`$

$$\mathrm{𝑉𝑎𝑟}(\overline{𝚝}_𝚒)(\underset{𝚓=\mathrm{𝟶}}{\overset{𝚒}{}}\mathrm{𝑉𝑎𝑟}(\overline{𝚜}_𝚓))=\mathrm{}.$$

A query $`\overline{𝙰}`$ is called *simply moded* iff the clause $`𝚚\overline{𝙰}`$ is, where $`𝚚`$ is any (dummy) atom of zero arity.

A program is called simply moded if every clause of it is. $`\mathrm{}`$

Thus, assuming that in every atom the input positions occur first, a clause is simply moded if all output positions of every body atom are filled in by distinct variables, which do not occur earlier in the body nor in an input position of the head.

It is worth noticing that – as shown by the little survey in \[AE93\] – most programs are already simply-moded and that often non simply-moded programs can naturally be transformed into simply-moded ones, for instance the non-simply-moded clause $`\mathrm{𝚕𝚊𝚜𝚝}(\mathrm{𝙻𝚒𝚜𝚝},\mathrm{𝙴𝚕}):\mathrm{𝚛𝚎𝚟𝚎𝚛𝚜𝚎}(\mathrm{𝙻𝚒𝚜𝚝},[\mathrm{𝙴𝚕}|\mathrm{\_}]).`$ can be transformed into $`\mathrm{𝚕𝚊𝚜𝚝}(\mathrm{𝙻𝚒𝚜𝚝},\mathrm{𝙴𝚕}):\mathrm{𝚛𝚎𝚟𝚎𝚛𝚜𝚎}(\mathrm{𝙻𝚒𝚜𝚝},\mathrm{𝙻𝚒𝚜𝚝}^{}),[\mathrm{𝙴𝚕}|\mathrm{\_}]=\mathrm{𝙻𝚒𝚜𝚝}^{}`$.

The property of being simply moded is also “persistent” in the sense that the resolvent of a simply moded query with a simply moded clause is simply moded.

In \[AE93\] it is proven that if the program and the query are simply moded, then they generate an LD-derivation which is *unification-free*, i.e. that each time an atom $`𝙰`$ is selected and resolved in it via a clause $`𝙷\overline{𝙱}`$, then the unification of $`𝙰`$ and $`𝙷`$ does not really require a full unification algorithm, but can always be reduced to a *double matching:* one (“from” $`𝙰`$ “to” $`𝙷`$) for the input positions and a second one (“from” $`𝙷`$ “to” $`𝙰`$) for the output ones. This result clearly shows that simply and well-moded logic programs are functional in nature (besides for the possibility of reporting multiple answers, of course).

## Appendix B More on Haskell

The following (nonsense) program embodies most of the concepts we use:

| append (\[ \],x) | = Suc x |
| --- | --- |
| append (x1,x2) | $`|`$ | (x:xs) $``$x1 |
|  | , | Suc tail $``$append (xs, x2) |
|  | , | let newtail = (x:tail) |
|  |  |  | = Suc newtail |
|  | $`|`$ | otherwise = Fail |

In a call of append (a,b), the first equation will be tried first. Here, a will be pattern matched to the empty list. If this succeeds, then x is matched to b (since both are variables, this will always succeed), and finally Suc x is returned. If the pattern match above failed, then the first guard will be tried, which tries to pattern match the first element of the tuple to a list with at least one element. Should this succeed, the result of a recursive call to append is matched against Suc tail, and if successful (x:tail) is bound to the variable $`\mathrm{𝗇𝖾𝗐𝗍𝖺𝗂𝗅}`$, followed by the returning of $`\mathrm{𝖲𝗎𝖼}\mathrm{𝗇𝖾𝗐𝗍𝖺𝗂𝗅}`$. If either of the pattern matches failed, then the second guard will be tried.

## Appendix C program SEQUENCE

This example is provided by the Prolog formalization of a problem from Coelho and Cotta \[CC88, pag. 193\]: arrange three 1’s, three 2’s, …, three 9’s in sequence so that for all $`i[1,9]`$ there are exactly $`i`$ numbers between successive occurrences of $`i`$.

| sublist(Xs, Ys) $``$ Xs is a sublist of the list Ys. |
| --- |
| sublist(Xs, Ys) $``$ app(\_, Zs, Ys), app(Xs, \_, Zs). |
| sequence(Xs) $``$ Xs is a list of 27 elements. |
| sequence(\[\_,\_,\_,\_,\_,\_,\_,\_,\_,\_,\_,\_,\_,\_,\_,\_,\_,\_,\_,\_,\_,\_,\_,\_,\_,\_,\_\]) . |
| question(Ss) $``$ Ss is a list of 27 elements forming the desired sequence. |
| question(Ss) $``$ |
|  | sequence(Ss), |
|  | sublist(\[1,\_,1,\_,1\], Ss), |
|  | sublist(\[2,\_,\_,2,\_,\_,2\], Ss), |
|  | sublist(\[3,\_,\_,\_,3,\_,\_,\_,3\], Ss), |
|  | sublist(\[4,\_,\_,\_,\_,4,\_,\_,\_,\_,4\], Ss), |
|  | sublist(\[5,\_,\_,\_,\_,\_,5,\_,\_,\_,\_,\_,5\], Ss), |
|  | sublist(\[6,\_,\_,\_,\_,\_,\_,6,\_,\_,\_,\_,\_,\_,6\], Ss), |
|  | sublist(\[7,\_,\_,\_,\_,\_,\_,\_,7,\_,\_,\_,\_,\_,\_,\_,7\], Ss), |
|  | sublist(\[8,\_,\_,\_,\_,\_,\_,\_,\_,8,\_,\_,\_,\_,\_,\_,\_,\_,8\], Ss), |
|  | sublist(\[9,\_,\_,\_,\_,\_,\_,\_,\_,\_,9,\_,\_,\_,\_,\_,\_,\_,\_,\_,9\], Ss). |
| augmented by the append program. |


format: text

text:
# References

NEW LOCAL SYMMETRY FOR QED IN TWO DIMENSIONS

R. P. MALIK *** E-mail: malik@boson.bose.res.in

S. N. Bose National Centre for Basic Sciences,

Block-JD, Sector-III, Salt Lake, Calcutta-700 098, India

Abstract: A new local, covariant and nilpotent symmetry is shown to exist for the interacting BRST invariant $`U(1)`$ gauge theory in two dimensions of space-time. Under this new symmetry, it is the gauge-fixing term that remains invariant and the corresponding transformations on the Dirac fields turn out to be the analogue of chiral transformations. The extended BRST algebra is derived for the generators of all the underlying symmetries, present in the theory. This algebra turns out to be the analogue of the algebra obeyed by the de Rham cohomology operators of differential geometry. Possible interpretations and implications of this symmetry are pointed out in the context of BRST cohomology and Hodge decomposition theorem.

The importance of symmetries in physics has gone beyond the mere requirement of an aesthetic appeal to the sophistication of explaining some of the landmark experiments. One such important symmetry in theoretical physics is the gauge symmetry which has turned out to provide the corner-stone for the modern developments in the ideas of unification. The main characteristic feature of theories, based on these symmetries, is the fact that they are endowed with the first-class constraints (in the language of Dirac) \[1-3\]. A cardinal example of such a class of theories is the quantum electrodynamics (QED) which represents a dynamically closed system of photon ($`U(1)`$ gauge field $`A_\mu `$) and electrically charged particles (e.g. electrons and positrons which are described by the Dirac fields $`\psi `$ and $`\overline{\psi }`$). For the covariant canonical quantization of these gauge theories, the Becchi-Rouet-Stora-Tyutin (BRST) symmetry  turns out to be quite handy. In this formalism, unitarity and gauge invariance are respected together at any arbitrary order of perturbation theory. The purpose of the present letter is to shed some light on the existence of some local, covariant and continuous symmetries which have not been explored hitherto in the context of two dimensional (2D) QED and to establish that this interacting theory provides a physically tractable field theoretical model for the Hodge theory. The generators for the underlying symmetries of the theory obey an algebra that is reminiscent of the algebra of de Rham cohomology operators of differential geometry defined on a compact manifold.

Let us begin with a $`D`$-dimensional BRST invariant Lagrangian density ($`_B`$) for the interacting $`U(1)`$ gauge theory in the Feynman gauge:

$$\begin{array}{ccc}_B=\frac{1}{4}F^{\mu \nu }F_{\mu \nu }+\overline{\psi }(i\gamma ^\mu _\mu m)\psi e\overline{\psi }\gamma ^\mu A_\mu \psi +B(A)+\frac{1}{2}B^2i_\mu \overline{C}^\mu C,\hfill & & \end{array}$$
$`(1)`$
where $`F_{\mu \nu }=_\mu A_\nu _\nu A_\mu `$ is the field strength tensor, $`B`$ is the Nakanishi-Lautrup auxiliary field, $`(\overline{C})C`$ are the Faddeev-Popov (anti)ghost fields ($`\overline{C}^2=C^2=0`$) and indices $`\mu ,\nu =0,1,2,\mathrm{}\mathrm{}D1`$ represent the flat Minkowski space-time directions. It can be checked that the above Lagrangian density remains quasi-invariant ($`\delta _B_B=\eta _\mu [B^\mu C]`$) under the following off-shell nilpotent ($`\delta _B^2=0`$) BRST transformations:

$$\begin{array}{ccc}\delta _BA_\mu \hfill & =& \eta _\mu C,\delta _BC=0,\delta _B\overline{C}=i\eta B,\delta _BB=0,\hfill \\ \delta _B\psi \hfill & =& i\eta eC\psi ,\delta _B\overline{\psi }=i\eta eC\overline{\psi },\delta _B(A)=\eta \mathrm{}C,\delta _BF_{\mu \nu }=0,\hfill \end{array}$$
$`(2)`$
where $`\eta `$ is an anticommuting ($`\eta C=C\eta ,\eta \overline{C}=\overline{C}\eta ,\eta \psi =\psi \eta ,\eta \overline{\psi }=\overline{\psi }\eta `$) space-time independent transformation parameter. Using Noether theorem, it is straightforward to check that the generator for the above transformations is the nilpotent ($`Q_B^2=0`$) BRST charge

$$\begin{array}{ccc}Q_B\hfill & =& d^{(D1)}x\left[_iF^{0i}C+B\dot{C}e\overline{\psi }\gamma _0C\psi \right],\hfill \\ & & d^{(D1)}x\left[B\dot{C}\dot{B}C\right],\hfill \end{array}$$
$`(3)`$
where the latter expression for $`Q_B`$ has been obtained by exploiting the equation of motion ($`_\mu F^{\mu \nu }^\nu B=e\overline{\psi }\gamma ^\nu \psi `$). The global scale invariance of (1) under $`Ce^\lambda C,\overline{C}e^\lambda \overline{C},A_\mu A_\mu ,BB`$ (where $`\lambda `$ is a global parameter), leads to the derivation of a conserved ghost charge ($`Q_g`$)

$$\begin{array}{ccc}Q_g=id^{(D1)}x\left[C\dot{\overline{C}}+\overline{C}\dot{C}\right].\hfill & & \end{array}$$
$`(4)`$
Together, these conserved charges satisfy the following algebra

$$\begin{array}{ccc}Q_B^2\hfill & =& \frac{1}{2}\{Q_B,Q_B\}=0,i[Q_g,Q_B]=+Q_B,\hfill \\ Q_{AB}^2\hfill & =& \frac{1}{2}\{Q_{AB},Q_{AB}\}=0,i[Q_g,Q_{AB}]=Q_{AB},\hfill \end{array}$$
$`(5)`$
where $`Q_{AB}`$ is the anti-BRST charge which can be readily obtained from (3) by the replacement :$`Ci\overline{C}`$ \[6-8\]. Note that $`C\pm i\overline{C},\overline{C}\pm iC`$ is the symmetry of the ghost action ($`I_{F.P.}=id^Dx_\mu \overline{C}^\mu C`$) in any arbitrary dimension of space-time.

In the past few years, many authors \[9-12\] have attempted to explore the possibilities of obtaining new BRST-type symmetries for the Lagrangian density (1) of QED in the hope of establishing a deeper connection with the mathematical aspects of BRST cohomology in any arbitrary dimension of space-time (see, e.g., Refs. ). However, the symmetry transformations turn out to be nonlocal and noncovariant. In the relativistic covariant formulation of these symmetries  the manifest nilpotency is lost and it is restored only under certain specific restrictions on the parameters of the theory. The central theme of our present short note is to show that in two dimensions of space-time there exists a local, continuous, covariant and nilpotent BRST-type symmetry under which the gauge-fixing term of the Lagrangian density (1) remains invariant and corresponding transformations on Dirac fields turn out to be the analogue of chiral transformations. This symmetry transformation is not the generalization of the $`D`$-dimensional symmetries \[9-12\] explored by others to two dimensions of space-time. Rather, it is a new symmetry in its own right. Contrary to the above symmetry transformation, it is the Abelian field strength tensor (two-form) that remains invariant under the usual BRST symmetry and the Dirac fields transform as the analogue of gauge transformations (see, e.g., eqn.(2)). We christen the new symmetry as the dual-BRST symmetry because the gauge-fixing term is Hodge dual to the field strength tensor (two-form) of Abelian $`U(1)`$ gauge theory in any arbitrary dimension of space-time The vector potential $`A_\mu `$ of the $`U(1)`$ gauge theory is defined through one-form $`A=A_\mu dx^\mu `$. The gauge-fixing term $`A=\delta A`$ is Hodge dual to the two-form $`F=dA`$ where $`\delta =\pm d`$ is the adjoint(dual) exterior derivative and $`d`$ is the exterior derivative (see, e.g., Ref. ). . This duality is also reflected at the level of transformations for the Dirac fields where the analogues of gauge- and chiral transformations are dual to each-other.

In two ($`1+1`$) dimensions of space-time, there exists only one component (i.e. electric field $`E=F_{01}`$) of the field strength tensor $`F_{\mu \nu }`$. Thus, the analogue of the BRST invariant Lagrangian density (1) is:

$$\begin{array}{ccc}_B=\frac{1}{2}E^2+\overline{\psi }(i\gamma ^\mu _\mu m)\psi e\overline{\psi }\gamma ^\mu A_\mu \psi +B(A)+\frac{1}{2}B^2i_\mu \overline{C}^\mu C,\hfill & & \end{array}$$
$`(6a)`$
which can be recast as:

$$\begin{array}{ccc}_{}=E\frac{1}{2}^2+\overline{\psi }(i\gamma ^\mu _\mu m)\psi e\overline{\psi }\gamma ^\mu A_\mu \psi +B(A)+\frac{1}{2}B^2i_\mu \overline{C}^\mu C,\hfill & & \end{array}$$
$`(6b)`$
by introducing another auxiliary field $``$. It can be checked that under the following off-shell nilpotent ($`\delta _D^2=0`$) dual-BRST transformations

$$\begin{array}{ccc}\delta _DA_\mu \hfill & =& \eta \epsilon _{\mu \nu }^\nu \overline{C},\delta _D\overline{C}=0,\delta _DC=i\eta ,\delta _D=0,\delta _DB=0,\hfill \\ \delta _D\psi \hfill & =& i\eta e\overline{C}\gamma _5\psi ,\delta _D\overline{\psi }=i\eta e\overline{C}\gamma _5\overline{\psi },\delta _D(A)=0,\delta _DE=\eta \mathrm{}\overline{C},\hfill \end{array}$$
$`(7)`$
the Lagrangian density (6b) (with $`m=0`$) transforms as: $`\delta _D_{}=\eta _\mu (^\mu \overline{C})`$  We adopt the notations in which the flat 2D Minkowski metric $`\eta _{\mu \nu }=`$ diag$`(+1,1),\gamma ^0=\sigma _2,\gamma ^1=i\sigma _1,\gamma _5=\gamma ^0\gamma ^1=\sigma _3,\{\gamma ^\mu ,\gamma ^\nu \}=2\eta ^{\mu \nu },\gamma _\mu \gamma _5=\epsilon _{\mu \nu }\gamma ^\nu ,\epsilon _{01}=\epsilon ^{10}=+1,F_{01}=_0A_1_1A_0=E=\epsilon ^{\mu \nu }_\mu A_\nu =F^{10},\mathrm{}=\eta ^{\mu \nu }_\mu _\nu =(_0)^2(_1)^2`$ and here $`\sigma ^{}s`$ are the usual $`2\times 2`$ Pauli matrices.. Exploiting the Noether theorem, it can be checked that the above transformations are generated by

$$\begin{array}{ccc}Q_D\hfill & =& 𝑑x\left[\dot{\overline{C}}+e\overline{\psi }\gamma _1\overline{C}\psi (_1B)\overline{C}\right],\hfill \\ & & 𝑑x\left[\dot{\overline{C}}\dot{}\overline{C}\right],\hfill \end{array}$$
$`(8)`$
where the latter expression for $`Q_D`$ has been obtained by using the equation of motion ($`\epsilon ^{\mu \nu }_\nu +^\mu B=e\overline{\psi }\gamma ^\mu \psi `$) for the photon field, present in the Lagrangian density (6b). Using the following BRST quantization conditions (with $`\mathrm{}=c=1`$):

$$\begin{array}{ccc}& & [A_0(x,t),B(y,t)]=i\delta (xy),\hfill \\ & & [A_1(x,t),(y,t)]=i\delta (xy),\hfill \\ & & \{\psi (x,t),\psi ^{}(y,t)\}=\delta (xy),\hfill \\ & & \{C(x,t),\dot{\overline{C}}(y,t)\}=\delta (xy),\hfill \\ & & \{\overline{C}(x,t),\dot{C}(y,t)\}=\delta (xy),\hfill \end{array}$$
$`(9)`$
(and rest of the (anti)commutators are zero), it can be seen that $`Q_D`$ is indeed the generator for the transformations (7) if we exploit the following relationship

$$\begin{array}{ccc}\delta _D\mathrm{\Phi }=i\eta [\mathrm{\Phi },Q_D]_\pm ,\hfill & & \end{array}$$
$`(10)`$
where $`[,]_\pm `$ stands for (anti)commutator for the generic field $`\mathrm{\Phi }`$ being (fermionic)bosonic in nature. It is straightforward to check that $`Q_D^2=\frac{1}{2}\{Q_D,Q_D\}=0`$ due to (9). A simpler way to see this fact is: $`\delta _DQ_D=i\eta \{Q_D,Q_D\}=0`$ by exploiting (7) and (8).

It is very natural to expect that the anticommutator of these two transformations ($`\{\delta _B,\delta _D\}=\delta _W`$) would also be the symmetry transformation ($`\delta _W`$) for the Lagrangian density (6b) (with $`m=0`$). This is indeed the case as can be seen that under the following bosonic ($`\kappa =i\eta \eta ^{}`$) transformations corresponding to $`\delta _W`$

$$\begin{array}{ccc}\delta _WA_\mu \hfill & =& \kappa (_\mu +\epsilon _{\mu \nu }^\nu B),\delta _W=0,\delta _WB=0,\hfill \\ \delta _W(A)\hfill & =& \kappa \mathrm{},\delta _WE=\kappa \mathrm{}B,\delta _WC=0,\delta _W\overline{C}=0,\hfill \\ \delta _W\psi \hfill & =& \kappa ie(\gamma _5B)\psi ,\delta _W\overline{\psi }=\kappa ie(\gamma _5B)\overline{\psi },\hfill \end{array}$$
$`(11)`$
the Lagrangian density (6b) (with $`m=0`$) transforms as: $`\delta _W_{}=\kappa _\mu [B^\mu ^\mu B]`$. Here $`\eta `$ and $`\eta ^{}`$ are the transformation parameters corresponding to the transformations $`\delta _B`$ and $`\delta _D`$ respectively. The generator for the above transformations is:

$$\begin{array}{ccc}W\hfill & =& 𝑑x\left[B(_1B+e\overline{\psi }\gamma _1\psi )(_1e\overline{\psi }\gamma _0\psi )\right],\hfill \\ & & 𝑑x\left[B\dot{}\dot{B}\right],\hfill \end{array}$$
$`(12)`$
where the latter expression for $`W`$ has been obtained due to the use of equation of motion: $`\epsilon ^{\mu \nu }_\nu +^\mu B=e\overline{\psi }\gamma ^\mu \psi `$. There are other simpler ways to derive the expression for $`W`$. For instance, it can be seen that anticommutator of $`Q_B`$ and $`Q_D`$ leads to the derivation of $`W`$ (i.e. $`\{Q_B,Q_D\}=W`$) if we exploit the basic (anti)commutators of equation (9). Furthermore, since $`Q_B`$ and $`Q_D`$ are generators for the transformations (3) and (7) respectively, it can be seen that the following relationships

$$\begin{array}{ccc}\delta _DQ_B\hfill & =& i\eta \{Q_B,Q_D\}=i\eta W,\hfill \\ \delta _BQ_D\hfill & =& i\eta \{Q_D,Q_B\}=i\eta W,\hfill \end{array}$$
$`(13)`$
lead to the definition and derivation of $`W`$. Together, all the above generators obey the following extended BRST algebra

$$\begin{array}{ccc}& & [W,Q_k]=0,k=g,B,D,AB,AD,\hfill \\ & & Q_B^2=Q_D^2=Q_{AB}^2=Q_{AD}^2=0,\{Q_D,Q_{AD}\}=0,\hfill \\ & & \{Q_B,Q_D\}=\{Q_{AB},Q_{AD}\}=W,\{Q_B,Q_{AB}\}=0,\hfill \\ & & i[Q_g,Q_B]=Q_B,i[Q_g,Q_{AB}]=Q_{AB},\hfill \\ & & i[Q_g,Q_D]=Q_D,i[Q_g,Q_{AD}]=Q_{AD},\hfill \end{array}$$
$`(14)`$
and the rest of the (anti)commutators are zero. Here $`Q_{AD}`$ is the anti-dual BRST charge which can be readily derived from (8) by the replacement :$`\overline{C}\pm iC`$. It is evident that the operator $`W`$ is the Casimir operator for the whole algebra. The mathematical aspects of the representation theory for the above kind of BRST algebra have been discussed in Refs. \[16-18\]. It will be noticed that the ghost number for $`Q_B`$ and $`Q_{AD}`$ is $`+1`$ and that of $`Q_D`$ and $`Q_{AB}`$ is $`1`$. Now, given a state $`|\varphi >`$ with ghost number $`n`$ in the quantum Hilbert space ( i.e. $`iQ_g|\varphi >=n|\varphi >`$), it can be readily seen, using the algebra (14), that

$$\begin{array}{ccc}iQ_gQ_B|\varphi >\hfill & =& (n+1)Q_B|\varphi >,iQ_gQ_{AD}|\varphi >=(n+1)Q_{AD}|\varphi >,\hfill \\ iQ_gQ_D|\varphi >\hfill & =& (n1)Q_D|\varphi >,iQ_gQ_{AB}|\varphi >=(n1)Q_{AB}|\varphi >,\hfill \\ iQ_gW|\varphi >\hfill & =& nW|\varphi >.\hfill \end{array}$$
$`(15)`$
This shows that the ghost numbers for the states $`Q_B|\varphi >`$ (or $`Q_{AD}|\varphi >`$), $`Q_D|\varphi >`$ (or $`Q_{AB}|\varphi >`$) and $`W|\varphi >`$ in the quantum Hilbert space are $`(n+1),(n1)`$ and $`n`$ respectively.

At this stage, it is worth mentioning that in Refs. \[19-21\], the analogous expressions for $`Q_B,Q_D,W`$ (cf. eqns.(3),(8),(12)) have been derived for the free 2D Abelian- and non-Abelian gauge theories (having no interaction with matter fields). Recently, these results have also been shown to exist for the free Abelian two-form gauge theory in $`(3+1)`$ dimensions of space-time . The topological properties of these free 2D theories have been shown to be encoded in the vanishing of the operator $`W`$ when equations of motion are exploited. On the contrary, as it turns out, the operator $`W`$ is defined off-shell as well as on-shell for the 2D interacting BRST invariant $`U(1)`$ gauge theory. This is because of the fact that even though $`U(1)`$ gauge field is topological (i.e. without any propagating degrees of freedom), it is coupled to the Dirac fields here and fermionic degrees of freedom are present in the off-shell as well as on-shell expression for $`W`$. Thus, the present theory is an example of an interacting topological field theory in 2D.

It is interesting to note that the algebra of $`Q_B,Q_D`$ and $`W`$ in equation (14) is exactly identical to the corresponding algebra for the exterior derivative ($`d,d^2=0`$), dual exterior derivative ($`\delta =\pm d,\delta ^2=0`$) and the Laplacian operator ($`\mathrm{\Delta }=(d+\delta )^2=d\delta +\delta d)`$ in the context of discussion of the de Rham cohomology . Furthermore, it can be readily seen that the operation of these generators on a state with ghost number $`n`$ (cf. eqn.(15)) is same as the operation of the above cohomological operators on a differential form of degree $`n`$. Thus, it is clear that the BRST cohomology can be defined comprehensively in terms of the above operators and Hodge decomposition theorem can be expressed cogently in the quantum Hilbert space of states where any arbitrary state $`|\varphi >_n`$ (with ghost number $`n`$) can be written as the sum of a harmonic state $`|\omega >_n`$ ($`W|\omega >_n=0,Q_B|\omega >_n=0,Q_D|\omega >_n=0`$), a BRST exact state ($`Q_B|\theta >_{n1}`$) and a co-BRST exact state ($`Q_D|\chi >_{n+1}`$). Mathematically, this statement can be expressed by the following equation §§§ This equation is the analogue of the Hodge decomposition theorem which states that, on a compact manifold, any arbitrary $`n`$-form $`f_n(n=0,1,2\mathrm{}..)`$ can be written as the sum of a harmonic form $`\omega _n`$ ($`\mathrm{\Delta }\omega _n=0,d\omega _n=0,\delta \omega _n=0`$), an exact form $`dg_{n1}`$ and a co-exact form $`\delta h_{n+1}`$ as: $`f_n=\omega _n+dg_{n1}+\delta h_{n+1}`$.

$$\begin{array}{ccc}|\varphi >_n=|\omega >_n+Q_B|\theta >_{n1}+Q_D|\chi >_{n+1}.\hfill & & \end{array}$$
$`(16)`$
It is obvious, therefore, that the above symmetry generators $`Q_B,Q_D`$ and $`W`$ have their counterparts in differential geometry as the de Rham cohomology operators $`d,\delta `$ and $`\mathrm{\Delta }`$ respectively  for the discussion of cohomological aspects of differential forms. It is a peculiarity of the BRST formalism that the above cohomological operators can be also identified with the generators $`Q_{AD},Q_{AB}`$ and $`W=\{Q_{AB},Q_{AD}\}`$ respectively. Thus, the mapping is: $`(Q_B,Q_{AD})d,(Q_D,Q_{AB})\delta ,W=\{Q_B,Q_D\}=\{Q_{AD},Q_{AB}\}\mathrm{\Delta }`$.

It will be very useful to explore the impact of this new symmetry in the context of symmetries of the Green’s functions for QED and derive the analogue of Ward-Takahashi identities. This new symmetry, being connected with the analogue of chiral transformation, is expected to play an important role in throwing some light on the 2D Adler-Bardeen-Jackiw anomaly in the framework of BRST cohomology and Hodge decomposition theorem. Furthermore, this symmetry might turn out to provide a key tool in proving the consistency and unitarity of the anomalous gauge theory in 2D (see, e.g., Refs.  and references therein). The generalization of this new symmetry to 2D non-Abelian gauge theory (having local gauge interaction with matter fields) is another future direction that can be pursued. The insights gained in these studies might provide a clue for the generalization of this new symmetry to physical four dimensional gauge theories. These are some of the issues under investigation and a detailed discussion will be reported elsewhere .