Overlapping Rules and Logic Variables in Functional Logic Programs^{⋆}

Sergio Antoy^{1} Michael Hanus^{2}

1 Computer Science Department, Portland State University, P.O. Box 751, Portland, OR 97207, U.S.A.

                             antoy@cs.pdx.edu

2 Institut für Informatik, CAU Kiel, D-24098 Kiel, Germany.

                        mh@informatik.uni-kiel.de

22nd International Conference on Logic Programming (ICLP06)

Seattle, WA, USA, August 17–20, 2006

\begin{matrix}c \\ ◯ \end{matrix} Springer-Verlag LNCS Vol. 4079, pages 87–101

Abstract. Functional logic languages extend purely functional languages with two features: operations defined by overlapping rules and logic variables in both defining rules and expressions to evaluate. In this paper, we show that only one of these features is sufficient in a core language. On the one hand, overlapping rules can be eliminated by introducing logic variables in rules. On the other hand, logic variables can be eliminated by introducing operations defined by overlapping rules. The proposed transformations between different classes of programs not only give a better understanding of the features of functional logic programs but also may simplify implementations of functional logic languages.

1 Motivation

Functional logic languages [20] integrate the best features of functional and logic languages in order to provide a variety of programming concepts. For instance, the concepts of demand-driven evaluation and higher-order functions from functional programming can be combined with logic programming features like computing with partial information (logic variables), constraint solving, and nondeterministic search for solutions. In contrast to purely functional languages, functional logic languages allow computations with overlapping rules (i.e., more than one rule can be applied to evaluate a function call) and logic variables (i.e., unbound variables occurring in the initial expression and/or rules, also called extra variables). Operationally, these features are supported by nondeterministic computation steps.

Functional logic languages are modeled by constructor-based term rewriting systems (TRS) with narrowing as the evaluation mechanism. A crucial choice in the design of a language, both at the source level and the implementation level, is the class of rewrite systems used to model the programs. Early languages (e.g., Babel [28] and K-Leaf [19]) were modeled by weakly orthogonal, constructor-based TRSs. Larger classes are more expressive, i.e., programs in

⋆ This work was partially supported by the German Research Council (DFG) grant Ha 2457/5-1 and the NSF grant CCR-0218224.

larger classes are textually shorter and/or conceptually simpler. Thus, modern languages, such as Curry [21, 23] and T OY [26], are modeled by the whole class of the constructor-based rewrite systems with extra variables. However, the implementation of a language modeled by a smaller class is likely to be simpler and/or more efficient.

For the above reason, program transformation among different classes of TRSs is an interesting research subject. The goal is to transform a program in the source language into an equivalent program in a language, referred to as the core language, that is conceptually simpler or could be implemented more efficiently. For example, the results of [5] show that any conditional constructorbased TRS can be transformed into an unconditional overlapping inductively sequential TRS [4]. The target class is a proper subclass of the source class, a situation that leads to conceptual and practial benefits. This paper studies two transformations similar to that described in [5] and with the same intent.

The first transformation maps the overlapping inductively sequential TRS with or without extra variables into the inductively sequential TRS with extra variables. This shows that if a language allows extra variables, then, at the core level, overlapping is not necessary. Of course, at the source level overlapping is a feature that contributes to the expressiveness of a language and therefore is desirable.

The second transformation eliminates logic variables from computations within the overlapping inductively sequential TRS. By “logic variables” we mean extra variables in rewrite rules and variables, which are free or unbound, in expressions to evaluate. A somewhat unexpected, though immediate, consequence of this transformation is that the power of narrowing computations can be obtained by mere rewriting. As for the previous transformation, at the source level logic variables contribute to the expressiveness of a language and therefore are desirable.

Loosely speaking, these results can be understood as the possibility to trade in a core language logic variables for a rather disciplined form of rule overlapping and vice versa. Section 2 reviews concepts and notations used in this paper. Section 3 defines the transformation that replaces overlapping with extra variables and states its correctness. Section 4 defines the transformation that replaces logic variables with overlapping and states its correctness. Section 5 offers our conclusion. The proofs of the results presented in this paper can be found in the full version of the paper [8].

2 Preliminaries

In this section we review some term rewriting [11, 18] notations and functional logic programming [20] concepts used in the remaining of this paper.

We consider a many-sorted signature Σ partitioned into a set C of constructors and a set F of (defined) functions or operations. We write c/n ∈ C and f/n ∈ F for n-ary constructor and operation symbols, respectively. Given a set of sorted variables X, the set of well-sorted terms and constructor terms are denoted by T (Σ, X) and T (C, X), respectively. We write Var(t) for the set of all the variables occurring in a term t. A term t is ground if Var(t) = ∅. A term is linear if it does not contain multiple occurrences of a variable. A term is operation-rooted (constructor-rooted) if its root symbol is an operation (constructor). We write \overline{o_{k}} for a sequence of objects o_{1}, …, o_{k}.

