text:
# Composing Programs in a Rewriting Logic for Declarative Programming

## 1 Introduction

Constructor-Based Conditional Rewriting Logic (CRWL)111CRWL must not be confused with the Rewriting Logic proposed in  as a unifying logical framework for concurrency. CRWL is a particular logic for dealing with indeterminism., presented in , is a quite general approach to declarative programming that combines (first-order) functional and logic paradigms by means of the notion of (possibly) non deterministic lazy function. The basic idea is that both relations and deterministic lazy functions are particular cases of non-deterministic lazy functions. This approach retains the advantages of deterministic functions while adding the possibility of modeling non-deterministic functions by means of non-confluent constructor-based term rewriting systems, where a given term may be rewritten to constructor terms (possibly with variables) in more than one way. Here a fundamental notion is that of joinability: two terms a,b are joinable iff they can be rewritten to a common —but not necessarily unique— constructor term. In , CRWL is introduced with two equivalent proof calculi that govern deduction in this logic, an algebraic semantics for programs (theories) based on a freely generated model, and an operational semantics, based on a lazy narrowing calculus for solving goals, that is sound and complete wrt the algebraic semantics.

Modularity is a central issue in all programming paradigms motivated by the need of mastering the complexity inherent in large programs. Modularity related with algebraic specifications (which, to some extent, can be viewed as a sort of first-order functional programming) has been extensively studied and all specification languages are extended for dealing with modules. In this field, a typical module consists of a body, an export interface, a list of imports and, possibly, a list of formal parameters, and typical operations with modules have to do with setting up hierarchical relationships between modules as the union of modules (with some constraints) and the application of a parameterized module to an actual module, and their semantics are given from a category-theoretic point of view . Nevertheless, there are other studies of modularity  with more flexible sets of operations semantically defined by means of operations on the sets of models, and also studies where modularity has been tackled with the tools of algebraic specifications as  where an axiomatic specification is given for an algebra of non-parameterized modules and it is proved that each expression can be reduced to another one with, at most, an occurrence of the export (hiding) operator, and  where a constructive specification is given for an algebra of parameterized modules (without hiding) in Maude, and each expression is reduced to a flat module.

In the logic programming field, modularity has been the objective of different proposals —see  for a survey about the subject— which basically have followed two different guidelines. One, focused on programming-in-the-large, extends logic programming with modular constructs as a meta-linguistic mechanism  and gives semantics to modules with the aid of the immediate consequence operator. And the other one, focused on programming-in-the-small, enriches the theory of Horn clauses with new logical connectives for dealing with modules . In the first line, there is the work  where an algebra of logic programs is studied. This algebra is based on three basic operations (union, intersection and encapsulation) defined at the semantic level and then translate to the syntactic level. It is proved that each program expression is equivalent to a, possibly infinite, flat program, and also a transformation is defined for mapping program expressions into finite programs by introducing system generated predicates and adding a hidden part to each program. Notions of module hiding some predicates and module importation are built up with the aid of the basic operations.

On the other hand, in functional-logic programming we do not know any study of modularity semantically well founded. With this paper we have tried to contribute to filling this gap at least in the CRWL context. In this context, we deal with data constructors, as in logic programming, and functions defined by conditional rewrite rules, instead of predicates defined by Horn clauses, and we have proved (see section 3.2) that an operator, similar to the immediate consequence operator of logic programs, can be defined to each CRWL-program and its least fixpoint coincides with the freely generated term-model given in . All this has motivated our decision of developing a study of programs structuring and modularity in CRWL, based on a meta-linguistic mechanism, similar to the one which appears in . However we have defined an algebra of program modules based on a different set of operations (union, deletion of a signature of function symbols, closure wrt a signature and renaming) defined at the syntactical level in such a way that each program expression can be reduced to a, possibly infinite, flat program. With these operations we can model as well as notions of module which hides some functions and module importation, module parameterization, instantiation and inheritance with overriding. Also, we have introduced a notion of protected signature labeling symbols with module expressions, which allows to define structured modules and a representation morphism that maps each program expression into a finite structured module. We use protected signature, not only for hiding functions as is done in  for predicates, but also for hiding data constructors.

An important aspect to be considered when a language is extended for modular programming is the sound integration of the behavior of the modular operations into the semantics of the language. The compositionality of the semantics of a programming language is particularly relevant when modularity is involved. In fact, one of the most critical aspects in modular systems is the possibility of making a separate compilation of modules, and this can only be made in the presence of this property. On the other hand, full abstraction measures the implementation details of the semantics of a programming language. A non-fully abstract semantics makes the intended meaning of a program to include non relevant aspects, which do not depend on the behavior of the program but on a particular “implementation”. In some sense, full abstraction can be seen as the complementary property of compositionality, and the adequacy of a semantics is established when both full abstraction and compositionality are obtained. In , the semantics of a program is given by its immediate consequence operator which captures the information concerning possible compositions, this semantics is compositional by construction and it is proved that also is fully abstract wrt a notion of observable behavior given by the success sets of programs (least fixpoints of their immediate consequence operators). In CRWL-programming, the semantics given by the immediate consequence operator is compositional but not fully abstract when we take the freely generated term-model as observable behavior. For this reason, we study several alternative semantics to find one that is compositional and fully abstract.

We are confident that our work could serve as a reference to other studies of modularity in functional-logic programming, and, although we are focused on the modular aspects of the semantics, the results obtained in this paper, as well as the study of a wide range of other issues concerning semantics, makes the current work also relevant from a purely semantic point of view, in the context of rewriting logic-based programming languages. The approach to modularity in CRWL-programming, that we present here, substantially extends a previous one in  with a more elaborate notion of program module and a new operation (renaming) that makes clear the difference between importation and instantiation, and a more recent one  with the notions of structured module and module representation that allows to express closed modules by means of a finite number of rules and also to deal with local constructor symbols.

The paper is organized as follows: In the next section we introduce the basic features of the CRWL approach to functional-logic programming and its model-theoretic semantics —for a detailed presentation we refer to . In Section 3 we introduce an immediate consequence operator $`𝒯_{}`$, for each CRWL-program $``$, and a fixpoint semantics that matches the free term-model $`_{}`$ proposed in . In Section 4 we define a notion of (plain) module together with a reduced set of operations on program modules, and we express some modular constructions with these operations. In Section 5 we give the $`𝒯`$-semantics that characterizes the meaning of a CRWL-program when we consider composition of programs and prove that this semantics is compositional but not fully abstract wrt the set of operations, taking $`_{}`$ as the observable behavior of a program $``$. In Section 6 we introduce a fully abstract semantics by denoting a program module with the set of all its consistent term-models (pre-fixpoints of $`𝒯_{}`$); but this semantics is not compositional for the deletion of a signature. In Section 7, we obtain a compositional and fully abstract semantics as an indexed family of sets of consistent term-models for single function. In Section 8, we introduce the notion of structured module as a finite representation of expressions made up from finite plain modules that allows the hiding of constructor symbols. Finally we present a discussion and some conclusions.

## 2 CRWL for Declarative Programming

### 2.1 Signatures, terms and formulas

A signature with constructors is a pair $`\mathrm{\Sigma }=(DS_\mathrm{\Sigma },FS_\mathrm{\Sigma })`$, where $`DS_\mathrm{\Sigma }`$ and $`FS_\mathrm{\Sigma }`$ are countable disjoint sets of strings $`h/n`$ with $`n𝐍`$. Each $`c`$ such that $`c/nDS_\mathrm{\Sigma }`$ is a constructor symbol with arity $`n`$ and each $`f`$ such that $`f/nFS_\mathrm{\Sigma }`$ is a (defined) function symbol with arity $`n`$. The set of all constructor symbols and the set of all function symbols with arity $`n`$ are denoted by $`DS_\mathrm{\Sigma }^n`$ and $`FS_\mathrm{\Sigma }^n`$, respectively. Given a signature (with constructors) $`\mathrm{\Sigma }`$ and a set $`𝒱`$ of variable symbols, disjoint from all of the sets $`DS_\mathrm{\Sigma }^n`$ and $`FS_\mathrm{\Sigma }^n`$, we define $`\mathrm{\Sigma }`$-terms as follows: each symbol in $`𝒱`$ and each symbol in $`DS_\mathrm{\Sigma }^0FS_\mathrm{\Sigma }^0`$ is a $`\mathrm{\Sigma }`$-term, and for each $`hDS_\mathrm{\Sigma }^nFS_\mathrm{\Sigma }^n`$ and $`t_1,\mathrm{},t_n`$ terms, $`h(t_1,\mathrm{},t_n)`$ is a term. $`\mathrm{𝐓𝐞𝐫𝐦}_\mathrm{\Sigma }`$ is the set of all $`\mathrm{\Sigma }`$-terms and $`\mathrm{𝐂𝐓𝐞𝐫𝐦}_\mathrm{\Sigma }`$ the subset of those $`\mathrm{\Sigma }`$-terms (called constructor terms) built up only with symbols in $`DS_\mathrm{\Sigma }`$ and $`𝒱`$. In order to cope with partial definition we add a new 0-arity constructor $``$ to each signature $`\mathrm{\Sigma }`$ obtaining an extended signature $`\mathrm{\Sigma }_{}`$ whose terms are called partial $`\mathrm{\Sigma }`$-terms. When the signature $`\mathrm{\Sigma }`$ is clear, we will omit explicit mention of it, and we will write $`\mathrm{𝐓𝐞𝐫𝐦}`$ and $`\mathrm{𝐂𝐓𝐞𝐫𝐦}`$ (or $`\mathrm{𝐓𝐞𝐫𝐦}_{}`$ and $`\mathrm{𝐂𝐓𝐞𝐫𝐦}_{}`$ for $`\mathrm{\Sigma }_{}`$) respectively. Following the approach to non-determinism in  we only consider C-substitutions $`\theta :𝒱\mathrm{𝐂𝐓𝐞𝐫𝐦}`$. These mappings have natural extensions $`\theta :\mathrm{𝐓𝐞𝐫𝐦}\mathrm{𝐓𝐞𝐫𝐦}`$, also noted as $`\theta `$, defined in the usual way, and the result of applying $`\theta `$ to the term $`t`$ is written $`t\theta `$. Analogously, we define partial C-substitutions as mappings $`\theta :𝒱\mathrm{𝐂𝐓𝐞𝐫𝐦}_{}`$. The set of all C-substitutions (partial C-substitutions) is written $`\mathrm{𝐂𝐒𝐮𝐛𝐬𝐭}`$ ($`\mathrm{𝐂𝐒𝐮𝐛𝐬𝐭}_{}`$).

A signature morphism $`\rho :\mathrm{\Sigma }\mathrm{\Sigma }^{}`$ from a signature $`\mathrm{\Sigma }=(DS_\mathrm{\Sigma },FS_\mathrm{\Sigma })`$ to a signature $`\mathrm{\Sigma }^{}=(DS_\mathrm{\Sigma }^{},FS_\mathrm{\Sigma }^{})`$ consists of two mappings, that we denote with the same symbol $`\rho :DS_\mathrm{\Sigma }DS_\mathrm{\Sigma }^{}`$ and $`\rho :FS_\mathrm{\Sigma }FS_\mathrm{\Sigma }^{}`$, that map strings $`h/n`$ into strings $`h^{}/n`$. By abuse of notation we will denote $`h^{}=\rho (h)`$. This allows us to define a mapping $`\rho :\mathrm{𝐓𝐞𝐫𝐦}_\mathrm{\Sigma }_{}\mathrm{𝐓𝐞𝐫𝐦}_\mathrm{\Sigma }_{}^{}{}_{}{}^{}`$ as follows:

$$\begin{array}{c}\rho (h)=_{def}h,\text{ for }h𝒱\{\}DS_\mathrm{\Sigma }^0FS_\mathrm{\Sigma }^0;\hfill \\ \rho (h(\overline{t}))=_{def}\rho (h)(\rho (t_1),\mathrm{},\rho (t_n)),\text{ for }hDS_\mathrm{\Sigma }^nFS_\mathrm{\Sigma }^n,n>0.\hfill \end{array}$$

We will consider signature morphisms $`\rho :\mathrm{\Sigma }\mathrm{\Sigma }`$ such that $`\rho (h/n)=h/n`$ for every string $`h/n`$ in $`DS_\mathrm{\Sigma }`$. Such morphisms will be called function symbol renamings.

Given a signature $`\mathrm{\Sigma }`$ and a set $`𝒱`$ of variable symbols, there are two kinds of atomic CRWL-formulas for $`a,b\mathrm{𝐓𝐞𝐫𝐦}_{}`$, reduction statements $`ab`$, with the intended meaning “$`a`$ can be reduced to $`b`$,” and joinability statements $`ab`$, with the intended meaning “$`a`$ and $`b`$ can be reduced to a common value in CTerm”. Terms $`t\mathrm{𝐂𝐓𝐞𝐫𝐦}`$ are intended to represent totally defined values whereas terms $`t\mathrm{𝐂𝐓𝐞𝐫𝐦}_{}`$ represent partially defined values —to model the behavior of non-strict functions. Reduction statements $`at`$ with $`t\mathrm{𝐂𝐓𝐞𝐫𝐦}_{}`$, called approximation statements, have the intended meaning that $`t`$ approximates a possible value of $`a`$, whereas $`at`$ with $`t\mathrm{𝐂𝐓𝐞𝐫𝐦}`$ have the intended meaning that $`t`$ represents a possible value of $`a`$ —an expression may denote several values capturing the behavior of non-deterministic functions. Substitutions $`\theta \mathrm{𝐂𝐒𝐮𝐛𝐬𝐭}_{}`$ and signature morphisms $`\rho :\mathrm{\Sigma }\mathrm{\Sigma }^{}`$ apply to formulas in the obvious way.

### 2.2 Programs and formal derivation

A CRWL-program is a CRWL-theory $``$ defined as a signature $`\mathrm{\Sigma }`$ together with a set of conditional rewrite rules of the general form

$$f(\overline{t})rC,$$

where $`f(\overline{t})`$ is the left hand side (lhs), $`r`$ the right hand side (rhs), $`C`$ the condition of the rule, $`f`$ is a function symbol with arity $`n0`$, and $`C`$ consists of finitely many (possibly zero) joinability statements between fully defined terms (with no occurrence of $``$). When $`n>0`$, $`\overline{t}`$ is a linear $`n`$-tuple (i.e., without repeated variables) of fully defined constructor terms $`t_i\text{CTerm}`$. When $`n=0`$ rules take the simpler form $`frC`$. Formal derivation of CRWL-statements from a given program $``$ is governed by two equivalent calculi (see ). We present here the so-called Goal-Oriented Proof Calculus (GPC) which focuses on top-down proofs of reduction and joinability statements:

| (Bo) | $`e`$, | $`\text{for }e\mathrm{𝐓𝐞𝐫𝐦}_{}`$; |
| --- | --- | --- |
| (RR) | $`ee`$, | $`\text{for }e𝒱DS^0`$; |
| (DS) | $`{\displaystyle \frac{e_1t_1\mathrm{}e_nt_n}{c\left(\overline{e}\right)c\left(\overline{t}\right)}}`$, | $`\text{for }cDS^n\text{ and }e_i,t_i\mathrm{𝐓𝐞𝐫𝐦}_{}`$; |
| (OR) | $`{\displaystyle \frac{e_1t_1\mathrm{}e_nt_nCrt}{f\left(\overline{e}\right)t}}`$, | $`\text{if }\left(f\left(\overline{t}\right)rC\right)\left[\right]_{}`$ $`\text{and }t`$; |
| (Jo) | $`{\displaystyle \frac{atbt}{ab}}`$, | $`\text{if }t\mathrm{𝐂𝐓𝐞𝐫𝐦}\text{ and }a,b\mathrm{𝐓𝐞𝐫𝐦}_{}`$; |

where $`[]_{}=\{(lrC)\theta |(lrC),\theta \mathrm{𝐂𝐒𝐮𝐛𝐬𝐭}_{}\}`$ is the set of possibly partial constructor instances of rewrite rules and C-substitutions apply to rules in the obvious way. Rule (Bo) shows that a CRWL-reduction is related to the idea of approximation, and rule (OR) states that only constructor instances of rewrite rules are allowed in this calculus reflecting the so-called “call-time-choice”  for non-determinism (values of arguments for functions are chosen before the call is made). When a reduction or joinability statement $`\phi `$ is derivable from a program $``$ we write $`_{CRWL}\phi `$ and we say that $`\phi `$ is provable in $``$. Goals for a program $``$ are finite conjunctions of atomic formulas, and solutions are C-substitutions that make goals derivable. In  a sound and complete lazy narrowing calculus for goal-solving can be found.

### 2.3 CRWL-Algebras and models

We interpret CRWL-programs over algebraic structures consisting of posets with bottom as carriers (i.e., sets $`D`$ with a partial order $`_D`$ and a least element $`_D`$), whose elements are thought of as finite approximations of possibly infinite values in the poset’s ideal completion , and monotonic mappings from elements to cones (non-empty subsets of a poset with bottom, downclosed wrt the partial order of the poset) as function symbol denotations reflecting possible non-determinism. Such a mapping $`f:D𝒞(E)`$ —where $`D`$, $`E`$ are posets with bottom, and $`𝒞(E)`$ is the set of cones of $`E`$— can be extended to a monotonic mapping $`\widehat{f}:𝒞(D)𝒞(E)`$, defined by $`\widehat{f}(C)=_{def}_{uC}f(u)`$ and also noted $`f`$ by abuse of notation. In particular, deterministic function symbols are represented by mappings $`f:D(E)`$ computing directed cones or ideals (i.e., cones $`𝒞`$ such that for all $`x,y𝒞`$ there exists $`z𝒞`$ with $`xz`$ and $`yz`$) where $`(E)`$ is the set of ideals of $`E`$. These mappings become continuous mappings between algebraic cpos after performing the ideal completion (for a comprehensive exposition of these notions we refer to ). These ideas are behind the notion of CRWL-algebra.

Given a signature $`\mathrm{\Sigma }`$ and a set $`𝒱`$ of variable symbols, a CRWL-algebra of signature $`\mathrm{\Sigma }`$ is an algebraic structure $`𝒜=(D_𝒜,\{c^𝒜\}_{cDS_\mathrm{\Sigma }},\{f^𝒜\}_{fFS_\mathrm{\Sigma }})`$ where the carrier $`D_𝒜`$ is a poset with bottom $`_𝒜`$, $`f^𝒜`$ is a monotonic mapping $`D_𝒜^n𝒞(D_𝒜)`$ for each $`fFS_\mathrm{\Sigma }^n`$ and $`c^𝒜`$ is a monotonic mapping $`D_𝒜^n(D_𝒜)`$ for each $`cDS_\mathrm{\Sigma }^n`$. Both $`f^𝒜`$ and $`c^𝒜`$ reduce to cones when $`n=0`$. In order to ensure preservation of finite and maximal elements in the ideal completion, we require for all $`u_1,\mathrm{},u_nD_𝒜`$ that there exists $`vD_𝒜`$ such that $`c^𝒜(u_1,\mathrm{},u_n)=v`$, where $`v`$ is the ideal generated by $`v`$ (i.e., the set $`\{dD_𝒜dv\}`$), and if all $`u_i`$ are maximal (totally defined) then $`v`$ must also be maximal. The class of all CRWL-algebras of signature $`\mathrm{\Sigma }`$ is denoted by $`\mathrm{𝐀𝐥𝐠}_\mathrm{\Sigma }`$. We are specially interested in CRWL-term algebras, which are CRWL-algebras with carrier $`\mathrm{𝐂𝐓𝐞𝐫𝐦}_{}`$, ordered by the approximation ordering$``$,” defined as the least partial ordering satisfying the following properties:

$$\begin{array}{ccc}(a)\hfill & t,& t\mathrm{𝐂𝐓𝐞𝐫𝐦}_{};\hfill \\ (b)\hfill & c(\overline{s})c(\overline{t})& \text{ if }s_it_i,i=1,\mathrm{},n,\text{ for }cDS_\mathrm{\Sigma }^n,n0;\hfill \end{array}$$

and fixed interpretation for constructor symbols: $`c^𝒜=c`$, for all $`cDS_\mathrm{\Sigma }^0`$, and $`c^𝒜(\overline{t})=c(\overline{t})`$, for all $`cDS_\mathrm{\Sigma }^n`$ and $`n0`$. Therefore, two CRWL-term algebras of the same signature $`\mathrm{\Sigma }`$ will only differ in their interpretations for the function symbols of $`\mathrm{\Sigma }`$. As a consequence of the above definition, for $`s,t\mathrm{𝐂𝐓𝐞𝐫𝐦}_{}`$, $`st`$ implies $`s=`$ or $`s=c(\overline{s})`$ and $`t=c(\overline{t})`$ for some $`cDS_\mathrm{\Sigma }^n`$ and $`n0`$ with each component $`s_it_i`$. Also, for $`s,t\mathrm{𝐂𝐓𝐞𝐫𝐦}_{}`$,

$$st_{\mathrm{𝐶𝑅𝑊𝐿}}ts.$$
(1)
It can be proved, by induction, that every $`\theta \mathrm{𝐂𝐒𝐮𝐛𝐬𝐭}_{}`$ is a monotonic mapping from $`\mathrm{𝐂𝐓𝐞𝐫𝐦}_{}`$ to $`\mathrm{𝐂𝐓𝐞𝐫𝐦}_{}`$, that is: $`sts\theta t\theta `$, for all $`s,t\mathrm{𝐂𝐓𝐞𝐫𝐦}_{}`$.

A valuation over a structure $`𝒜\mathrm{𝐀𝐥𝐠}_\mathrm{\Sigma }`$ is any mapping $`\eta :𝒱D_𝒜`$. $`\eta `$ is totally defined when $`\eta (X)`$ is maximal for all $`X𝒱`$. $`\mathrm{𝐕𝐚𝐥}(𝒜)`$ is the set of all valuations over $`𝒜`$ and $`\mathrm{𝐃𝐞𝐟𝐕𝐚𝐥}(𝒜)`$ the set of all totally defined valuations. Given a valuation $`\eta `$ we can evaluate each partial $`\mathrm{\Sigma }`$-term in $`𝒜`$ as follows:

$$\begin{array}{cccc}\hfill [[]]_\eta ^𝒜& =_{def}& _𝒜,\hfill & \\ \hfill [[X]]_\eta ^𝒜& =_{def}& \eta (X),\hfill & X𝒱;\hfill \\ \hfill [[c]]_\eta ^𝒜& =_{def}& c^𝒜,\hfill & cDS_\mathrm{\Sigma }^0FS_\mathrm{\Sigma }^0;\hfill \\ \hfill [[h(\overline{e})]]_\eta ^𝒜& =_{def}& \widehat{h}^𝒜([[e_1]]_\eta ^𝒜,\mathrm{},[[e_n]]_\eta ^𝒜),\hfill & hDS_\mathrm{\Sigma }^nFS_\mathrm{\Sigma }^n,n>0.\hfill \end{array}$$

