Algebraic Semantics for Higher-order Functional-Logic Programming

Makoto Hamana Doctral Program in Engineering, University of Tsukuba, Tsukuba 305, Japan E-mail: hamana@score.is.tsukuba.ac.jp

ABSTRACT

In this paper we give a semantics of higher-order functional-logic programming in the framework of typed universal algebra. The functional-logic language concerned here is an applicative term rewriting system in which there is no lambda abstraction mechanism. Therefore ordinary first-order narrowing can be used to solve higher-order query. The soundness and completeness of narrowing for both the initial and minimal applicative Herbrand model is shown. We discuss the requirements of “minimal” for applicative Herbrand model, which means that any elements in the domain must have denotations of some terms, is need to obtain the completeness of narrowing in the applicative case of functional-logic programming.

1. Introduction

Semantics of first-order functional-logic programming has been deeply investigated. Two approaches are known for giving semantics. One approach is based on term rewriting. In this approach, a program of functional-logic languages is regarded as a conditional term rewriting system [10, 1], a query as satisfiability of an equation with respect to the underlying equational theory. Since conditional narrowing is a sound and complete procedure for establishing convertibility [9], operational models of some existing functional-logic languages are based on (refined version of) conditional narrowing, e.g., ALF [8], Ev [6].

The other approach is to extend declarative semantics of logic programming languages. This approach was first described by Levi et al. [11] for their logic plus functional language K-LEAF. In this approach, a program is to define (partial) functions on the complete Herbrand universe that contains infinite data structures and solving a query is finding a substitution that is a solution for the query in the least complete Herbrand model. The language BABEL [14] also has the semantics along this approach. Sound and complete operational models for these languages were given.

Recently higher-order extensions of functional-logic languages are investigated. The language SFL [4][5], which is a higher-order extension of BABEL, has the form of applicative equations for a program. Two semantics for SFL were proposed in [4]. One is the “declarative semantics” of SFL which has essentially the semantics along the declarative approach described above, where a slight difference is that each element in the Herbrand universe has applicative form. The other is the “denotational semantics” of SFL which is a also declarative approach essentially but the Herbrand universe is extended to the universe that contains function spaces because functions are used as data in higher-order programming.

The rewriting approach for semantics of higher-order functional-logic language is given in [15]. In this approach, a program is an applicative term rewriting system and the presented narrowing calculus for higher-order functional-logic programming is shown to be sound and complete for proving convertibility generated from applicative term rewriting, which is actually first-order.

The semantics presented in this paper is a further development of both SFL’s “denotational” approach [4] and applicative term rewriting approach [15]. We treat a program as an applicative term rewriting system in operational semantics, i.e., first-order conditional narrowing is used to solve a higher-order query. For algebraic semantics, first we present the initial model in a class of all models of a program as the quotient of convertibility generated from the applicative term rewriting. Next we give another model, which is called “minimal applicative Herbrand model”. The carrier of this model contains function spaces, which is similar to the “denotational semantics” of SFL. The important difference compared with it is that our semantics is sound and complete for operational model of narrowing unlike SFL’s “denotational semantics”. This desirable result comes from the minimality of applicative Herbrand model in our semantics defined in Section 5.

The paper is organized as follows. In Section 2, we define the syntax of a functional-logic language Ev. In Section 3, we construct the initial model, called quotient applicative term model, of Ev by a quotient of congruence generated from term rewriting. In Section 4, we review first-order conditional narrowing and apply its soundness and completeness results to the quotient applicative term model. In Section 5, we construct the minimal applicative Herbrand model and discuss why minimality is required in order to obtain the completeness of solving higher-order query under an applicative term rewriting system. In Section 6, we establish soundness and completeness of operational model of narrowing for the minimal applicative Herbrand model. In Section 7, we conclude the paper.

2. Syntax of a Higher-order Functional-Logic Language Ev

In this section we define syntax of a higher-order functional-logic language Ev. The language of Ev is generated from many-sorted signature. We use the notation and terminology of higher type universal algebra [12].

Definition 2.1 [Many-sorted Algebra] A set S of sorts and B of type basis are any nonempty set. A set S of sort is a type structure S over a type basis B if S = B ∪ {σ → τ | σ, τ ∈ S}. Each element σ ∈ S is termed a type; each element σ ∈ B and each element of the form σ → τ ∈ S are termed a base type and function type respectively. For simplicity, we assume a type basis B is always a singleton set {o} where the type o is the only base type. The theory developing in this paper will be straightforwardly extended to the case that B is any nonempty set. An S-sorted signature F is an S^{∗} × S indexed collection of disjoint sets F = {F^{w,τ} | w ∈ S^{∗}, τ ∈ S} where S^{∗} denotes the set of all sequences generated from S.