Example 1. In the following, we write datatype declarations in Curry syntax [23], i.e., a sort S is defined by enumerating its constructors in the form

data S = C_{1} s_{11} … s_{1a_{1}} | … | C_{n} s_{n1} … s_{na_{n}}

Thus, C_{i} is a constructor of sort S and arity a_{i} with argument sorts s_{i1}, …, s_{ia_{i}}. For instance, the sorts of Boolean values and natural numbers in Peano’s notation are defined as

  data Bool = True | False
  data Nat  = O | S Nat  □

A pattern is a linear term of the form f(t_{1}, …, t_{n}) where f/n ∈ F is an operation symbol and t_{1}, …, t_{n} are constructor terms. A constructor-based rewrite system is a set of pairs of terms or rewrite rules of the form

l → r

where l is a pattern and l and r are of the same sort. An operation f is defined by all the rewrite rules whose left-hand side is rooted by f. A functional logic program is a constructor-based rewrite system. Traditionally, term rewriting systems have the additional requirement Var(r) ⊆ Var(l). However, in functional logic programming variables occurring in Var(r) but not in Var(l), called extra variables, are often useful. Therefore, we allow rewrite rules with extra variables in functional logic programs. We denote the set of extra variables of a rewrite rule l → r, defined as Var(r)\Var(l), with Evar(l → r).

To formally define computations w.r.t. a given program, additional notions are necessary. A position p in a term t is represented by a sequence of natural numbers. Positions are used to identify specific subterms. Thus, t|_{p} denotes the subterm of t at position p, and t[s]_{p} denotes the result of replacing the subterm t|_{p} with the term s (see [18] for details). A substitution is an idempotent mapping σ : X → T (Σ, X) such that its domain Dom(σ) = {x | σ(x) ≠ x} is finite and x and σ(x) are of the same sort for all variables x. We denote a substitution σ by the finite set {x ↦ σ(x) | x ∈ Dom(σ)}. In particular, ∅ denotes the identity substitution. We denote by σ|_{V} the restriction of a substitution σ to a set of variables V. A (ground) constructor substitution σ has the property that σ(x) is a (ground) constructor term for all x ∈ Dom(σ). The composition σ ∘ η of two substitutions is defined by (σ ∘ η)(x) = η(σ(x)) for all variables x. Substitutions are extended to morphisms on terms in the obvious way. The subsumption ordering is a binary relation on terms defined by u ≤ v if there is a substitution σ with σ(u) = v. In this case, v is also called an instance of u. If, in addition, v is a (ground) constructor term, we call it (ground) constructor instance. If u ≤ v and v ≤ u, then u and v differ only for a renaming of variables.

We write u < v if u ≤ v and v ≰ u. A unifier of two terms s and t is a substitution σ such that σ(s) = σ(t). The unifier σ is most general if for any other unifier σ′ there exists a substitution η with σ′ = σ ∘ η. Furthermore, we denote by s ⊲ t the most general unifier of s and t restricted to Var(s).

A rewrite step t →_{p,l→r,η} t′ w.r.t. a given rewrite system R is defined if there are a position p in t, a rule l → r ∈ R with fresh variables, and a substitution η with t|_{p} = η(l) such that t′ = t[η(r)]_{p}. We impose the condition on the freshness of the variables since we allow extra variables in rewrite rules. The indices in the notation of a rewrite step are omitted when inconsequential. →^{+} and →^{∗} denote the transitive and reflexive-transitive closure of the relation →, respectively.

Functional logic languages compute solutions of free variables occurring in expressions by instantiating these variables to constructor terms so that a rewrite step becomes applicable. The combination of variable instantiation and rewriting is called narrowing. Formally, t ⇝_{σ} t′ is a narrowing step if σ(t) →_{p,l→r,η} t′ where σ is a substitution, t|_{p} is not a variable, and Dom(η) ⊆ Var(l). We denote by t_{0} ⇝^{∗}_{σ} t_{n} a sequence of narrowing steps t_{0} ⇝_{σ_{1}} … ⇝_{σ_{n}} t_{n} with σ = σ_{1}∘⋯∘σ_{n} (if n = 0 then σ = ∅). We omit the substitution in the notation of both narrowing steps and sequences when irrelevant to the discussion.

