Interactive Functional-logic Programming by Conditional Term Rewriting Systems (Extended Abstract)

Makoto Hamana

Department of Intelligence Science and Technology, Kyoto University, Kyoto 606-8501, Japan

                          hamana@kuis.kyoto-u.ac.jp

Abstract

Functional-logic programming languages are an integration of functional and logic programming languages. We add side-effect feature to a functional-logic programming language without destructing referential transparency and give the operational semantics as conditional term rewriting. We formalize interactive functional-logic programs as universally quantified equations in Moggi’s computational metalanguage. To give operational semantics, we define a translation from the computational metalanguage to conditional term rewriting systems which preserves the semantics of the side-effect monad. The idea of the translation is based on the observation that the conditional part of conditional rewrite systems can be considered as a sequential computation part. We show the soundness of the translation and completeness of narrowing for solving equation with respect to interactive functional-logic programs.

1 Introduction

Functional-logic programming languages are an integration of functional and logic programming languages. For a recent overview of the field, see [5]. A first-order functional-logic program (abbreviated as FLP, hereafter) is given by equations of the same form as in functional programs, like

f(x) = x + 1.

Execution in functional-logic programming means to provide an equation called a query and to obtain values for variables contained in the query. For example, if we give the query

?−f(x) = 8

to a system of a functional-logic programming language, under the above program, the system returns the answer

x ↦ 7.

Modern functional-logic languages have a unified operational treatment of the functional and logic part of the execution and a clear view of mathematical semantics [5].

Operational semantics of a functional-logic programming language presented in the paper is based on conditional term rewriting. A program of the functional-logic language is regarded as a conditional term rewriting system and a query is considered to be the question for convertibility between the two sides of equations. To solve the query is to find substitutions that establish such convertibility. Conditional narrowing has been developed as a method for this purpose, which can be considered as an equational version of SLD-resolution. Since conditional narrowing is a sound and complete procedure for establishing this convertibility [7], the operational models of some existing functional logic languages are based on refined versions of conditional narrowing.

In this paper, we add interaction to a first-order functional-logic language and give the operational semantics by a translation. Here the word “interaction” is meant in the sense of Barendregt’s consideration of “interactive functional programming” [2]. More precisely, “interaction” means computation with side-effects outside of the programming environment, like file systems, user inputs, terminal outputs, etc. This kind of programming feature is necessary in realistic programs. The recent, most dominant styles of treating interaction in pure functional languages are

• the monadic style as in Haskell [12], and

• the explicit state passing style as in Clean [1].

The monadic style proposed by Wadler [12] is based on Moggi’s work on notions of computation in categorical framework using monads. But Wadler’s approach does not exactly match the original idea of Moggi, i.e., in the monadic style, Moggi’s semantics is implemented in pure functional programs. We think that this is the reason of some complication in the use of monads in functional programs. Hence, in our approach, we proceed as follows: We go back to the original idea of Moggi’s formalization of computations and follow it [8]:

(i) We extend the syntax of the first-order functional-logic language to the syntax of interactive first-order functional-logic programming language expressing sequential computations by introducing let-terms (Section 3,4).

(ii) Semantics of let-terms is given by the strong monad for side-effects [8].

(iii) We give a translation from a set of axioms of the computational metalanguage into a conditional term rewriting system (Section 5).

2 Preliminaries

We use standard notations and terminology of term rewriting [3]. We recall only some less common definitions concerning term rewriting. A term is linear if there is no multiple occurrence of the same variable. A conditional term rewriting system (CTRS) R is called 3-CTRS [7] if V(l) ∪ V(\overrightarrow{s_{i} = t_{i}}) ⊇ V(r) for every l → r ⇐ \overrightarrow{s_{i} = t_{i}}. A CTRS R is called properly oriented [11] if every l → r ⇐ \overrightarrow{s_{i} = t_{i}} ∈ R with V(l) ⊉ V(r) satisfies V(s_{i}) ⊆ V(l) ∪ ⋃_{j=1}^{i−1} V(t_{j}) for