In this way each partial $`\mathrm{\Sigma }`$-term is evaluated to a cone. For each CRWL-algebra $`𝒜`$, every $`\eta \mathrm{𝐕𝐚𝐥}(𝒜)`$, and $`e\mathrm{𝐓𝐞𝐫𝐦}_{}`$, the following properties are proved in ,

1. $`[[e]]_\eta ^𝒜𝒞(D_𝒜)`$.
2. $`[[e]]_\eta ^𝒜(D_𝒜)`$, if $`e`$ is only built from deterministic functions (i.e., function symbols interpreted by ideal valued functions).
3. $`[[e]]_\eta ^𝒜=v`$ for some $`vD_𝒜`$, if $`e\mathrm{𝐂𝐓𝐞𝐫𝐦}_{}`$. Moreover, when $`e\mathrm{𝐂𝐓𝐞𝐫𝐦}`$ and $`\eta \mathrm{𝐃𝐞𝐟𝐕𝐚𝐥}(𝒜)`$, $`v`$ is maximal.
4. (Substitution Lemma) $`[[e\theta ]]_\eta ^𝒜=[[e]]_\rho ^𝒜`$, for $`\theta \mathrm{𝐂𝐒𝐮𝐛𝐬𝐭}_{}`$, where $`\rho `$ is the uniquely determined valuation that satisfies $`\rho (X)=[[X\theta ]]_\eta ^𝒜`$, for all $`X𝒱`$.

From these results and taking into account that each substitution is equivalent to a valuation over any CRWL-term algebra, we have the following complementary results for term algebras:

###### Proposition 2.1

For each CRWL-term algebra $`𝒜`$ and every $`\eta \mathrm{𝐕𝐚𝐥}(𝒜)`$ we have:

1. $`[[t]]_\eta ^𝒜=t\eta `$ for every $`t\mathrm{𝐂𝐓𝐞𝐫𝐦}_{}`$;
2. $`[[h(\overline{t})]]_\eta ^𝒜=h^𝒜(\overline{t}\eta )`$ for all $`hDS_\mathrm{\Sigma }^nFS_\mathrm{\Sigma }^n`$, $`n>0`$, and $`t_1,\mathrm{},t_n\mathrm{𝐂𝐓𝐞𝐫𝐦}_{}`$;
3. $`[[e\theta ]]_\eta ^𝒜=[[e]]_{\theta \eta }^𝒜`$ for all $`e\mathrm{𝐓𝐞𝐫𝐦}_{}`$ and $`\theta \mathrm{𝐂𝐒𝐮𝐛𝐬𝐭}_{}`$, where $`\theta \eta `$ represents the function composition $`\eta \theta `$.

Proof.
(1) is easily proved by induction on the structure of $`t`$ and (2) follows from (1). By the Substitution Lemma, $`[[e\theta ]]_\eta ^𝒜=[[e]]_\rho ^𝒜`$ for a valuation $`\rho `$ uniquely determined by the condition $`\rho (X)=[[X\theta ]]_\eta ^𝒜,X𝒱`$, and by (1), $`[[X\theta ]]_\eta ^𝒜=X\theta \eta ;`$ then $`\rho =\theta \eta `$ and we obtain (3). $`\mathrm{}`$

Models in CRWL are introduced from the following notion of satisfiability:

* $`𝒜`$ satisfies a reduction statement $`ab`$ under a valuation $`\eta \mathrm{𝐕𝐚𝐥}(D_𝒜)`$, or $`𝒜_\eta (ab)`$, iff $`[[a]]_\eta ^𝒜[[b]]_\eta ^𝒜`$.
* $`𝒜`$ satisfies a joinability statement $`ab`$ under a valuation $`\eta \mathrm{𝐕𝐚𝐥}(D_𝒜)`$, or $`𝒜_\eta (ab)`$, iff $`[[a]]_\eta ^𝒜[[b]]_\eta ^𝒜\text{ contains a maximal element in }D_𝒜`$.
* $`𝒜`$ satisfies a rule $`lrC`$, or $`𝒜(lrC)`$, iff $`𝒜_\eta C\text{ implies }𝒜_\eta (lr),\text{ for every valuation }\eta \mathrm{𝐕𝐚𝐥}(D_𝒜)`$.
* $`𝒜`$ is a model of a program $``$, i.e., $`𝒜`$, iff $`𝒜`$ satisfies all rules in $``$.

CRWL-provability is sound and complete wrt this model-theoretic semantics when we consider totally defined valuations only. In  is proved that for any program $``$ and any approximation or joinability statement $`\phi `$,

$$_{CRWL}\phi 𝒜_\eta \phi ,\text{ for every }𝒜\text{ model of }\text{ and }\eta \mathrm{𝐃𝐞𝐟𝐕𝐚𝐥}(D_𝒜).$$
(2)
This result is achieved with the help of a CRWL-term algebra $`_{}`$ characterized by the following interpretation for any defined function symbol $`fFS_\mathrm{\Sigma }^n`$, $`n0`$,

$$f^{_{}}(\overline{t})=_{def}\{r\mathrm{𝐂𝐓𝐞𝐫𝐦}_{}_{CRWL}f(\overline{t})r\}.$$

$`_{}`$ is such that $`_{CRWL}\phi _{}_{id}\phi `$ for any approximation or joinability statement $`\phi `$. According to this result, $`_{}`$ is taken as the canonical model of the program $``$. Also in  it is proved that this model is freely generated by $`𝒱`$ in the category of all models of $``$. This is the model-theoretical semantics of the program $``$.

Given a signature $`\mathrm{\Sigma }`$ and a function symbol renaming $`\rho :\mathrm{\Sigma }\mathrm{\Sigma }`$, for each CRWL-term algebra $`𝒜=(\mathrm{𝐂𝐓𝐞𝐫𝐦}_{},\{c^𝒜\}_{cDS_\mathrm{\Sigma }},\{f^𝒜\}_{fFS_\mathrm{\Sigma }})`$ of this signature we can define another CRWL-term algebra

$$𝒜_\rho =(\mathrm{𝐂𝐓𝐞𝐫𝐦}_{},\{c^{𝒜_\rho }\}_{cDS_\mathrm{\Sigma }},\{f^{𝒜_\rho }\}_{fFS_\mathrm{\Sigma }})$$

such that $`f^{𝒜_\rho }=\rho (f)^𝒜`$. The relation between evaluation and satisfaction in $`𝒜`$ and evaluation and satisfaction in $`𝒜_\rho `$ is stated by the following proposition.

###### Proposition 2.2

Given a signature $`\mathrm{\Sigma }`$, for every CRWL-term algebra $`𝒜`$ of this signature, every function symbol renaming $`\rho :\mathrm{\Sigma }\mathrm{\Sigma }`$, and all $`\theta \mathrm{𝐂𝐒𝐮𝐛𝐬𝐭}_{}`$, we have

1. $`(\rho (t))\theta =\rho (t\theta )`$, for all $`t\mathrm{𝐓𝐞𝐫𝐦}_{}`$.
2. $`[[\rho (t)]]_\theta ^𝒜=[[t]]_\theta ^{𝒜_\rho }`$, for all $`t\mathrm{𝐓𝐞𝐫𝐦}_{}`$.
3. $`𝒜_\theta \rho (\phi )𝒜_\rho _\theta \phi `$, for any reduction or joinability statement $`\phi `$.

Proof.
The two first statements can be proved by induction over the structure of $`t`$, whereas the third one is directly derived from (2).

$`\mathrm{}`$

## 3 Fixpoint Semantics

In this section we will prove, for every CRWL-program $``$, that $`_{}`$ is the least fixpoint of an operator defined over CRWL-term algebras. The approach we use here is similar to that applied in the field of logic programming . However, the notion of interpretation, and the corresponding mathematical aspects, have to be reformulated in the context of CRWL-term algebras. This approach has been also used in  in the context of a previous formalism to model functional-logic programming. However, this work does not deal with some relevant aspects (e.g., non-determinism) of the CRWL-programming version we are considering here.

### 3.1 The lattice of all CRWL-term algebras

Let $`\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$ be the set of all CRWL-term algebras of a signature $`\mathrm{\Sigma }`$ associated to a CRWL-program $``$. We can define the relationship $`𝒜`$ between two algebras $`𝒜,\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$ in the following way:

$$𝒜_{def}\text{ for each }fFS_\mathrm{\Sigma }^n\text{ and }n>0,f^𝒜(\overline{t})f^{}(\overline{t}),$$

when $`n=0`$, $`f^𝒜f^{}`$. This relationship is obviously a partial ordering and $`(\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma },)`$ is a poset. This poset has a bottom $`_\mathrm{\Sigma }`$ and a top $`_\mathrm{\Sigma }`$ characterized by the following interpretations, for each $`fFS_\mathrm{\Sigma }^n`$ and $`n0`$,

$$\begin{array}{ccc}\hfill f^_\mathrm{\Sigma }(\overline{t})& =_{def}& ,\hfill \\ \hfill f^_\mathrm{\Sigma }(\overline{t})& =_{def}& \mathrm{𝐂𝐓𝐞𝐫𝐦}_{}.\hfill \end{array}$$

Given a subset $`𝐒\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$, the following definitions

$$\begin{array}{ccc}\hfill f^𝐒(\overline{t})& =_{def}& _{𝒜𝐒}f^𝒜(\overline{t}),\hfill \\ \hfill f^𝐒(\overline{t})& =_{def}& _{𝒜𝐒}f^𝒜(\overline{t}),\hfill \end{array}$$

for each $`fFS_\mathrm{\Sigma }^n`$ and $`n0`$, characterize two CRWL-term algebras, $`𝐒`$ and $`𝐒`$ respectively, because the union and intersection of any number of cones are cones also, and the resulting functions in the above definitions are obviously monotonic if $`f^𝒜`$ is monotonic for all $`𝒜𝐒`$. Clearly, $`𝐒`$ and $`𝐒`$ are the least upper bound and the greatest lower bound of $`𝐒`$, respectively. So, $`(\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma },)`$ is a complete lattice.

Valuations (substitutions) of terms in term algebras can be considered continuous mappings from algebras to cones in the sense given by the following lemma.

###### Lemma 3.1 (Continuity of valuations in $`\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$)

For each term $`e\mathrm{𝐓𝐞𝐫𝐦}_{}`$ and each substitution $`\theta \mathrm{𝐂𝐒𝐮𝐛𝐬𝐭}_{}`$

1. $`𝒜[[e]]_\theta ^𝒜[[e]]_\theta ^{}`$, for $`𝒜,\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$.
2. $`[[e]]_\theta ^𝐃=_{𝒜𝐃}[[e]]_\theta ^𝒜`$, for all directed subsets $`𝐃\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$.

Proof.
The first statement is proved by induction on the structure of $`e`$. If $`e\{\}𝒱DS_\mathrm{\Sigma }^0`$ then $`[[e]]_\theta ^𝒜`$ does not depend on the particular term algebra $`𝒜`$ and $`[[e]]_\theta ^𝒜=[[e]]_\theta ^{}`$. Else, if $`eFS_\mathrm{\Sigma }^0`$, $`𝒜`$ implies $`e^𝒜e^{}`$ and then $`[[e]]_\theta ^𝒜[[e]]_\theta ^{}`$. Finally, if $`e=h(\overline{e})`$ with $`hDS_\mathrm{\Sigma }^nFS_\mathrm{\Sigma }^n`$ and $`n>0`$, assuming $`[[e_i]]_\theta ^𝒜[[e_i]]_\theta ^{}`$, for $`i=1,\mathrm{},n`$, as the induction hypothesis, for every $`t[[e]]_\theta ^𝒜`$ we have $`th^𝒜(\overline{t})`$ for some $`t_i[[e_i]]_\theta ^𝒜`$, which implies $`th^{}(\overline{t})`$ with $`t_i[[e_i]]_\theta ^{}`$ as a consequence of $`𝒜`$ and the induction hypothesis. Thus, we get $`t[[e]]_\theta ^{}`$, and consequently $`[[e]]_\theta ^𝒜[[e]]_\theta ^{}`$.

To prove the second statement we only need to prove the following inclusion $`[[e]]_\theta ^𝐃_{𝒜𝐃}[[e]]_\theta ^𝒜`$ because the inclusion in the other way is trivially derived from the first statement. We also proceed by induction on $`e`$. If $`e\{\}𝒱DS_\mathrm{\Sigma }^0`$ then, as $`[[e]]_\theta ^𝒜`$ does not depend on $`𝒜`$, $`[[e]]_\theta ^𝐃=[[e]]_\theta ^𝒜`$ for all $`𝒜𝐃`$. Else, if $`eFS_\mathrm{\Sigma }^0`$ then $`[[e]]_\theta ^𝐃=e^𝐃`$ and, by definition, $`e^𝐃=_{𝒜𝐃}e^𝒜`$. So, in all these cases, $`[[e]]_\theta ^𝐃=_{𝒜𝐃}[[e]]_\theta ^𝒜`$. Finally, if $`e=h(\overline{e})`$ with $`hDS_\mathrm{\Sigma }^nFS_\mathrm{\Sigma }^n`$ and $`n>0`$, assuming $`[[e_i]]_\theta ^𝐃_{𝒜𝐃}[[e_i]]_\theta ^𝒜`$, $`i=1,\mathrm{},n`$, as the induction hypothesis, for every $`t[[e]]_\theta ^𝐃`$ we have $`th^𝐃(\overline{t})`$ for some $`t_i[[e_i]]_\theta ^𝐃`$, $`i=1,\mathrm{},n`$. By definition $`h^𝐃(\overline{t})=_{𝒜𝐃}h^𝒜(\overline{t})`$ and from this and the induction hypothesis we can deduce $`th^{𝒜_0}(\overline{t})`$ with $`t_i[[e_i]]_\theta ^{𝒜_i}`$, for some $`𝒜_0,𝒜_1,\mathrm{},𝒜_n𝐃`$. Since $`𝐃`$ is directed, there exists $`𝒜𝐃`$, such that $`𝒜_i𝒜`$, $`i=0,1,\mathrm{},n`$, and so $`th^𝒜(\overline{t})`$ with $`t_i[[e_i]]_\theta ^𝒜`$, which implies $`t[[e]]_\theta ^𝒜`$ and $`[[e]]_\theta ^𝐃_{𝒜𝐃}[[e]]_\theta ^𝒜`$. $`\mathrm{}`$

Another interesting result relates satisfiability of joinability statements in the least upper bound of a directed set of term algebras with satisfiability in, at least, one of the algebras of the set.

###### Lemma 3.2

Let $`C`$ be a finite set of joinability statements and $`𝐃`$ a directed subset of $`\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$, then $`𝐃_\theta C`$ implies that there exists $`𝒜𝐃`$ such that $`𝒜_\theta C`$.

Proof.
It is sufficient to prove that this lemma holds when $`C`$ reduces to one joinability statement $`rs`$, because with more statements we shall obtain algebras $`𝒜_1,\mathrm{},𝒜_n`$, one for each joinability statement, and the upper bound $`\{𝒜_1,\mathrm{},𝒜_n\}`$ will satisfy all joinability statements in $`C`$. By definition, $`𝐃_\theta rs`$ implies that there exists a totally defined term $`t[[r]]_\theta ^𝐃[[s]]_\theta ^𝐃`$ and by lemma 3.1, $`t[[r]]_\theta ^𝐃t[[r]]_\theta ^{𝒜_1}`$ for some $`𝒜_1𝐃`$ and $`t[[s]]_\theta ^𝐃t[[s]]_\theta ^{𝒜_2}`$ for some $`𝒜_2𝐃`$. By the first statement of lemma 3.1, considering $`𝒜𝐃`$ such that $`𝒜_i𝒜`$, $`i=1,2`$, we have a term algebra such that $`t[[r]]_\theta ^𝒜[[s]]_\theta ^𝒜`$ and consequently $`𝒜_\theta rs.`$ $`\mathrm{}`$

### 3.2 The algebra transformer associated with a program

Given a CRWL-program $``$, with a signature $`\mathrm{\Sigma }`$, we can define an algebra transformer $`𝒯_{}:\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$, similar to the immediate consequences operator used in logic programming, by fixing the interpretation of each function symbol $`fFS_\mathrm{\Sigma }^n`$, in a transformed algebra $`𝒯_{}(𝒜)`$, as the result of one step applications of reduction statements corresponding to instances —not necessarily ground— of those rules of $``$, defining $`f`$, satisfied in $`𝒜`$. We formalize this idea defining, for each $`fFS_\mathrm{\Sigma }^n`$, $`n0`$,

$$f^{𝒯_{}(𝒜)}(\overline{t})=_{def}\{t(f(\overline{s})rC)[]_{},s_it_i,𝒜_{id}C,t[[r]]_{id}^𝒜\}\{\},$$