The requirement that Dom(η) ⊆ Var(l), as in [5], ensures that no extra variable in a rule is instantiated during a narrowing step. An extra variable in a rewrite rule is generally intended as a place holder for any term, e.g., see [12] where extra variables are allowed in the conditions of rewrite rules. In constructor-based rewrite systems, a more suitable convention should allow an extra variable to stand only for constructor terms, since terms that cannot be reduced to a constructor term are intended as errors. By contrast, requiring that extra variables remain uninstantiated in a rewrite step appears as treating extra variables as constants, thus foregoing the computational power that they provide. However, when computations are performed by narrowing, particularly using an efficient strategy, it seems most sensible to avoid instantiating extra variables in the step that introduces them. The reason is that these variables become logic variables in subsequent steps and therefore may be narrowed. The advantage of instantiating them in a narrowing step after they are introduced, as opposed to instantiating them in the step that introduces them, is that the latter would have no information on choosing useful instantiations, whereas the former could instantiate them with choices useful to perform a step. In particular, efficient strategies such as [4, 7] will instantiate logic variables only as far as necessary to perform needed steps. This level of specialization seems impossible to achieve at the time extra variables are introduced, unless the step introducing them performs some kind of lookahead.

For an example of the expressiveness of code using extra variables, consider the following definition (in Curry syntax) of an operation that computes the last element of a list:

    last l | l =:= x++[e] = e  where x,e free

where “++” denotes the concatenation of lists. Narrowing instantiates the extra variables x and e to satisfy the equation. The instantiation of e is the result of the computation.

Narrowing is implemented by a strategy intended to limit the steps of an expression to a small set that suffices to ensure the completeness of the results. An important narrowing strategy, needed narrowing [7], is defined on the subclass of the inductively sequential TRSs. This class can be characterized by definitional trees [3] that are also useful to formalize and implement demand-driven narrowing strategies. Since only the left-hand sides of rules are important for the applicability of needed narrowing, the following formulation of definitional trees [4] considers patterns partially ordered by subsumption.

A definitional tree of an operation f is a non-empty set T of linear patterns partially ordered by subsumption having the following properties:

Leaves property: The maximal elements of T, called the leaves, are exactly the (variants of) the left-hand sides of the rules defining f. Non-maximal elements are also called branches.

Root property: T has a minimum element, called the root, of the form

f(x_{1}, …, x_{n}) where x_{1}, …, x_{n} are pairwise distinct variables. Parent property: If π ∈ T is a pattern different from the root, there exists a

unique π′ ∈ T, called the parent of π (and π is called a child of π′), such that π′ < π and there is no other pattern π′′ ∈ T (Σ, X) with π′ < π′′ < π.

Induction property: All the children of a pattern π differ from each other only at a common position, called the inductive position, which is the position of a variable in π.^{3}

An operation is called inductively sequential if it has a definitional tree. Traditionally, it is also required that the rules do not contain extra variables [7]. Here, we relax this requirement: A TRS is inductively sequential with extra variables (ISX ) if all its defined operations are inductively sequential. Purely functional programs and the vast majority of functions in functional logic programs are inductively sequential.

Example 2. The following operations are inductively sequential w.r.t. the datatype declarations of Example 1:

  leq(O,x)  → True
  leq(S(x),O)  → False
  leq(S(x),S(y)) → leq(x,y)
  cond(True,x) → x
  nine → S(S(S(S(S(S(S(S(S(0)))))))))

The operation smallnum denotes a number less than ten and is defined by an ISX rule containing an extra variable x:

3 There might exist distinct definitional trees of an operation. In this case one can use any tree for computing a needed narrowing step of a term since the need of the step does not depend on the selected tree.

  smallnum → cond(leq(x,nine),x)  □

Functional logic languages extend purely functional languages by allowing overlapping rules. We are interested only in a disciplined form of overlapping. Two distinct rewrite rules l_{1} → r_{1} and l_{2} → r_{2} are called overlapping if the left-hand sides l_{1} and l_{2} are variants of each other, i.e., they are equal by subsumption. We denote the set of all rules with the same left-hand side l by the single (meta) rule l → r_{1} ? ⋯? r_{k}, where “?” is a meta symbol and r_{1}, …, r_{k} are the righthand sides. A TRS is overlapping inductively sequential (OIS) if all its defined operations are inductively sequential when overlapping rules with identical lefthand sides are joined into a single rule as above. The purpose of this paper is to show that an ISX program executed by narrowing can be transformed into an OIS program executed by rewriting and vice versa, i.e., the classes ISX and OIS loosely speaking have the same expressiveness.

Next, we define the needed narrowing strategy on inductively sequential rewrite systems.

Definition 1. Let R be an inductively sequential TRS where each function symbol has a uniquely associated definitional tree. We define the function λ from operation-rooted terms to sets of triples (position, rule, substitution) as follows. Let t = f(t_{1}, …, t_{n}) be an operation-rooted term, T the definitional tree associated to f, and π a maximal pattern of T that unifies with t. Then λ(t) is the least set satisfying

λ(t) ∋ \begin{cases}(Λ, π → r, t⊲ π) & if π is a leaf of T and π → r \\ & is a variant of a rewrite rule \\ (q · p, R, η ∘ σ) & if π is a branch of T, \\ & where q is the inductive position of π, \\ & η = t⊲ π, and (p, R, σ) ∈ λ(η(t|_{q})) \end{cases}
□