all i ∈ \{1,…, n\}. A CTRS R is called right-stable if every l → r ⇐ \overrightarrow{s_{i} = t_{i}} ∈ R satisfies (V(l) ∪ ⋃_{j=1}^{i−1} V(s_{j} = t_{j}) ∪ V(s_{i})) ∩ V(t_{i}) = ∅ and t_{i} is either a linear constructor term or a ground normal form with respect to the system obtained by removing the conditions of rewrite rules, for every i = 1,…, n. The set of variables occurring in a syntactic object e is denoted by V(e). A sequence of syntactic objects e_{1},…, e_{n} is often abbreviated as \overrightarrow{e_{i}}.

3 The Computational Metalanguage

Moggi’s computational metalanguage [9] is a formal system designed for describing and reasoning about several kinds of computations, which includes partial computation, nondeterministic computations, computations with side-effects, exceptions and continuations. The computational metalanguage is an extension of many-sorted equational logic where the extensions are (i) the introduction of computational types, and (ii) the introduction of let-terms having the computational types.

The most important feature of the computational metalanguage is that it distinguishes between values and computations by types, and nests of let-terms express sequential computation. We extend Moggi’s computational metalanguage to include conditional and existentially quantified equations for syntax. We simply call such extended computational metalanguage the computational metalanguage.

Definition 3.1 A set S of sorts for the computational metalanguage is a set of types given by α ::= b | T α. We use the naming convention that α, α_{1},… denote types and b, b_{1},… denote base types. We think of T α as a type of computations of elements of type α and a base type as a type of values. A FLP signature Σ is an S-sorted signature which is divided into two disjoint sets Con and Fun, where Con is a set of constructor symbols and Fun is a set of function symbols. The raw terms are defined as follows:

t ::= x
| k
| f(t_{1},…, t_{n})
| [t]_{T}
| let x := t_{1} in t_{2}

where k is a constant symbol of zero arity and f a function symbol of non-zero arity n in the signature Σ. A typing context, usually written as Γ, Δ,…, is a finite sequence (x_{1}:α_{1},…, x_{n}:α_{n}) of (variable,sort)-pairs, where x_{i}’s are mutually different. The typing rules of terms are given in Figure 1. The set of all well-typed terms under Γ is denoted by T_{Σ}(Γ). Universally quantified conditional equation

∀Γ(s = t : α ⇐ s_{1} = t_{1}:β_{1}, ⋯, s_{n} = t_{n}:β_{n})

and existentially quantified equation

∃Δ(s_{1} = t_{1} : β_{1}, ⋯, s_{n} = t_{n} : β_{n})

are formulas of the computational metalanguage.