that is basically a union of cones $`[[r]]_{id}^𝒜`$. This definition corresponds to a monotonic mapping because all rule instances $`(f(\overline{s})rC)[]_{}`$, applicable to arguments $`\overline{t^{}}`$ are also applicable to arguments $`\overline{t}`$ such that $`t_i^{}t_i`$, for $`i=1,\mathrm{},n`$, and so the corresponding interpretation characterizes a CRWL-term algebra. From this definition of $`𝒯_{}`$ we can derive the continuity of the operator in $`\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$.

###### Proposition 3.3

For each program $``$ its associated operator $`𝒯_{}`$ is continuous.

Proof.
$`𝒯_{}`$ is monotonic. Given $`𝒜,\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$ such that $`𝒜`$, $`𝒜_{id}C_{id}C`$ for every set $`C`$ of joinability statements, and by Lemma 3.1, $`[[e]]_{id}^𝒜[[e]]_{id}^{}`$ for every term $`e`$; hence, every rule instance $`(f(\overline{s})rC)[]_{}`$ applicable to obtain $`f^{𝒯_{}(𝒜)}(\overline{t})`$ also will be applicable to obtain $`f^{𝒯_{}()}(\overline{t})`$, and therefore $`𝒯_{}(𝒜)𝒯_{}()`$. $`𝒯_{}`$ is continuous. For every directed set $`𝐃\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$, $`𝒯_{}(𝐃)\{𝒯_{}(𝒜)|𝒜𝐃\}`$ because each rule instance $`(f(\overline{s})rC)[]_{}`$ that is applicable to obtain $`f^{𝒯_{}(𝐃)}(\overline{t})`$, by Lemmas 3.1 and 3.2, is also applicable to obtain $`_{𝒜𝐃}f^{𝒯_{}(𝒜)}(\overline{t})`$, and this expression is $`f^{\{𝒯_{}(𝒜)|𝒜𝐃\}}(\overline{t})`$. The inclusion in the other way is trivial. $`\mathrm{}`$

Thus, $`𝒯_{}`$ has a least fixpoint $`_{}`$ given by $`𝐀_{}`$ (that is also the least pre-fixpoint), where $`𝐀_{}`$ is the chain of CRWL-term algebras $`𝒜_i,i𝐍`$, such that

$$𝒜_0=_\mathrm{\Sigma }\mathrm{}𝒜_{i+1}=𝒯_{}(𝒜_i)\mathrm{}$$

$`_{}`$ is also denoted as $`𝒯_{}^{}{}_{}{}^{\omega }(_\mathrm{\Sigma })`$ (see ). In order to prove that $`_{}`$ coincides with $`_{}`$ we need two lemmata, one characterizing the set of term models and other relating CRWL-provability with $`𝐀_{}`$ satisfiability.

###### Lemma 3.4 (Model characterization)

Given a program $``$, $``$ is a term model for $``$ iff $`𝒯_{}()`$

Proof.
First, we will prove that $`𝒯_{}()`$ for each term model $``$. Let us consider $`f^{𝒯_{}()}(\overline{t})`$ for $`fFS_\mathrm{\Sigma }^n,n>0`$, with all $`t_i\mathrm{𝐂𝐓𝐞𝐫𝐦}_{}`$. If there exists a rule instance $`(f(\overline{s})rC)[]_{}`$ with $`r`$, $`s_it_i`$, and $`_{id}C`$ then as $``$ is a model of $``$, $`[[r]]_{id}^{}[[f(\overline{s})]]_{id}^{}`$. By Proposition 2.1 (2), $`[[f(\overline{s})]]_{id}^{}=f^{}(\overline{s})`$, and by $`f^{}`$ monotonic, $`f^{}(\overline{s})f^{}(\overline{t})`$, and $`[[r]]_{id}^{}f^{}(\overline{t})`$. Thus, $`f^{𝒯_{}()}(\overline{t})f^{}(\overline{t})`$, and consequently $`𝒯_{}()`$. For $`fFS_\mathrm{\Sigma }^0`$ the proof is similar but somewhat simpler.

Now we will prove that every term algebra $``$ such that $`𝒯_{}()`$ is a model for $``$. Given a rule $`(f(\overline{t})rC)`$, for $`\theta \mathrm{𝐂𝐒𝐮𝐛𝐬𝐭}_{}`$ such that $`_{id}C\theta `$, or equivalently $`_\theta C`$ (by Proposition 2.1 (3)), we can consider $`f^{𝒯_{}()}(\overline{t}\theta )`$, and because of the instance $`(f(\overline{t})rC)\theta []_{}`$ we have $`[[r\theta ]]_{id}^{}f^{𝒯_{}()}(\overline{t}\theta )`$. By hypothesis, $`f^{𝒯_{}()}(\overline{t}\theta )f^{}(\overline{t}\theta )`$; by Proposition 2.1 (3), $`[[r\theta ]]_{id}^{}=[[r]]_\theta ^{}`$; and by Proposition 2.1 (2), $`f^{}(\overline{t}\theta )=[[f(\overline{t})]]_\theta ^{}`$; thus, $`[[r]]_\theta ^{}[[f(\overline{t})]]_\theta ^{}`$ which is $`_\theta f(\overline{t})r`$, and $``$ satisfies the rule $`f(\overline{t})rC`$. $`\mathrm{}`$

###### Lemma 3.5

Given $`e\mathrm{𝐓𝐞𝐫𝐦}_{}`$ and $`t\mathrm{𝐂𝐓𝐞𝐫𝐦}_{}`$, we have

$$_{CRWL}et𝒜_i_{id}et,\text{ for some }𝒜_i𝐀_{}.$$

Proof.
As $`𝒯_{}(𝐀_{})=𝐀_{}`$, by the model characterization lemma, $`𝐀_{}`$ will be a model of $``$. Thus, by equivalence (2), $`_{CRWL}et`$ implies $`𝐀_{}_{id}et`$ or $`t[[e]]_{id}^𝐀_{}`$ that is equivalent to $`t[[e]]_{id}^𝐀_{}`$. By lemma 3.1, $`[[e]]_{id}^𝐀_{}=_{𝒜_i𝐀_{}}[[e]]_{id}^{𝒜_i}`$, so there will be an $`𝒜_i`$ such that $`t[[e]]_{id}^{𝒜_i}`$ that means $`𝒜_i_{id}et`$. $`\mathrm{}`$

From the above results we obtain the following proposition.

###### Proposition 3.6

For every program $``$, $`_{}`$ is the least fixpoint (and the least pre-fixpoint) of $`𝒯_{}`$.

Proof.
First we can prove $`𝐀_{}_{}`$, from $`𝒜_0_{}`$, $`𝒯_{}(_{})_{}`$ (because $`_{}`$ is a model of $``$) and the continuity of $`𝒯_{}`$ that assures $`𝒜_i_{}`$ for all $`i`$. Now we can prove that $`_{}𝐀_{}`$ by proving, for each $`fFS_\mathrm{\Sigma }^n`$, that $`f^{_{}}(\overline{t})f^𝐀_{}(\overline{t})`$, for $`t_1,\mathrm{},t_n\mathrm{𝐂𝐓𝐞𝐫𝐦}_{}`$, and this inclusion is proved by reasoning with elements. By definition, $`tf^{_{}}(\overline{t})`$ is equivalent to $`_{CRWL}f(\overline{t})t`$ and, by Lemma 3.5, this implies $`𝒜_i_{id}f(\overline{t})t`$, for some $`𝒜_i𝐀_{}`$. Taking into account that, by Proposition 2.1 (2) $`[[f(\overline{t})]]_{id}^{𝒜_i}=f^{𝒜_i}(\overline{t})`$ we obtain $`tf^{𝒜_i}(\overline{t})`$ and $`tf^𝐀_{}(\overline{t})`$. $`\mathrm{}`$

Thus, if we consider the meaning of a program $``$ as the least fixpoint of its associated transformer $`𝒯_{}`$, then this fixpoint semantics coincides with the model-theoretic semantics as it happens in logic programming. In fact, this semantics would correspond to the C-semantics in .

###### Definition 3.7 (Least model semantics)

For each program $``$ we define its least model semantics as: $`[\{\}]_{LM}=_{def}_{}`$.

## 4 An Algebra of CRWL-Program Modules

For designing large programs it is convenient to separate the whole task into subtasks of manageable size and construct programs in a structured fashion by combining and modifying smaller programs. This idea has been extended to many programming languages giving rise to different notions of program module, each one being attached to a programming paradigm. In CRWL-programming we are going to follow an approach close to that developed in  for logic programming, where modules are open programs in the sense that function definitions in a module can be completed with definitions for the same functions in other modules. We will consider a global signature with bottom $`\mathrm{\Sigma }_{}=(DS_\mathrm{\Sigma }_{},FS_\mathrm{\Sigma }_{})`$ and a countable set $`𝒱`$ of variable symbols and will construct modules and module expressions with symbols of these sets. $`\mathrm{\Sigma }_{}`$ and $`𝒱`$ will characterize the environment where modules are written. Also we will consider all constructor symbols in $`DS_\mathrm{\Sigma }_{}`$ common to all program modules as it is usual in other proposals of modularity for declarative programming, like , where compositionality and full abstraction are dealt with. With this decision we give up any possibility of data abstraction and the only contribution of a program module to the environment will be a set of (definition) rules for a subsignature of function symbols. We will take this subsignature to denote the exportable resources of the module, and the set of rules as its body. In a program module, function symbols may appear —in the rhs of a rule— with no definition rule in this module. Although it may be assumed that all function symbols are defined in each program module by assuming an implicit rule $`f(\overline{t})`$ for each function symbol $`f`$ with no definition rule, these symbols will be assumed to be provided by other modules and they will be taken to denote the resources that have to be imported. They will be the parameters of the module. From these considerations we propose the following definition for the notion of module in CRWL-programming

###### Definition 4.1 (Module)

A module in CRWL-programming is a tuple $`<\sigma _p,\sigma _e,>`$ where

* $``$ is a set of program rules $`f(\overline{t})rC`$ ($`r`$),
* $`\sigma _e`$ is the (exported) signature of function symbols with a definition rule in $``$,
* $`\sigma _p`$ is the (parameter) signature of those function symbols with no definition rule in $``$ that appear in any rule (i.e., they are invoked but not defined).

$``$ is the body of the module and $`(\sigma _p,\sigma _e)`$ its interface. The interface of a module could be inferred from its body if one knows which are the constructor symbols. However, as we consider all constructor symbols common to all program modules, we do not include an explicit declaration of these symbols in any module and have to make explicit parameter signatures in order to distinguish between function and constructor symbols. In this way, every symbol not occurring in $`\sigma _e`$ nor $`\sigma _p`$ will be a constructor symbol. Next, we have an example of a module definition.

###### Example 4.2

This example shows a module for constructing ordered lists of natural numbers with functions for inserting elements, checking the type of an element, and compare natural numbers.

```
  OrdNatList =
    < {},                               % Parameter signature
      {isnat/1, leq/2, insert/2},       % Exported signature
      { isnat(zero)    -> true.
        isnat(succ(X)) -> isnat(X).
        leq(zero,zero)       -> true.
        leq(zero,succ(X))    -> isnat(X).
        leq(succ(X),zero)    -> false <= isnat(X) >< true.
        leq(succ(X),succ(Y)) -> leq(X,Y).
        insert(X,[])     -> [X]              <= isnat(X) >< true.
        insert(X,[Y|Ys]) -> [X|[Y|Ys]]       <= leq(X,Y) >< true.
        insert(X,[Y|Ys]) -> [Y|insert(X,Ys)] <= leq(X,Y) >< false.}>

```

In this module the parameter signature is empty, and symbols like `zero/0`, `succ/1`, `[]/0`, `[_|_]/2` with no definition rule are considered constructor symbols, because they are not included in the parameter signature (and obviously because they occur in arguments of left hand sides).

We write $`\mathrm{𝐏𝐌𝐨𝐝}(\mathrm{\Sigma }_{})`$ for the class of all program modules which can be defined with a signature $`\mathrm{\Sigma }_{}`$, $`\mathrm{𝐒𝐮𝐛𝐒𝐢𝐠}(\mathrm{\Sigma }_{})`$ for the set of all subsignatures of a signature $`\mathrm{\Sigma }_{}`$, and $`\mathrm{𝐏𝐫𝐠}(\mathrm{\Sigma }_{})`$ for the class of all sets of rules (programs) which can be defined with $`\mathrm{\Sigma }_{}`$. On $`\mathrm{𝐏𝐌𝐨𝐝}(\mathrm{\Sigma }_{})`$ we define three projections:

* $`\mathrm{𝑝𝑎𝑟}:\mathrm{𝐏𝐌𝐨𝐝}(\mathrm{\Sigma }_{})\mathrm{𝐒𝐮𝐛𝐒𝐢𝐠}(\mathrm{\Sigma }_{})`$ such that $`\mathrm{𝑝𝑎𝑟}(<\sigma _p,\sigma _e,>)=\sigma _p`$,
* $`\mathrm{𝑒𝑥𝑝}:\mathrm{𝐏𝐌𝐨𝐝}(\mathrm{\Sigma }_{})\mathrm{𝐒𝐮𝐛𝐒𝐢𝐠}(\mathrm{\Sigma }_{})`$ such that $`\mathrm{𝑒𝑥𝑝}(<\sigma _p,\sigma _e,>)=\sigma _e`$, and
* $`\mathrm{𝑟𝑙}:\mathrm{𝐏𝐌𝐨𝐝}(\mathrm{\Sigma }_{})\mathrm{𝐏𝐫𝐠}(\mathrm{\Sigma }_{})`$ such that $`\mathrm{𝑟𝑙}(<\sigma _p,\sigma _e,>)=`$,

which give respectively the parameter signature, the exported signature, and the body of a module.

### 4.1 Basic Operations on Modules

In this section we present a set of basic operations with modules that allows us to express typical features of modularization techniques such as information hiding/abstraction, import/export relationships and inheritance related to function symbols as is done in , but our set of operations is different and we give syntactic definitions for it. We use three operations: union of programs, closure wrt a signature and deletion of a signature, that are sufficient to express the most extended ways of composing modules and their relationships, and we do not need the intersection of programs, used in  to model hiding, because we directly deal with signatures in the closure. In order to give more flexibility in expressing importation and instantiation, we also include a renaming operation. We define our operations in such a way that all module expressions can be reduced to a flat module $`<\sigma _p,\sigma _e,>`$ —where $``$ could be an infinite set of rules. This is something like a  presentation semantics .

First we define the union of two modules as the module obtained as the simple union of signatures and rules.

###### Definition 4.3 (Union)

Given two modules $`𝒫_1=<\sigma _p^1,\sigma _e^1,_1>`$ and $`𝒫_2=<\sigma _p^2,\sigma _e^2,_2>`$, their union is defined as the module:

$$𝒫_1𝒫_2=_{def}<(\sigma _p^1\sigma _p^2)(\sigma _e^1\sigma _e^2),\sigma _e^1\sigma _e^2,_1_2>.$$

Each argument in this operation is considered an open program that can be extended or completed with the other argument possibly with additional rules for its exported function symbols.

###### Example 4.4

Let us consider the following module with a function to give change for an amount of money. Values for coins are provided by the non-deterministic function `coin/0`, whereas `getcoin/1` gives different possibilities to get a coin for a fixed amount. Finally, the function `change/1` returns a list with the coins corresponding to the change. In this example, we are assuming a predefined arithmetic with the usual notation for natural numbers. This was not the case in Example 4.2.

```
  MoneyChange =
    < {_=<_/2, _-_/2},
      {coin/0,getcoin/1,change/1},
      { coin -> 1. coin -> 5. coin -> 10.
        getcoin(N) -> C <= coin >< C, C =< N >< true.
        change(0) -> [].
        change(N) -> [C|change(N-C)] <= getcoin(N) >< C. } >

```

We can extend this module with another module for providing new coins:

```
  NewCoins = <{},{coin/0},{coin -> 15. coin -> 20.}>

```

simply by joining them to obtain
`MoneyChange` $``$ `NewCoins =`

```
    < {_=<_/2, _-_/2},
      {coin/0,getcoin/1,change/1},
      { coin -> 1. coin -> 5. coin -> 10. coin -> 15. coin -> 20.
        getcoin(N) -> C <= coin >< C, C =< N >< true.
        change(0) -> [].
        change(N) -> [C|change(N-C)] <= getcoin(N) >< C. } >

```

Union of modules is idempotent, associative, commutative, and there exists a null element: the module $`𝒪=<\sigma _o,\sigma _o,\mathrm{}>`$, where $`\sigma _o`$ is the empty signature of function symbols, representing the module with no rule.

###### Proposition 4.5

The union of modules has the following properties:

1. $`𝒫𝒪=𝒫`$, for every module $`𝒫`$.
2. $`𝒫𝒫=𝒫`$, for every module $`𝒫`$.
3. $`(𝒫𝒫_1)𝒫_2=𝒫(𝒫_1𝒫_2)`$, for all modules $`𝒫`$, $`𝒫_1`$ and $`𝒫_2`$.
4. $`𝒫_1𝒫_2=𝒫_2𝒫_1`$, for all modules $`𝒫_1`$ and $`𝒫_2`$.

Proof.
Obvious from the definition of the union of modules. $`\mathrm{}`$

The second operation is the closure of a module wrt a given signature $`\sigma `$. This operation makes accessible the signature $`\sigma `$ in an extensional way (i.e. only provable approximations can be used) and hides the rest. To define this operation, we need to introduce the notion of canonical rewrite rule.

###### Definition 4.6 (Canonical rewrite rule)

Given a term $`f(\overline{t})`$, with $`fFS_\mathrm{\Sigma }^n`$ and each $`t_i\mathrm{𝐂𝐓𝐞𝐫𝐦}_{}`$, and $`r\mathrm{𝐂𝐓𝐞𝐫𝐦}_{}`$, we define the canonical rewrite rule $`crr(f(\overline{t}),r)`$ which reduces $`f(\overline{t})`$ to $`r`$, as the rule $`f(\overline{t}^{})rC`$, constructed by substituting in $`\overline{t}`$ each occurrence of a repeated variable $`X`$ or $``$ with a fresh variable $`Y`$ and adding in $`C`$ a joinability statement $`XY`$ for each occurrence of a repeated variable $`X`$, and a statement $`XX`$ for each variable $`X`$ in $`r`$ and each variable with only one occurrence in $`\overline{t}`$.

In this way we obtain a program rule (with $`\overline{t}^{}`$ linear and each $`t_i^{}\mathrm{𝐂𝐓𝐞𝐫𝐦}`$) from which $`f(\overline{t})r`$ can be proved, because for $`\theta _{\overline{t}}\mathrm{𝐂𝐒𝐮𝐛𝐬𝐭}_{}`$ such that $`\theta _{\overline{t}}(Y)=X`$ for each fresh variable $`Y`$ that substitutes an occurrence of $`X`$ in $`\overline{t}`$, $`\theta _{\overline{t}}(Y)=`$ for each fresh variable $`Y`$ that substitutes an occurrence of $``$, and $`\theta _{\overline{t}}(X)=X`$ for all other variables, $`C\theta _{\overline{t}}`$ always can be proved and $`(f(\overline{t}^{})r)\theta _{\overline{t}}`$ is $`f(\overline{t})r`$.

###### Example 4.7

The canonical rewrite rule which reduces $`f(,b(X,Y),X)`$ to $`a(X,Z)`$ is:

$`f(V,b(X,Y),X1)a(X,Z)`$ $``$ $`\{X1X,YY,ZZ\},`$
and the associated substitution $`\theta _{\overline{t}}`$ is such that $`\theta _{\overline{t}}(X1)=X`$, $`\theta _{\overline{t}}(V)=`$, and $`\theta _{\overline{t}}(W)=W`$ for all other variables $`W`$. In this case $`C\theta _{\overline{t}}=\{XX,YY,ZZ\}`$ and all these joinability statements can be trivially derived from (RR) and (Jo), and therefore $`f(,b(X,Y),X)a(X,Z)`$ by the (OR) rule.

Now, we can define the closure of a module as follows.

###### Definition 4.8 (Closure wrt a signature)

Given a module $`𝒫=<\sigma _p,\sigma _e,>`$, its closure $`\overline{𝒫}^\sigma `$ wrt a signature of function symbols $`\sigma `$ is defined as the module:

$$<\sigma _o,\sigma _e^{},\{crr(f(\overline{t}),r)f/n\sigma ,r\mathrm{𝐂𝐓𝐞𝐫𝐦}_{},r,_{CRWL}f(\overline{t})r\}>,$$

where $`\sigma _o`$ denotes the empty signature of function symbols, $`t_i\mathrm{𝐂𝐓𝐞𝐫𝐦}_{}`$ for each component of the tuple $`\overline{t}`$, and $`\sigma _e^{}`$ is the corresponding exported signature.

The closure of a module is a module with a possibly infinite set of rules (although the exported signature is always finite) equivalent to the union of the graphs in $`_𝒫`$ of all functions defined in $`𝒫`$ and contained in $`\sigma `$. Note that $`\sigma _e^{}\sigma _e\sigma `$ because a function in $`\sigma _e\sigma `$ that depends on functions in the parameter signature could remain with no definition rule —or with the only rule $`f(\overline{t})`$— after closing the module. As a syntactic simplification we will write $`\overline{𝒫}`$ instead of $`\overline{𝒫}^{\sigma _e}`$ for each module $`𝒫=<\sigma _p,\sigma _e,>`$.

###### Example 4.9

Let us consider the following module about week days, where two functions are defined to get the `next` day and the day `before` of a given day.

```
  WeekDays = < {},
               {next/1,before/1},
               { next(mo) -> tu.   next(tu) -> we.   next(we) -> th.
                 next(th) -> fr.   next(fr) -> sa.   next(sa) -> su.
                 next(su) -> mo.
                 before(X) -> Y <= next(Y) >< X. }                     >

```

The closure of this module wrt its whole exported signature is the module
$`\overline{\mathrm{𝚆𝚎𝚎𝚔𝙳𝚊𝚢𝚜}}`$ `=`

```
             < {},
               {next/1,before/1},
               { next(mo) -> tu.   next(tu) -> we.   next(we) -> th.
                 next(th) -> fr.   next(fr) -> sa.   next(sa) -> su.
                 next(su) -> mo.
                 before(tu) -> mo.  before(we) -> tu.  before(th) -> we.
                 before(fr) -> th.  before(sa) -> fr.  before(su) -> sa.
                 before(mo) -> su. }            >

```

Closure wrt a signature is in some way the counterpart of the encapsulation operation ‘$``$’ in , but it is more general because it has a twofold effect: hiding all rules in the module and restricting the visible signature, so we need no intersection of modules —as is needed in — to restrict visibility in a closed module. Variables and bottom can appear in the rules of a closed module, but no functions in the parameter signature.

###### Proposition 4.10

Closure of modules has the following properties, where $`\sigma `$, $`\sigma _1`$ and $`\sigma _2`$ are signatures of function symbols,

1. $`\overline{𝒫}^\sigma =𝒪`$, for every module $`𝒫`$ and every signature $`\sigma `$ such that $`\sigma \mathrm{𝑒𝑥𝑝}(𝒫)=\sigma _o`$.
2. $`\overline{𝒪}^\sigma =𝒪`$, for every signature $`\sigma `$ and the null module $`𝒪`$.
3. $`\overline{𝒫}^{\sigma _1\sigma _2}=\overline{𝒫}^{\sigma _1}\overline{𝒫}^{\sigma _2}`$, for every module $`𝒫`$ and signatures $`\sigma _1`$, $`\sigma _2`$.
4. $`\overline{\overline{𝒫}^{\sigma _1}}^{\sigma _2}=\overline{𝒫}^{\sigma _1\sigma _2}=\overline{\overline{𝒫}^{\sigma _2}}^{\sigma _1}`$, for every module $`𝒫`$ and signatures $`\sigma _1`$, $`\sigma _2`$.
5. $`\overline{𝒫_1𝒫_2}^\sigma =\overline{𝒫_1}^\sigma \overline{𝒫_2}^\sigma `$, for modules $`𝒫_1`$ and $`𝒫_2`$ defining disjoint signatures and such that neither $`𝒫_1`$ nor $`𝒫_2`$ use the signature defined in the other module.

Proof.
Obvious from the definitions of the closure and the union of modules. $`\mathrm{}`$

Our third operation is the deletion of a signature in a module.

###### Definition 4.11 (Deletion of a signature)

Given a module $`𝒫=<\sigma _p,\sigma _e,>`$, the deletion in $`𝒫`$ of a signature of function symbols $`\sigma `$ produces the module:

$$𝒫\sigma =_{def}<\sigma _p^{},\sigma _e\sigma ,\sigma >,$$

where $`\sigma `$ denotes the set of those rules in $``$ defining function symbols not appearing in $`\sigma `$, and $`\sigma _p^{}`$ denotes the corresponding parameter signature.

We do not give an explicit expression for $`\mathrm{𝑝𝑎𝑟}(𝒫\sigma )`$ in terms of $`\mathrm{𝑝𝑎𝑟}(𝒫)`$ because new parameters can appear and old ones can disappear with the deletion of rules in $`\mathrm{𝑟𝑙}(𝒫)`$. However, $`\mathrm{𝑝𝑎𝑟}(𝒫\sigma )\sigma _p(\sigma _e\sigma )`$ is satisfied.

###### Example 4.12

In the module `OrdNatList` of Example 4.2 we can delete or abstract the signature `{isnat/1,leq/2}` to obtain the following parameterized module

```
  OrdNatList\{isnat/1,leq/2} =
    < {isnat/1,leq/2},
      {insert/2},
      { insert(X,[])     -> [X]              <= isnat(X) >< true.
        insert(X,[Y|Ys]) -> [X|[Y|Ys]]       <= leq(X,Y) >< true.
        insert(X,[Y|Ys]) -> [Y|insert(X,Ys)] <= leq(X,Y) >< false. } >

```

The resulting module is now parameterized by the two symbol functions `isnat/1` and `leq/2`, whereas only the function `insert/2` is exported.

This operation recalls the undefine clause in the object-oriented language Eiffel, and we will use it (combined with the union) to perform inheritance with overriding. Note the differences between the deletion of a signature and the closure wrt a signature. The former operation removes rules defining function symbols in the signature —but not those rules containing invocations in their rhs or condition— whereas the latter only hides the definitions of the functions in the signature, but maintains their consequences —hiding all other functions.

###### Proposition 4.13

The deletion of a signature (of function symbols) in a module has the following properties, where $`\sigma `$, $`\sigma _1`$ and $`\sigma _2`$ are signatures of function symbols,

1. $`𝒫\sigma =𝒪`$, for every module $`𝒫`$ and every $`\sigma `$ such that $`\mathrm{𝑒𝑥𝑝}(𝒫)\sigma `$.
2. $`𝒫\sigma =𝒫`$, for every module $`𝒫`$ and every $`\sigma `$ such that $`\mathrm{𝑒𝑥𝑝}(𝒫)\sigma =\sigma _o`$.
3. $`(𝒫\sigma _1)\sigma _2=𝒫(\sigma _1\sigma _2)=(𝒫\sigma _2)\sigma _1`$, for all modules $`𝒫`$ and $`\sigma _1`$, $`\sigma _2`$.
4. $`(𝒫_1𝒫_2)\sigma =(𝒫_1\sigma )(𝒫_2\sigma )`$, for all modules $`𝒫_1`$, $`𝒫_2`$ and signatures $`\sigma `$.
5. $`(\overline{𝒫}^{\sigma _1})\sigma _2=\overline{𝒫}^{(\sigma _1\sigma _2)}`$, for all modules $`𝒫`$ and signatures $`\sigma _1`$, $`\sigma _2`$.
6. $`\overline{𝒫}^\sigma =\overline{𝒫}(\sigma _e\sigma )`$, for a module $`𝒫`$, with exported signature $`\sigma _e`$, and all $`\sigma `$.

Proof.
Obvious from the definitions of the deletion, union and closure. $`\mathrm{}`$

Finally, we introduce a renaming operation that allows us to change function symbols with other function symbols of the same arity, in the global signature $`\mathrm{\Sigma }_{}`$. Therefore, given a module $`𝒫`$ and a function symbols renaming $`\rho `$, we define the renaming of $`𝒫`$ by $`\rho `$ as a new module $`\rho (𝒫)`$ where rules are conveniently renamed. The following definition formalizes this idea.

###### Definition 4.14 (Renaming)

Given a module $`𝒫=<\sigma _p,\sigma _e,>`$ and a function symbol renaming $`\rho `$, $`𝒫`$ renamed by $`\rho `$ is the module

$$\rho (𝒫)=_{def}<\rho ^{}(\sigma _p)\rho ^{}(\sigma _e),\rho ^{}(\sigma _e),\rho ^{}()>,$$

where $`\rho ^{}(\sigma )`$ is the signature resulting from applying $`\rho `$ to all symbols in $`\sigma `$, and $`\rho ^{}()`$ is the set of rules resulting from applying $`\rho `$ to all rules in $``$.

The following example illustrates the usefulness of this operation to adequate parameter names of a module.

###### Example 4.15

In the module `OrdNatList\{isnat/1,leq/2}` of Example 4.12 we can rename the function symbol `isnat/1` with the new name `isbasetype/1` to obtain a more appropriate parameterized module

```
  OrdList = {isnat/1 -> isbasetype/1}(OrdNatList\{isnat/1,leq/2}),