In each recursive step during the computation of λ, a position and a substitution is composed with the results computed by the recursive call. Thus, each needed narrowing step can be represented as (p_{1} ⋯ p_{k}, R, σ_{1} ∘ ⋯ ∘ σ_{k}), where p_{k} = Λ, p_{j} is an inductive position for all j ∈ {1, …, k − 1}, and σ_{j} a most general unifier restricted to the term variables computed in each recursive call for all j ∈ {1, …, k}. This representation of a needed narrowing step is called its canonical decomposition.

Proposition 1 ([4]). Let R be an overlapping inductively sequential TRS and t an operation-rooted term. If (p, l → r, σ) ∈ λ(t), then t ⇝_{p,l→r,σ} σ(t[r]_{p}) is a needed narrowing step, also denoted by t ⇝^{NN}_{p,l→r,σ} σ(t[r]_{p}).

The need of the step computed by λ in Proposition 1 is modulo the nondeterministic choice of the right-hand side. The term t cannot be narrowed to a constructor term without a step at p with a rule l → r′. However, it may be possible that r ≠ r′.

3 Eliminating Overlapping Rules

In this section we show that using rules with multiple right-hand sides does not increase the expressiveness of a functional logic language already providing inductively sequential rewrite systems with extra variables. For this purpose, we introduce a transformation from OIS into ISX systems and prove that needed narrowing computes the same results on the original and the transformed system.

Definition 2 (Transformation from OIS into ISX). We define a transformation OE (Overlapping Elimination) on TRSs. Non-overlapping rewrite rules are not changed. Overlapping rewrite rules of the form f(\overline{t_{n}}) → r_{1} ? ⋯? r_{k} are replaced by a single rule f(\overline{t_{n}}) → f′(y, \overline{x_{l}}) where Var(\overline{t_{n}}) = \{x_{1}, …, x_{l}\}, y is a new free variable, and f′ is a new function symbol defined by the new rules

f′(I_{1}, \overline{x_{l}}) → r_{1}
⋮
f′(I_{k}, \overline{x_{l}}) → r_{k}

The constants I_{j} are the elements of a new index type defined by

    data Ix = I_{1} | · · · | I_{k}

In practice, one can use the same index type (e.g., natural numbers) for all the rules. □

The transformation only adds new function and constructor symbols. Thus, every term w.r.t. the original signature is also a term w.r.t. the transformed signature. In the following, we denote the original TRS by R and the transformed TRS by R′ = OE(R).

Example 3. Consider an operation parent that nondeterministically returns either the mother or the father of the argument:

    parent(x) → mother(x) ? father(x)

The OE transformed program is:

    data Iparent = I0 | I1
    parent(x) → parent'(y,x)
    parent'(IO,x) → mother(x)
    parent'(I1,x) → father(x)  □

Proposition 2. If R is overlapping inductively sequential, then the transformed system R′ is inductively sequential with extra variables.

The transformation is correct if, loosely speaking, any result computed by the original program can be computed by the transformed program and vice versa. This concept is formulated by the next theorem. The soundness is based on the fact that any narrowing step in the original system can be simulated in the transformed system by either the same step or two consecutive steps using the introduced rules. The completeness is based on the fact that every needed narrowing step in the transformed system that introduces a function symbol not occurring in the signature of the original system is immediately followed by a needed narrowing step that removes that symbol.

Theorem 1 (Correctness of OE). Let R be a OIS TRS, R′ = OE(R), and t, s terms of R. The following claims hold.

Soundness If t ⇝^{NN *}_{σ′} s w.r.t. R′, then there exists a derivation t ⇝^{NN *}_{σ} s w.r.t. R

such that σ =_{Var(t)} σ′. Completeness If t ⇝^{NN *}_{σ} s w.r.t. R, then there exists a derivation t ⇝^{NN *}_{σ′} s w.r.t.

R′ such that σ =_{Var(t)} σ′.

4 Eliminating Logic Variables

In the previous section, we have shown that the class of the inductively sequential TRSs with extra variables, ISX, is at least as expressive as the class of the overlapping inductively sequential TRSs, OIS. This result is interesting because it enables us to trade in the implementation of a language the complications of overlapping, or multiple right-hand sides, for the presence of extra variables. Since we already allow extra variables in the OIS programs, we simply eliminate overlapping in the transformation.

In this section, we present a somewhat complementary result. We show that the overlapping inductively sequential TRSs, without extra variables, denoted OIS^{−}, are at least as expressive as the ISX programs. We use a transformation that eliminates unbound variables entirely, i.e., also from the “top-level” or initial term being evaluated. Therefore, a computation in the OIS^{−} programs is by rewriting, not narrowing. This result is interesting because it enables us to trade in the implementation of a language the complications of narrowing, in particular the use of substitutions, for the presence of multiple right-hand sides in the program rules.