An S-sorted F-algebra is a pair ⟨A, F_{A}⟩, consisting of an S-indexed collection A = {A^{τ}|τ ∈ S} of non-empty carrier sets A^{s} and an indexed collection F_{A} = {F_{A}^{w,s} | w ∈ S^{∗}, τ ∈ S} of sets of operations. For each sequence of sorts w = σ_{1}… σ_{n} ∈ S^{∗} and each sort s ∈ S, F_{A}^{w,τ} = {f_{A} | f ∈ F^{w}, τ ∈ S}, where f_{A} : A^{σ^{1}}×… ×A^{σ^{n}} → A^{τ}. An S-sorted homomorphism from an S-sorted algebra A to B is an S-indexed family of mapping ϕ^{σ} : A→B such that for each σ ∈ S, each w = σ_{1}, …, σ_{n} ∈ S^{∗}, any function symbol f ∈ F^{w,σ} and any a_{1}, …, a_{n} ∈ A^{w}, ϕ^{σ}(f_{A}(a_{1}, …, a_{n})) = f_{B}(ϕ^{σ^{1}}, …, ϕ^{σ^{n}}). An S-typed signature F is an S-sorted signature F such that for each function type (σ → τ) ∈ S we have an application symbol ap^{σ→τ} ∈ F^{σ→τσ,τ}. Let F be an S-typed signature. An F-algebra A is an S-typed algebra if for each function type (σ→τ) ∈ S, the following conditions are satisfied:

• A^{σ→τ} ⊆ (A^{σ} → A^{τ}),

• ap_{A}^{σ→τ} : A^{σ→τ} × A^{σ} → A^{τ}, ap_{A}^{σ→τ}(f, t) = f(t).

Definition 2.2 [Applicative Terms] Let S be a type structure. We will use a notation∘^{n} which denotes n-curried function type o→… →o where → is right associative. We assume that S-typed signature F is a disjoint union of Con, Fun and {{ap^{σ→τ}} | σ, τ ∈ S} where Fun = {Fun^{σ} | σ ∈ S} and Con = {Con^{σ} | n ∈ ℕ, σ = o^{n} → o}; Fun^{σ} is a set of defined function symbols with type σ and Con^{σ} is a set of constructor symbols with type σ. A defined function symbol is called function symbol for short, hereafter.

A set Var of variables is an S-indexed collection of disjoint sets Var = {Var^{s} | s ∈ S}. An applicative term t of type σ, denoted by t : σ, is obtained by applying the following rules finitely many times:

\overline{c : σ} for each c ∈ Con^{σ} \overline{f : σ} for each f ∈ Fun^{σ}

\overline{x : σ} for each x ∈ Var^{σ} \frac{s : σ → τ, t : σ}{ap^{σ→τ}(s, t) : τ}

The set AT (Var) of all applicative terms is an S-indexed collection AT (Var) = {AT (Var)^{σ} | σ ∈ S} of disjoint sets AT (Var)^{σ} of all applicative terms of a type σ. We use curried notation for an applicative terms, for example, we write f 0 1 as ap(ap(f, 0), 1). A term that does not contain any occurrence of a defined function symbol is called data term.