```

where we have denoted the corresponding renaming function $`\rho `$ as the set of pairs $`f/n\rho (f/n)`$ such that $`f/n\rho (f/n)`$. This module has the following appearance

```
  OrdList =
    <{isbasetype/1,leq/2},
     {insert/2},
     {insert(X,[])     -> [X]              <= isbasetype(X) >< true.
      insert(X,[Y|Ys]) -> [X|[Y|Ys]]       <= leq(X,Y) >< true.
      insert(X,[Y|Ys]) -> [Y|insert(X,Ys)] <= leq(X,Y) >< false.} >

```

Now, the parameters become `isbasetype/2` and `leq/2`.

We will use this operation to change function names in exportation, importation and, specially, in instantiation for matching function names in the parameter signature of a module with function names in the exported signature of another module. See Section 4.2 for some illustrative examples.

###### Proposition 4.16

Renaming of modules has the following properties, where $`\rho `$, $`\rho _1`$ and $`\rho _2`$ are function symbol renamings,

1. $`\iota (𝒫)=𝒫`$, for every module $`𝒫`$, where $`\iota `$ is the identity renaming.
2. $`\rho (𝒪)=𝒪`$, for every $`\rho `$.
3. $`\rho _2(\rho _1(𝒫))=(\rho _2\rho _1)(𝒫)`$, for all modules $`𝒫`$ and all $`\rho _1`$, $`\rho _2`$.
4. $`\rho (𝒫_1𝒫_2)=\rho (𝒫_1)\rho (𝒫_2)`$, for all modules $`𝒫_1`$, $`𝒫_2`$ and all $`\rho `$.
5. $`\rho (\overline{𝒫}^\sigma )=\overline{\rho (𝒫)}^{\rho ^{}(\sigma )}`$, for all modules $`𝒫`$, signatures $`\sigma `$ and injective $`\rho `$.
6. $`\rho (𝒫\sigma )=\rho (𝒫)\rho ^{}(\sigma )`$, for all modules $`𝒫`$, signatures $`\sigma `$ and injective $`\rho `$.

Proof.
Obvious from the definitions of deletion, union, closure and renaming. $`\mathrm{}`$

### 4.2 Other Modular Constructions in CRWL-programming

Our notion of module is basically that of a program inside a context made up of other programs providing explicit rules for function symbols and implicit declarations of constructor symbols, all together defining a global signature $`\mathrm{\Sigma }_{}`$. In this section, we will show how the operations that we have defined above can be used to model typical module interconnections used in conventional modular programming languages. We will introduce new operations with modules for these relationships, but all these will be defined as derived expressions from the basic set. These expressions will reflect the relationship between the module denoted by the expression and its component modules, and the resulting modules will be interpreted as flat modules in all cases.

The closure of a module $``$ wrt a signature $`\sigma `$ gives a form of encapsulation, hiding those function symbols in $``$ that are not in $`\sigma `$, and making the function symbols in $``$ and $`\sigma `$ visible but only in an extensional way, i.e., by the results —as partial constructor $`\mathrm{\Sigma }`$-terms— of the function applications to constructor $`\mathrm{\Sigma }`$-terms (including variables). Thus, we can provide an export with encapsulation operation ‘$`\mathrm{}`$’ over modules, in this simple way

$$\sigma \mathrm{}=_{def}\overline{}^\sigma .$$

The union of modules reflects the behavior of some logic programming systems that allow adding new programs —saved in separate files— to the main database. With this operation, but modifying one of its arguments, we can express different forms of importation and instantiation. We can define an import operation $``$ between modules as the union of a module $``$ —representing the body of the importing module— with the closure of the imported module $`𝒩`$ as follows

$$𝒩=_{def}\overline{𝒩}.$$

Module $`𝒩`$ imports $`𝒩`$, which means that only the consequences of the functions defined in $`𝒩`$ are imported, and not their rules. When $`\mathrm{𝑒𝑥𝑝}()\mathrm{𝑒𝑥𝑝}(𝒩)=\sigma _o`$ we have a typical importation because functions defined in $`𝒩`$ are only reduced in $`𝒩`$. We can also express selective importation of a signature $`\sigma `$ from $`𝒩`$ by combining importation with exportation, in order to restrict the visible signature of the imported module:

$$(\sigma \mathrm{}𝒩),\text{ with }\sigma \mathrm{𝑒𝑥𝑝}(𝒩)$$

This expression is equivalent to $`\overline{𝒩}^\sigma `$ by Proposition 4.10(4). Multiple importation or (selective) importation from several modules can be written as

$$(\mathrm{}((\sigma _1\mathrm{}𝒩_1))\mathrm{})(\sigma _k\mathrm{}𝒩_k),$$

where the importation order is not relevant by Propositions 4.5(3,4) and 4.10(4,5). It can be easily proved that this expression is equivalent to the single importation

$$((\sigma _1\mathrm{}𝒩_1)\mathrm{}(\sigma _k\mathrm{}𝒩_k)).$$

Importation with renaming can be expressed by an expression of the form

$$\rho (\sigma \mathrm{}𝒩)$$

with $`\sigma \mathrm{𝑒𝑥𝑝}(𝒩)`$, and an injective function symbol renaming $`\rho `$ (see Proposition 4.16(5)). By the properties of renaming this expression is equivalent to

$$(\rho ^{}(\sigma )\mathrm{}\rho (𝒩))$$

and can be reduced to $`\rho (\overline{𝒩}^\sigma )`$.

###### Example 4.17

Let us consider the module `OrdList` in Example 4.15 and the new module

```
  OrdNat =
    < {},
      {isnat/1, leq/2, geq/2},
      { isnat(zero)    -> true.
        isnat(succ(X)) -> isnat(X).
        leq(zero,zero)       -> true.
        leq(zero,succ(X))    -> isnat(X).
        leq(succ(X),zero)    -> false <= isnat(X) >< true.
        leq(succ(X),succ(Y)) -> leq(X,Y).
        geq(X,Y)             -> leq(Y,X). } >

```

where we define the predicate `isnat/1` and the two order relationships `leq/2` (less than or equal to) and `geq/2` (greater than or equal to). The importation

$$\mathrm{𝙾𝚛𝚍𝙻𝚒𝚜𝚝}\mathtt{\{isnat/1\; ->\; isbasetype/1\}(OrdNat)}$$

is a module with an infinite number of rules for `isbasetype/1`, `leq/2` and `geq/2` (all possible reductions to true or false), that behaves as calls to `isbasetype/1` and `leq/2` are reduced in `OrdNat` as calls to `isnat/1` and `leq/2` itself respectively.

Thus a typical program $``$ with a hierarchical structure in the sense of standard modular programming, i.e., importing from several modules $`𝒩_1,\mathrm{},𝒩_k`$, possibly with renaming, can be built up from a plain program $`𝒫`$ —its body— and the imported modules as

$$=𝒫(\rho _1(\sigma _1\mathrm{}𝒩_1)\mathrm{}\rho _k(\sigma _k\mathrm{}𝒩_k)),$$

with $`\sigma _1\mathrm{𝑒𝑥𝑝}(𝒩_1)`$, …, $`\sigma _k\mathrm{𝑒𝑥𝑝}(𝒩_k)`$ and $`\mathrm{𝑝𝑎𝑟}(𝒫)(\rho _1^{}(\sigma _1)\mathrm{}\rho _k^{}(\sigma _k))`$. This expression can be reduced to $`𝒫\rho _1(\overline{𝒩_1}^{\sigma _1})\mathrm{}\rho _k(\overline{𝒩_k}^{\sigma _k})`$.

Because our basic modules can be parameterized, we can instantiate function symbols of the parameterized signature of a module $``$ with function symbols, of the same arity but different name, exported by other module $`𝒩`$, simply by renaming suitably the parameters of $``$ to fit (a part of) the exported signature of $`𝒩`$. Thus we obtain an instantiation operation that we denote $`[𝒩,\rho ]`$ and define as

$$[𝒩,\rho ]=_{def}\rho ()𝒩,$$

where $`\rho `$ is the function symbol renaming that characterizes the instantiation. This operation makes sense when $`\rho ^{}(\mathrm{𝑝𝑎𝑟}())\mathrm{𝑒𝑥𝑝}(𝒩)\sigma _o`$. When $`\mathrm{𝑝𝑎𝑟}(\rho ())\mathrm{𝑒𝑥𝑝}(𝒩)`$ the instantiation is total and is partial in another case. Note that instantiation can be seen as a special form of importation. The difference between a (renamed) importation $`\rho (𝒩)`$ and an instantiation $`\rho ()𝒩`$ is that in the former, symbols in the parameter signature of $``$ refer to actual names in the exported signature of the imported module $`𝒩`$ (renamed by $`\rho `$), whereas in the latter, symbols in the parameter signature of $``$ behave as true parameters being replaced (by $`\rho `$) with actual values of the exported signature of $`𝒩`$.

###### Example 4.18

Let us consider again the module `OrdList` in Example 4.15 and the module `OrdNat` defined in Example 4.17. The instantiation

$$\mathtt{OrdList[OrdNat,\{isbasetype/1\; ->\; isnat/1,\; leq/2\; ->geq/2\}]}$$

is equivalent to a module, also with an infinite number of rules, but defining the predicates `isnat/1` and `geq/2` instead of `isbasetype/1` and `leq/2` respectively.

Deletion of a signature $`\sigma `$ in a module removes all rules defining function symbols in that signature but maintains the occurrences of these symbols in the rhs of the other rules. This operation can be used to  abstract a signature $`\sigma `$ from a module $``$ in the following way

$$[\sigma ]=_{def}\sigma .$$

This abstraction operation makes sense when $`\sigma \mathrm{𝑒𝑥𝑝}()`$ and each function symbol in $`\sigma `$ appears in some rule of $`\mathrm{𝑟𝑙}(\sigma )`$. This operation is very useful for making generic modules from concrete ones but unfortunately it is not implemented in conventional modular programming systems. As an example of the use of this operation we refer to Example 4.12. Also, with the deletion operation, we can model a sort of inheritance relationship between modules. Inheritance with overriding may be captured by means of union and deletion of a signature in the following way

$$\mathrm{𝑖𝑠𝑎}𝒩=_{def}(𝒩\mathrm{𝑒𝑥𝑝}()).$$

Module $`\mathrm{𝑖𝑠𝑎}𝒩`$ inherits all functions in $`𝒩`$ —with their rules— not defined in $``$ and uses the rules of $``$ for all functions defined in $``$, overriding the definition rules in $`𝒩`$, for common functions. In this case, overriding is carried out by deleting the common signature of the inherited module before adding it to the derived module.

###### Example 4.19

Let us consider a module defining some operations on polygonal lines and parameterized wrt an addition operation `_+_/2`, a predicate `ispoint/1` to test if something is a point, and operations `distance/2` and `translatepoint/2` for computing the distance between points and the point resulting of applying a translation, given by a vector (its second argument), to another point (its first argument).

```
  Polygonal =
  <{_+_/2, ispoint/1, distance/2, translatepoint/2 },
   {perimeter/1,translate/2 },
   {perimeter([P1])         -> zero <= ispoint(P1) >< true.
    perimeter([P1|[P2|Ps]]) -> distance(P1,P2)+perimeter([P2|Ps]).
    translate([P1],V)         -> [translatepoint(P1,V)].
    translate([P1|[P2|Ps]],V) -> [translatepoint(P1,V)|translate([P2|Ps],V)].} >

```

(where we suppose that `distance/2` and `translatepoint/2` check that their arguments are points). Let us also consider another module defining some operations on squares and also parameterized wrt a multiplication operation `_*_/2`, and the above operations `ispoint/1` and `distance/2`.

```
  Square =
  < {_*_/2, ispoint/1, distance/2},
    {issquare/1, side/1, perimeter/1, surface/1},
    {issquare([P1,P2,P3,P4]) -> true <= distance(P1,P2) >< distance(P2,P3),
                                        distance(P2,P3) >< distance(P3,P4),
                                        distance(P1,P2) >< distance(P3,P4).
      side([P1,P2,P3,P4]) -> distance(P1,P2) <= issquare([P1,P2,P3,P4]) >< true.
      perimeter(C) -> 4*side(C)       <= issquare(C) >< true.
      surface(C)   -> side(C)*side(C) <= issquare(C) >< true.} >.

```

With these modules we could define a new module `SquarePolygone` making module `Square` inherit from `Polygonal`,

$$\mathtt{SquarePolygone\; =\; Square\; isa\; Polygonal.}$$

The resulting module would be

```
  SquarePolygone =
  < {_+_/2, _*_/2, ispoint/1, distance/2, translatepoint/2},
    {issquare/1, side/1, perimeter/1, surface/1, translate/2},
    {issquare([P1,P2,P3,P4]) -> true <= distance(P1,P2) >< distance(P2,P3),
                                        distance(P2,P3) >< distance(P3,P4),
                                        distance(P1,P2) >< distance(P3,P4).
      side([P1,P2,P3,P4]) -> distance(P1,P2) <= issquare([P1,P2,P3,P4]) >< true.
      perimeter(C) -> 4*side(C)       <= issquare(C) >< true.
      surface(C)   -> side(C)*side(C) <= issquare(C) >< true.
      translate([P1],V)         -> [translatepoint(P1,V)].
      translate([P1|[P2|Ps]],V) -> [translatepoint(P1,V)|translate([P2|Ps],V)].} >.

```

Note that `perimeter/1`, defined in the module `Polygonal`, has been redefined with the version of the module `Square`. The function `translate/2` has been inherited from `Polygonal`.

## 5 A Compositional Semantics

A module is basically a program because its interface can be extracted from its set of rules when we know the data constructor symbols, and operations defined on modules are operations on their sets of rules, i.e., operations on programs. The difference between a program and a program module is that a module can be thought of as a program piece that can be assembled with other pieces to build larger programs (this is one of the main reasons of making explicit their interfaces).

With this idea in mind, the model-theoretic semantics defined for CRWL-programs is not suitable for program modules because it is not compositional wrt the operations defined over modules as we can see in the following example.

###### Example 5.1

Let $`\mathrm{\Sigma }`$ be a signature $`(\{a/0,b/0,c/0\},\{p/1,r/1\})`$, and modules $`𝒫_1`$ and $`𝒫_2`$ with the following sets of rules:

$$rl(𝒫_1)=\{p(a)c\}rl(𝒫_2)=\{p(a)c,r(b)cp(b)c\}.$$

These modules have the same model-theoretic semantics, $`_{𝒫_1}=_{𝒫_2}`$, which is the CRWL-algebra $`𝒜`$ with functions $`p^𝒜`$ and $`r^𝒜`$ such that

$$\begin{array}{c}p^𝒜(a)=\{c,\},p^𝒜(b)=p^𝒜(c)=p^𝒜()=\{\},p^𝒜(X)=\{\},X𝒱\hfill \\ r^𝒜(a)=\{\},r^𝒜(b)=r^𝒜(c)=r^𝒜()=\{\},r^𝒜(X)=\{\},X𝒱.\hfill \end{array}$$

However, their unions with $`𝒬`$, such that $`rl(𝒬)=\{p(b)c\}`$, have different model-theoretic semantics. The intended model of $`𝒫_1𝒬`$ has a function $`r^{_{𝒫_1𝒬}}`$ such that $`r^{_{𝒫_1𝒬}}(b)=\{\}`$, whereas $`r^{_{𝒫_2𝒬}}(b)=\{c,\}`$. So, $`_{𝒫_1𝒬}_{𝒫_2𝒬}`$.

The compositionality of the semantics of a programming language is particularly relevant when modularity is involved. In fact, one of the most critical aspects in modular systems is the possibility of making a separate compilation of modules, and this can only be made in the presence of some kind of compositionality.

### 5.1 Compositionality and Full Abstraction

In order to study the compositionality and full abstraction of a semantics, we have to clearly set out these notions. We will adopt the approach proposed in , where compositionality and full abstraction are defined in terms of the equivalence relation between programs induced by the semantics.

###### Definition 5.2 (Compositional relation)

Given an equivalence relation $``$ defined between programs, an observation function Ob defined for programs, and a set Oper of operations with programs, we say that

1. $``$ preserves Ob iff for all programs $`𝒫`$ and $`𝒬`$, $`𝒫𝒬Ob(𝒫)=Ob(𝒬);`$
2. $``$ is a congruence wrt Oper iff for all programs $`𝒫_i`$ and $`𝒬_i`$ and all $`O\mathrm{𝑂𝑝𝑒𝑟}`$, $`𝒫_i𝒬_i`$, for $`i=1,\mathrm{},n`$, implies $`O(𝒫_1,\mathrm{},𝒫_n)O(𝒬_1,\mathrm{},𝒬_n)`$;
3. $``$ is compositional wrt $`(\mathrm{𝑂𝑏},\mathrm{𝑂𝑝𝑒𝑟})`$ iff it is a congruence wrt Oper and preserves $`Ob`$.

To set the notion of full abstraction for an equivalence relation, we need some way of distinguishing programs and for that reason we introduce the notion of context. Given a set of operations on programs Oper, and a metavariable $`𝒳`$, we define contexts $`C[[𝒳]]`$ inductively as follows: $`𝒳`$ and each program is a context, also for each operation $`O\mathrm{𝑂𝑝𝑒𝑟}`$ with $`n`$ program arguments and $`C_1,\mathrm{},C_n`$ contexts, $`O(C_1,\mathrm{},C_n)`$ is a context. Two programs $`𝒫`$ and $`𝒬`$ are distinguishable under $`(\mathrm{𝑂𝑏},\mathrm{𝑂𝑝𝑒𝑟})`$ if there exists a context $`C[[𝒳]]`$ such that $`C[[𝒫]]`$ and $`C[[𝒬]]`$ have different external behavior, i.e. $`Ob(C[[𝒫]])Ob(C[[𝒬]])`$. When $`𝒫`$ and $`𝒬`$ are indistinguishable under $`(\mathrm{𝑂𝑏},\mathrm{𝑂𝑝𝑒𝑟})`$ we will write $`𝒫_{\mathrm{𝑂𝑏},\mathrm{𝑂𝑝𝑒𝑟}}𝒬`$, i.e. for all contexts $`C`$, $`\mathrm{𝑂𝑏}(C[[𝒫]])=\mathrm{𝑂𝑏}(C[[𝒬]])`$.

###### Definition 5.3 (Fully abstract relation)

An equivalence relation $``$ is fully abstract wrt $`(\mathrm{𝑂𝑏},\mathrm{𝑂𝑝𝑒𝑟})`$ iff for all programs $`𝒫`$ and $`𝒬`$, $`𝒫_{\mathrm{𝑂𝑏},\mathrm{𝑂𝑝𝑒𝑟}}𝒬𝒫𝒬.`$

A semantics $`𝒮`$ for a programming language provides a meaning for programs and also induces an equivalence relation $`_𝒮`$ between programs: two programs are equivalent iff they have the same meaning in this semantics. This equivalence relation is used for defining compositionality and full abstraction for semantics.

###### Definition 5.4 (Compositional and fully abstract semantics)

A semantics $`𝒮`$ is compositional or fully abstract wrt $`(\mathrm{𝑂𝑏},\mathrm{𝑂𝑝𝑒𝑟})`$ iff its corresponding relation $`_𝒮`$ is compositional or fully abstract, respectively, wrt $`(\mathrm{𝑂𝑏},\mathrm{𝑂𝑝𝑒𝑟})`$.

Obviously, for each pair $`(\mathrm{𝑂𝑏},\mathrm{𝑂𝑝𝑒𝑟})`$ there exits a compositional and fully abstract relation between programs, the relation

$$𝒫_{(\mathrm{𝑂𝑏},\mathrm{𝑂𝑝𝑒𝑟})}𝒬_{def}\mathrm{𝑂𝑏}(C[[𝒫]])=\mathrm{𝑂𝑏}(C[[𝒬]]),\text{for every context}C[[𝒳]].$$

For each compositional equivalence relation $``$, it is easy to see that $`𝒫𝒬𝒫_{(\mathrm{𝑂𝑏},\mathrm{𝑂𝑝𝑒𝑟})}𝒬`$, and for each fully abstract equivalence relation $``$, $`𝒫_{(\mathrm{𝑂𝑏},\mathrm{𝑂𝑝𝑒𝑟})}𝒬𝒫𝒬`$. Thus, $`_{(\mathrm{𝑂𝑏},\mathrm{𝑂𝑝𝑒𝑟})}`$ will be the only equivalence relation which is both compositional and fully abstract wrt $`(\mathrm{𝑂𝑏},\mathrm{𝑂𝑝𝑒𝑟})`$. And the more adequate semantics for programs (wrt $`(\mathrm{𝑂𝑏},\mathrm{𝑂𝑝𝑒𝑟})`$) will be a semantics that induces this relation.

### 5.2 The $`𝒯`$-Semantics

To find a compositional semantics we may think about programs as open in the sense that we can build up programs from other programs adding rules for new functions and also for already defined functions (of the signature $`\mathrm{\Sigma }`$ we were in) and imagine them as algebra transformers as is done in  and . The operator $`𝒯_𝒫`$ considered as a function $`\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$ is a good candidate for the intended meaning of a program $`𝒫`$. First, we have to note that the set $`[\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }]`$ of all continuous functions from $`\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$ to $`\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$, ordered by the relation