As for the OE transformation, a functional logic program is an overlapping inductively sequential, many sorted, constructor-based TRSs with extra variables. This time, though, our goal is to eliminate extra variables, instead of overlappings. Thus, we denote with XE, extra variable elimination, this transformation. For any sort S, we consider a constant operation, instanceOfS, that enumerates the values of the sort S. We call this operation a generator of S.

Definition 3 (instanceOf). Let S be a sort defined by a datatype declaration of the form

data S = C_{1} t_{11} … t_{1a_{1}} | … | C_{n} t_{n1} … t_{na_{n}}

The operation instanceOfS is defined by the overlapping rules

    instanceOfS → C_{1}(instanceOft_{11},. . .,instanceOft_{1a_{1}})

? …

                 ? C_{n}(instanceOft_{n1},. . .,instanceOft_{na_{n}})  □

If S is a primitive or builtin sort, e.g., integers or characters, then we will assume that the operation instanceOfS is primitive or builtin as well. However, the following example shows that generators of primitive sorts, even infinite ones, can be coded by ordinary rules.

Example 4. Suppose that a sort “tree of integers” is defined by

    data TreeInt = Leaf | Branch Int TreeInt TreeInt

the generator of TreeInt is

    instanceOfTreeInt
       → Leaf
        ? Branch(instanceOfInt,instanceOfTreeInt,instanceOfTreeInt)

Below are two plausible ordinary definitions of the generator of the integers:

    instanceOfInt → 0 ? genNeg ? genPos
    genNeg → -1 ? genNeg - 1
    genPos → 1 ? genPos + 1

or also

    instanceOfInt → gen(0)
    gen(x) → if x>=0 then x ? gen(-(x+1))
                       else x ? gen(-x)

□

In the following, we consider only ordinary rewrite systems over algebraic datatypes. For such systems, Definition 3 immediately implies the following prop-

erty of instanceOf.

Lemma 1 (Completeness of generators). For every ground constructor term t of sort S, there exists a rewrite sequence of instanceOfS to t.

The XE transformation replaces any free variable v in a term with an operation that evaluates to any value that could instantiate the variable v during a computation.

Definition 4 (Extra variable elimination). Let V be a set of (sorted) variables. Then the instantiation substitution IO_{V} is defined as

IO_{V} = {x ↦ instanceOfs_{x} | x ∈ V has sort s_{x}}

For every term t we define

XE(t) = IO_{Var(t)}(t) □

The following lemma extends Lemma 1 to terms with variables.

Lemma 2. For every variable x and constructor term u of the same sort,

XE(x) →^{∗} XE(u).

Definition 5 (Transformation from OIS into OIS^{−}). Let R be an OIS program. We define XE(R) = R′ ∪ I, where I defines a fresh symbol instanceOfS for every sort S in the signature of R, and l → r′ is a rule of R′ iff l → r is a rule of R and r′ = IO_{Evar(l→r)}(r). □

Proposition 3. If R is an overlapping inductively sequential TRSs, then XE(R) is an overlapping inductively sequential TRSs without extra variables.

To claim the correctness of the XE transformation, we need to show that, under appropriate conditions and qualifications, every computation in the original system has a corresponding computation in the transformed system and vice versa. First, we discuss the completeness of XE. We state the completeness for narrowing derivations that compute constructor substitutions.

Lemma 3 (Completeness of XE derivations). Let R an OIS program. For any term t and constructor term u, if t ⇝^{∗} u w.r.t. R where the substitution of each narrowing step is a constructor substitution, then for any ground constructor instance v of u, XE(t) →^{∗} v w.r.t. XE(R).

The evaluation of expressions with free variables, particularly in the tradition of logic programming, produces variable bindings. These bindings are lost by the XE transformation. We will discuss how to recover this information after introducing new concepts that simplify the problem.

For narrowing derivations with arbitrary substitutions, the proof of Lemma 3 fails since instanceOf rewrites only to constructor terms. To extend the proof to obtain a more general result, we need to consider a variation of instanceOf defined as follows:

    instanceOfS → s_{1}(instanceOft_{11},. . .,instanceOft_{1a_{1}})

? …

                 ? s_{n}(instanceOft_{n1},. . .,instanceOft_{na_{n}})

where {s1, …, s_{n}} are all the signature symbols of sort S and the arguments of s_{i} have sorts t_{i1}, …, t_{ia_{i}}. However, this extension is not relevant in practice since narrowing strategies used in functional logic languages compute only constructor substitutions [6, 7].

In general, the transformation XE is not sound, i.e., there are rewrite derivations in the transformed system that have no correspondence in the original system.

Example 5. Consider the following program defining an operation that evaluates to an arbitrary even number:

  even → x+x

Applying XE to this program yields:

  even → instanceOfInt + instanceOfInt

Consequently, the term even can be evaluated as follows:

  even → instanceOfInt + instanceOfInt →^{+} 0 + 1 → 1  □