An assignment ϕ is a mapping from a set of variables X to an S-sorted F-algebra A and often presented as {x_{1} ↦t_{1}, ⋯, x_{n} ↦t_{n}}, where [σ](x_{i}) = t_{i} for each x_{i} ∈ X, i = 1, ⋯, n. Especially, an assignment from X to a subset AT (Y) of terms is called substitution. The assignment ϕ is uniquely extended to a homomorphism ϕ^{#} from AT (X) to A as follows:

ϕ^{#}(f) = f_{A},  f ∈ Fun,
ϕ^{#}(c) = c_{A},  c ∈ Con,
ϕ^{#}(x) = ϕ(x),  x ∈ Var,
ϕ^{#}(ap^{σ→τ}(t_{1}, t_{n})) = ap_{A}^{σ→τ}(ϕ^{#}(t_{1}), ϕ^{#}(t_{n})).

Definition 2.3 [Applicative Equations] Let s, t ∈ AT (X)^{σ} and s_{1}, …, s_{n} ∈ AT (X)^{o} where σ ∈ S and X ⊆ Var. A conditional equation is a formula of the form

∀X(s = t ⇐ s_{1} = true, ⋯, s_{n} = true).

We always assume the set X of quantified variables is exactly the set of variables occurring in the body of formula. We often write the quantified variables X as the sequence x_{1} : σ_{1}, …, x_{n} : σ_{n} which denotes x_{1} ∈ Var^{σ^{1}}, …, x_{n} ∈ Var^{σ^{n}}. An existentially quantified equation is a formula of the form

∃X(s = t).

A conditional equation ∀X(s = t ⇐ s_{1} = t_{1}, ⋯, s_{n} = t_{n}) is valid in an S-sorted F-algebra A, or A is a model of the conditional equation, denoted by A ⊧ ∀X(s = t ⇐ s_{1} = t_{1}, ⋯, s_{n} = t_{n}), if for all assignments α : X → A, α^{#}(s) = α^{#}(t) whenever α^{#}(s_{i}) = α^{#}(t_{i}) for all i = 1, ⋯, n. An existentially quantified equation ∃X(s = t) is valid in A, denoted by A ⊧ ∃X(s = t), if there exists an assignment α : X →A, called a witness, such that α^{#}(s) = α^{#}(t). An F-algebra A is a model of a set of conditional equations E if for all conditional equations ∀X(s = t ⇐ s_{1} = t_{1}, ⋯, s_{n} = t_{n}) in E, A ⊧ ∀X(s = t ⇐ s_{1} = t_{1}, ⋯, s_{n} = t_{n}). The notation E ⊧ ∀X(s = t) means that for any model A of E, A ⊧ ∀X(s = t). Likewise the notation E ⊧ ∃X(s = t) means that for any model A of E, A ⊧ ∃X(s = t).

Next we define strict equality. We intend that “data” in functional-logic programming are data terms. Therefore we need a computable equality on data terms. We define “built-in” axioms for any programs to express such an equality in the following.

Hereafter we assume an S-sorted signature for functional-logic programs is equipped with symbols true ∈ Con^{o} and steq, & ∈ Fun^{o→o→o}.

Definition 2.4 [Strict Equality] We write “&” as an infix operator that is right associative. We define a set of equations R_{Con} as follows:

R_{Con} =^{def} {∀∅(steq c c = true) | c ∈ Con^{o}}
∪ \{ \begin{matrix}∀x_{1}, ⋯, x_{n}, y_{1}, ⋯, y_{n} : o \\ (steq(d x_{1} ⋯ x_{n})(d y_{1} ⋯ y_{n})) \\ = (steq x_{1} y_{1}) & ⋯ & (steq x_{n} y_{n})) | d ∈ Con^{o^{n}→o}\} \end{matrix}

∪ {∀x : o(true & x = x)},

We call an equation of the form (steq s t) = true, where the terms s and t do not contain any occurrence of steq, strict equation and the induced equality from R_{Con} strict equality.

Definition 2.5 [Functional-Logic Program] A set R of applicative conditional equations is a program if for each equation ∀X(l = r ⇐ c) in R the following conditions are satisfied:

1. R contains the axioms for strict equality R_{Con}.

2. A variable occurring in r always occurs in l.

3. l is linear, i.e., it does not contain multiple occurrences of the same variables.

4. l is the form f t_{1} ⋯ t_{n} where f ∈ Fun^{σ^{1}→···→σ^{n}→σ} and the terms t_{1} : σ_{1}, ⋯, t_{n} : σ_{n} do not contain function symbols, i.e., each term is built from only variables and constructors.

5. R is non-ambiguous. That is, in this case, for any two different equations ∀X_{1}(l_{1} = r_{1} ⇐ c_{1}) and ∀X_{2}(l_{2} = r_{2} ⇐ c_{2}) in R, l_{1} and l_{2} are not unifiable.

6. All equations in the conditional part c are strict equations.

Note that any functional-logic program as defined above is confluent because the conditional term rewriting system obtained from a functional-logic program by interpreting the conditional equations as conditional rewrite rules is an orthogonal III_{n}^{a} type-2^{b} conditional term rewriting system [1].

Definition 2.6 [Query and Execution of Functional-Logic Program] Let R be a program and s, t ∈ AT (X) where X is a finite subset of Var. A query is an existentially quantified strict equation of the form

∃X(steq s t = true).

aThe terminology “III_{n}” means that each equations in the conditions is the form t = d where d is a closed normal form with respect to the system obtained by removing the conditions [1].

bThe terminology “type-2” means that a conditional term rewriting system R may only contain extra variables in the conditions [13]

Execution of a functional-logic program R is to prove that the validity of the query

R ⊧ ∃X(steq s t = true)

is valid by obtaining a witness of the existential equation.

Example 2.7 Let the symbols plus ∈ Fun^{o→o→o}, map ∈ Fun^{(o→o)→o→o} and Nil, 0 ∈ Con^{o}, S ∈ Con^{o→o}, Cons ∈ Con^{o→o→o}. Following is an example of program consisting of an addition function on encoded natural numbers and “map” function over list.

R = \{ \begin{matrix}∀y : o & (plus 0 y = y) \\ ∀x, y : o & (plus (S x) y = S (plus x y)) \\ ∀f : o → o & (map f Nil = Nil) \\ ∀f : o → o, x, xs : o & (map f (Cons x xs) \\ & = Cons (f x) (map f xs) \end{matrix} \} .

Under the program R, examples of a query are:

R ⊧ ∃z : o(steq (plus (S 0) z) (S z)) = true,

or

R ⊧ ∃f : o → o (steq (map f [0, (S 0)]) [S 0, S (S 0)] = true).

Operational and algebraic semantics presented in this paper will be concerned with this kind of query where solutions are not only of base types but also of function types.

3. Quotient Applicative Term Model

In this section we construct the initial model of Ev by a quotient of congruence generated from term rewriting. For an program R conditional term rewriting [1] is defined.

Definition 3.1 [Conditional Term Rewriting] A rewrite relation →_{R} on applicative terms AT (Var) for a program R between applicative terms are inductively defined as follows:

→_{R_{0}}  =^{def} ∅,
→_{R_{n+1}}  =^{def} \{ \begin{matrix}⟨C[lθ], C[rθ]⟩ | & ∀X(l = r ⇐ s_{1} = true, …, s_{k} = true) ∈ R, \\ & θ : X → AT (Var), C is a context, \\ & s_{i}θ →_{R_{n}}^{∗} true for every i = 1, …, k\}, \end{matrix}

→_{R} =^{def} ⋃_{n∈ℕ} →_{R_{n+1}}.

Here →^{∗} denotes the reflexive and transitive closure of →. We can easily check rewriting by →_{R} preserves sort, i.e., if s ∈ AT (Var)^{σ} and s →∗_{R} t then t ∈ AT (Var)^{σ}.

Definition 3.2 [Quotient Applicative Term Algebra] Let R be a program. Define the equivalence relation ↔_{G(R)}^{∗} =^{def} ↔∗_{R} ∩AT (∅) × AT (∅) where ↔∗_{R} is the reflexive, transitive and symmetric closure of →∗_{R}. The ↔∗_{R}- equivalence class of a term t ∈ AT (∅) is denoted by [t], namely [t] =^{def} {s ∈ AT (∅) | s ↔_{G(R)}^{∗} t}. The quotient applicative term algebra AQ_{R} is a pair ⟨AT (∅)/↔_{G(R)}^{∗} , F_{AQ_{R}}⟩, consisting of an S-indexed collection AT (∅)/↔_{G(R)}^{∗}= {AT (∅)^{σ}/↔_{G(R)}^{∗}| σ ∈ S} of carrier sets and an indexed collection F_{AQ_{R}} = {F_{AQ_{R}}^{w,σ} | w ∈ S^{∗}, σ ∈ S} of operations. For each sequence of sorts w = σ_{1}… σ_{n} ∈ S^{∗} and each sort σ ∈ S,

F_{AQ_{R}}^{w,σ} =^{def} {f_{AQ_{R}} | f ∈ F^{w,σ},
f_{AQ_{R}} : (AT (∅)^{σ^{1}}/↔_{G(R)}^{∗})×… ×(AT (∅)^{σ^{n}}/↔_{G(R)}^{∗})
→(AT (∅)^{σ}/↔_{G(R)}^{∗})
f_{AQ_{R}}([t_{1}], ⋯, [t_{n}]) = [f(t_{1}, ⋯, t_{n})]}.

Note that the applicative term algebra AT (∅) a many-sorted term algebra. So from the result of many-sorted algebra [3], the quotient AQ_{R} is the initial model of the class of all models of R. Moreover, a version of Herbrand theorem [3] also holds. We state an applicative version of their result in the following.

Theorem 3.3 [Herbrand’s Theorem for Applicative Equations] The quotient applicative term algebra AQ_{R} is a model of a program R. Moreover the following propositions hold:

R ⊧ ∃X(steq s t = true)
⇔ AQ_{R} ⊧ ∃X(steq s t = true)
⇔ AQ_{R} ⊧ ∀∅((steq s t)θ = true) for some θ : X → AT (∅)
⇔ (steq s t)θ →∗_{R} true.

4. Operational Model of Narrowing

We use first-order narrowing as an operational model of Ev. First-order narrowing can also work in higher-order functional-logic language Ev. Because, as noted before, applicative terms are syntactically first-order terms.

Definition 4.1 [Conditional Narrowing] Let R be a program and S, T be terms that are conjunction (by the function symbol & ) of strict equations or true’s. Narrowing relation ⇝ on AT (Var) is defined as follows: S ⇝_{θ} T if there exists a non-variable position u ∈ Pos(S), a new variant (with respect to variable-renaming) ∀X(l = r ⇐ steq s_{1} t_{1} = true, ⋯, steq s_{n} t_{n} = true) of a conditional equation in R, and a substitution θ such that

• θ is a most general unifier of S_{|u} and l,

• T = (S[r]_{u} & (steq s_{1} t_{1}) & ⋯ & (steq s_{n} t_{n}))θ.

We write S ⇝_{θ}^{∗} T if there exists a narrowing derivation (S ≡)S_{1} ⇝_{θ_{1}} S_{2} ⇝_{θ_{2}} ⋯ ⇝_{θ_{n−1}} S_{n}(≡ T) such that θ = θ_{n−1}∘⋯∘θ_{2}∘θ_{1}.

Conditional narrowing defined above is sound and complete for rewriting presented below. We use the completeness result of conditional narrowing with respect to sufficiently normalizable solution for orthogonal type-2 conditional term rewriting systems with strict equality obtained by Ida and Okui [9]. We adapt their result to our setting.

Theorem 4.2 [Soundness and Completeness of Conditional Narrowing for Rewriting] Let R be a program and ∃X(steq s t = true) a query. Conditional narrowing is sound for rewriting, i.e., if (steq s t) ⇝_{θ}^{∗} true where θ : X → AT (Z) then (steq s t)θ →∗_{R} true. Moreover conditional narrowing is complete for rewriting, i.e., for arbitrary normalized substitution^{c} θ : X → AT (Z), if (steq s t)θ →∗_{R} true then there exists a narrowing derivation (steq s t) ⇝_{θ′}^{∗} true where θ′ : X → AT (Y) such that ρ∘θ′ = θ for any ρ : Y → AT (Z).

Combining Theorems 3.3 and 4.2, we get the soundness and completeness of narrowing with respect to the quotient applicative term model.

Theorem 4.3 Let R be a program and ∃X(steq s t = true) a query. The query AQ_{R} ⊧ ∃X(steq s t = true) is valid with a witness γ : X → AQ_{R} such that for each x ∈ X, an equivalence class γ(x) contains a normal form if and only if there exits a narrowing derivation (steq s t) ⇝_{θ}^{∗} true with a normalized substitution θ : X → AT (Y). In the both direction of the implication, AQ_{R}[[ ]]∘ρ∘θ = γ holds for any substitution ρ : Y → AT (∅) where the mapping AQ_{R}[[ ]] is the unique homomorphism from AT (∅) to AQ_{R}.

5. Minimal Applicative Herbrand Model

We construct another model, called minimal applicative Herbrand model. This model provides the following natural meaning of a higher-order functional-logic program:

cA substitution θ is called normalized if for all x ∈ X, xθ is a normal form.

• Data in higher-order functional-logic programming are (infinite) data terms and functions (not function symbols) defined by a program of an applicative term rewriting system.

• Functions in a higher-order functional-logic programming are partial functions on the domain of data.

• A query of a higher-order functional-logic programming is an existentially quantified strict equation which can contain function type variable as quantified variables.

Soundness and completeness of narrowing with respect to the minimal applicative Herbrand model shows that such intuitive explanations are completely correct.

Definition 5.1 [Applicative Herbrand Universe] An applicative Herbrand universe H^{o} is a set of finite and infinite binary trees that is deduced from the following deduction rules.

\overline{c : σ} for each c ∈ Con^{σ}  \overline{⊥ : o}  \frac{s : σ → τ, t : σ}{s t [figure: ap^{σ→τ}] : τ}

H^{o} =^{def} {t | t : o is derived by the above rules}.

The set of finite trees in H^{o} exactly corresponds to the set of all ground data terms with the type o by identifying a tree as a term. Applying the above deduction rules infinitely many times, infinite trees are deduced.

Definition 5.2 [Applicative Herbrand Algebra] Let F = Con∪Fun∪{{ap^{σ→τ}} | σ, τ ∈ S} be an S-typed signature. An S-typed Falgebra A = ⟨H, F_{A}⟩ is an applicative Herbrand algebra if its carrier is an S-indexed collection H = {H^{σ} | σ ∈ S} where the base type carrier is H^{o} and the function type carrier H^{σ→τ} is the set (H^{σ} → H^{τ}) of all continuous functions for each function type σ → τ. The operations F_{A} satisfy the following:

Con_{A}^{o^{n}→o} = {c_{A} | c ∈ Con^{o^{n}→o}, c_{A} ∈ H^{o^{n}→o}, c_{A} t_{1} ⋯ t_{n} = c t_{1} ⋯ t_{n}},
Fun_{A}^{σ→τ} = {f_{A} | f ∈ Fun^{σ→τ}, f_{A} ∈ H^{σ→τ}, f_{A} is a continuous function }

for each σ, τ ∈ S.

In the definition of applicative Herbrand algebra, the operations for function symbols are not specified, only defined as some continuous functions. So an S-typed algebra A that can be a model of a program is an algebra that has suitable set of functions for Fun_{A} corresponding to the program.

Definition 5.3 Let A be an applicative Herbrand algebra. For each σ ∈ S the order ⊑_{H}^{σ} on H^{σ} is defined as:

• For the base type o, ⊑_{H}^{o} is a usual approximation ordering on trees,

• For each function type (σ → τ) ∈ S, ⊑_{H}^{σ}^{→}^{τ} is a usual pointwise ordering on functions.

Define HA as the class of all applicative Herbrand algebra and an order ⊑_{HA} on HA as:

A ⊑_{HA} B ⟺^{def} f_{A} ⊑_{H}^{σ} f_{B} for each f ∈ F^{σ}.

Proposition 5.4 For each σ ∈ S, ⟨H^{σ}, ⊑_{H}^{σ} ⟩ and ⟨HA, ⊑_{HA} ⟩ are algebraic^{d} cpos.

We denote the least elements of the cpos H and HA by ⊥_{H} and ⊥_{HA}.

Definition 5.5 [Construction of the Least Applicative Herbrand Model] Let F be an S-typed signature and R be a program. Define an operator T_{R} : HA→HA as:

T_{R}(A) =^{def} ⟨H, {{ap_{A}^{σ→τ}} | σ, τ ∈ S} ∪ Con_{A}
∪ {{Φ_{A}(f) ∈ H^{σ} | f ∈ Fun^{σ}} | σ ∈ S}⟩

where for each f ∈ Fun^{σ^{1}→...→σ_{n}→τ}, a mapping Φ_{A}(f) : H^{σ^{1}}→… →H^{σ^{n}} → H^{τ} is defined as:

Φ_{A}(f)(h_{1}) ⋯ (h_{n}) =^{def} \{ \begin{matrix}δ^{#}(r) & if & ∃( ∀X(f l_{1} ⋯ l_{n} = r \\ & ⇐ s_{1} = true, ⋯, s_{n} = true ) ∈ R, \\ & ∃δ : X → A, \\ & ∀i ∈ \{1, ⋯, n\}; h_{i} = δ^{#}(l_{i}), \\ & ∀i ∈ \{1, ⋯, m\}; δ^{#}(s_{i}) = true, \\ ⊥_{H} & otherwise. \end{matrix}

The operator T_{R} is a continuous function on HA. This can be proved by showing that each construct of T_{R} are continuous. By the fixpoint theorem on cpos, T_{R} has the least fixpoint expressed as follows:

AH_{R}′ =^{def} ⨆_{i∈N} T_{R}^{i}(⊥_{HA}).

dA domain D is algebraic if for all x ∈ D, the set S_{x} = {z | z ⊑ x and z is compact} is directed and x = ⨆ S_{x}.

Theorem 5.6 AH_{R}′ is the least (with respect to ⊑_{HA} ) applicative Herbrand model of a program R. Proof It is proven in the same way as the first-order case [2],[7].

The carrier of AH_{R}′ contains many elements that cannot be denoted by applicative terms. For example, consider a program R = {∀x : o(id x = x)} and a query

R ⊧ ∃f : o → o(steq (f 1) 1 = true)

where the signature F = Con ∪ Fun and Con^{o} = {1}, Fun^{o→o} = {id}. A witness of the above query in AH_{R}′ is ξ = {f ↦id_{AH_{R}}′} : {f} → AH_{R}′ where id_{AH_{R}}′ ∈ H^{o→o} is an identity function on H^{o}. The witness ξ can be “represented”as a substitution θ = {f ↦id}. This means that the system of the functional-logic language Ev can return an answer for the query as the form of the applicative term.

On the other hand, there exits another witness for the above query, which is ζ = {f ↦α} where a function α ∈ H^{o→o} defined as α(x) = 1 ∈ H^{o}. But the witness ζ can not be represented by a substitution because the function α ∈ H^{o→o} is not a denotation of any applicative term constructed from the signature F.

This unsatisfactory result is caused by the definition of the carrier of function types. In this example, since the carrier H^{o→o} is defined as the set of all continuous functions on (H^{o} → H^{o}), α is an element of H^{o→o}, so α is a witness of that query. However, in order to obtain the answer substition corresponding the witness of queries, we will exclude such α from the admissible witnesses that cannot be represented by substitutions to applicative terms. By minimizing the carriers of AH_{R}′ that only contain elements that can be denoted by applicative terms, this suitable model is obtained.

Definition 5.7 Let R be a program. The S-typed F-algebra AH_{R} is the homomorphic image of the unique homomorphism from AT (∅) to AH_{R}′.

As the consequence of Theorem 5.6, we obtain the following.

Corollary 5.8 AH_{R} is a model of a program R.

We call the F-algebra AH_{R} minimal applicative Herbrand model. The terminology “minimal” comes from the notion of minimal algebra [12] which is also called term generated in the literature.

6. Soundness and Completeness

In this section we show that the minimal applicative Herbrand model is sound and complete for the operational model of narrowing. The soundness and completeness results express the correspondence between a witness in minimal applicative Herbrand model and a computed substitution by narrowing.

Theorem 6.1 [Soundness of Narrowing for AH_{R}] Let R be a program and ∃X(steq s t = true) a query.

(steq s t) ⇝_{θ}^{∗} true
⇒ AH_{R} ⊧ ∃X(steq s t = true)
with a witness δ : X → AH_{R}

where θ : X→AT (Y) and δ = AH_{R}[[ ]]∘ρ^{#}∘θ for arbitrary substitution ρ : Y →AT (∅). Here AH_{R}[[ ]] denotes the unique homomorphism form AT (∅) to AH_{R}. Proof Suppose (steq s t) ⇝_{θ}^{∗} true. Then by the soundness of narrowing for rewriting, for any substitution ρ : Y → AT (∅), (steq s t)θρ →∗_{R} true. So AQ_{R}[[(steq s t)θρ]] = AQ_{R}[[true]]. Let ϕ : AQ_{R} → AH_{R} be the unique homomorphism. Since AH_{R}[[ ]] = ϕ∘AQ_{R}[[ ]],

AH_{R}[[ ]]∘ρ^{#}∘θ (steq s t) = ϕ(AQ_{R}[[(steq s t)θρ]]) = ϕ(AQ_{R}[[true]]) = true.

Hence AH_{R} ⊧ ∃X(steq s t = true). ■

We define an S-indexed subclass AD = {AD^{σ} | σ ∈ S} ⊆ AT (∅) as follows:

AD^{o} = { all ground data terms },
AD^{σ→τ} = AT (∅)^{σ→τ} for each σ, τ ∈ S.

This class AD plays an intermediate role for witnesses between AH_{R} and AQ_{R}.

Lemma 6.2 Let R be a program and ∃X(steq s t = true) a query.

AH_{R} ⊧ ∃X(steq s t = true)
⇒ AQ_{R} ⊧ ∀∅((steq s t)ξ = true) for some ξ : X → AD.

Proof Suppose δ is a witness of ∃X(steq(s, t) = true), i.e., a mapping δ : X → AH_{R} which satisfies δ^{#}(steq(s, t)) = true. The assignment δ assigns for each x ∈ X either a base type element or function type element. To classify these two, we use metavariables x_{i}’s for the variables assigning to the base type elements and y_{i}’s for the variables assigning to the function type elements. Namely, we assume the following:

X = {x_{1}, …, x_{m}, y_{1}, …, y_{n}},
δ = {x_{1} ↦h_{1}, …, x_{m} ↦h_{m}, y_{1} ↦f_{1}, …, y_{n} ↦f_{n}}

where h_{i}’s are the base type elements and f_{j}’s are the function type elements. We fix these f_{i}’s. Define a function ans : H^{m+n} → H such that

ans(h_{1}, …, h_{m}, f_{1}, …, f_{n}) = μ^{#}(steq s t)
where μ(x_{i}) = h_{i} for i = 1, …, m,
μ(y_{i}) = d_{i} for i = 1, …, n.

The function “ans” returns the value “true” if the arguments are witnesses of the query ∃X(steq s t) in AH_{R}. Note that the function “ans” is continuous. Then,

δ^{#}(steq s t)
= ans(h_{1}, …, h_{m}, f_{1}, …, f_{n})
= ans(⨆{z_{1} | compact z_{1} ⊑ h_{1}}, …, ⨆{z_{1} | compact z_{1} ⊑ h_{m}}, f_{1}, …, f_{n})
= ⨆{ans(z_{1}, …, z_{m}, f_{1}, …, f_{n}) | compactz_{i} ⊑ h_{i} for each i = 1, …, m}

(by the continuity of ans)

= true (by assumption)

We fix z_{i}’s determined above. Then we see that there exist compact elements ẑ_{1}, …, ẑ_{m} ∈ H such that

ans(ẑ_{1}, …, ẑ_{m}, f_{1}, …, f_{n}) = true.

Taking arbitrary elements d_{1}, … d_{n} ∈ AD^{o} that satisfy d_{1} ⊒ ẑ_{1}, …, d_{n} ⊒ ẑ_{m}, we obtain

ans(d_{1}, …, d_{m}, f_{1}, …, f_{n}) = true.

By the construction of AH_{R}, for each f_{i}, there exists u_{i} ∈ AT (∅) such that AH_{R}[[u_{i}]] = f_{i}. Hence letting ξ = {x_{1} ↦d_{1}, …, x_{m} ↦d_{m}, y_{1} ↦u_{1}, …, y_{m} ↦u_{m}}, we have

AQ_{R} ⊧ ∀∅ ((steq s t)ξ = true).
■

Theorem 6.3 [Completeness of Narrowing for AH_{R}] Let R be a program and ∃X(steq s t = true) a query. If

AH_{R} ⊧ ∃X(steq s t = true)

holds with a witness δ : X → AH_{R} then there exists

• a narrowing derivation (steq s t) ⇝_{θ}^{∗} true with a answer substitution θ : X → AT (Y),

• a mapping ϕ : AH_{R} → AD which depends on δ and θ, and

• a substitution ρ : Y → AD which depends on θ and ϕ

such that

ρ^{#}∘θ = ϕ∘δ.

Proof We will show the following diagram commutes:

X  X  X
δ↓  ↓^{ξ}  ↓^{θ}
AH_{R} ⟶^{ϕ} AD ⟵^{ρ^{#}} AT (Y)

where ξ is a mapping determined in the following.

Suppose δ is a witness of ∃X(steq(s, t) = true), i.e., δ : X → AH_{R} such that δ^{#}(steq(s, t)) = true. By Lemma 6.2, there exists an assignment

ξ : X → AD such that ξ^{#}(steq s t) = true.

By the Axiom of Choice, there exists a function Ψ such that

Ψ(δ) = ξ.

Define a function ϕ : AH_{R} → AD such that

ϕ(h) =^{def} \{ \begin{matrix}Ψ(δ)(x) & if there exists x ∈ X such that δ(x) = h \\ ⊥ & otherwise. \end{matrix}

Then clearly ξ = ϕ∘δ. Since (steq s t)ξ →∗_{R} true, by the completeness of narrowing for rewriting, there exists a narrowing derivation (steq s t) ⇝_{θ}^{∗} true with an answer substitution θ : X → AT (Y) such that θ ≼ ξ, i.e., there exists a substitution

ρ : Y → AD such that ρ^{#}∘θ = ξ.

Hence ρ^{#}∘θ = ϕ∘δ. ■

7. Conclusion

We have presented two models of a higher-order functional-logic language Ev, which are the quotient applicative Herbrand model and the minimal applicative Herbrand model and showed the soundness and completeness of narrowing with respect to both models in algebraic framework.

References [1] J. A. Bergstra and J. W. Klop. Conditional rewrite rules: Confluence and ter-

mination. Journal of Computer and System Sciences, 32(3):323–362, 1986.

[2] E. Giovannetti, G. Levi, C. Moiso, and C. Palamidessi. Kernel-LEAF: A logic plus functional language. Journal of Computer and System Sciences, 42(2):139– 185, 1991.

[3] J. Goguen and J. Meseguer. Models and equality for logical programming. Lecture Notes in Computer Science 250, pages 1–22, 1987.

[4] J. C. González-Moreno, M.T.Hortalá-González, and M. Rodríguez-Artalejo. Denotational versus declarative semantics for functional programming. Lecture Notes in Computer Science 626, pages 134–148, 1992.

[5] J. C. González-Moreno, M.T.Hortalá-González, and M. Rodríguez-Artalejo. On the completeness of narrowing as the operational semantics of functional logic programming. Lecture Notes in Computer Science 702, pages 216–230, 1992.

[6] M. Hamana, T. Nishioka, K. Nakahara, A. Middeldorp, and T. Ida. A design and implementation of a functional-logic language based on applicative term rewriting systems. Transactions of Information Processing Society of Japan, 36(8):1897–1905, 1995.

[7] Makoto Hamana. Semantics of a functional-logic language. Master’s thesis, University of Tsukuba, 1995.

[8] M. Hanus. Compiling logic programs with equality. In Proceedings of the 2nd Workshop on Programming Language Implementation and Logic Programming, Lecture Notes in Computer Science 456, pages 387–401, 1990.

[9] T. Ida and S. Okui. Outside-in conditional narrowing. IEICE Transactions on Information and Systems, E77-D(6), 1994.

[10] S. Kaplan. Conditional rewrite rules. Theoretical Computer Science, 33(2):175– 193, 1984.

[11] G. Levi, C. Palamidessi, P. G. Bosco, E. Giovannetti, and C. Moiso. A complete semantics characterization of K-LEAF, a logic language with partial functions. In Proceedings 1987 Symposium on Logic Programming, pages 318–327, Rockville, MD, 1987. IEEE Computer Society Press.

[12] K. Meinke. Universal algebra in higher types. Theoretical Complete Science, 100:385–417, 1992.

[13] A. Middeldorp and E. Hamoen. Completeness results for basic narrowing. Applicable Algebra in Engineering, Communication and Computing, 5(3/4):213–253, 1994.

[14] J. J. Moreno-Navarro and M. Rodríguez-Artalejo. Logic programming with functions and predicates: The language BABEL. Journal of Logic Programming, 12:191–223, 1992.

[15] K. Nakahara, A. Middeldorp, and T. Ida. A complete narrowing calculus for higher-order functional logic programming. In Proceedings of Seventh International Conference on Programming Languages: Implementations, Logics, and Programming 95 (PLILP’95), Lecture Notes in Computer Science 982, pages 97–114, 1995.