$$𝒯_1𝒯_2_{def}𝒜\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }(𝒯_1(𝒜)𝒯_2(𝒜)),$$

with the least upper bound and the greatest lower bound of a finite set $`\{𝒯_i\}_{iI}`$ of functions pointwise defined as

$$(_{iI}𝒯_i)(𝒜)=_{iI}(𝒯_i(𝒜))\text{ and }(_{iI}𝒯_i)(𝒜)=_{iI}(𝒯_i(𝒜))$$

respectively, and with bottom $`𝕋_{}`$ and top $`𝕋_\mathrm{\Sigma }`$ such that

$$𝕋_{}(𝒜)=_\mathrm{\Sigma }\text{ and }𝕋_\mathrm{\Sigma }(𝒜)=_\mathrm{\Sigma },𝒜\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma },$$

is a complete lattice as a consequence of $`(\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma },)`$ being a complete lattice. Now, we can associate a program with the corresponding immediate consequence operator, instead of its least fixpoint.

###### Definition 5.5 ($`𝒯`$-semantics)

We define the $`𝒯`$-semantics by denoting the meaning of a program $`𝒫`$ by its algebra transformer $`[\{𝒫\}]_T=_{\mathrm{𝑑𝑒𝑓}}𝒯_𝒫`$, where $`𝒯_𝒫`$ is intended as $`𝒯_{rl(𝒫)}`$.

This semantics entails the following equivalence relation on programs: $`𝒫_T𝒬_{def}𝒯_𝒫=𝒯_𝒬`$. Thus, two programs are $`_T`$-equivalent if both define the same immediate consequences operator. In this context, and coinciding with logic programming, a natural choice of the observable behavior of a program $``$ is its model-theoretic semantics. So we will adopt as observation function $`Ob()=_{\mathrm{𝑑𝑒𝑓}}_{}`$. Notice that $`_{}`$ captures the graphs of all functions defined in $``$, whereas functions not included in the program are considered totally undefined (their images only can be reduced to $``$). The semantics $`[\{\}]_T`$ is compositional wrt this observation function and the set of operations $`Oper=\{,\overline{()}^\sigma ,()\sigma ,\rho ()\}`$. We can prove this fact by proving that $`[\{\}]_T`$ is homomorphic in the following sense.

###### Theorem 5.6

Given a global signature $`\mathrm{\Sigma }`$ and a countable set of variable symbols $`𝒱`$, for all programs $`𝒫`$, $`𝒫_1`$ and $`𝒫_2`$ defined over $`\mathrm{\Sigma }`$, every subsignature of function symbols $`\sigma FS_\mathrm{\Sigma }`$, and every function symbol renaming $`\rho `$, we have the following results

$$\begin{array}{cccc}(a)\hfill & \hfill [\{𝒫_1𝒫_2\}]_T& =& [\{𝒫_1\}]_T[\{𝒫_2\}]_T;\hfill \\ (b)\hfill & \hfill [\{\overline{𝒫}^\sigma \}]_T& =& \lambda 𝒜([\{𝒫\}]_T^\omega (_\mathrm{\Sigma }))|_\sigma ;\hfill \\ (c)\hfill & \hfill [\{𝒫\sigma \}]_T& =& [\{𝒫\}]_T𝕋_{exp(𝒫)\sigma };\hfill \\ (d)\hfill & \hfill [\{\rho (𝒫)\}]_T& =& 𝒯_{\rho ^1}[\{𝒫\}]_T𝒯_\rho ;\hfill \end{array}$$

where, for every algebra $`𝒜\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$ and every subsignature $`\sigma FS_\mathrm{\Sigma }`$, $`𝒜|_\sigma `$ is the term algebra characterized by

$$\begin{array}{cccc}\hfill f^{𝒜|_\sigma }(\overline{t})& =& f^𝒜(\overline{t}),\hfill & \text{ for all }t_1,\mathrm{},t_n\mathrm{𝐂𝐓𝐞𝐫𝐦}_{},\text{ if }f/n\sigma ,\hfill \\ \hfill f^{𝒜|_\sigma }(\overline{t})& =& \{\},\hfill & \text{ for all }t_1,\mathrm{},t_n\mathrm{𝐂𝐓𝐞𝐫𝐦}_{},\text{ otherwise.}\hfill \end{array}$$

For each subsignature $`\sigma FS_\mathrm{\Sigma }`$, $`𝕋_\sigma `$ is the constant algebra transformer that, for all $`𝒜\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$ produces the same term algebra $`_\sigma `$ characterized by

$$\begin{array}{cccc}\hfill f^_\sigma (\overline{t})& =& \mathrm{𝐂𝐓𝐞𝐫𝐦}_{},\hfill & \text{ for all }t_1,\mathrm{},t_n\mathrm{𝐂𝐓𝐞𝐫𝐦}_{},\text{ if }f/n\sigma ,\hfill \\ \hfill f^_\sigma (\overline{t})& =& \{\},\hfill & \text{ for all }t_1,\mathrm{},t_n\mathrm{𝐂𝐓𝐞𝐫𝐦}_{},\text{ otherwise.}\hfill \end{array}$$

And, for each rename $`\rho `$, $`𝒯_\rho `$ and $`𝒯_{\rho ^1}`$ are the algebra transformers defined by $`𝒯_\rho (𝒜)=𝒜_\rho `$ and $`𝒯_{\rho ^1}(𝒜)=𝒜_{\rho ^1}`$ where $`𝒜_\rho `$ and $`𝒜_{\rho ^1}`$ are the term algebras characterized by

$$f^{𝒜_\rho }=\rho (f)^𝒜\text{ and }f^{𝒜_{\rho ^1}}=\{\begin{array}{cc}\{g^𝒜|f=\rho (g)\},\hfill & \text{when this set is not empty,}\hfill \\ f^_\mathrm{\Sigma }\hfill & \text{otherwise,}\hfill \end{array}$$

for every function symbol $`f`$ in $`FS_\mathrm{\Sigma }`$.

Proof.
$`(a)`$ For the first result we have to prove that $`𝒯_{𝒫_1𝒫_2}(𝒜)=𝒯_{𝒫_1}(𝒜)𝒯_{𝒫_2}(𝒜)`$, for all $`𝒜\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$. For each $`fFS_\mathrm{\Sigma }^n`$, with $`n0`$, and $`t_1,\mathrm{},t_n\mathrm{𝐂𝐓𝐞𝐫𝐦}_{}`$, $`f^{𝒯_{𝒫_1𝒫_2}(𝒜)}(\overline{t})=f^{𝒯_{𝒫_1}(𝒜)}(\overline{t})f^{𝒯_{𝒫_2}(𝒜)}(\overline{t}),`$ because every rule in $`𝒫_1𝒫_2`$ with an instance that can be used in the construction of $`f^{𝒯_{𝒫_1𝒫_2}(𝒜)}(\overline{t})`$ is also a rule in $`𝒫_1`$ or $`𝒫_2`$, and the same instance can be used to construct $`f^{𝒯_{𝒫_1}(𝒜)}(\overline{t})`$ or $`f^{𝒯_{𝒫_2}(𝒜)}(\overline{t})`$ respectively, because the applicability of this instance only depends on its arguments and the term algebra $`𝒜`$. Reciprocally, every rule in $`𝒫_1`$ or $`𝒫_2`$ with an instance applicable to construct $`f^{𝒯_{𝒫_1}(𝒜)}(\overline{t})`$ or $`f^{𝒯_{𝒫_2}(𝒜)}(\overline{t})`$ is a rule in $`𝒫_1𝒫_2`$ with the same instance applicable to construct $`f^{𝒯_{𝒫_1𝒫_2}(𝒜)}(\overline{t})`$ for the same reason. Finally, by definition of the operation $``$ between term algebras, $`f^{𝒯_{𝒫_1}(𝒜)}(\overline{t})f^{𝒯_{𝒫_2}(𝒜)}(\overline{t})=f^{𝒯_{𝒫_1}(𝒜)𝒯_{𝒫_2}(𝒜)}(\overline{t}),`$ and therefore $`f^{𝒯_{𝒫_1𝒫_2}(𝒜)}(\overline{t})=f^{𝒯_{𝒫_1}(𝒜)𝒯_{𝒫_2}(𝒜)}(\overline{t})`$.

$`(b)`$ In order to prove the second result, as $`𝒯_𝒫^\omega (_\mathrm{\Sigma })=_𝒫`$, we only have to prove $`𝒯_{\overline{𝒫}^\sigma }(𝒜)=_𝒫|_\sigma `$ for all $`𝒜\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$. For $`fFS_\mathrm{\Sigma }^n`$ and $`t_1,\mathrm{},t_n\mathrm{𝐂𝐓𝐞𝐫𝐦}_{}`$, if $`f/n\sigma `$ then there is no rule for $`f`$ in $`\overline{𝒫}^\sigma `$ and $`f^{𝒯_{\overline{𝒫}^\sigma }(𝒜)}(\overline{t})=\{\}=f^{_𝒫|_\sigma }`$, and if $`f/n\sigma `$ then we will prove that $`f^{𝒯_{\overline{𝒫}^\sigma }(𝒜)}(\overline{t})=f^_𝒫(\overline{t})`$. For $`tf^{𝒯_{\overline{𝒫}^\sigma }(𝒜)}(\overline{t})`$ there exists $`crr(f(\overline{s}),r)=f(\overline{s}^{})rC`$ in $`\overline{𝒫}`$ and a substitution $`\theta `$ such that $`t[[r\theta ]]_{id}^A=r\theta `$ with $`\overline{s}^{}\theta \overline{t}`$ and $`𝒜_{id}C\theta `$, what means that $`\theta `$ is totally defined in variables of $`\overline{s}`$ and $`r`$. By the special joinability statement of $`C`$ we can obtain a total substitution $`\theta ^{}`$ (by considering only the part of $`\theta `$ involving the variables of $`\overline{s}`$ and $`r`$) such that $`\overline{s}\theta ^{}\overline{s}^{}\theta \overline{t}`$ and $`r\theta ^{}=r\theta `$. Since $`𝒫_{\mathrm{𝐶𝑅𝑊𝐿}}f(\overline{s})r`$, $`rf^_𝒫(\overline{s})`$, and as $`_𝒫`$ is consistent (see Section 6.2), $`r\theta ^{}f^_𝒫(\overline{s}\theta ^{})`$ and by the monotonicity of $`f^_𝒫`$, $`r\theta f^_𝒫(\overline{t})`$ and so, $`tf^_𝒫(\overline{t})`$. Reciprocally, $`tf^_𝒫(\overline{t})`$ implies $`𝒫f(\overline{t})t`$ or $`crr(f(\overline{t}),r)\overline{𝒫}`$ and, by considering $`\theta _{\overline{t}}`$, we have $`[[t\theta _{\overline{t}}]]_{id}^A=tf^{𝒯_{\overline{𝒫}^\sigma }(𝒜)}(\overline{t})`$ for every term algebra $`𝒜`$ and so, $`tf^{𝒯_{\overline{𝒫}^\sigma }(𝒜)}(\overline{t})`$

$`(c)`$ For this result we have to prove that $`𝒯_{𝒫\sigma }(𝒜)=𝒯_𝒫(𝒜)𝕋_{exp(𝒫)\sigma }(𝒜)`$, for all $`𝒜\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$, and this is equivalent to $`f^{𝒯_{𝒫\sigma }(𝒜)}=f^{𝒯_𝒫(𝒜)}`$, for all $`f/nexp(𝒫)\sigma `$, and $`f^{𝒯_{𝒫\sigma }(𝒜)}(\overline{t})=\{\}`$, for all $`f/n\sigma `$. The first equality is easily proved by taking into account that $`𝒫`$ and $`𝒫\sigma `$ have the same rules for each $`f/nexp(𝒫)`$ and remembering that the applicability of every instance of these rules to construct $`f^{𝒯_{𝒫\sigma }(𝒜)}(\overline{t})`$ and $`f^{𝒯_𝒫(𝒜)}(\overline{t})`$ only depends on its arguments and the term algebra $`𝒜`$. The second equality is trivial because there is no rule in $`𝒫\sigma `$ for $`f/n\sigma `$.

$`(d)`$ For the last result we have to prove that $`𝒯_{\rho (𝒫)}(𝒜)=𝒯_{\rho ^1}(𝒯_𝒫(𝒯_\rho (𝒜)))`$ for all $`𝒜\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$. On the one hand $`f^{𝒯_{\rho (𝒫)}(𝒜)}(\overline{t})`$ is constructed from all rules $`g(\overline{s})rC`$ in $`𝒫`$, with $`\rho (g)=f`$, such that, for any $`\theta \mathrm{𝐂𝐒𝐮𝐛𝐬𝐭}_{}`$, $`(\rho (s_i))\theta t_i`$, for $`i=1,\mathrm{},n`$, and $`𝒜_{id}(\rho (C))\theta `$, by considering the union of the corresponding cones $`[[(\rho (r))\theta ]]_{id}^𝒜`$. On the other hand, $`f^{𝒯_{\rho ^1}(𝒯_𝒫(𝒯_\rho (𝒜)))}(\overline{t})`$ is $`f^{𝒯_{\rho ^1}(𝒯_𝒫(𝒜_\rho ))}(\overline{t})`$ and by the definition of $`𝒯_{\rho ^1}`$ this is equal to $`(\{g^{𝒯_𝒫(𝒜_\rho )}|\rho (g)=f\})(\overline{t})`$ which is the union of the cones $`g^{𝒯_𝒫(𝒜_\rho )}(\overline{t})`$, and each cone is constructed from all rules $`g(\overline{s})rC`$ in $`𝒫`$ such that, for any $`\theta \mathrm{𝐂𝐒𝐮𝐛𝐬𝐭}_{}`$, $`s_i\theta t_i`$, for $`i=1,\mathrm{},n`$, and $`𝒜_\rho _{id}C\theta `$, by considering the union of the corresponding cones $`[[r\theta ]]_{id}^{𝒜_\rho }`$. But, as the function renaming $`\rho `$ does not affect constructor terms or variables we have $`(\rho (s_i))\theta =s_i\theta `$; from Proposition 2.2(1), $`(\rho (C))\theta =\rho (C\theta )`$; and from Proposition 2.2(3), $`𝒜_{id}(\rho (C\theta ))𝒜_\rho _{id}C\theta `$. So, the same rules of $`𝒫`$ are used to construct $`f^{𝒯_{\rho (𝒫)}(𝒜)}(\overline{t})`$ and $`f^{𝒯_{\rho ^1}(𝒯_𝒫(𝒯_\rho (𝒜)))}(\overline{t})`$, and from Proposition 2.2(1,2), we conclude that both cones coincide. $`\mathrm{}`$

Thus, the meaning of the union of two programs $`(a)`$ can be extracted from the meaning of each one, the meaning of the closure of a program $`(b)`$ is obtained from the fixpoint of the program semantics, and deleting a signature from a program $`(c)`$ is semantically equivalent to the intersection of the program semantics with an algebra transformer which depends on the exported signature of the program. Nevertheless, the intersection we are mentioning here is not an operation over programs (as in ) but an operation on algebra transformers. The meaning of a renamed program $`(d)`$ can be obtained as the composition of the meaning of the program with two algebra transformers associated with the renaming and its reverse.

###### Corollary 5.7 (Compositionality of $`[\{\}]_T`$)

The semantics $`[\{\}]_T`$ is compositional with respect to $`(Ob,\{,\overline{()}^\sigma ,()\sigma ,\rho ()\})`$.

Proof.
The notion of observable, which coincides with the least fixpoint of the semantics, is obviously preserved by this semantics. On the other hand, the congruence property is directly derived from the previous theorem. We only need to justify that $`[\{𝒫\}]_T𝕋_{exp(𝒫)\sigma }=[\{𝒬\}]_T𝕋_{exp(𝒬)\sigma }`$, for every subsignature $`\sigma FS_\mathrm{\Sigma }`$, when $`[\{𝒫\}]_T=[\{𝒬\}]_T`$, independently on whether $`exp(𝒫)`$ is equal to $`exp(𝒬)`$ or not. In fact, if $`f/nexp(𝒫)\sigma `$ and $`f/nexp(𝒬)\sigma `$ then $`f/nexp(𝒬)`$, which implies $`f^{𝒯_𝒬(𝒜)}(\overline{t})=\{\}`$, for all $`t_1,\mathrm{},t_n\mathrm{𝐂𝐓𝐞𝐫𝐦}_{}`$ and $`f^{𝒯_𝒫(𝒜)}(\overline{t})=\{\}`$ because $`𝒯_𝒫=𝒯_𝒬`$. The same result is obtained if we suppose $`f/nexp(𝒫)\sigma `$ and $`f/nexp(𝒬)\sigma `$. Therefore, $`f^{(𝒯_𝒫𝕋_{exp(𝒫)\sigma })(𝒜)}(\overline{t})=f^{(𝒯_𝒬𝕋_{exp(𝒬)\sigma })(𝒜)}(\overline{t})`$. $`\mathrm{}`$

As the above corollary states, $`[\{\}]_T`$ is compositional wrt union, closure, deletion and renaming, when the canonic model of a program is taken as its observable behavior. However, the following example shows that it is not fully abstract.

###### Example 5.8

Let $`\mathrm{\Sigma }`$ be a signature $`(\{c/0,d/0\},\{f/0\})`$ and let $`𝒫`$ and $`𝒬`$ be the modules such that $`rl(𝒫)=\{fc,fd\}`$ and $`rl(𝒬)=\{fc,fdfc\}`$. They are indistinguishable under $`\{,\overline{()}^\sigma ,()\sigma ,\rho ()\}`$, but they are not $`_T`$-equivalent. In fact, $`𝒯_𝒫(_\mathrm{\Sigma })𝒯_𝒬(_\mathrm{\Sigma })`$ because $`f^{𝒯_𝒫(_\mathrm{\Sigma })}=\{c,d,\}`$ whereas $`f^{𝒯_𝒬(_\mathrm{\Sigma })}=\{c,\}`$.

The $`𝒯`$-semantics distinguishes more than the model-theoretic semantics, since the immediate consequence operator captures what is happening in each reduction step, but the non-full abstraction result means that this semantics distinguishes more than necessary. It is too fine. In the next section we will try a coarser semantics —also studied in logic programming — defined from the sets of pre-fixpoints of $`𝒯`$.

## 6 A Fully Abstract Semantics

In this section, a fully abstract semantics is presented, which is also compositional except for the deletion operation. For a better motivation, we will not introduce this semantics directly. Instead, we will define a first approximation, the so-called  term model semantics (Definition 6.1), which only is compositional (wrt the union, closure and renaming operations), and then we will obtain the full abstraction property by restricting the term models (Definition 6.10).

### 6.1 The Term Model Semantics

Formally, we will introduce the first semantics by directly considering the corresponding equivalence relation.

###### Definition 6.1 (Model equivalence)

Two programs $`𝒫`$ and $`𝒬`$ are model-equivalent iff their algebra transformers have the same pre-fixpoints

$$𝒫_M𝒬𝒜\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }(𝒯_𝒫(𝒜)𝒜𝒯_𝒬(𝒜)𝒜).$$

By Lemma 3.4 this means that two programs are equivalent iff they have the same term models.

This equivalence relation corresponds to the following semantics:

$$[\{𝒫\}]_M=_{\mathrm{𝑑𝑒𝑓}}\{|\text{ is a term model of }𝒫\}$$

which will be called  loose model-theoretic semantics, or simply term model semantics. In order to derive the corresponding result about compositionality, we need an auxiliary property about $`𝒯_\rho `$ and $`𝒯_{\rho ^1}`$.

###### Lemma 6.2