This examples shows that all the occurrences of an instanceOf operation originating from the same variable should be reduced to the same value. Derivations where this condition is satisfied are called admissible. We will show that the XE transformation is sound for admissible derivations.

The problem in the previous example would be eliminated by having only one occurrence of instanceOfInt. Therefore, we introduce a notation of terms where only one occurrence is represented so that the derivation above is no longer possible. Our notation uses pairs ⟨t, χ⟩ of a term t and a substitution χ which represents the term χ(t). The substitution χ will be defined as IO_{Var(t)} so that it contains a single occurrence of an instanceOf operation for each free variable of t. An example of this representation, using the familiar let notation for defining substitutions, is shown in Display (1). We define rewrite steps on this representation. A redex may occur in either t or χ. Rewriting in t corresponds to standard rewriting, whereas a rewrite step in χ may correspond to a multistep [24] in χ(t) if the bound variable has several occurrences in t.

Definition 6 (Transformation to term/substitution pairs). For every term t we define XEP(t) = ⟨t, IO_{Var(t)}⟩. For every OIS program R we define XEP(R) = R′ ∪ I, where I is as in Definition 5, and l → r′ is a rule of R′ iff l → r is a rule of R and r′ = ⟨r, IO_{Evar(l→r)}⟩. □

Definition 7 (Rewriting on term/substitution pairs). Let R be an OIS program and XEP(R) = R′ ∪ I. Let t be a term and XEP(t) = ⟨t, χ⟩. We define a rewrite step on XEP(t) as follows. ⟨t, χ⟩ → ⟨t′, χ′⟩ if one of the following conditions holds:

(type-1 step) there exist a position p in t, a variant l → ⟨r, ψ⟩ with fresh variables of a rule in R′, a substitution σ such that Dom(σ) ⊆ Var(l), σ(l) = t|_{p},

t′ = t[σ(r)]_{p}, and χ′ = χ|_{Var(t′)} ∪ ψ

(type-2 step) there exist a variable v ∈ Dom(χ) with χ(v) = instanceOfS and a rule

        instanceOfS → c(instanceOfS_{1}, . . . , instanceOfS_{k})

according to Definition 3 such that t′ = {v ↦ c(v_{1}, …, v_{k})}(t), χ′ = (χ\{v ↦ instanceOfS}) ∪ {v_{i} ↦ instanceOfS_{i} | i = 1, …, k} where v_{1}, …, v_{k} are fresh variables.

□

The term/substitution representation is an appealing formalism for this problem because it can be directly mapped to let binding constructs available in many programming languages. For instance, the transformed program of Example 5 can be coded in Curry [23] with a let binding as

     even = let x = instanceOfInt in x+x  (1)

The semantics of the let binding construct is defined in such a way that all occurrences of let bound variables are replaced by the same replacement [1, 25] (efficiently implemented by sharing). Our notion of rewriting is a natural adaptation of this semantics.

Theorem 2 (Correctness of XEP). Let R be a OIS TRS, R′ = XEP(R), t, s terms of R, and t′ = XEP(t). Then the following claims hold.

Soundness If t′ →^{∗} ⟨v, ν⟩ is a derivation w.r.t. R′, then there exists a narrowing derivation t ⇝^{∗} u w.r.t. R with u ≤ ν(v). In particular, if ν(v) is a constructor term, then ν = ∅ and u is a constructor term.

Completeness If t ⇝^{∗} s w.r.t. R, then there exists a derivation t′ →^{∗} s′ w.r.t. R′ such that s′ = XEP(s). In particular, if s is a constructor term, then there exists a derivation t′ →^{∗} ⟨v, ∅⟩ w.r.t. R′ for any ground constructor instance v of s.

The proof of this theorem relies on a commutativity property of reductions and transformations. More precisely, given an ordinary term t, the result of transforming t into a term/substitution pair and reducing it is equivalent to computing some reduction sequence of t and transforming the final reduct into a term/substitution pair.

The above results show that, loosely speaking, variables and overlapping rules have the same computational power in a functional logic language. To keep track of the binding of logic variables replaced by the XEP transformation, we transform the initial term t of a computation into a tuple (t, x_{1}, …, x_{n}) where x_{1}, …, x_{n} are the variables of t. The evaluation of the tuple will be (e, b_{1}, …, b_{n}) where e is the computed value and b_{1}, …, b_{n} constitute the computed answer. A remaining obstacle is that bindings may contain variables whereas in our approach b_{1}, …, b_{n} are ground. To overcome this obstacle, one may adopt the convention that an occurrence of instanceOf is only evaluated if its value is necessary to perform a type-1 step. Observe that type-1 steps are never performed in b_{1}, …, b_{n}.