Definition 3.2 An assignment θ from Γ to a Σ-algebra A, denoted by θ : Γ → A, is an S-indexed family {θα : Xα → Aα | α ∈ S} of functions where Xα is a set of all variables of a sort α occurring in Γ. A substitution is an assignment θ : Γ → T_{Σ}(Γ′) to a term algebra (i.e. set of terms) T_{Σ}(Γ′). The substitution θ is obviously extended to θ^{#} on terms. We often write tθ instead of θ^{#}(t) for the application of substitutions. A substitution σ is often presented as the set {x_{1} ↦ t_{1}, . ., x_{n} ↦ t_{n}}, where σ(x_{i}) = t_{i} for i = 1, . ., n.

Definition 3.3 Let R is a set of universally quantified conditional equations called axioms. We write R ⊢_{cml} e where a theorem e is deduced from a set R of axioms and LET (Figure 3) by using the deduction rules of the computational metalanguage given in Figure 2.

(variable)_{\overline{Γ,x:α ▷ x:α}} (constant)_{\overline{Γ ▷ k:α}} k:α ∈ Σ
(term)\frac{Γ ▷ t_{1}:α_{1},...,Γ ▷ t_{n}:α_{n}}{Γ ▷ f(t_{1},...,t_{n}):β}
([ ])\frac{Γ ▷ t:α}{Γ ▷ [t]_{T}:Tα} (let)\frac{Γ ▷ s:Tα Γ,x:α ▷ t:Tβ}{Γ ▷ let x:=s in t:Tβ}

Figure 1: Typing rules of terms

(ax.)\frac{∀Γ(s_{1}θ=t_{1}θ:α_{1})···∀Γ(s_{n}θ=t_{n}θ:α_{n})}{∀Γ(sθ=tθ:α)}

for ∀Γ′(s = t : α ⇐ s_{1} = t_{1} : α_{1}, ⋯) ∈ R and for any substitution θ : Γ′ → T_{Σ}(Γ)

usual (reflexive),(symmetric),(transitive) and (congruence) rule for each f ∈ Σ.

(∃ intro.)\frac{∀∅(s_{1}θ=t_{1}θ:α_{1})···∀∅(s_{n}θ=t_{n}θ:α_{n})}{∃Δ(s_{1}=t_{1}:α_{1},···,s_{n}=t_{n}:α_{n})}

for any substitution θ : Δ → T_{Σ}

(perm. )\frac{∀Γ(s=t:α)}{∀Γ′(s=t:α)} ([ ].ξ)\frac{∀Γ(t_{1}=t_{2}:α)}{∀Γ([t_{1}]_{T} =[t_{2}]_{T}):Tα}

where Γ′ is a permutation of Γ

(let.ξ)\frac{∀Γ(t_{1}=t_{2}:Tα_{1}) ∀Γ,x:α_{1}(t′_{1}=t′_{2}:Tα_{2})}{∀Γ((let x:=t_{1} in t′_{1})=(let x:=t_{2} in t′_{2}):Tα_{2})}

Figure 2: Inference rules of the computational metalanguage

(ass) ∀Γ((let x_{2} := (let x_{1} := t_{1} in t_{2}) in t_{3})

= (let x_{1} := t_{1} in (let x_{2} := t_{2} in t_{3})) : T α_{3})

(let.β) ∀Γ((let x_{1} := [t]_{T} in t_{2}) = t_{2}[t]_{x_{1}} : T α_{2})

(unit) ∀Γ((let x_{1} := t_{1} in [t_{1}]_{T}) = t_{1} : T α_{1}).

Figure 3: Axiom schema LET

4 Interactive First-order FLPs Based on the Computational Metalanguage

In this section, we define interactive functional-logic programs as particular form of axioms of the computational metalanguage and queries as existentially quantified equations.

Definition 4.1 (Interactive first-order FLP) A set R of axioms is called an interactive FLP if R is a properly-oriented orthogonal 3-CTRS^{1} that satisfies the following conditions for each axiom ∀Γ(l = r ⇐ \overrightarrow{s_{i} = t_{i}}) in R:

(i) l is of the form f(t_{1},…, t_{n}) where f : b_{1},…, b_{n} → α ∈ Fun and t_{1},…, t_{n} are constructor terms.

(ii) If the type of r is a computational type, the conditional part must be empty.

(iii) All the equations s_{1} = t_{1},…, s_{n} = t_{n} are strict equations^{2} of the form steqα(s, t) = true on base types.

These syntactic conditions of FLPs are designed to be that narrowing is complete with respect to the translated CTRSs from interactive FLPs.

Execution of interactive FLPs is to prove the query, which is an existentially quantified equation, under the interactive FLP R as a set of axioms by obtaining answer substitutions using the deduction system of the computational metalanguage, i.e.

R ⊢_{cml} ∃Δ . \overrightarrow{s_{i} = t_{i}}.

The interpretaion of the type constructor T α is the monad for side-effect [8].

Example 4.2 We omit universal quantifications in examples. The following FLP is defining the two functions, i.e. readseq reads k-characters from the input channel and returns the list of them, and main reads five characters and then writes the third character of them into the output channel.

Sort set S:

Int, Unit, IntList, IO Int, IO Unit, …

Signature Σ

read : IO Int, write : Int → IO Unit, readseq : Int → IO IntList, main : IO Unit ∈ Fun () : Unit, :: : Int,IntList → IntList, [] : IntList ∈ Con nth : IntList,Int → Int, (and other built-in functions …) ∈ Fun Interactive FLP R

1An interactive FLP R is not a usual CTRS because it contains let-terms. However the definition of properly orientedness, orthogonality and type-3-ness are applicable to the interactive FLP of the following reasons:

• orthogonality only depends on the left-hand sides of R and they are non-let-terms,

• properly orientedness and type-3-ness are conditions on variable occurrences.

2The notion of strict equations is important in functional-logic languages, but in this paper the detail of definition is omitted because of the irrelevance to the interaction feature. The complete definition can be found in [4].

readseq(0) = [[]]IO readseq(k) = let n:=read in

let u := readseq(k-1) in [n::u]IO

main = let u:= readseq(5) in

let m:= [nth(u,3)]IO in write(m)

5 A Translation from Interactive FLPs to CTRSs

Next, we give the operational semantics for interactive FLPs. Moggi did not give a reduction based operational semantics. If we give such an operational semantics for the computational metalanguage directly, it may not be sufficient one because it seems to be no way to reduce let-terms to non-let-terms without specifying the interpretation of T.

So our strategy to give the operational semantics is to use term rewriting for evaluating, and narrowing for solving equations for interactive FLPs. Since an interactive FLP contains letterms, rewriting needs to handle let-terms. Instead of directly defining rewriting on let-terms, we first translate let-terms to usual conditional rewrite rules, and then use usual conditional term rewriting and narrowing. The reason for taking this approach is that if we use usual conditional term rewriting for interactive FLPs, soundness and completeness result of conditional narrowing can be obtained by using existing results. Since soundness and completeness of a solving method for queries are most important properties of FLP, we think that the translation approach we take here for interactive FLPs is convenient to ensure these properties without a complicated proof of completeness.

The ideas of the translation from interactive FLPs to CTRSs are the following:

• to be explicit “state passing variables” in function terms of a computational type T α, and

• to use the conditional part of a conditional rewrite rule for expressing sequential computation, instead of using a let-term in an interactive FLP.

The second idea comes from Suzuki et al.’s consideration of “conditions as where-clauses” and its justification in rewriting theory [11].

First we give a notion of normal form of let-terms, which is used in the translation. let-normal forms are well-typed terms given by the following grammar:

m ::= x | k | f(t_{1},…, t_{n}) | let x := t in m

where t_{1},…, t_{n}, t are well-typed non-let-terms. We can choose exactly one let-normal form that includes exactly the same let-binding variables m from the (α)-equivalence class of a let-normal form of s. We define the function normalize which maps any term to such chosen let-normal form.

Definition 5.1 Let R be an interactive FLP over an S-sorted FLP signature Σ. Define the new sort set S^{∘} generated by the following grammar:

S^{∘} ∋ α ::= b | St | b × St

where b ∈ S and St (the type of states) is new type not occurring in S. The translation ( )^{∘} from an interactive FLP R to a CTRS R^{∘} over the S^{∘}-sorted signature Σ^{∘} is defined in Figure 4. This translation function ( )^{∘} is overloaded for several syntactic objects, i.e., signatures, well-typed terms, rules and equations, and furthermore the auxiliary function ( )^{•} over rules and equations.

Example 5.2 The translated CTRS R^{∘} from the interactive FLP R presented in Example 4.2 is as follows.

readseq(0,s0) → [] readseq(S(k),s0) → ⟨n::u, s2⟩

⇐read(s0)=⟨n,s1⟩, readseq(k,s1)=⟨u,s2⟩ main(s0) → write(m,s2)

⇐readseq(s0)=⟨u,s1⟩, nth(u,3,s1)=⟨m,s2⟩

We easily obtain the following result.

Proposition 5.3 If R is an interactive first-order FLP over an interactive FLP signature Σ, then R^{∘} is a properly oriented 3-CTRS over a signature Σ^{∘}.

In order to use term rewriting as an operational semantics of functional-logic programming, confluence of CTRSs is an indispensable property (for example, to guarantee unique result). Suzuki et al. show that a properly oriented 3-CTRS is confluent [11] and conditional narrowing is complete for this class of CTRSs [10].

6 Soundness of the Translation ( )^{∘}

In this section, we show that the translation ^{∘} is a sound translation with respect to the deduction system of the computational metalanguage. We start by defining built-in interactive axioms.

Definition 6.1 (Built-in interactive axioms) Let R be an interactive FLP over the S-sorted signature Σ. An set R_{b} of axioms is called built-in interactive axioms if the following conditions are satisfied:

• R_{b} is a first-order FLP over S^{∘}-sorted signature Σ^{∘}.

• For each axiom l = r ∈ R_{b}, l has the form f(t_{1},…, t_{n}, s) where f : b_{1},…, b_{n}, St → α × St ∈ Fun, is called interactive function symbol.

• For any interactive function symbol f : b_{1},…, b_{n}, St → α×St and ground terms t_{1},…, t_{n}, there exist ground terms a : α, s : St such that

f(t_{1},…, t_{n}) →_{R^{∘}∪R_{b}}^{∗} ⟨a, s⟩.

Example 6.2 read, write in Example 4.2 are built-in interactive function symbols. An example of built-in interactive axioms for them are the following:

For signatures:

(k : b)^{∘} =^{def} k : b
(k : T β)^{∘} =^{def} k : St → β × St
(f : α_{1},…, α_{n} → b)^{∘} =^{def} f : α_{1},…, α_{n} → b
(f : α_{1},…, α_{n} → T β)^{∘} =^{def} f : α_{1},…, α_{n}, St → β × St
Σ^{∘} =^{def} {f^{∘} | f ∈ Σ} ∪ {⟨ , ⟩^{b} : b × St | base type b ∈ S}.

For well-typed terms:

(Γ ▷ t : b, s_{0})^{∘} =^{def} Γ ▷ t : b
(Γ ▷ x : T β, s_{0}) =^{def} (Γ ▷ x : β × St, ∅)
(Γ ▷ [t]_{T} : T β, s_{0})^{∘} =^{def} (Γ, s_{0} : St ▷ (t, s_{0}) : β × St, ∅)
(Γ ▷ f(t_{1},…, t_{n}) : T β, s_{0})^{∘} =^{def} (Γ, s_{0} : St ▷ f(t_{1},…, t_{n}, s_{0}) : β × St, ∅).

(Γ ▷ let x_{1} := a_{1} in … let x_{n} := a_{n} in t : T β, s_{0})^{∘}

=^{def} (Γ, s_{0} : St ▷ g(\overrightarrow{z_{i}}, s_{0}) : β × St,

\{g(\overrightarrow{z_{i}}, s_{0}) = (t, s_{n})^{∘} ⇐ (a_{1}, s_{0})^{∘} = ⟨x_{1}, s_{1}⟩,…, (a_{n}, s_{n−1})^{∘} = ⟨x_{n}, s_{n}⟩\})

For conditional rewrite rules of FLPs:

R^{∘} =^{def} {(∀Γ . l → r : α)^{∘} | ∀Γ . l → r : α ∈ R}.
(∀Γ . l → r : α)^{∘} =^{def} (∀Γ . l → normalize(r) : α)^{•}
(∀Γ . l → r : b)^{•} =^{def} ∀Γ . l → r : b
(∀Γ . l → t : T β)^{•} =^{def} ∀Γ, s_{0} : St . l′ → t′ : β × St

where (l′, ∅) =^{def} (l, s_{0})^{∘}, (t′, ∅) =^{def} (t, s_{0})^{∘}

(∀Γ ▷ l → let x_{1} := a_{1} in … let x_{n} := a_{n} in t : T β)^{•}
=^{def} ∀Γ, \overrightarrow{x_{i} : α_{i}}, \overrightarrow{s_{i} : St} . (l, s_{0})^{∘} → (t, s_{n})^{∘} : β × St

⇐ (a_{1}, s_{0})^{∘} = ⟨x_{1}, s_{1}⟩,…, (a_{n}, s_{n−1})^{∘} = ⟨x_{n}, s_{n}⟩ where t is a non-let-term.

Figure 4: Translation ( )^{∘} For equations:

(∀Γ . s = t : α)^{∘} =^{def} (∀Γ . normalize(s) = normalize(t) : α)^{•}
(∀Γ . s = t : b)^{•} =^{def} ∀Γ . s = t : b
(∀Γ . s = t : T β)^{•} =^{def} (∀Γ, s_{0} : St . s′ = t′ : β × St, δ_{1} ∪ δ_{2})

where (s′, δ_{1}) =^{def} (s, s_{0})^{∘} and (t′, δ_{2}) =^{def} (t, s_{0})^{∘}

(∃Δ . \overrightarrow{s_{i} = t_{i} : α_{i}})^{∘} =^{def} (\overrightarrow{e_{i}}, ⋃ δ_{i})
where (e_{i}, δ_{i}) =^{def} (normalize(s_{i}) = normalize(t_{i}))^{•} for each i
(s = t : b)^{•} =^{def} (s = t : b, ∅)
(s = t : T β)^{•} =^{def} (s′ = t′ : β × St, δ_{1} ∪ δ_{2})
where (s′, δ_{1}) =^{def} (s, s_{0})^{∘} and (t′, δ_{2}) =^{def} (t, s_{0})^{∘}.

Note:

• A typing context Γ is often omitted in ( )^{∘} for well-typed terms.

• s_{0},…, s_{n} are variables not occurring in Γ.

• g is a fresh function symbol and \{\overrightarrow{z_{i} : α_{i}}\} =^{def} V (let x_{1} := a_{1} in … let x_{n} := a_{n} in t) in the last clause of the translation of well-typed terms.

Figure 5: Translation ( )^{∘} (continued) read : IntList → Int × IntList read(n::s)=⟨n,s⟩ write : Int → Unit × IntList write(n,s)=⟨⟨⟩,n::s⟩

The translation ^{∘} is sound for existentially quantified theorem in the following sense.

Theorem 6.3 Let R be an interactive first-order FLP over an S-sorted signature Σ and R_{b} a set of built-in interactive axioms over an S^{∘}-sorted signature Σ^{∘}. If

R ⊢_{cml} ∃Δ . \overrightarrow{u_{i} = t_{i} : α_{i}}

with an answer substitution θ : Δ → T_{Σ}, then

R^{∘} ∪ δ ∪ ⋃ ζ_{j} ∪ R_{b} ⊢ ∃Δ . \overrightarrow{e_{i}}σ

for every (∃Δ . \overrightarrow{e_{i}}σ) ∈ E where

• σ : (s_{0}) → T_{Σ}

• (E, δ) =^{def} (∃Δ . \overrightarrow{u_{i} = t_{i} : α_{i}})^{∘}

• an answer substitution is θ^{∘} : Δ → T_{Σ^{∘}} such that θ^{∘}(x_{j}) =^{def} v, where Δ = (x_{1},…, x_{n}) and (v, ζ_{j}) =^{def} (θ(x_{j}), s_{0})^{∘} for each j = 1,…, n.

Proof See [4].

In terms of logic, many sorted conditional equational logic adding interactive built-in axioms and an interactive FLP R is, in some sense (because the form of theorems are slightly changed), a conservative extension of the computational metalanguage.

7 Interaction and Solving Equations

In this section, we discuss how interaction and solving in the interactive functional-logic language are related. In Section 6, we showed that the translation ^{∘} was sound translation. In view of solving of query, this result derive the completeness of narrowing with respect to interactive FLPs. We state this result below.

We introduce some terminology. A substitution θ : (x_{1} : α_{1},…, x_{n} : α_{n}) → T_{Σ}(Γ) is normalizable if for each i = 1,…, n, θ(x_{i}) has a normal form. For a normalizable substitution θ, θ↓_{R} denotes the normalized substitution defined by θ↓_{R} (x) =^{def} a where a is the normal form of θ(x). We write σ ≤ τ[Γ] if there exists a substitution ρ : Γ′ → T_{Σ}(Γ′′) such that ρ^{#} ∘ σ = τ. We write s ⇝_{ρ,R}^{∗} t for many-step conditional narrowing with the answer substitution ρ by using rules in the CTRS R. The definition, soundness and completeness of conditional narrowing for CTRSs are in [7].

Theorem 7.1 [Completeness of narrowing for interactive FLPs] Let R be an interactive first-order FLP over an S-sorted signature Σ, and R_{b} a set of built-in interactive axioms over an S^{∘}-sorted signature Σ^{∘}. Suppose

R ⊢_{cml} ∃Δ . \overrightarrow{u_{i} = t_{i} : α_{i}}

with an answer substitution θ : Δ → T_{Σ}. We apply Theorem 6.3. Let R′ = R^{∘} ∪ δ ∪ ⋃ ζ_{j} ∪ R_{b}. If the substitution θ^{∘} determined by Theorem 6.3 is a normalizable answer substitution with respect to R′, then for every (∃Δ . \overrightarrow{e_{i}}σ) ∈ E, we obtain the following narrowing derivation

\overrightarrow{e_{i}}σ ⇝_{ρ,R′}^{∗} ⊤

where ρ ≤ θ^{∘}↓_{R′} [Δ] and ⊤ denotes a sequence of the constant true. Proof

R ⊢_{cml} ∃Δ . \overrightarrow{u_{i} = t_{i} : α_{i}}
⇒ R′ ⊢ ∃Δ . \overrightarrow{e_{i}}σ (Theorem 6.3)
⇔ R′ ⊢ ∀∅ . \overrightarrow{e_{i}}σθ^{∘} by (∃ intro.) rule
⇔ e_{i}σθ^{∘} →_{R′}^{∗} true
⇒ e_{i}σ ⇝_{ρ,R′}^{∗} ⊤ where ρ ≤ θ^{∘}↓_{R′} [Δ].

The last implication follows from the completeness of narrowing for properly-oriented rightstable 3-CTRSs [11].

The above result says that we can obtain the answer substitution of a given query with respect to an interactive FLP by using conditional narrowing.

8 Conclusion and related work

In this paper we introduced interaction to a functional-logic language, which was a first attempt in the theory of functional-logic languages. We defined syntax of the language as an extension of Moggi’s computational metalanguage and took the monad for side-effects as the categorical semantics. The main contribution of this paper is to have given a translation from the computational metalanguage to a conditional term rewriting system and proven its soundness between two logics, i.e., the computational metalanguage and conditional equational logic. This result gives correct solving method of an existentially quantified equation having side-effect functions.

As related work, the functional-logic language Curry also has side-effects feature[6]. Curry use the monadic style for side-effects, which is exactly same as in Hakell. The advantage of proposed approach in this paper to Curry’s monadic style is

• simplicity of language which avoids complicated higher-order constructs in monadic style by using the idea of where-caluse as sequational computation with only first-order terms and

• direct applicability of existing several operational semantics for first-oder FLPs to interactive FLPs.

References

[1] Achten, P. and Plasmeijer, M.: The Ins and Outs of Concurrent Clean I/O, Journal of Functional Programming, Vol. 5,No. 1(1995), pp. 81–110.

[2] Barendreght, H.: Interactive Functional Programming, Proceedings of Second Fuji International Workshop on Functional and Logic Programming, World Scientific, 1996, pp. 192–193.

[3] Dershowitz, N. and Jouannaud, J.-P.: Rewrite Systems, Handbook of Theoretical Computer Science(van Leeuwen, J.(ed.)), Vol. B, The MIT Press/Elsevier, 1990, pp. 243–320.

[4] Hamana, M.: Semantics for Interactive Higher-order Functional-logic Programming, PhD Thesis, University of Tsukuba, 1998.

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

[6] Hanus, M., Antoy, S., Kuchen, H., Fraguas, F. J. L., Lux, W., Moreno-Navarro, J., and Steiner, F.: Curry: An Integrated Functional Logic Language, Oct 1999. Version 0.6.

[7] Middeldorp, A. and Hamoen, E.: Completeness Results for Basic Narrowing, Applicable Algebra in Engineering, Communication and Computing, Vol. 5,No. 3/4(1994), pp. 213–253.

[8] Moggi, E.: Computational Lambda-Calculus and Monads, LFCS ECS-LFCS-88-66, University of Edinburgh, 1988.

[9] Moggi, E.: Notions of Computation and Monads, Information and Computation, Vol. 93(1991), pp. 55–92.

[10] Suzuki, T.: Studies on Conditional Narrowing for Rewrite Systems with Extra Variables, PhD Thesis, University of Tokyo, 1998.

[11] Suzuki, T., Middeldorp, A., and Ida, T.: Level-Confluence of Conditional Rewrite Systems with Extra Variables in Right-Hand Sides, Proceedings of the 6th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science 914, 1995, pp. 179–193.

[12] Wadler, P.: Comprehending monads, ACM Conference on Lisp and Functional Programming, Nice, France, June 1990, pp. 61–78.