Given two term algebras $`𝒜,\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$, for every function symbol renaming $`\rho `$,

$$𝒜_{\rho ^1}𝒜_\rho \text{ or, equivalently, }𝒯_{\rho ^1}(𝒜)𝒜𝒯_\rho ().$$

Proof.
Let $`𝒜`$ and $``$ be two term algebras such that $`𝒜_{\rho ^1}`$. Then, for all function symbols $`f`$, $`f^{𝒜_{\rho ^1}}(\overline{t})f^{}(\overline{t})`$, for $`t_1,\mathrm{},t_n\mathrm{𝐂𝐓𝐞𝐫𝐦}_{}`$. This is equivalent to $`\{g^𝒜(\overline{t})|f=\rho (g)\}f^{}(\overline{t})`$. Thus, for all function symbols $`g`$, by considering their images $`\rho (g)=f`$, we obtain $`g^𝒜(\overline{t})\rho (g)^{}(\overline{t})=g^_\rho (\overline{t})`$ or, equivalently, $`𝒜_\rho `$. The implication in the other way is obtained by reversing this reasoning. $`\mathrm{}`$

This lemma claims that $`𝒯_{\rho ^1}`$ is, essentially, the reverse operator for $`𝒯_\rho `$.

###### Theorem 6.3 (Compositionality of $`[\{\}]_M`$)

For all programs $`𝒫,𝒬,𝒫_i,𝒬_i`$,

1. $`𝒫_M𝒬`$ implies $`Ob(𝒫)=Ob(𝒬)`$.
2. $`𝒫_i_M𝒬_i`$ for $`i=1,2`$, implies $`𝒫_1𝒫_2_M𝒬_1𝒬_2`$.
3. $`𝒫_M𝒬`$ implies $`\overline{𝒫}^\sigma _M\overline{𝒬}^\sigma `$, for every signature $`\sigma `$.
4. $`𝒫_M𝒬`$ implies $`\rho (𝒫)_M\rho (𝒬)`$, for every function symbol renaming $`\rho `$.

Therefore, the semantics $`[\{\}]_M`$ is compositional wrt $`(\mathrm{𝑂𝑏},\{,\overline{()}^\sigma ,\rho ()\})`$.

Proof.
1. If $`𝒫_M𝒬`$ then $`𝒫`$ and $`𝒬`$ have the same set of term models and, in particular, they have the same least term model. So $`Ob(𝒫)=Ob(𝒬).`$

2. Let $`𝒜`$ be a term model of $`𝒫_1𝒫_2`$, then $`𝒯_{𝒫_1𝒫_2}(𝒜)𝒜`$ and, by Theorem 5.6(a), $`𝒯_{𝒫_1}(𝒜)𝒯_{𝒫_2}(𝒜)=(𝒯_{𝒫_1}𝒯_{𝒫_2})(𝒜)=𝒯_{𝒫_1𝒫_2}(𝒜)𝒜`$, therefore $`𝒯_{𝒫_i}(𝒜)𝒜`$, for $`i=1,2`$. From $`𝒫_i_M𝒬_i`$, we obtain $`𝒯_{𝒬_i}(𝒜)𝒜`$, for $`i=1,2`$, and again by Theorem 5.6(a) $`𝒯_{𝒬_1𝒬_2}(𝒜)=(𝒯_{𝒬_1}𝒯_{𝒬_2})(𝒜)=𝒯_{𝒬_1}(𝒜)𝒯_{𝒬_2}(𝒜)𝒜`$, and $`𝒜`$ will be a term model of $`𝒬_1𝒬_2`$. By reasoning in a similar way, it can be obtained that all term models of $`𝒬_1𝒬_2`$ are also term models of $`𝒫_1𝒫_2`$ and this proves that $`𝒫_1𝒫_2_M𝒬_1𝒬_2`$.

3. To prove the third statement we only need to take into account that, by the first statement, $`𝒫_M𝒬`$ implies $`_𝒫=_𝒬`$ and therefore $`_𝒫|_\sigma =_𝒬|_\sigma `$, for all $`\sigma FS_\mathrm{\Sigma }`$. And, by Theorem 5.6(b), this implies $`𝒯_{\overline{𝒫}^\sigma }=𝒯_{\overline{𝒬}^\sigma }`$. Therefore, they will have the same pre-fixpoints and consequently $`\overline{𝒫}^\sigma _M\overline{𝒬}^\sigma `$.

4. Finally, for each term model $`𝒜`$ of $`\rho (𝒫)`$, $`𝒯_{\rho (𝒫)}(𝒜)𝒜`$ or $`(𝒯_𝒫(𝒜_\rho ))_{\rho ^1}𝒜`$, by Theorem 5.6(d). From this, by Lemma 6.2, we obtain $`𝒯_𝒫(𝒜_\rho )𝒜_\rho `$. Thus, if $`𝒫_M𝒬`$ we have $`𝒯_𝒬(𝒜_\rho )𝒜_\rho `$, and again, by applying Lemma 6.2 and Theorem 5.6(d), we derive $`𝒯_{\rho (Q)}(𝒜)𝒜`$. So $`𝒜`$ is a term model of $`\rho (𝒬)`$. By reasoning in a similar way, it can be proved that all term models of $`\rho (𝒬)`$ are also term models of $`\rho (𝒫)`$ which proves that $`\rho (𝒫)_M\rho (𝒬)`$. $`\mathrm{}`$

Unfortunately, this semantics is not compositional wrt deletion.

###### Example 6.4

Let $`\mathrm{\Sigma }`$ be the signature $`(\{a/0,b/0\},\{f/0,g/0\})`$ and let $`𝒫`$ and $`𝒬`$ be two modules with rules $`rl(𝒫)=\{fa,gb\}`$ and $`rl(𝒬)=\{fa,gbfa\}`$. Both modules have the same term models, those term algebras $`𝒜`$ with $`af^𝒜`$ and $`bg^𝒜`$. But by deleting $`f/0`$ in each module we have $`𝒫\{f/0\}`$ and $`𝒬\{f/0\}`$ with $`rl(𝒫\{f/0\})=\{gb\}`$ and $`rl(𝒬\{f/0\})=\{gbfa\}`$, and now $`_\mathrm{\Sigma }`$ is a model of $`𝒬\{f/0\}`$ whereas it is not a model of $`𝒫\{f/0\}`$.

For a different reason, the semantics $`[\{\}]_M`$ is not fully abstract.

###### Example 6.5

Let $`\mathrm{\Sigma }`$ be the signature $`(\{a/0\},\{f/0,g/1\})`$ and let $`𝒫`$ and $`𝒬`$ be two modules with rules $`rl(𝒫)=\{fag(a)a\}`$ and $`rl(𝒬)=\{fag(X)a\}`$, where the rule in $`𝒫`$ is an instance of the rule in $`𝒬`$. Obviously, both modules are indistinguishable but they do not have the same term models. In fact, if we consider the algebra $`𝒜`$ such that: $`f^𝒜=\{\}`$, $`g^𝒜(X)=\{a,\}`$ and $`g^𝒜(a)=\{\}`$, $`𝒜`$ is a model of $`𝒫`$ but it is not a model of $`𝒬`$.

### 6.2 Consistent Term Algebras

To prove the full abstraction property we need to consider a different equivalence relation (i.e. semantics). If we observe the above counter-example, we can see that, for the term algebra $`𝒜`$ used to distinguish $`[\{𝒫\}]_M`$ from $`[\{𝒬\}]_M`$, $`g^𝒜(X)=\{a,\}`$ and $`g^𝒜(a)=\{\}`$; that is, $`𝒜`$ is such that the instantiation of the variable $`X`$ derives in a loss of information for the interpretation of $`g`$ because $`g^𝒜(X\theta )`$ is smaller than $`(g^𝒜(X))\theta `$, for $`\theta =\{X/a\}`$. In general, the notion of term algebra (see Section 2.3) does not impose any relation between $`g^𝒜(\overline{t}\theta )`$ and $`(g^𝒜(\overline{t}))\theta `$. This is not reasonable if we take into account the role of term algebras when they are used to model programs. On the contrary, the interpretation of a function symbol (in a term algebra) applied to arguments with variables must be related to the interpretation of the same function symbol when these variables are instantiated. With this idea in mind, we introduce the notion of  consistency in a term algebra.

###### Definition 6.6 (Consistency of term algebras)

A term algebra $`𝒜\mathrm{𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$ is consistent iff for every $`fFS_\mathrm{\Sigma }^n`$ and $`t_i\mathrm{𝐂𝐓𝐞𝐫𝐦}_{}`$ $`(i=1,\mathrm{},n)`$, $`f^𝒜(\overline{t}\theta )(f^𝒜(\overline{t}))\theta `$ for all $`\theta \mathrm{𝐂𝐒𝐮𝐛𝐬𝐭}`$, where $`(f^𝒜(\overline{t}))\theta `$ stands for the set $`\{u\theta |uf^𝒜(\overline{t})\}`$.

We will denote by $`\mathrm{𝐂𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$ the family of all consistent term algebras. Note that consistency is only required for total substitutions (i.e. substitutions which do not include partial constructor terms). This is due to the special treatment of $``$, which is considered as lack of information. The notion of consistency here introduced is close to that of closure under substitutions defined for interpretations in , and is also related with the notion of C-interpretation considered in , but our requirements are weaker than those ones. To justify the reasonable nature of consistent term algebras we will prove several desirable properties. For instance, the immediate consequences operator maps consistent algebras into consistent algebras, and the canonical model of a program is consistent.

###### Lemma 6.7

For every $`𝒜\mathrm{𝐂𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$, $`r\mathrm{𝐓𝐞𝐫𝐦}_{}`$, and $`\theta \mathrm{𝐂𝐒𝐮𝐛𝐬𝐭}`$, $`[[r]]_{id}^𝒜\theta [[r\theta ]]_{id}^𝒜`$.

Proof.
The proof is by induction on the structure of $`r`$. There are several base cases: $`r\{\}DS_\mathrm{\Sigma }^0`$, $`r𝒱`$, or $`rFS_\mathrm{\Sigma }^0`$. In the first case, $`[[r]]_{id}^𝒜=[[r\theta ]]_{id}^𝒜`$ and these cones have no terms with variables. In the second case, $`[[r]]_{id}^𝒜\theta =\{\theta (r),\}`$, and this is a subset of $`[[r\theta ]]_{id}^𝒜`$. In the third case, $`[[r]]_{id}^𝒜\theta [[r\theta ]]_{id}^𝒜`$ because $`r\theta =r`$ and $`r^𝒜\theta r^𝒜`$ for $`𝒜`$ consistent. In the general case, $`r=h(\overline{e})`$, with $`hDS_\mathrm{\Sigma }^nFS_\mathrm{\Sigma }^n`$, $`e_i\mathrm{𝐓𝐞𝐫𝐦}_{}`$ $`(i=1,\mathrm{},n)`$, and $`n>0`$. Then, $`[[h(\overline{e})\theta ]]_{id}^𝒜=[[h(\overline{e}\theta )]]_{id}^𝒜=_{u_i[[e_i\theta ]]_{id}^𝒜}h^𝒜(\overline{u})`$. Assuming $`[[e_i]]_{id}^𝒜\theta [[e_i\theta ]]_{id}^𝒜`$ $`(i=1,\mathrm{},n)`$, as the induction hypothesis, we obtain $`_{u_i[[e_i\theta ]]_{id}^𝒜}h^𝒜(\overline{u})_{u_i[[e_i]]_{id}^𝒜\theta }h^𝒜(\overline{u})=_{v_i[[e_i]]_{id}^𝒜}h^𝒜(\overline{v}\theta )`$. Since $`𝒜`$ is consistent, $`h^𝒜(\overline{v}\theta )h^𝒜(\overline{v})\theta `$, and therefore $`_{v_i[[e_i]]_{id}^𝒜}h^𝒜(\overline{v}\theta )_{v_i[[e_i]]_{id}^𝒜}h^𝒜(\overline{v})\theta =(_{v_i[[e_i]]_{id}^𝒜}h^𝒜(\overline{v}))\theta =[[h(\overline{e})]]_{id}^𝒜\theta `$. So, $`[[h(\overline{e})\theta ]]_{id}^𝒜[[h(\overline{e})]]_{id}^𝒜\theta `$. $`\mathrm{}`$

###### Proposition 6.8

Given a program $`𝒫`$, if $`𝒜\mathrm{𝐂𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$, then $`𝒯_𝒫(𝒜)\mathrm{𝐂𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$.

Proof.
Let $`fFS_\mathrm{\Sigma }^n`$ and $`t_1,\mathrm{},t_n\mathrm{𝐂𝐓𝐞𝐫𝐦}_{}`$. If $`uf^{𝒯_𝒫(𝒜)}(\overline{t})`$ then there exists a rule $`f(\overline{s})rC`$ in $`[𝒫]_{}`$ such that $`s_it_i`$ $`(i=1,\mathrm{},n)`$, $`𝒜_{id}C`$, and $`u[[r]]_{id}^𝒜`$. For $`\theta \mathrm{𝐂𝐒𝐮𝐛𝐬𝐭}`$, $`u\theta [[r]]_{id}^𝒜\theta [[r\theta ]]_{id}^𝒜`$ by Lemma 6.7, and $`𝒜_{id}C\theta `$ because, if $`abC`$ then there exists $`t[[a]]_{id}^𝒜[[b]]_{id}^𝒜`$, with $`t\mathrm{𝐂𝐓𝐞𝐫𝐦}`$, and $`[[a\theta ]]_{id}^𝒜[[a]]_{id}^𝒜\theta `$ and $`[[b\theta ]]_{id}^𝒜[[b]]_{id}^𝒜\theta `$ again by Lemma 6.7, so $`t\theta [[a]]_{id}^𝒜\theta [[b]]_{id}^𝒜\theta `$, and $`t\theta \mathrm{𝐂𝐓𝐞𝐫𝐦}`$ because $`\theta \mathrm{𝐂𝐒𝐮𝐛𝐬𝐭}`$. Thus, we can consider the rule $`f(\overline{s}\theta )r\theta C\theta `$, which is also in $`[𝒫]_{}`$, with $`s_i\theta t_i\theta `$ $`(i=1,\mathrm{},n)`$, to derive that $`u\theta f^{𝒯_𝒫(𝒜)}(\overline{t}\theta )`$. $`\mathrm{}`$

###### Proposition 6.9

Given a program $`𝒫`$, the canonical term model $`_𝒫`$ is consistent.

Proof.
Clearly, $`_\mathrm{\Sigma }`$ is consistent. Thus, by Proposition 6.8, $`𝒯_𝒫^n(_\mathrm{\Sigma })\mathrm{𝐂𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$, for all $`n0`$, and then $`𝒯_𝒫^\omega (_\mathrm{\Sigma })\mathrm{𝐂𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$ since for every $`f/nFS_\mathrm{\Sigma }`$, $`(f^{𝒯_𝒫^\omega (_\mathrm{\Sigma })}(\overline{t}))\theta =(_{n0}f^{𝒯_𝒫^n(_\mathrm{\Sigma })}(\overline{t}))\theta =_{n0}(f^{𝒯_𝒫^n(_\mathrm{\Sigma })}(\overline{t}))\theta _{n0}f^{𝒯_𝒫^n(_\mathrm{\Sigma })}(\overline{t}\theta )=f^{𝒯_𝒫^\omega (_\mathrm{\Sigma })}(\overline{t}\theta )`$. $`\mathrm{}`$

### 6.3 The Consistent Term Model Semantics

Now, we may define an equivalence relation based only on consistent term models.

###### Definition 6.10 (Consistent model equivalence)

For programs $`𝒫`$ and $`𝒬`$, we define the consistent model equivalence as

$$𝒫_{CM}𝒬_{def}𝒜\mathrm{𝐂𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }(𝒯_𝒫(𝒜)𝒜𝒯_𝒬(𝒜)𝒜).$$

This equivalence is clearly weaker than the model equivalence and corresponds to the following semantics

$$[\{𝒫\}]_{CM}=\{|\text{ is a consistent term model of }𝒫\}$$

which will be called loose consistent model-theoretic semantics, or simply consistent term model semantics. Obviously, $`[\{𝒫\}]_{CM}=[\{𝒫\}]_M\mathrm{𝐂𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$, and the compositionality property of this semantics may be obtained in a similar way as the compositionality of the term model semantics.

###### Theorem 6.11 (Compositionality of $`[\{\}]_{CM}`$)

For all programs $`𝒫,𝒬,𝒫_i,𝒬_i`$,

1. $`𝒫_{CM}𝒬`$ implies $`Ob(𝒫)=Ob(𝒬)`$.
2. $`𝒫_i_{CM}𝒬_i`$ for $`i=1,2`$, implies $`𝒫_1𝒫_2_{CM}𝒬_1𝒬_2`$.
3. $`𝒫_{CM}𝒬`$ implies $`\overline{𝒫}^\sigma _{CM}\overline{𝒬}^\sigma `$, for every signature $`\sigma `$.
4. $`𝒫_{CM}𝒬`$ implies $`\rho (𝒫)_{CM}\rho (𝒬)`$, for every function symbol renaming $`\rho `$.

Therefore, the semantics $`[\{\}]_{CM}`$ is compositional wrt $`(\mathrm{𝑂𝑏},\{,\overline{()}^\sigma ,\rho ()\})`$.

Proof.
We can repeat the proof of Theorem 6.3 but considering pre-fixpoints in $`\mathrm{𝐂𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$ and taking into account that the least model of a program is consistent. $`\mathrm{}`$

Example 6.4 also illustrates the non-compositionality of $`[\{\}]_{CM}`$ wrt the deletion operation because the programs $`𝒫`$ and $`𝒬`$ only define functions without arguments. However, this semantics is fully abstract; to prove this fact, we need an auxiliary result, showing how a (minimal) program $`𝒫`$ can be constructed from a consistent term algebra $`𝒜`$ and an element $`t[[r]]_{id}^𝒜`$ such that $`𝒜`$ is a model of $`𝒫`$ and $`t[[r]]_{id}^_𝒫`$. Proposition 6.13 formalizes this idea. In order to simplify the proof of this result, we will prove some properties about the notion of canonical rewrite rule already introduced in Definition 4.6.

###### Lemma 6.12

For each canonical rewrite rule $`crr(e,r)`$, $`𝒯_{\{crr(e,r)\}}`$ is constant and if $`e=f(\overline{t})`$ then, for every term algebra $`𝒜`$,

$$h^{𝒯_{\{crr(e,r)\}}(𝒜)}(\overline{s})=\{\begin{array}{cc}_{\eta \mathrm{𝐂𝐒𝐮𝐛𝐬𝐭}}\{[[r\eta ]]_{id}^𝒜|\overline{t}\eta \overline{s}\}\{\}\hfill & \text{if }h=f,\hfill \\ \{\}\hfill & \text{otherwise}\hfill \end{array}$$

Proof.
In fact, when we apply $`𝒯_{\{crr(e,r)\}}`$ to a term algebra $`𝒜`$, only the interpretation of $`f`$ is affected. It is obvious that $`f^{𝒯_{\{crr(e,r)\}}(𝒜)}(\overline{s})`$ contains $`_{\eta \mathrm{𝐂𝐒𝐮𝐛𝐬𝐭}}\{[[r\eta ]]_{id}^𝒜|\overline{t}\eta \overline{s}\}`$. On the other hand, if $`uf^{𝒯_{\{crr(e,r)\}}(𝒜)}(\overline{s})`$ then there exists an instantiation $`f(\overline{t^{}}\eta ^{})r\eta ^{}C\eta ^{}`$ of the rule $`crr(e,r)`$, with $`\eta ^{}\mathrm{𝐂𝐒𝐮𝐛𝐬𝐭}_{}`$, such that $`\overline{t}^{}\eta ^{}\overline{s}`$, $`𝒜_{id}C\eta ^{}`$ and $`u[[r\eta ^{}]]_{id}^𝒜`$. The definition of $`C`$ forces $`\eta ^{}`$ to be total for all variables of $`crr(e,r)`$ that do not replace occurrences of $``$ in $`\overline{t}`$. Now, we can define the total substitution $`\eta \mathrm{𝐂𝐒𝐮𝐛𝐬𝐭}`$ as $`X\eta =X^{}\eta ^{}`$ for each variable $`X`$ such that $`X=X^{}\theta _{\overline{t}}`$, for any variable $`X^{}`$ and $`\theta _{\overline{t}}`$ being the substitution considered in the Definition 4.6, and $`Y\eta =Y`$ for all other variables $`Y`$. Note that the definition of $`\eta `$ is correct because if $`X_1\theta _{\overline{t}}=X_2\theta _{\overline{t}}`$ then $`X_1\eta ^{}=X_2\eta ^{}`$ since $`X_1X_2C`$ and $`𝒜_{id}C\eta ^{}`$. Moreover $`r\eta =r^{}\eta ^{}`$ and $`\overline{t}\eta \overline{t}^{}\eta ^{}`$, and so $`\overline{t}\eta \overline{s}`$ and $`u[[r\eta ]]_{id}^𝒜`$. As $`[[r\eta ]]_{id}^𝒜`$ has the same value for all algebras $`𝒜\mathrm{𝐓𝐀𝐥𝐠}_{}`$, $`𝒯_{\{crr(e,r)\}}`$ will be constant. $`\mathrm{}`$

###### Proposition 6.13

Let $`𝒜\mathrm{𝐂𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$ be a consistent term algebra, and $`r\mathrm{𝐓𝐞𝐫𝐦}_{}`$. Then, for every $`t[[r]]_{id}^𝒜`$, a program $`_t`$ exists such that $`t[[r]]_{id}^__t\text{ and }𝒯__t(𝒜)𝒜`$. Moreover, $`𝒯__t`$ is constant.

Proof.
We will proceed by induction on the structure of $`r`$. We can distinguish two base cases: $`r𝒱DS_\mathrm{\Sigma }^0\{\}`$ and $`rFS_\mathrm{\Sigma }^0`$. In the first case, $`[[r]]_{id}^𝒜=r=[[r]]_{id}^__t`$, for every program $`_t`$, in particular for $`_t=\mathrm{}`$, and $`𝒯_{\mathrm{}}`$ is constant with $`𝒯_{\mathrm{}}(𝒜)=_\mathrm{\Sigma }𝒜`$. In the second case, if $`r=f`$ and $`tf^𝒜`$ let be $`_t=\{crr(f,t)\}`$, by Lemma 6.12(2), $`𝒯__t`$ is constant and $`f^{𝒯__t(𝒜)}=_{\eta \mathrm{𝐂𝐒𝐮𝐛𝐬𝐭}}[[t\eta ]]_{id}^𝒜=_{\eta \mathrm{𝐂𝐒𝐮𝐛𝐬𝐭}}t\eta `$ (since $`f`$ has no arguments,). Obviously $`tf^{𝒯__t(𝒜)}`$ and $`tf^{𝒯__t(_\mathrm{\Sigma })}f^{𝒯__t^\omega (_\mathrm{\Sigma })}=f^__t=[[r]]_{id}^__t`$. Since $`𝒜`$ is consistent, $`t\eta f^𝒜\eta (f\eta )^𝒜=f^𝒜`$ for all $`\eta \mathrm{𝐂𝐒𝐮𝐛𝐬𝐭}`$ and $`f^{𝒯__t(𝒜)}f^𝒜`$, and as the rest of function symbols are non-defined in $`𝒯__t(𝒜)`$, we obtain $`𝒯__t(𝒜)𝒜`$.

In the general case, $`r=h(\overline{e})`$ with $`hFS_\mathrm{\Sigma }^nDS_\mathrm{\Sigma }^n`$ and $`e_i\mathrm{𝐓𝐞𝐫𝐦}_{}`$ ($`i=1,\mathrm{},n`$). As $`t[[h(\overline{e})]]_{id}^𝒜`$ implies that there exist $`v_i[[e_i]]_{id}^𝒜`$ $`(i=1,\mathrm{},n)`$ such that $`th^𝒜(\overline{v})`$, by applying the induction hypothesis to each pair $`v_i`$, $`e_i`$, we have programs $`_i`$ such that $`v_i[[e_i]]_{id}^__i`$ with $`𝒯__i`$ constant and $`𝒯__i(𝒜)𝒜`$. Now.

1. If $`hDS_\mathrm{\Sigma }^n`$ let be $`_t=_{i=1}^n_i`$. As $`_i_t`$, we have $`__i__t`$ and, by Lemma 3.1, $`[[e_i]]_{id}^__i[[e_i]]_{id}^__t`$ what implies $`v_i[[e_i]]_{id}^__t`$ ($`i=1,\mathrm{},n`$) and $`h^__t(\overline{v})_{u_i[[e_i]]_{id}^__t}h^__t(\overline{u})=[[h(\overline{e})]]_{id}^__t=[[r]]_{id}^__t`$; but $`th^𝒜(\overline{v})=h^__t(\overline{v})`$, since $`h(\overline{v})\mathrm{𝐂𝐓𝐞𝐫𝐦}_{}`$, and so $`t[[r]]_{id}^__t`$. On the other hand, by Theorem 5.6 (a), $`𝒯__t(𝒜)=_{i=1}^n𝒯__i(𝒜)𝒜`$ and $`𝒯__t`$ is constant.
2. If $`hFS_\mathrm{\Sigma }^n`$ let be $`_t=(_{i=1}^n_i)\{crr(h(\overline{v}),t)\}`$. If $`crr(h(\overline{v}),t)=h(\overline{v}^{})tC`$; then, for the substitution $`\theta _{\overline{v}}`$ (see Definition 4.6), $`\overline{v}=\overline{v}^{}\theta _{\overline{v}}`$ and $`C\theta _{\overline{v}}`$ only contains joinability statements $`XX`$, which are entailed by every term algebra, so $`th^{𝒯_{\{crr(h(\overline{v}),t)\}}(_\mathrm{\Sigma })}(\overline{v})h^{𝒯__t(_\mathrm{\Sigma })}(\overline{v})h^__t(\overline{v})`$. As $`[[e_i]]_{id}^__i[[e_i]]_{id}^__t`$, $`v_i[[e_i]]_{id}^__t`$ ($`i=1,\mathrm{},n`$) and $`h^__t(\overline{v})[[h(\overline{e})]]_{id}^__t=[[r]]_{id}^__t`$, and therefore $`t[[r]]_{id}^__t`$. As, by Theorem 5.6 (a), $`𝒯__t=(_{i=1}^n𝒯__i)𝒯_{crr(h(\overline{v}),t)}`$, $`𝒯__t`$ is constant. By Lemma 6.12(2),

$$h^{𝒯_{\{crr(r,t)\}}(𝒜)}(\overline{w})=\underset{\eta \mathrm{𝐂𝐒𝐮𝐛𝐬𝐭}}{}\{[[t\eta ]]_{id}^𝒜|\overline{v}\eta \overline{w}\}\{\},$$

$`t\eta h^𝒜(\overline{v}\eta )`$ for every $`\eta \mathrm{𝐂𝐒𝐮𝐛𝐬𝐭}_{}`$ and $`𝒜\mathrm{𝐂𝐓𝐀𝐥𝐠}_{}`$, and $`h^𝒜(\overline{v}\eta )h^𝒜(\overline{w})`$ when $`\overline{v}\eta \overline{w}`$ by the monotonicity of $`h^𝒜`$, therefore $`h^{𝒯_{\{crr(r,t)\}}(𝒜)}(\overline{w})h^𝒜(\overline{w})`$; moreover, for every function symbol $`gh`$, $`g^{𝒯_{\{crr(r,t)\}}(𝒜)}(\overline{w})=\{\}h^𝒜(\overline{w})`$. Therefore $`𝒯_{\{crr(r,t)\}}(𝒜)𝒜`$. As by the induction hypothesis $`𝒯__i(𝒜)𝒜`$ ($`i=1,\mathrm{},n`$), it results $`𝒯_{}(𝒜)𝒜`$.

$`\mathrm{}`$

Now, we can obtain the full abstraction property for $`[\{\}]_{CM}`$.

###### Theorem 6.14 (Full abstraction of $`[\{\}]_{CM}`$)

The semantics $`[\{\}]_{CM}`$ is fully abstract wrt $`(\mathrm{𝑂𝑏}`$, $`\{,\overline{()}^\sigma ,()\sigma ,\rho ()\})`$

Proof.
We will prove that programs $`𝒫`$ and $`𝒬`$ such that $`𝒫_{CM}𝒬`$ are always distinguishable, so non-distinguishability of programs has to imply semantics equivalence. If $`𝒫_{CM}𝒬`$ we can assume, without loss of generality, that there exists $`𝒜\mathrm{𝐂𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$ such that $`𝒯_𝒫(𝒜)𝒜`$ and $`𝒯_𝒬(𝒜)𝒜`$, what means that there exist $`fFS_\mathrm{\Sigma }^n`$ and $`t_i\mathrm{𝐂𝐓𝐞𝐫𝐦}_{}(i=1\mathrm{}n)`$ such that $`tf^{𝒯_𝒬(𝒜)}(\overline{t})`$ and $`tf^𝒜(\overline{t})`$. By the definition of $`𝒯_𝒬(𝒜)`$, we have $`f(\overline{s})rC[𝒬]_{}`$ such that $`\overline{s}\overline{t}`$, $`𝒜_{id}C`$, and $`t[[r]]_{id}^𝒜`$. If $`C=\{a_jb_j\}_{j=1}^m`$ then there exists a maximal $`l_j[[a_j]]_{id}^𝒜[[b_j]]_{id}^𝒜`$, for $`j=1,\mathrm{},m`$, and we may consider the programs $`_t`$ for $`t[[r]]_{id}^𝒜`$, $`_{l_j}`$ for $`l_j[[a_j]]_{id}^𝒜`$ and $`_{l_j}^{}`$ for $`l_j[[b_j]]_{id}^𝒜`$ ($`j=1,\mathrm{},m`$), as in the previous proposition, and $`=_t(_{j=1}^m_{l_j})(_{j=1}^m_{}^{}{}_{l_j}{}^{})`$. Obviously, $`𝒯_{}(𝒜)𝒜`$ and $`__t,_{_{l_j}},_{_{l_j}^{}}_{}`$. If we define the context $`C[[𝒳]]=𝒳`$ it can be proved that $`Ob(C[[𝒫]])Ob(C[[𝒬]])`$. In fact, as it will be shown, $`tf^{_{C[[𝒬]]}}(\overline{t})`$, but $`tf^{_{C[[𝒫]]}}(\overline{t})`$. Note that $`tf^{𝒯_𝒬(_{})}(\overline{t})`$ because $`t[[r]]_{id}^{_{}}`$ and $`l_j[[a_j]]_{id}^{_{}}[[b_j]]_{id}^{_{}}`$, and $`f^{𝒯_𝒬(_{})}(\overline{t})=f^{𝒯_𝒬(𝒯_{}^\omega (_\mathrm{\Sigma }))}(\overline{t})f^{𝒯_𝒬^\omega (_\mathrm{\Sigma })}(\overline{t})=f^{_{C[[𝒬]]}}(\overline{t})`$ because $`𝒯_𝒬,𝒯_{}𝒯_𝒬`$, so $`tf^{_{C[[𝒬]]}}(\overline{t})`$. But $`𝒯_{C[[𝒫]]}^k(_\mathrm{\Sigma })𝒜`$, for all $`k0`$, because it is trivially true for $`k=0`$ and if we assume $`𝒯_{C[[𝒫]]}^k(_\mathrm{\Sigma })𝒜`$ then, by the monotonicity of $`𝒯_{C[[𝒫]]}`$ and the properties of $``$, $`𝒯_{C[[𝒫]]}^{k+1}(_\mathrm{\Sigma })=𝒯_{C[[𝒫]]}(𝒯_{C[[𝒫]]}^k(_\mathrm{\Sigma }))𝒯_{C[[𝒫]]}(𝒜)=𝒯_𝒫(𝒜)𝒯_{}(𝒜)𝒜`$ and thus, $`_{C[[𝒫]]}𝒜`$. As $`tf^𝒜(\overline{t})`$ also $`tf^{_{C[[𝒫]]}}(\overline{t})`$. $`\mathrm{}`$

## 7 A Compositional and Fully Abstract Semantics

The fact that the consistent term model semantics is fully abstract but not compositional wrt the deletion of a subsignature means that this semantics is more abstract than necessary. We need a finer semantics but not as fine as the $`𝒯`$-semantics. One way of obtaining such a semantics is by increasing the number of pre-fixpoints (related to the $`𝒯`$-operator) to be considered when we compare two programs, and, in order to obtain compositionality wrt the deletion operation, we may consider the consistent term models of all programs obtained by deleting a subsignature. With this idea we define the following equivalence between programs

###### Definition 7.1 (Deletion equivalence)

For programs $`𝒫`$ and $`𝒬`$, we define the deletion equivalence as

$$𝒫_D𝒬_{def}\sigma FS_\mathrm{\Sigma }(𝒫\sigma _{CM}𝒬\sigma ).$$

This equivalence is finer than the consistent model equivalence and coarser than the equivalence induced by the $`𝒯`$-semantics. In fact, $`𝒫_D𝒬`$ implies $`𝒫_{CM}𝒬`$ because this relationship coincides with $`𝒫\sigma _0_{CM}𝒬\sigma _0`$, where $`\sigma _0`$ is the empty signature. And if $`𝒫_T𝒬`$, or equivalently $`𝒯_𝒫=𝒯_𝒬`$, it can be proved that $`𝒯_{𝒫\sigma }=𝒯_{𝒬\sigma }`$, for all $`\sigma FS_\mathrm{\Sigma }`$, and then $`𝒫\sigma _{CM}𝒬\sigma `$, for all $`\sigma FS_\mathrm{\Sigma }`$, which is $`𝒫_D𝒬`$. The deletion equivalence is compositional wrt all operations.

###### Theorem 7.2 (Compositionality of $`_D`$)

For all programs $`𝒫,𝒬,𝒫_i,𝒬_i`$,

1. $`𝒫_D𝒬`$ implies $`Ob(𝒫)=Ob(𝒬)`$.
2. $`𝒫_i_D𝒬_i`$ for $`i=1,2`$, implies $`𝒫_1𝒫_2_D𝒬_1𝒬_2`$.
3. $`𝒫_D𝒬`$ implies $`\overline{𝒫}^\sigma _D\overline{𝒬}^\sigma `$, for every signature $`\sigma FS_\mathrm{\Sigma }`$.
4. $`𝒫_D𝒬`$ implies $`𝒫\sigma _D𝒬\sigma `$, for every signature $`\sigma FS_\mathrm{\Sigma }`$.
5. $`𝒫_D𝒬`$ implies $`\rho (𝒫)_D\rho (𝒬)`$, for every function symbol renaming $`\rho `$.

Thus, the equivalence $`_D`$ is compositional wrt $`(\mathrm{𝑂𝑏},\{,\overline{()}^\sigma ,()\sigma ,\rho ()\})`$.

Proof.

1. Trivial because $`𝒫_D𝒬`$ implies $`𝒫\sigma _0_{CM}𝒬\sigma _0`$, for the empty signature $`\sigma _0`$, so $`𝒫_{CM}𝒬`$ and $`_𝒫=_𝒬`$ or $`Ob(𝒫)=Ob(𝒬)`$.

2. $`𝒫_i_D𝒬_i`$ implies $`𝒫_i\sigma _{CM}𝒬_i\sigma `$, for all $`\sigma FS_\mathrm{\Sigma }`$, and $`𝒫_i\sigma _{CM}𝒬_i\sigma `$ ($`i=1,2`$) implies $`(𝒫_1\sigma )(𝒫_2\sigma )_{CM}(𝒬_1\sigma )(𝒬_2\sigma )`$, by Theorem 6.11(2). But, by Proposition 4.13(4), $`(𝒫_1𝒫_2)\sigma =(𝒫_1\sigma )(𝒫_2\sigma )`$. So $`𝒫_i_D𝒬_i`$, for $`i=1,2`$, implies $`(𝒫_1𝒫_2)\sigma _{CM}(𝒬_1𝒬_2)\sigma `$, for all $`\sigma FS_\mathrm{\Sigma }`$, which means $`𝒫_1𝒫_2_D𝒬_1𝒬_2`$.

3. $`𝒫_D𝒬`$ implies $`𝒫_{CM}𝒬`$. By Theorem 6.11(3), this implies $`\overline{𝒫}^{\sigma \sigma ^{}}_{CM}\overline{𝒬}^{\sigma \sigma ^{}}`$, for all signatures $`\sigma ,\sigma ^{}FS_\mathrm{\Sigma }`$. And, by Proposition 4.13(5), $`\overline{𝒫}^{\sigma \sigma ^{}}=\overline{𝒫}^\sigma \sigma ^{}`$. Thus, $`𝒫_D𝒬`$ implies $`\overline{𝒫}^\sigma \sigma ^{}_{CM}\overline{𝒬}^\sigma \sigma ^{}`$, for all signature $`\sigma ^{}FS_\mathrm{\Sigma }`$, which is $`\overline{𝒫}^\sigma _D\overline{𝒬}^\sigma `$.

4. By definition, $`𝒫_D𝒬`$ implies $`𝒫(\sigma \sigma ^{})_{CM}𝒬(\sigma \sigma ^{})`$, for all signatures $`\sigma ,\sigma ^{}FS_\mathrm{\Sigma }`$. By Proposition 4.13(3), $`𝒫(\sigma \sigma ^{})=(𝒫\sigma )\sigma ^{}`$. Thus, $`𝒫_D𝒬`$ implies $`(𝒫\sigma )\sigma ^{}_{CM}(𝒬\sigma )\sigma ^{}`$, for all $`\sigma ^{}FS_\mathrm{\Sigma }`$, which is $`𝒫\sigma _D𝒬\sigma `$.

5. Given a function symbol renaming $`\rho `$ and a signature $`\sigma FS_\mathrm{\Sigma }`$, let $`\sigma _\rho `$ be the signature $`\{fFS_\mathrm{\Sigma }|\rho (f)\sigma \}`$. By definition, $`𝒫_D𝒬`$ implies $`𝒫\sigma _\rho _{CM}𝒬\sigma _\rho `$. By Theorem 6.11(4), this implies $`\rho (𝒫\sigma _\rho )_{CM}\rho (𝒬\sigma _\rho )`$. It can also be proved easily that $`\rho (𝒫\sigma _\rho )=\rho (𝒫)\sigma `$. So, $`𝒫_D𝒬`$ implies $`\rho (𝒫)\sigma _{CM}\rho (𝒬)\sigma `$, for all $`\sigma FS_\mathrm{\Sigma }`$, which means that $`\rho (𝒫)_D\rho (𝒬)`$. $`\mathrm{}`$

###### Theorem 7.3 (Full abstraction of $`_D`$)

The equivalence $`_D`$ is fully abstract wrt $`(\mathrm{𝑂𝑏}`$, $`\{,\overline{()}^\sigma ,()\sigma ,\rho ()\})`$

Proof.
We only need prove that $`𝒫_D𝒬`$ implies that there exists a context where we can discriminate the observable behavior of both programs. But $`𝒫_D𝒬`$ implies that there exists a signature $`\sigma FS_\mathrm{\Sigma }`$ such that $`𝒫\sigma _{CM}𝒬\sigma `$, and this implies that there exists a context $`C^{}[[𝒳]]`$ such that $`Ob(C^{}[[𝒫\sigma ]])Ob(C^{}[[𝒬\sigma ]])`$ because the equivalence $`_{CM}`$ is fully abstract. Thus by considering the context $`C[[𝒳]]=C^{}[[𝒳\sigma ]]`$ we have that $`Ob(C[[𝒫]])Ob(C[[𝒬]])`$. $`\mathrm{}`$

###### Definition 7.4 (Deletion semantics)

We define the deletion semantics of a program $`𝒫`$ as

$$[\{𝒫\}]_D=\{𝐌_{f/n}(𝒫)f/nFS_\mathrm{\Sigma }\},$$

where $`𝐌_{f/n}(𝒫)`$ is the set of all consistent term models of the rules of $`𝒫`$ that define $`f/n`$.

The deletion semantics induces the deletion equivalence.

###### Proposition 7.5

$$𝒫_D𝒬_{def}[\{𝒫\}]_D=[\{𝒬\}]_D$$

Proof.
If $`𝒫_D𝒬`$ then, for each $`f/nFS_\mathrm{\Sigma }`$, we have $`𝒫\sigma _{f/n}_{CM}𝒬\sigma _{f/n}`$ for $`\sigma _{f/n}=(exp(𝒫)exp(𝒬))\{f/n\}`$, which means $`𝐌_{f/n}(𝒫)=𝐌_{f/n}(𝒬)`$, for each $`f/nFS_\mathrm{\Sigma }`$; thus $`[\{𝒫\}]_D=[\{𝒬\}]_D`$. Reciprocally, if $`[\{𝒫\}]_D=[\{𝒬\}]_D`$ then, for each $`\sigma FS_\mathrm{\Sigma }`$, $`[\{𝒫\sigma \}]_{CM}`$ = $`\{𝐌_{f/n}(𝒫)|f/n(exp(𝒫)exp(𝒬))\sigma \}`$ (where the intersection reduces to $`\mathrm{𝐂𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$ when the signature $`(exp(𝒫)exp(𝒬))\sigma `$ is empty), and because $`𝐌_{f/n}(𝒫)=𝐌_{f/n}(𝒬)`$, for all $`f/nFS_\mathrm{\Sigma }`$, we have $`𝒫\sigma _{CM}𝒬\sigma `$ for each $`\sigma FS_\mathrm{\Sigma }`$, and consequently, $`𝒫_D𝒬`$. $`\mathrm{}`$

Thus, the deletion semantics is compositional and fully abstract wrt (Ob,$`\{`$, $`\overline{()}^\sigma `$, $`()\sigma `$, $`\rho ()\}`$).

## 8 Introducing Hidden Symbols

In this section we explore an alternative to modules with an infinite number of rules, generated by the closure operation, that also supports local constructor symbols. For this aim we will consider a global or visible signature $`\mathrm{\Sigma }`$ and a set $`𝒱`$ of variable symbols together with a new set $`\mathrm{\Omega }`$ of labels that we identify with the set of module names and module expressions. With this set we obtain a labeled signature $`\mathrm{\Omega }\times \mathrm{\Sigma }=(\mathrm{\Omega }\times DS_\mathrm{\Sigma },\mathrm{\Omega }\times FS_\mathrm{\Sigma })`$ which we will consider as protected or non accessible for users and writers of modules, that is, hidden. This signature will be only managed by the module system for internal representation of module expressions. Pairs $`(M,f)`$ of $`\mathrm{\Omega }\times \mathrm{\Sigma }`$, called labeled symbols, will be denoted by $`M\text{.}f`$.

As we have seen in Section 4.1 the purpose of the closure of a module is to hide the definitions of function symbols, making only their results visible. To this aim, the rules of a module are replaced with all (possibly infinite) approximations that can be derived from them. But we can obtain an internal representation of the closure operation, with a finite number of rules, with the aid of labeled symbols, following an idea that appears in  applied to the hiding of predicate definitions in logic programs. We go further into this idea applying it to deal with local constructor symbols.

### 8.1 A Finite Representation of Closure

Let $`𝒫=<\sigma _p,\sigma _e,>`$ a module of PMod($`\mathrm{\Sigma }_{}`$) with a finite set of rules. We can protect its rules translating them to a protected signature by labeling all function symbols with the module’s name and introducing a bridge rule $`f(\overline{X})𝒫\text{.}f(\overline{X})`$ for each function symbol $`f/n\sigma _e`$. In this way we obtain a module $`𝒫^{}`$ in the signature $`\overline{\mathrm{\Sigma }}_{}=(DS_\mathrm{\Sigma }_{},FS_\mathrm{\Sigma }_{}(\mathrm{\Omega }\times FS_\mathrm{\Sigma }_{}))`$ with an isolated (hidden) part $`_H`$, made up of all translated rules, and a bridge part $`_B`$ for accessing the isolated part, made up of all bridge rules. Obviously with this module we can derive the same approximations, for visible function symbols, as with $`\overline{𝒫}`$ in every context. We will call these modules structured modules to distinguish them from plain modules used up to now. In general, a structured module will be a module

$$<\sigma _p,\sigma _e,_V_B_H>$$

with a visible parameter signature $`\sigma _p`$, a visible exported signature $`\sigma _e`$, and a set of rules with three —possibly empty— parts, a visible part $`_V`$ made up of rules only with function symbols in $`FS_\mathrm{\Sigma }`$, a hidden part $`_H`$ made up of rules only with function symbols in $`\mathrm{\Omega }\times FS_\mathrm{\Sigma }`$, and a bridge part $`_B`$ made up of bridge rules $`f(\overline{X})𝒫\text{.}g(\overline{X})`$, for any label $`𝒫\mathrm{\Omega }`$, such that each symbol $`𝒫\text{.}g`$ has a definition rule in $`_H`$. Also, $`\sigma _e`$ is made up of all function symbols with a definition rule in $`_V`$ or $`_B`$, and $`\sigma _p`$ is made up of all parameter function symbols which appear in $`_V`$. We define union, deletion of functional signature and renaming in the same way as we did in Section 4.1, but we will use deletion and renaming involving only visible signature, and, instead of closure, we define a structured closure for a structured module $`𝒫=<\sigma _p,\sigma _e,_V_B_H>`$ as the module $`𝒫^{}=<\mathrm{},\sigma _e,_B^{}_H^{}>`$ obtained by applying the renaming $`\tau (𝒫)`$, that transforms each visible function symbol $`f`$ of $`_V`$ and $`_B`$ into $`𝒫\text{.}f`$ and maintains all labeled symbols, and adding new bridge rules corresponding to the function symbols of $`\sigma _e`$. Now, we can define a representation morphism from modular expressions made up from finite plain modules to structured modules in the following way:

* $`\iota (𝒫)=𝒫`$, for each finite plain module $`𝒫`$;
* $`\iota (𝒫𝒬)=\iota (𝒫)\iota (𝒬)`$, for module expressions $`𝒫`$ and $`𝒬`$;
* $`\iota (𝒫\sigma )=\iota (𝒫)\sigma `$, for each module expression $`𝒫`$ and visible signature $`\sigma `$;
* $`\iota (\rho (𝒫))=\rho (\iota (𝒫))`$, for each module expression $`𝒫`$ and visible signature renaming $`\rho `$;
* $`\iota (\overline{𝒫})=(\iota (𝒫))^{}`$, for each module expression $`𝒫`$.

###### Example 8.1

Let `OrdList` and `OrdNat` be the modules defined in the example 4.15 and 4.17, respectively, and let `P` be the name of the module $`\iota (\mathrm{𝙾𝚛𝚍𝙽𝚊𝚝})`$. The representation of `OrdList` $``$ `{isnat/1->isbasetype/1}`($`\overline{\mathrm{𝙾𝚛𝚍𝙽𝚊𝚝}}`$) will be the structured module $`\iota (\mathrm{𝙾𝚛𝚍𝙻𝚒𝚜𝚝})\mathtt{\{isnat/1->isbasetype/1\}}(𝙿^{}),`$ with the following aspect

```
    <{},
     {isbasetype/1,leq/2,geq/2,insert/2},
     {   % visible rules
      insert(X,[])     -> [X]              <= isbasetype(X) >< true.
      insert(X,[Y|Ys]) -> [X|[Y|Ys]]       <= leq(X,Y) >< true.
      insert(X,[Y|Ys]) -> [Y|insert(X,Ys)] <= leq(X,Y) >< false.
         % bridge rules
      isbasetype(X) -> P.isnat(X).
      leq(X,Y) -> P.leq(X,Y).
      geq(X,Y) -> P.geq(X,Y).
         % hidden rules
      P.isnat(zero)    -> true.
      P.isnat(succ(X)) -> P.isnat(X).
      P.leq(zero,zero)       -> true.
      P.leq(zero,succ(X))    -> P.isnat(X).
      P.leq(succ(X),zero)    -> false <= P.isnat(X) >< true.
      P.leq(succ(X),succ(Y)) -> P.leq(X,Y).
      P.geq(X,Y)             -> P.leq(Y,X). } >

```

The behaviour of a structured module $`𝒫=<\sigma _p,\sigma _e,_V_B_H>`$ wrt the visible signature can be expressed with the aid of the algebra transformer

$$𝒰_𝒫:\mathrm{𝐂𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }\mathrm{𝐂𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }$$

defined, for each $`𝒜`$, as $`𝒰_𝒫(𝒜)=𝒯_{_V_B}(𝒯__H^\omega (_{\overline{\mathrm{\Sigma }}})\overline{𝒜})|_\mathrm{\Sigma }`$, where $`\overline{𝒜}`$ is the extension of $`𝒜`$ to an algebra of $`\mathrm{𝐂𝐓𝐀𝐥𝐠}_{\overline{\mathrm{\Sigma }}}`$ obtained by adding functions $`𝒫\text{.}f^{\overline{𝒜}}`$ defined as $`𝒫\text{.}f^{\overline{𝒜}}(\overline{t})=`$, for each $`f/nFS_\mathrm{\Sigma }`$ and $`𝒫\mathrm{\Omega }`$, and $`|_\mathrm{\Sigma }`$ means the reduct of the algebra $`\mathrm{𝐂𝐓𝐀𝐥𝐠}_{\overline{\mathrm{\Sigma }}}`$ obtained by forgetting all functions denoting labeled function symbols. In this expression, $`𝒯__H^\omega (_{\overline{\mathrm{\Sigma }}})`$ represents all the information which can be obtained from the hidden rules; this information is added to the extended algebra because this information has to be disponible for the immediate consequences operator corresponding to the visible and bridge rules in order to obtain the approximations for the visible functions. The relationship, at the semantical level, between program modules and structured modules is given in the following theorem.

###### Theorem 8.2

For each modular expression $``$, made up from finite plain programs, and its implementation $`\iota ()`$, we have $`𝒯_{}=𝒰_{\iota ()}`$.

Proof.
This theorem can be proved by induction on the structure of $``$.

(1) If $``$ is a simple expression (a module name) then $`\iota ()_B=\mathrm{}=\iota ()_H`$ and $`𝒰_{\iota ()}=𝒯_{\iota ()_V}(\overline{𝒜})|_\mathrm{\Sigma }=𝒯_{}(𝒜)`$ because $`𝒯_{\iota ()_V}`$ neither uses nor produces any information about labeled signature.

(2) If $`=𝒫𝒬`$ and $`𝒯_𝒫=𝒰_{\iota (𝒫)}`$ and $`𝒯_𝒬=𝒰_{\iota (𝒬)}`$, by Theorem 5.6 (a) we have $`𝒯_{𝒫𝒬}(𝒜)=𝒯_𝒫(𝒜)𝒯_𝒬(𝒜)=𝒰_{\iota (𝒫)}(𝒜)𝒰_{\iota (𝒬)}(𝒜)`$. Also, by definition of $`\iota `$, $`𝒰_{\iota (𝒫𝒬)}=𝒰_{\iota (𝒫)\iota (𝒬)}`$ and

$$𝒰_{\iota (𝒫)\iota (𝒬)}(𝒜)=𝒯_{(\iota (𝒫)_V\iota (𝒫)_B)(\iota (𝒬)_V\iota (𝒬)_B)}(𝒯_{\iota (𝒫)_H\iota (𝒬)_H}^\omega (_{\overline{\mathrm{\Sigma }}})\overline{𝒜})|_\mathrm{\Sigma }\text{.}$$

By Theorem 5.6 (a) and taken into account that $`\iota (𝒫)_H`$ contains all possible rules about its (labeled) function symbols and $`𝒯_{\iota (𝒬)_H}^\omega (_{\overline{\mathrm{\Sigma }}})`$ only contains relevant information about function symbols in $`\iota (𝒬)_H`$, the expession above is equal to

$$𝒯_{(\iota (𝒫)_V\iota (𝒫)_B)}(𝒯_{\iota (𝒫)_H}^\omega (_{\overline{\mathrm{\Sigma }}})\overline{𝒜})|_\mathrm{\Sigma }𝒯_{(\iota (𝒬)_V\iota (𝒬)_B)}(𝒯_{\iota (𝒬)_H}^\omega (_{\overline{\mathrm{\Sigma }}})\overline{𝒜})|_\mathrm{\Sigma }$$

that is, $`𝒰_{\iota (𝒫)}(𝒜)𝒰_{\iota (𝒬)}(𝒜)`$.

(3) If $`=𝒫/\sigma `$, $`\sigma `$ is a subsignature of visible function symbols, and $`𝒯_𝒫=𝒰_{\iota (𝒫)}`$, by Theorem 5.6 (c), $`𝒯_{𝒫\sigma }=𝒯_𝒫𝕋_{exp(𝒫)\sigma }=𝒰_{\iota (𝒫)}𝕋_{exp(𝒫)\sigma }`$, and by the definition of $`\iota `$, $`𝒰_{\iota (𝒫\sigma )}(𝒜)=𝒰_{\iota (𝒫)\sigma }(𝒜)`$, but again by Theorem 5.6 (c),

$$𝒯_{(\iota (𝒫)_V\iota (𝒫)_B)\sigma }=𝒯_{\iota (𝒫)_V\iota (𝒫)_B}𝕋_{exp(\iota (𝒫)_V\iota (𝒫)_B)\sigma }=𝒯_{\iota (𝒫)_V\iota (𝒫)_B}𝕋_{exp(𝒫)\sigma },$$

because $`exp(𝒫)=exp(\iota (𝒫)_V\iota (𝒫)_B)`$. So, $`𝒰_{\iota (𝒫\sigma )}(𝒜)=𝒰_{\iota (𝒫)}𝕋_{exp(𝒫)\sigma }`$.

(4) If $`=\rho (𝒫)`$, $`\rho `$ is a visible signature renaming, and $`𝒯_𝒫=𝒰_{\iota (𝒫)}`$, by Theorem 5.6 (d), $`𝒯_{\rho (𝒫)}=𝒯_{\rho ^1}𝒯_𝒫𝒯_\rho =𝒯_{\rho ^1}𝒰_{\iota (𝒫)}𝒯_\rho `$. Also, by definition of $`\iota `$,

$$𝒰_{\iota (\rho (𝒫))}(𝒜)=𝒰_{\rho (\iota (𝒫))}(𝒜)=𝒯_{\rho (\iota (𝒫)_V\iota (𝒫)_B)}(𝒯_{\iota (𝒫)_H}^\omega (_{\overline{\mathrm{\Sigma }}})\overline{𝒜})|_\mathrm{\Sigma }$$

and, again by Theorem 5.6 (d), the above expression is equal to

$$𝒯_{\rho ^1}(𝒯_{\iota (𝒫)_V\iota (𝒫)_B}(𝒯_\rho (𝒯_{\iota (𝒫)_H}^\omega (_{\overline{\mathrm{\Sigma }}})\overline{𝒜})))|_\mathrm{\Sigma },$$

but $`𝒯_\rho `$ and $`𝒯_{\rho ^1}`$ only modify the interpretation of visible function symbols and $`𝒯_\rho (\overline{𝒜})=\overline{𝒯_\rho (𝒜)}`$ and $`𝒯_{\rho ^1}()|_\mathrm{\Sigma }=𝒯_{\rho ^1}(|_\mathrm{\Sigma })`$ for $`\mathrm{𝐂𝐓𝐀𝐥𝐠}_{\overline{\mathrm{\Sigma }}}`$. So, the above expression is equal to $`𝒯_{\rho ^1}(𝒯_{\iota (𝒫)_V\iota (𝒫)_B}(𝒯_{\iota (𝒫)_H}^\omega (_{\overline{\mathrm{\Sigma }}})\overline{𝒯_\rho (𝒜)}))|_\mathrm{\Sigma }=𝒯_{\rho ^1}(𝒰_{\iota (𝒫)}(𝒯_\rho (𝒜)))\text{.}`$

(5) If $`=\overline{𝒫}`$ and $`𝒯_𝒫=𝒰_{\iota (𝒫)}`$, by Theorem 5.6 (b) $`𝒯_{\overline{𝒫}}`$ applies every term algebra into $`𝒯_𝒫^\omega (_\mathrm{\Sigma })=𝒰_{\iota (𝒫)}^\omega (_\mathrm{\Sigma })`$, and by the definition of $`\iota `$, $`𝒰_{\iota (\overline{𝒫})}=𝒰_{\iota (𝒫)^{}}`$; so, we have to prove $`𝒰_{\iota (𝒫)^{}}(𝒜)=𝒰_{\iota (𝒫)}^\omega (_\mathrm{\Sigma })`$ for all $`𝒜\mathrm{𝐂𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$. Let $`\iota (𝒫)=<\sigma _p,\sigma _e,_V_B_H>`$ and $`\iota (𝒫)^{}=<\mathrm{},\sigma _e,_B^{}_H^{}>`$, where $`_B^{}=\{f(\overline{X})𝒫\text{.}f(\overline{X})|f/n\sigma _e\}`$ and $`_H^{}=\tau (𝒫)(_V_B)_H`$. For all $`𝒜\mathrm{𝐂𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }`$,

$$𝒰_{\iota (𝒫)^{}}=𝒯__B^{}(𝒯__H^{}^\omega (_{\overline{\mathrm{\Sigma }}})\overline{𝒜})|_\mathrm{\Sigma }=𝒯__B^{}(𝒯__H^{}^\omega (_{\overline{\mathrm{\Sigma }}}))|_\mathrm{\Sigma },$$

because $`𝒯__B^{}`$ only uses information about labeled function symbols and $`\overline{𝒜}`$ has no information about such symbols, and

$$𝒰_{\iota (𝒫)}^\omega (_\mathrm{\Sigma })=(𝒯_{_V_B}(Id𝒯_{\overline{_H}}))^\omega (_\mathrm{\Sigma })|_\mathrm{\Sigma },$$

and, as $`𝒯__B^{}`$ and $`𝒯_{_V_B}`$ only produce information about symbol functions of $`\sigma _e`$, we only have to prove $`𝒯__B^{}(𝒯__H^{}^\omega (_{\overline{\mathrm{\Sigma }}}))=(𝒯_{_V_B}(Id𝒯_{\overline{_H}}))^\omega (_\mathrm{\Sigma })`$. But it can be proved that $`𝒯__B^{}(𝒯__H^{}^i(_{\overline{\mathrm{\Sigma }}}))(𝒯_{_V_B}(Id𝒯_{\overline{_H}}))^i(_\mathrm{\Sigma })𝒯__B^{}(𝒯__H^{}^\omega (_{\overline{\mathrm{\Sigma }}}))`$ for all $`i0`$. $`\mathrm{}`$

From this theorem we obtain that for two equivalent module expressions $`𝒫`$ and $`𝒬`$ (i.e. $`𝒫`$ and $`𝒬`$ have the same components but, possibly, different expressions with the operations), $`𝒰_{\iota (𝒫)}=𝒰_{\iota (𝒬)}`$ although it is possible that $`\iota (𝒫)`$ differs from $`\iota (𝒬)`$ due to the occurrence of closure operations. Also, the models of a program module $`𝒫`$ will be the pre-fixpoints of $`𝒰_{\iota (𝒫)}`$ and we can define the visible semantics of structured modules based on this operator. In particular we obtain the deletion semantics by considering, for each structured module $`𝒫=<\sigma _p,\sigma _e,_V_B_H>`$, the indexed family of sets of pre-fixpoints of $`𝒰_{𝒫(\sigma _ef)}`$ for each $`f/n\sigma _e`$.

### 8.2 Local Constructor Symbols

To simplify the theoretical study of programs composition in CRWL-programming, and to capture the idea of module as open program, we have assumed that constructor symbols are common to all programs. However, as it was discussed in Section 4, this assumption prevents to hide constructor symbols, what is not acceptable from a practical point of view.

We can hide constructor symbols by labeling them as we have done with function symbols to protect them against user manipulations. Labeled constructor symbols can only be manipulated in the internal representation of the closure of the module corresponding to their label. Outside this module, function symbols defined on labeled constructor symbols can only be applied to variable symbols or to other function applications that can be reduced to this labeled constructor symbols. To realize this idea we only need to modify our closure implementation extending it to manage constructor symbols also. So, we define closure hiding a subsignature $`C`$ of constructor symbols for a module $`𝒫`$ as a (non plain) module $`\overline{𝒫}_C`$ such that $`\iota (\overline{𝒫}_C)=𝒫_C^{}`$ where $`𝒫_C^{}`$ is obtained as $`𝒫^{}`$ but now the renaming $`\tau (𝒫)`$ also transforms each visible constructor symbol $`c`$ of $`C`$ into $`𝒫\text{.}c`$.

###### Example 8.3

Let us suppose a module `LNat` for lists of natural numbers which exports the function symbols `isnat/1`, `_<_/2` and `_++_/2`, and consider the following module for binary search trees of natural numbers where tree constructors `nil/0` and `mktree/3` are used.

```
  BST =
  <{isnat/1, _<_/2, _++_/2}, {empty/0, insert/2, inorder/1},
   {empty -> nil .
    insert(N,nil) -> mktree(N,nil,nil) <= isnat(N) >< true .
    insert(N,mktree(M,T1,T2)) -> mktree(M,T1,T2) <= N >< M, isnat(N) >< true .
    insert(N,mktree(M,T1,T2)) -> mktree(M,insert(N,T1),T2) <= N<M >< true .
    insert(N,mktree(M,T1,T2)) -> mktree(M,T1,insert(N,T2)) <= M<N >< true .
    inorder(nil) -> [] .
    inorder(mktree(M,T1,T2)) -> inorder(T1)++[M|inorder(T2)] <= isnat(M) >< true .}>

```

We may hide the tree constructors by considering $`\overline{(\mathrm{𝙻𝙽𝚊𝚝}\mathrm{𝙱𝚂𝚃})}_{\{nil,mktree\}}`$. This module will have the following representation:

```
  <{}, {isnat/1, _<_/2, _++_/2, empty/0, insert/2, inorder/1},
   { ...                                        % bridge rules of LNat
    empty -> BST.empty .                        % bridge rules of BST
    insert(N,T1) -> BST.insert(N,T1) .
    inorder(T1) -> BST.inorder(T1) .

    ...                                         % hidden part of LNat
    BST.empty -> BST.nil .                      % hidden part of BST
    BST.insert(N,BST.nil) -> BST.mktree(N,BST.nil,BST.nil)
                                        <= BST.isnat(N) >< true .
    BST.insert(N,BST.mktree(M,T1,T2)) -> BST.mktree(M,T1,T2)
                                        <= N >< M, BST.isnat(N) >< true .
    BST.insert(N,BST.mktree(M,T1,T2)) -> BST.mktree(M,BST.insert(N,T1),T2)
                                        <= N NBST.< M >< true .
    BST.insert(N,BST.mktree(M,T1,T2)) -> BST.mktree(M,T1,BST.insert(N,T2))
                                        <= M MBST.< N >< true .
    BST.inorder(BST.nil) -> [] .
    BST.inorder(BST.mktree(M,T1,T2)) -> BST.inorder(T1) BST.++ [M|BST.inorder(T2)]
                                        <= BST.isnat(M) >< true .}>

```

And we can use this module, without access to hidden constructor symbols, by only using the exported signature and visible constructor symbols, as in the following module for sorting lists:

```
 LSort =
 <{empty/0, insert/2, inorder/1},
  {listTotree/1, lsort/1},
  {listTotree([]) -> empty .
   listTotree([N|L]) -> insert(N,listTotree(L)) .
   lsort(L) -> inorder(listTotree(L)) .} >

```

that has to be joined to $`\overline{(\mathrm{𝙻𝙽𝚊𝚝}\mathrm{𝙱𝚂𝚃})}_{\{nil,mktree\}}`$ to obtain $`\overline{(\mathrm{𝙻𝙽𝚊𝚝}\mathrm{𝙱𝚂𝚃})}_{\{nil,mktree\}}\mathrm{𝙻𝚂𝚘𝚛𝚝}`$.

The behaviour of a structured module $`𝒫=<\sigma _p,\sigma _e,_V_B_H>`$ with hidden constructor symbols wrt the visible signature can be expressed with the aid of the algebra transformer

$$𝒰_𝒫:\mathrm{𝐂𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }\mathrm{𝐂𝐓𝐀𝐥𝐠}_\mathrm{\Sigma }$$

defined for each $`𝒜`$ as $`𝒰_𝒫(𝒜)=𝒯_{_V_B}(𝒯__H^\omega (_{\overline{\mathrm{\Sigma }}})\overline{𝒜})|_\mathrm{\Sigma }`$, where now $`\overline{𝒜}`$ is the extension of $`𝒜`$ to an algebra of $`\mathrm{𝐂𝐓𝐀𝐥𝐠}_{\mathrm{\Omega }\times \mathrm{\Sigma }}`$ obtained by adding functions $`𝒫\text{.}f^{\overline{𝒜}}`$, defined as $`𝒫\text{.}f^{\overline{𝒜}}(\overline{t})=`$, for each $`f/nFS_\mathrm{\Sigma }`$ and $`𝒫\mathrm{\Omega }`$, and defining $`f^{\overline{𝒜}}(\overline{t})=f^𝒜(\overline{t}^{})`$ where tuple $`\overline{t}^{}`$ is obtained from $`\overline{t}`$ by changing each term beginning with a labeled constructor term for $``$, for each $`f/nFS_\mathrm{\Sigma }`$, and $`|_\mathrm{\Sigma }`$ means the reduct of the algebra $`\mathrm{𝐂𝐓𝐀𝐥𝐠}_{\mathrm{\Omega }\times \mathrm{\Sigma }}`$ obtained by restricting the carrier to $`\mathrm{𝐂𝐓𝐞𝐫𝐦}_{}`$ and forgetting all functions denoting labeled function symbols.

Obviously, the representation of the closure wrt the functional signature is a particular case of closure hiding a set of constructor symbols when this set is empty.

## 9 Discussion

Research in component-based software development is currently becoming a very active area for the logic programming community. In fact, we can find several proposals in the field of computational logic for dealing with the design and development of large software systems. Other related fields, like functional-logic programming are now proving that the integration of logic variables and functions may increase the expressive power of a programming language. A number of attempts are being made in this direction  to achieve a consensus on the characteristics a functional-logic language has to present.

The current work tries to contribute to all these efforts by presenting a notion of module in the context of functional-logic programming, and by providing a number of operations (satisfying some expected algebraic properties) expressive enough to model typical modularization issues like export/import relationships, hiding information, inheritance, and a sort of abstraction. We have chosen the Constructor-based Conditional Rewriting Logic  to develop our proposal and, in this context, we have explored a rather wide range of semantics for program modules and we have studied some of their relevant properties, in particular, those concerning compositionality and full abstraction wrt the observation function $`Ob(𝒫)=_𝒫`$ and the set $`\{,\overline{()}^\sigma ,()\sigma ,\rho ()\}`$ of module operations. Although these features are interesting enough from a theoretical point of view, they present a special significance when module reusing, module refining or module transforming are involved. The least model semantics, $`[\{\}]_{LM}`$, is a fully abstract semantics, which is only compositional wrt $`\{\overline{()}^\sigma ,\rho ()\}`$, but only for injective function renamings $`\rho `$. On the contrary, the $`𝒯`$-semantics, $`[\{\}]_T`$, is compositional (wrt all operations), but is not fully abstract. The third proposal, the loose model-theoretic semantics, $`[\{\}]_M`$, is also compositional (except for the deletion operation), although the full abstraction property is not satisfied. A fully abstract semantics, $`[\{\}]_{CM}`$, may be obtained by considering a consistency property on term algebras, which is also compositional wrt the union, closure and renaming operations. To recover the compositionality wrt deletion we need a finer semantics able to capture the “independent” meaning of each function in a module; this is the case of the deletion semantics, $`[\{\}]_D`$, which still is fully abstract and compositional wrt all operations. We have also studied the ($`𝒯Id`$)-semantics, $`[\{\}]_{TI}`$, but we have not included this study in this paper because it exhibits the same properties as the $`𝒯`$-semantics. Table 1 summarizes the properties satisfied by each one of the analyzed semantics. It is possible to establish a semantics hierarchy ranging from the model-theoretic semantics to the $`𝒯`$-semantics on the basis of the following order for the equivalence relationships induced by these semantics

$$_T_{TId}_D_{CM}_C$$

where they are ordered upon their strength. The $`𝒯`$-equivalence relation, $`_T`$, is the strongest one, and it is contained obviously into the ($`𝒯Id`$)-equivalence relation, $`_{TId}`$. Taking into account that this equivalence relation is compositional but not fully abstract, it will be contained in $`_D`$, which is also contained in the consistent term-model equivalence, $`_{CM}`$. Obviously, the least term-model equivalence, $`_{LM}`$, is the weakest one.

In order to establish some conclusions about the compositionality and the full abstraction of all these semantics, we are going to discuss the information exhibited in Table 1. In this table, we can observe a sort of dependency between fulfilling compositionality/full abstraction and the strength of the equivalence relationship defined by the semantics, in such a way that the strongest ones are compositional whereas the weakest ones are fully abstract. The best semantics must be an intermediate semantics satisfying both properties; in our case, the semantics $`[\{\}]_D`$. A similar study was already made by Brogi in  in the field of logic programming, but he did not deal with variables, and avoided the complexity inherent to the non-ground term algebras. Another difference (apart from the context) with respect to the current work is the set of operations we are considering, which does not coincide with the set of inter-module operations defined by Brogi. One of the most significative operations described by him is the intersection of programs. This operation makes the $`(𝒯Id`$)-semantics compositional and fully abstract in a logic programming context. However, the difficult justification of this operation in our framework (the functional-logic programming paradigm) has inclined us to think in an alternative: the deletion operation. We believe that this operation is more natural (as a composing mechanism) than program intersection. This has an inconvenience: the ($`𝒯Id`$)-semantics is not fully abstract (although it is compositional) wrt our operations. In fact, the intersection of programs is a very powerful tool to distinguish programs (more than the deletion operation), and it can be used to delete a single rule, whereas our deletion operation only can be used to delete a whole set of rules defining a function. Nevertheless, we have found a fully abstract and compositional semantics, also for the deletion operation, which completes the results provided by this work.

## Acknowledgments

We would like to thank Mario Rodríguez Artalejo and Ana Gil Luezas for their helpful comments and suggestions on the initial versions of this work. We would also like to thank Narciso Martí-Oliet for their insightful comments and suggestions, that greatly helped us improving the quality and presentation of the paper. This work has been partially supported by the Spanish project TIC98-0445-C03-03.