The size of search space of a computation is roughly the same in both systems. In XEP(R) an occurrence of an instanceOf operation is evaluated only when demanded by its context. This evaluation corresponds to a step in which some variable v is instantiated in R. There is a small difference in favor of R, though, which is difficult to quantify. If the evaluation of an occurrence of instanceOf is demanded by an incompletely defined operation, some replacement of instanceOf may have no corresponding binding for v.

5 Conclusion

We have presented two transformations on functional logic programs. The first transformation eliminates overlapping rules by introducing auxiliary functions and extra variables. Together with the results of [5], this transformation shows that any functional logic program can be mapped into an inductively sequential TRS with extra variables so that it can be executed by needed narrowing. Hence, the class ISX is a reasonable core language for functional logic programming. The second transformation completely eliminates logic variables from functional logic computations by replacing them with operations defined by overlapping rules.

The correctness of this transformation requires the consistent evaluation of these new operations w.r.t. the logic variable occurrences. This can be achieved by sharing which is usually available in lazy languages.

The results presented in this paper provide a better understanding of the features of functional logic languages and their interactions. Although the source level of such languages extend purely functional languages by overlapping rules and extra variables, our results show that only one of these alternative concepts is enough for a core language.

Apart from these theoretical considerations, our results have also a practical interest since a simplified core language can reduce the implementation effort it requires. For instance, typical implementations of core languages are based on abstract machines that bridge the gap between the source level and the hardware (e.g., [9, 22, 27]). Usually, these machines provide instructions and data structures to support the implementation of both overlapping rules and logic variables. Our results enable the simplification of these abstract machines. For instance, specific instructions to handle computations that use overlapping rules need not be considered in an abstract machine if the OE transformation is applied in the compilation process. This is done in the implementations described in [15, 30], although without any formal justification. Likewise, the handling of logic variables (e.g., data structures such as binding arrays and binding instructions) can be removed if the XEP transformation is applied. Which of the two alternatives is more convenient depends on the concrete architecture of the machine. A simplified core language can also reduce the effort to build tools for functional logic languages. For instance, recent tools for debugging functional logic programs (e.g., tracers [14], profilers [13], slicers [29]) or program optimization (e.g., partial evaluation [2]) are based on a core language that supports both overlapping rules and logic variables which could be simplified using our results. The effects that each transformation may have on the efficiency of the execution of a program are a subject for future investigation.

After submitting this paper, we received from Paco López-Fraguas a draft [17] describing a transformation substantially identical to our XEP. They prove theoretical results very similar to ours but within the framework of CRWL, and present some benchmarks that show that eliminating logic variables does not incur any substantial efficiency loss.

Finally, the XEP transformation also sheds some new light on the role of logic variables in declarative programming. It has been sometimes argued (in the functional programming community) that the instantiation of a logic variable during a computation is similar to a side effect due to its global visibility. For instance, this has led to the modeling of logic variables as references in Haskell [16]. However, our results show that the binding of a logic variable can be also interpreted as the stepwise evaluation of an operation so that the power of narrowing computations can be obtained by rewriting.

We have presented our results for a first-order many-sorted functional logic language. The extension, with standard approaches (e.g., see [10, 31]), to higherorder programs presents no difficulties. The extension to polymorphically typed languages is not so obvious since the XEP transformation assumes that the type of each logic variable is known at compile time. This information is always available in a many-sorted TRS but could be difficult to obtain in a polymorphic functional logic language where logic variables might have an arbitrary type. In this case, one could define a specific “polymorphic” instanceOf operation that evaluates to values of all possible types. However, this is not practical due to an increase of the search space size and the possibility of ill-typed expressions during a computation. An appropriate solution to this problem is a topic for future research.

References

1. E. Albert, M. Hanus, F. Huch, J. Oliver, and G. Vidal. Operational Semantics for Declarative Multi-Paradigm Languages. Journal of Symbolic Computation, Vol. 40, No. 1, pp. 795–829, 2005.

2. E. Albert, M. Hanus, and G. Vidal. A Practical Partial Evaluator for a Multi-Paradigm Declarative Language. Journal of Functional and Logic Programming, Vol. 2002, No. 1, 2002.

3. S. Antoy. Definitional Trees. In Proc. of the 3rd International Conference on Algebraic and Logic Programming, pp. 143–157. Springer LNCS 632, 1992.

4. S. Antoy. Optimal Non-Deterministic Functional Logic Computations. In Proc. International Conference on Algebraic and Logic Programming (ALP’97), pp. 16– 30. Springer LNCS 1298, 1997.

5. S. Antoy. Constructor-based Conditional Narrowing. In Proc. of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2001), pp. 199–206. ACM Press, 2001.

6. S. Antoy. Evaluation Strategies for Functional Logic Programming. Journal of Symbolic Computation, Vol. 40, No. 1, pp. 875–903, 2005.

7. S. Antoy, R. Echahed, and M. Hanus. A Needed Narrowing Strategy. Journal of the ACM, Vol. 47, No. 4, pp. 776–822, 2000.

8. S. Antoy and M. Hanus. Overlapping Rules and Logic Variables in Functional Logic Programs. Technical Report 0608, Christian-Albrechts-Universität Kiel, 2006.

9. S. Antoy, M. Hanus, J. Liu, and A. Tolmach. A Virtual Machine for Functional Logic Computations. In Proc. of the 16th International Workshop on Implementation and Application of Functional Languages (IFL 2004), pp. 108–125. Springer LNCS 3474, 2005.

10. S. Antoy and A. Tolmach. Typed Higher-Order Narrowing without Higher-Order Strategies. In Proc. 4th Fuji International Symposium on Functional and Logic Programming (FLOPS’99), pp. 335–352. Springer LNCS 1722, 1999.

11. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

12. J.A. Bergstra and J.W. Klop. Conditional Rewrite Rules: Confluence and Termination. Journal of Computer and System Sciences, Vol. 32, No. 3, pp. 323–362, 1986.

13. B. Braßel, M. Hanus, F. Huch, J. Silva, and G. Vidal. Run-Time Profiling of Functional Logic Programs. In Proceedings of the International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR’04), pp. 182–197. Springer LNCS 3573, 2005.

14. B. Braßel, M. Hanus, F. Huch, and G. Vidal. A Semantics for Tracing Declarative Multi-Paradigm Programs. In Proceedings of the 6th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP’04), pp. 179–190. ACM Press, 2004.

15. B. Braßel and F. Huch. Translating Curry to Haskell. In Proc. of the ACM SIGPLAN 2005 Workshop on Curry and Functional Logic Programming (WCFLP 2005), pp. 60–65. ACM Press, 2005.

16. K. Claessen and P. Ljunglöf. Typed Logical Variables in Haskell. In Proc. ACM SIGPLAN Haskell Workshop, Montreal, 2000.

17. J. de Dios Castro and F.J. López-Fraguas. Elimination of Extra Variables in Functional Logic Programs. Personal communication, 2006.

18. N. Dershowitz and J.-P. Jouannaud. Rewrite Systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Vol. B, pp. 243–320. Elsevier, 1990.

19. E. Giovannetti, G. Levi, C. Moiso, and C. Palamidessi. Kernel LEAF: A Logic plus Functional Language. Journal of Computer and System Sciences, Vol. 42, No. 2, pp. 139–185, 1991.

20. M. Hanus. The Integration of Functions into Logic Programming: From Theory to Practice. Journal of Logic Programming, Vol. 19&20, pp. 583–628, 1994.

21. M. Hanus. A Unified Computation Model for Functional and Logic Programming. In Proc. of the 24th ACM Symposium on Principles of Programming Languages (Paris), pp. 80–93, 1997.

22. M. Hanus and R. Sadre. An Abstract Machine for Curry and its Concurrent Implementation in Java. Journal of Functional and Logic Programming, Vol. 1999, No. 6, 1999.

23. M. Hanus (ed.). Curry: An Integrated Functional Logic Language (Vers. 0.8.2).

Available at http://www.informatik.uni-kiel.de/~curry, 2006.

24. G. Huet and J.-J. Lévy. Computations in Orthogonal Rewriting Systems. In J.- L. Lassez and G. Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson, pp. 395–443. MIT Press, 1991.

25. J. Launchbury. A Natural Semantics for Lazy Evaluation. In Proc. 20th ACM Symposium on Principles of Programming Languages (POPL’93), pp. 144–154. ACM Press, 1993.

26. F. López-Fraguas and J. Sánchez-Hernández. TOY: A Multiparadigm Declarative System. In Proc. of RTA’99, pp. 244–247. Springer LNCS 1631, 1999.

27. W. Lux and H. Kuchen. An Efficient Abstract Machine for Curry. In K. Beiersdörfer, G. Engels, and W. Schäfer, editors, Informatik ’99 — Annual meeting of the German Computer Science Society (GI), pp. 390–399. Springer, 1999.

28. J.J. Moreno-Navarro and M. Rodríguez-Artalejo. Logic Programming with Functions and Predicates: The Language BABEL. Journal of Logic Programming, Vol. 12, pp. 191–223, 1992.

29. C. Ochoa, J. Silva, and G. Vidal. Dynamic Slicing Based on Redex Trails. In Proc. of the ACM SIGPLAN 2004 Symposium on Partial Evaluation and Program Manipulation (PEPM’04), pp. 123–134. ACM Press, 2004.

30. A. Tolmach, S. Antoy, and M. Nita. Implementing Functional Logic Languages Using Multiple Threads and Stores. In Proc. of the Ninth ACM SIGPLAN International Conference on Functional Programming (ICFP’04), pp. 90–102. ACM Press, 2004.

31. D.H.D. Warren. Higher-order extensions to PROLOG: are they needed? In Machine Intelligence 10, pp. 441–454, 1982.