Valmi Dufour-Lussier

Jean Lieber

Emmanuel Nauer

Yannick Toussaint

Improving case retrieval by enrichment of the domain ontology

Keywords: ontology refinement, formal concept analysis, progressive retrieval

One way of processing case retrieval in a case-based reasoning (CBR) system is using an ontology in order to generalise the target problem in a progressive way, then adapting the source cases corresponding to the generalised target problem. This paper shows how enriching this ontology improves the retrieval and final results of the CBR system. An existing ontology is enriched by automatically adding new classes that will refine the initial organisation of classes. The new classes come from a data mining process using formal concept analysis. Additional data about ontology classes are collected explicitly for this data mining process. The formal concepts generated by the process are introduced into the ontology as new classes. The new ontology, which is better structured, enables a more fine-grained generalisation of the target problem than the initial ontology. These principles are tested out within TAAABLE, 1 a CBR system that searches cooking recipes satisfying constraints given by a user, or adapts recipes by substituting certain ingredients for others. The ingredient ontology of TAAABLE has been enriched thanks to ingredient properties extracted from recipe texts.

Introduction

This paper studies the effect of the domain ontology on a case-based reasoning (CBR) system and the improvement of result quality using a more fine-grained ontology.

TAAABLE [START_REF] Badra | Taaable: Text Mining, Ontology Engineering, and Hierarchical Classification for Textual Case-Based Cooking[END_REF] is a system as a candidate of the Computer Cooking Contest. It is also used as a brain teaser for research in knowledge based systems, including CBR and ontology engineering. Like many CBR systems, TAAABLE uses an ontology to retrieve the source cases that are the most similar to a target case. TAAABLE retrieves and creates cooking recipes by adaptation. According to constraints given by the user, such as inclusion or rejection of ingredients, the type or the origin of the dish, the compatibility with some diets (vegetarian, nut-free, etc.), the system looks up, in the recipe base (which is a case base), whether some recipes satisfy these constraints. Recipes, if they exist, are returned to the user; otherwise the system is able to retrieve similar recipes (i.e. recipes that match partially the target query) and adapts these recipes, creating new ones. Searching similar recipes is guided by several ontologies, i.e. hierarchies of classes (ingredient hierarchy, dish type hierarchy and dish origin hierarchy), in order to relax constraints by generalising the user query. Relaxation is iterative and progressive. The goal is to find the most specific generalisation of the target case (the one with the minimal cost) for which recipes exist in the case base. Adaptation consists of substituting some ingredients of the source cases by the ones required by the user.

Many CBR systems use class or index hierarchies (taxonomies, ontologies, objectbased hierarchies [START_REF] Bergmann | Similarity measures for object-oriented case representations[END_REF], etc.) for retrieval, especially to compute similarity between cases. Therefore, the ontology structure impacts retrieval, raising the issue of how to refine this ontology for improving this process. This paper proposes a novel approach to automatise this refinement.

The main idea for realising this goal is as follows. In a given ontology, the siblings of a class C may be either close to C of far from it, depending on the level of details of this part of the ontology. For instance, if an ingredient ontology is very detailed for berries (i.e. with a deep hierarchy below the class Berry) and very coarse for vegetables (i.e. each vegetable class is a direct subclass of the class Vegetable) then the similarity between a blackberry and a blueberry would counter-intuitively be much lower than the similarity between a pumpkin and a parsnip. Generalisation of the query is the basis for case retrieval and it is computed using a similarity measure defined on ontologies. Introducing new classes into the ontology provides a more fine-grained generalisation. Going up in a more structured hierarchy will return less and more similar cases than going up in a less structured hierarchy.

A data mining process based on formal concept analysis (FCA) extracts new classes and enriches the initial ontology by structuring it better. Additional sources are collected and used to introduce new properties about classes of the initial ontology. This work helps avoid adaptation failures, i.e. creating a recipe that is not cookable because some actions that were applied to the substituted ingredient are not applicable to the substitution ingredient: for instance, when substituting mascarpone (a creamy cheese) for mozzarella (a semi-firm cheese), the slice action will not be applicable anymore.

The paper is organised as follows: Section 2 presents TAAABLE inference engine principles, Section 3 describes related work about existing approaches for improving retrieval in CBR and ontology refinement using FCA, Section 4 details the ontology refinement process, and Section 5 shows on an example the effect of the refined ontology in the TAAABLE system.

Reasoning principles in TAAABLE

TAAABLE retrieves cases using query generalisation, then adapts them by substitution. This section gives a simplified description of the TAAABLE system. For more details about the TAAABLE inference engine, see e.g. [START_REF] Badra | Taaable: Text Mining, Ontology Engineering, and Hierarchical Classification for Textual Case-Based Cooking[END_REF].

Case retrieval.

Domain ontology. An ontology O defines the main classes and relations relevant to cooking, and guides retrieval. O is a set of atomic classes organised into several hierarchies (ingredient, dish type, dish origin). Given two classes B and A of this ontology, A is subsumed by B, denoted by "B

A", iff the set of instances of A is included in the set of instances of B. For instance, "Riccota (referring to the Italian fresh cheese) is subsumed by FreshCheese" means that all instances of Riccota are instances of FreshCheese. For the sake of simplicity, only the ingredient hierarchy is considered in the remainder of this paper. A part of this hierarchy is given in Fig. 1.

Source cases. For the inference engine, recipes are represented by a conjunction of the ingredients they call for, and is encoded in the same language as the one of the queries. Thus, a recipe with ricotta, tomato, olive oil, and salt, is represented by: R = ∃ing.Ricotta ∃ing.Tomato ∃ing.OliveOil ∃ing.Salt (1)

Target query. In the TAAABLE system, a query Q is a conjunction of terms ∃ing.I, where I is a class in the ingredient hierarchy, meaning that the recipe should contain the ingredient I. For example, searching a recipe with tomato and fresh cheese corresponds to Q = ∃ing.Tomato ∃ing.FreshCheese. If C and D are two conjunctions (for example, two queries), C = i ∃ing.A i is subsumed by D = j ∃ing.B j if, for each j, there exists at least one i such that A i is subsumed by B j in O.

Given a recipe R and a query Q, R solves Q if the set of recipes represented by R is included in the set of recipes represented by Q. Thus, the recipe represented by [START_REF] Asiimwe | Automatically Acquiring Structured Case Representations: The SMART Way[END_REF] solves the query Q = ∃ing.FreshCheese ∃ing.Tomato. This can be computed simply by testing if R is more specific than Q. It is important to notice that R solves Q does not mean that it is a "good" solution, even if the hypothesis that recipes of the case base are "good" is made (this is a working hypothesis: as no information about the quality of the recipes in the case base is available, it is simplest to consider the recipes as being good or, at least, equally good).

Algorithm. The algorithm consits in an iterated generalisation of the target query minimising cost, until at least one recipe of the case base solves the modified query. The query that has been modified at iteration t is noted Γ t (Q), and Γ 0 is the identity. The generalisation cost of Γ t , denoted by cost(Γ t ), grows with t (see below for the cost function definition). Each generalisation Γ t is written as a composition of substitutions A B such that (A, B) is a specialisation link between A and B in the hierarchy representing the ontology. Furthermore, this composition must be applied to

Q: if Γ = (A p B p ) • . . . • (A 2 B 2 ) • (A 1 B 1 ) then A 1 is an element of the conjunc- tion Q, A 2 is an element of the conjunction (A 1 B 1 )(Q), etc.
The algorithm running through the generalisation space of Q is an A* algorithm which takes as parameter the cost function. It stops when at least one recipe R such that R solves Γ t (Q) is found.

The cost function. Let Γ be a composition of substitutions. Function cost is additive for the composition: cost(σ 2 • σ 1 ) = cost(σ 1 ) + cost(σ 2 ). For a basic substitution σ = A B (where A is subsumed by B), the cost is computed as follows:

cost(A B) = µ(B) -µ(A) with µ(X) =
number of recipes with X total number of recipes Therefore, 0 ≤ cost(A B) ≤ 1.

Function cost has the following property: if Γ has a cost computed with respect to a given ontology and a new node is added into this ontology (without changing the recipe base), then the cost of Γ will not change. For instance, if Γ = Ricotta FreshCheese and the ItalianFreshCheese class is "added" into the ontology "between" Ricotta and FreshCheese, the cost of Γ remains unchanged. So, there is an essential difference between this cost function and one based on the number of edges separating two nodes (number that grows by adding an intermediate node). This property ensures stability of the cost regardless of the introduction of intermediate classes.

Adaptation. Let Q be a query, Γ a generalisation function of this query, and R a recipe solving Γ (Q). Let T i , B j and S k be classes such as Q = i ∃ing.T i (T as target), Γ (Q) = j ∃ing.B j and R = k ∃ing.S k (S as source). Γ (Q) is more general than both R and Q, thus for all j, there exists k and i such that S k and T i are subsumed by B j . Then the adaptation consists of substituting T i for S k for all B j , such that B j = T i . If several T i or S k correspond to one B j , several adaptations are possible and are returned to the user. These substitutions, along with the preparation instructions, give the modifications that must be applied to the recipe in order to address the query.

Example. Let Q = ∃ing.Tomato ∃ing.Mascarpone ∃ing.Oil. Among the generalisations of this query, say that Γ = Mascarpone FreshCheese is the substitution with the minimal cost (apart from identity). As Ricotta is subsumed by FreshCheese in the ontology, TAAABLE retrieves the recipe R given by [START_REF] Asiimwe | Automatically Acquiring Structured Case Representations: The SMART Way[END_REF]. The adaptation will consist in substituting S k = Ricotta by T i = Mascarpone (generalisationspecialisation through B j = FreshCheese).

However, a non-realistic adaptation can be returned, in which some actions have to be applied to objects on which they cannot be applied to. We will address this problem after introducing our approach to ontology refinement.

FreshCheese sliceAble beatAble cutAble mashAble

Mascarpone × × Ricotta × × × × Mozzarella × × × FromageFrais × × CottageCheese × × × QuesoFresco × × × ×
Table 1. A binary context with 6 objects (cheeses from the FreshCheese category) described by 5 properties (the FreshCheese category and 4 cooking actions which can be applied to these cheeses).

Formal concept analysis for ontology refinement

The goal of the refinement process is to add intermediate classes into the initial hierarchy of the system. These additional classes will enable for a better distinction of the similarity between classes immediately subsumed initially by a same class.

Formal concept analysis

FCA is a classification method based on lattice theory. A formal context is a triple K = (G, M, I), where G is a set of individuals (called objects), M a set of properties (called attributes) and I the relation on G × M stating that an object is described by a property [START_REF] Ganter | Formal Concept Analysis: Mathematical Foundations[END_REF]. Table 1 shows an example context: G is a set of 6 objects (which are fresh cheese subclasses), M is the set of 5 properties applicable to those cheeses. Among theses properties, one (FreshCheese) comes from the initial hierarchy. FreshCheese is a class which is more general than the 6 cheese classes that have to be classified (in other words, FreshCheese denotes both the class of fresh cheese in the ontology and the property of being a fresh cheese). The 4 other properties are cooking actions that can be applied: sliceAble (can be sliced), beatAble (can be beaten), cutAble (can be cut), and mashAble (can be mashed).

The approach for merging properties coming from several contexts, for a given set of objects, is called context apposition. Formally, if K 1 = (G, M 1 , I 1 ) and K 2 = Fig. 3. The lattice corresponding to the binary context given in Table 1.

(G, M 2 , I 2 ) are two binary contexts about the same set of objects G, a binary context, written K 1 |K 2 merging K 1 and K 2 can be built by:

K 1 |K 2 = (G, M 1 ∪M 2 , I 1 ∪I 2 ) [4].
A formal concept is a pair (P, O) where P is a set of properties (the intent of the formal concept), O is a set of objects (the extent of the formal concept), such that (1) P is the set of all properties shared by objects in O and (2) O is the set of all objects sharing properties P . For example, ({FreshCheese, beatAble, mashAble}, {QuesoFresco, Ricotta, CottageCheese}) is a formal concept (node number 5 in Fig. 3).

The set C K of all formal concepts of the context K = (G, M, I) is partially ordered by extent inclusion, also called the specialisation (denoted by ≤ K ), between concepts. L = C K , ≤ K is a complete lattice, called the concept lattice. The lattice L can be drawn as a Hasse diagram where nodes are concepts, and edges are specialisation links. Fig. 3 illustrates the lattice corresponding to the binary context given in Table 1. The top concept (with number 1, in the figure) contains all the objects. In our example, its intent is FreshCheese, a property shared by all the objects. By contrast, the bottom concept is defined by the set of all properties. In our example, its extent is empty as none of the objects is described by all the properties.

A number of algorithms have been proposed for the construction of concept lattices (see [START_REF] Ganter | Formal Concept Analysis: Mathematical Foundations[END_REF]). For our application, we used CORON, a software platform implementing a rich set of algorithmic methods for symbolic data mining, including concept lattice construction algorithms [START_REF] Szathmary | CORON: A Framework for Levelwise Itemset Mining Algorithms[END_REF]. Fig. 3 was generated by GALICIA,2 another FCA tool, which provides visualisation functionalities.

Ontology building using FCA

Many works propose using FCA to build ontologies. Cimiano [START_REF] Cimiano | Learning concept hierarchies from text corpora using formal concept analysis[END_REF] proposes an approach to build a concept hierarchy from texts in the tourism domain. The objects (hotels, cars, bicycles, tours, etc.) are characterised by the actions that can be applied to them (can be reserved, can be driven, can be rented, etc.). In order to reduce the lattice size, a numerical classification is used as a first step of the binary context building.

Stumme et al. [START_REF] Stumme | FCA-MERGE: Bottom-Up Merging of Ontologies[END_REF] propose an approach to merging two ontologies. The ontology classes are identified in the texts and a binary context is built for each of the two ontologies, in which classes are characterised by the documents in which they appear. Context apposition is used for aggregating the classes of the two ontologies according to their presence in the texts. [START_REF] Bendaoud | Formal Concept Analysis: A unified framework for building and refining ontologies[END_REF] shows how FCA can be used as a unified framework for ontology building and refinement. It points out that the information that may be extracted from the texts depends on the textual resources itself. Thus, from a scientific paper, objects can be extracted and properties can be linked to objects as it is done in [START_REF] Cimiano | Learning concept hierarchies from text corpora using formal concept analysis[END_REF]. But an ontology organises classes of a given domain into a hierarchy. This information about the specific/generic organisation is seldom present in scientific papers. In Bendaoud et al. [START_REF] Bendaoud | Formal Concept Analysis: A unified framework for building and refining ontologies[END_REF], these two types of information are managed separately and are then combined with context apposition to build a single lattice.

We use this type of approach to build the ingredient ontology in the cooking domain. Recipe texts are used in order to characterise the ingredients according to how they are cooked, and the initial ontology is used in order to get the specific/generic relations.

Ontology refinement process

FCA has been succesfully used in CBR: in [START_REF] Asiimwe | Automatically Acquiring Structured Case Representations: The SMART Way[END_REF] for building cases from texts (objects correspond to texts and properties to relevant terms), in [START_REF] Díaz-Agudo | Classification Based Retrieval Using Formal Concept Analysis[END_REF] for organising a case base for the purpose of retrieval. In the present work, FCA is used for ontology refinement.

The goal of the refinement process is to add intermediate classes into the initial hierarchy of the system. To do that, the classes of the initial ontology are characterised with additional properties. These properties enable the creation of a binary context that will be exploited for building a concept lattice with FCA. The formal concepts of the lattice are inserted into the initial hierarchy in order to enrich its organisation. The following four steps describe the ontology building and refinement process. We detail those steps with examples about an ingredient hierarchy refinement.

Ingredient hierarchy overview

The initial ingredient hierarchy has been semi-automatically created from common sense classifications (e.g. a citrus fruit is a fruit). All ingredients used in the recipe base have been introduced. The ingredient hierarchy currently contains 1500 classes. An excerpt is shown in Fig. 1. The ontology (and the recipes of the case base) are managed in a semantic wiki [START_REF] Badra | Knowledge Acquisition and Discovery for the Textual Case-Based Cooking system WikiTaaable[END_REF]. The high level of the hierarchy contains general classes: Vegetable, Fruit , Dairy, Meat, etc. The low level of the hierarchy contains classes that are ingredients actually used in the recipes.

From the sole hierarchy, the similarity between two sibling ingredients (i.e. immediate subclasses of a single class) cannot be ranked. For example, mascarpone is as close to mozzarella as it is to ricotta. Consequently, when a query is generalised for case retrieval, if Mascarpone is generalised to FreshCheese, the set of remaining cases will contain recipes using mozzarella as well as recipes using mascarpone. This is why we want to refine the hierarchy organisation for gathering initial classes that are similar (i.e. classes that share at least one property). Generalising a class C into a parent concept will ensure that sibling classes of C own at least the same properties as C. The generalisation will be more fine-grained.

Local refinement

The action of refining a limited part of the ontology is called local refinement. For instance, we could refine locally the sub-part about Nut (walnut, pecan nut, etc.), the sub-part about Berry (raspberry, blueberry, etc.), the sub-part about FreshCheese, etc. This approach has been preferred to global refinement for several reasons:

-Focusing on a part of the hierarchy (i.e. a subset of classes) is a way to limit the size of the binary context by reducing the number of objects and the number of associated properties. A reduced context will produce a lattice with a smaller size, which can be viewed and interpreted more easily. -We do not want to build classes gathering ingredients that do not belong in the same part of the hierarchy. For instance, we do not want to group kiwis and onions merely because it is possible to apply a given action, such as to peel, to both. -For each part of the hierarchy, the properties taken into account for the binary context may be different: to toast makes sense for nuts but not for liquids.

Therefore we ought to focus on the refinement of (bottom) parts of the hierarchy, while maintaining the top structure. The local refinements will be plugged into the initial ontology (see hereafter). Formally, R refers to the class which is the root of the part of the hierarchy that has to be refined. The context K R = (G R , M R , I R ) is the binary context composed of:

a set of objects: in this work, objects used for FCA are classes of the ingredient hierarchy, e.g. Orange, more specific than R: G R = {x | R x}, a set of properties (cooking actions) M R selected to characterise and discriminate the objects of G R , the relation I R such that I R relates i ∈ G R to a ∈ M R if the action a can be applied to the ingredient i.

The next two sections illustrate the refinement process for R = FreshCheese.

Building the binary context for the refinement

The ontology refinement aims at modifying an existing ontology. Properties of the initial ontology must be retained, and new properties introduced to organise the classes (ingredients) better against each other. Aggregating ricotta with mascarpone and distinguishing these two fresh cheeses from mozzarella is an expected outcome. Two binary contexts must be merged:

-A binary context capturing the initial ontology structure by associating to each ingredient class their superclasses, e.g. the object Ricotta has the properties Ricotta and FreshCheese. -A binary context describing ingredients through the culinary actions that can be performed on them. For instance, ricotta and mascarpone can be beaten but mozzarella cannot, though mozzarella can be sliced, which is not the case for creamy cheeses.

Ingredient properties are extracted from 73795 recipes taken from Recipe Source. 3Ingredient properties are extracted both from the ingredient list, which includes some cooking actions, and from the textual preparation, from which the actions applied to the ingredients are extracted using NLP tools [START_REF] Dufour-Lussier | Text adaptation using formal concept analysis[END_REF]. The latter approach uses both classical morpho-syntactic analysis methods and a discourse representation specifically developed for procedural texts (instruction texts, including recipes). The discourse representation is well adapted for solving some complex anaphoric phenomena appearing in those types of texts. An example of a recipe used for property extraction is given in Fig. 4.

Extracting the properties of the ingredient list is done through an automatic annotation process, because the recipes are initially in a textual form. This annotation process was designed in order to obtain a formal representation of the recipes that can be handled by the CBR engine. The annotation process uses a terminological base for indexing the recipes by classes of the ingredient hierarchy. The quantities, the units, and the ingredient modifiers such as chopped, diced, crumbled, etc. (cf. Fig. 4) are also extracted. These modifiers are mostly cooking actions applied to the ingredients. Pairs (ingredient, modifier) and pairs (ingredient,applied action) extracted from the textual preparation are used for building the binary context. Some examples can be seen in the annotated recipe example given in Fig. 4. The set of properties M R of K R contains the cooking actions required for refining the ingredients of G R . For example, let R =

× × × × FatFreeCottageCheese × × × × × CreamCheese × × × × × × FatFreeCreamCheese × × × × × × × FromageFrais × × × × × LowFatFromageFrais × × × × × × Mozzarella × × × × Mascarpone × × × × × QuesoFresco × × × × Ricotta × × × × × Table 2.
A binary context for cheeses from the FreshCheese category, described by generic/specific properties and cooking actions that can be applied to the cheeses.

FreshCheese and M R = {mashAble, meltAble, beatAble, mixAble, sliceAble, cutAble, crumbleAble}. Then, table 2 presents the binary context K FreshCheese .

Merging the local lattice and the initial hierarchy

Given a class R of the initial hierarchy and the lattice L R built from the context K R , the initial ontology is refined by adding ontology classes corresponding to some of the concepts of L R . The choice of these concepts in L R is based on the notion of reduced extent of a concept C of L R . Following the terminology of object-oriented languages, the reduced extent E r (C) of C is the set of direct instances of C. In other words, an object x belongs to the reduced extent of C if it belongs to the extent of C but does not belong to the extent of any direct descendant D of C in the lattice:

E r (C) = E(C) \ {E(D) | D: direct descendant of C in the lattice}
It can be proven that x ∈ E r (C) iff the properties of C are exactly the ones of I(C), the intent of C (whereas an x ∈ E(C) may have additional properties, outside of I(C)).

Moreover, for a context K R built as explained in the previous section, for each concept C of L R , either E r (C) = ∅ or E r (C) contains exactly one element. Fig. 5 is the lattice L FreshCheese (with the reduced extents instead of the extents). The grey concepts C are the ones that are chosen in order to be added to the initial ontology. The concept with an empty extent (concept 16 in Fig. 5) covers no instance and thus is not added to the ontology. Some concepts correspond to classes that are already in the ontology and need not be added. This is the case for the root concept, (in the example, FreshCheese, concept 1), and for the concepts C having exactly one The remaining FCA concepts are structuring concepts that are added to the ontology (concepts 2 to 5, in grey in the Fig. 5). Such a node C has an empty reduced extent, thus its extent equals the union of the extents of its direct descendants in L R . Its intent factorises properties of its subconcepts. Adding such a concept to the ontology, means reifying a new ontology class with a label obtained by concatenation of the intent properties. For example, the concept 5 leads to the class in the ontology whose label is FreshCheese_beatAble_meltable_mixAble. This class refers to the fresh cheeses that can be beaten, melted, and mixed. The part of the refined ontology regarding fresh cheeses is given on the right hand-side of Fig. 6.

Effect of the ontology refinement on the CBR process: an example

This section shows how the ontology refinement affects the CBR system. An example is given of TAAABLE's performance before and after the refinement in order to show In order to evaluate the effect of the refinement, two TAAABLE systems were instantiated: TAAABLE 0 using the initial ontology and TAAABLE 1 using the refined ontology. The two systems were given the same query to answer. Fig. 7 shows the answer of the two systems to a query asking for a recipe with tomato and mascarpone. Since no recipe contains both those ingredient in the case base, the two systems search for similar cases.

For TAAABLE 0 , the retrieval stops after the generalisation Mascarpone Fresh-Cheese. At this step, 8 recipes satisfying the query ∃ing.Tomato ∃ing.FreshCheese are found and adapted by substituting Mascarpone for FreshCheese. Some of the recipes contain several FreshCheeses. In this case, the system proposes to substitute one or more ingredients (this is the case for the recipes numbered 1, 3 and 5). For TAAABLE 1 , the retrieval is more fine-grained: the generalisation stops on the FreshCheese_beatAble_meltable_mixAble class, which is more specific than Fre- shCheese. This class represents the fresh cheeses that can be beaten, melted, and mixed, actions that are applicable to mascarpone. The analysis of the results presented in Fig. 7 shows that:

-TAAABLE 1 returns only 4 answers, while TAAABLE 0 returns 8 answers (including the 4 answers of TAAABLE 1 with different substitutions). The generalisation is less sharp in the case of the refined ontology than with the initial one. -The substitutions proposed by TAAABLE 0 are more variable than the ones proposed by TAAABLE 1 . With TAAABLE 1 , mascarpone is substituted for ricotta or cream cheese, while TAAABLE 0 additionally proposes to substitute mascarpone for mozzarella, non-fat cottage cheese or queso fresco. And the larger the set of substituting ingredients, the more likely the adaptation is to fail, because there is less similarity between the ingredients.

Examining the proposed substitutions recipe by recipe allows to evaluate the adaptation success or failure. If the adaptation fails, the reason for failure is identified. Table 3 gives, for each recipes of TAAABLE 0 , the actions that were applied to the substituted ingredient. If the action cannot be applied to the substituting ingredient -in our case, the mascarpone -the adaptation fails. These failures are marked with a cross in the Failure column. There are 3 clear cases of failure, for the following recipes:

-Pasta gratin with etc. in which the mascarpone should be grated; -Lasagne a la baroque in which the mascarpone should be sliced; -Southwest stew in which the mascarpone should be crumbled.

There are also three half-failures for answers in which TAAABLE 0 proposes to choose the ingredient that has to be substituted. So, adapting the Pasta garden recipe may be considered as a success if the mascarpone replaces the ricotta, but as a failure if the mascarpone replaces the mozzarella and that it must be shredded. It is the same for the Nofuss lasagna recipe, where substituting ricotta succeeds while substituting mozzarella fails, and for the Eggplant parmigiana recipe where substituting ricotta succeeds while substituting mozzarella fails. To conclude, 6 of the 11 substitutions fail with TAAABLE 0 on this example. Table 4 gives, for each recipe of TAAABLE 1 , the actions that must be applied to the substituted ingredient, a failure being marked with a cross. We see that the refined ontology improves the final result as none of the failed adaptations proposed by TAAABLE 0 are proposed by TAAABLE 1 : there is no case of either clear nor halffailure. However, one recipe of TAAABLE 0 (Tex-mex lasagna) for which the adaptation succeeds is not proposed by TAAABLE 1 because of the increased distance between NonFatCottageCheese and Mascarpone in TAAABLE 1 's ontology. This results from the stop condition of the algorithm of TAAABLE which runs through the generalisation space. This problem can be solved by asking, in the system interface, to further search similar recipes beyond the current generalisation, at the risk of introducing again failed adaptations.

Conclusion

This paper shows how a domain ontology refinement immediately affects the retrieval process of a CBR system and how it improves the final result of the TAAABLE system. Our approach enables a more progressive retrieval of source cases and, within the framework of TAAABLE, some adaptation failures are eliminated. Beyond the results of our approach, illustrated by a concrete example, this work raises some issues that must be addressed.

A first issue is the supervision of the set of properties taken into account for the refinement. In this work, this set has been limited manually because there are potentially more than 250 cooking actions. Selecting a priori some properties (cooking actions) that discriminate the ingredients limits unwanted aggregations. However, as the use context of an ingredient may change, it is not impossible, that given a set of actions A 1 , an ingredient i be closer to an ingredient i 1 and, given another set of actions A 2 = A 1 , i be closer to i 2 = i 1 . So, for one context, ricotta could be closer to mascarpone and, in another context, closer to cottage cheese.

Another issue is case indexation. Each (recipe) case is actually indexed by its ingredients, regardless of how they are used. Improving the case representation by indexing them by the ingredients jointly with their transformations is another way to eliminate some of the adaptation failures of this type.

Finally, another point planned in order to improve the adaptation in TAAABLE is to manage action sequences and guarantee that the actions are applicable after the adaptation, by using pre-conditions based on domain knowledge: ingredient consistency (solid, liquid, soft. . . ), ingredient sensory properties (sweet, salted. . . ), etc. This knowledge makes it possible to check whether, after the adaptation, the recipe is cookable.

Fig. 1 .

 1 Fig. 1. A part of the ingredient hierarchy, including the details of the FreshCheese class.

Fig. 2

 2 illustrates how B, C, and D which are indistinguishably similar on the left-hand side are distinguished better after introducing an intermediate class (in this example, C and D more similar to each other than to B).

Fig. 2 .

 2 Fig. 2. Refining the ontology by introducing a new class.

Fig. 4 .

 4 Fig.4. Example of a recipe. The recipe contains a textual list of ingredients and preparation steps. Each ingredient line is parsed in order to extract structured data: quantity, unit, ingredient and additional pieces of information such as an action already applied or some precision about the ingredient (e.g. fresh).

F

  r e s h C h e e s e C o t t a g e C h e e s e F a t F r e e C o t t a g e C h e e s e C r e a m C h e e s e F a t F r e e C r e a m C h e e s e F r o m a g e F r a i s L o w F a t F r o m a g e F r a i s M o z z a r e l l a M a s c a r p o n e Q u e s o F r e s c o R i c o t t a m a s h A b l e m e l t A b l e b e a t A b l e m i x A b l e s l i c e A b l e c r u m b l e A b l e c u t A b l e CottageCheese

Fig. 5 .

 5 Fig. 5. Concept lattice restructuring the fresh cheeses.

Fig. 6 .

 6 Fig. 6. Initial (left) and refined (right) ontology from the FreshCheese class down.

Fig. 7 .

 7 Fig. 7. TAAABLE0 and TAAABLE1's answers to the query ∃ing.Tomato ∃ing.Mascarpone.

Table 3 .

 3 List of actions applied to the substituted ingredients of recipes returned by TAAABLE 0 with tomato and mascarpone. A cross in the failure column indicates adaptation failure because an action cannot be applied upon the substitution ingredient.

		Substituted ingredient Applied actions Failure
	Eggplant parmigiana	Ricotta	add
		Mozzarella	cut	×
	Pasta gratin with etc.	Mozzarella	grate	×
	Pasta garden pie	Mozzarella	shred, sprinkle	×
		Ricotta	stir
	Tex mex lasagna	NonFatCottageCheese	mix
	No-fuss lasagna	Mozzarella	shred	×
		Ricotta	mix
	Lasagne a la baroque	Mozzarella	slice, add	×
	3-step veggie pizza	CreamCheese	sprinkle
	Southwest stew	QuesoFresco	crumble	×

Table 4 .

 4 List of actions applied to the substituted ingredients of recipes returned by TAAABLE 1 with tomato and mascarpone. A cross in the failure column indicates adaptation failure because an action cannot be applied upon the substitution ingredient. For TAAABLE 1 , there is in fact no such failure.

		Substituted ingredient Applied actions Failure
	Pasta garden pie	Ricotta	mix
	No-fuss lasagna	Ricotta	mix
	3-step veggie pizza	CreamCheese	sprinkle
	Eggplant parmigiana	Ricotta	add

http://taaable.fr

http://www.iro.umontreal.ca/~galicia

http://www.recipesource.com/

Acknowledgements. The authors wish to thank the reviewers for their helpful comments and suggestions for future work.


Colin Riba
email: colin.riba@ens-lyon.fr

On the Representation of Stream Functions in Denotational Domains

We investigate the representation of functions on streams in some denotational domains. As expected, a total continuous stream function can always be represented by a Scott-continuous function, and moreover by a strongly stable map in the corresponding Hypercoherence.

It seems however difficult to represent an arbitrary stream function by a monotone map on Scott domains such that the stream function is continuous if and only if its representant is Scott-continuous. The difficulty is that the set of Scott-approximants of an open subset of a not (topologically) compact set of streams may not be Scott-open. We show that this problem does not occur in the compact case.

Introduction

We investigate the representation of functions on streams in Scott domains for the corresponding PCF types [START_REF] Plotkin | LCF Considered as a Programming Language[END_REF].

As expected, it is easy to define from an arbitrary f : A ω → B ω , a map f * on the corresponding domains which is always Scott-continuous. Such an f * always underapproximates f , and represents f if and only if f is continuous. As also expected, it is not difficult to adapt the definition scheme of f * in order to get a Strongly Stable map in the corresponding Hypercoherences [START_REF] Ehrhard | Hypercoherences: A strongly stable model of linear logic[END_REF][START_REF] Ehrhard | Projecting sequential algorithms on strongly stable functions[END_REF].

The main question discussed in this paper is: how to "uniformly" define a (monotone) representant f * for an arbitrary f , such that f * is Scott-continuous if f is continuous. This question is motivated by the use of stream functions to model infinite computations in frameworks related to software verification such as Büchi automata (see e.g. [START_REF] Thomas | Automata on Infinite Objects[END_REF][START_REF] Grädel | Automata, Logics, and Infinite Games: A Guide to Current Research[END_REF]), or in game based frameworks related to descriptive set theory [START_REF] Semmes | A Game for the Borel Functions[END_REF]. These frameworks consider more than continuous functions or open sets of streams. It seems interesting to understand how Curry-Howard based interpretations can give an account of these phenomena. Since Scott-topology on type 1 maps is not far from the usual product topology on streams, we do not expect to give an account of these behaviours in usual Scott domains. However, as a first step it seems important to understand how a stream function f can, first, be represented by a monotone map f * on the corresponding domain independently from the continuity of f , and then, to relate the continuity of f with the Scott-continuity of f * .

The main results of this paper suggest that this is not as easy as it seems. The difficulty is that in general, the set of Scott-approximants (in the cpo A ω of Scott-continuous maps from the flat cpo ω ⊥ to the flat cpo A ⊥ ) of an open subset of A ω form a Scott-open subset of A ω only when A ω is compact. This contrasts with the converse situation, where the set of streams α ∈ A ω whose lift α ⊥ belong to a Scott-open subset of A ω is always an open subset of A ω .

Technically, we relax the straightforward definition of f * from a monotone map of Scott-finite elements (that we call finitary in this paper), and do not require that the result on a arbitrary element of a cpo is uniquely determined by the finitary elements below it. Such a relaxation seems necessary in order to prevent f * from being automatically Scott-continuous.

Our result on Scott-topology makes this difficult (if not impossible) to work in the general case. We show that this works well when A ω is topologically compact (i.e. when the alphabet A is finite). This corresponds to the kind of streams dealt-with in automata theory [START_REF] Thomas | Automata on Infinite Objects[END_REF][START_REF] Grädel | Automata, Logics, and Infinite Games: A Guide to Current Research[END_REF].

Section 2 gives technical preliminaries and formulates the main question discussed in the paper. In Sect. 3, we gather (more or less well-known) material on the representation of continuous stream functions by Scott-continuous maps. Our main contributions are in Sect.4. Finally, we give in Sect. 5 an account in Hypercoherences of some of the material of Sect. 3. We conclude in Sect. 6, where we also briefly discuss other possible choices for the representation of streams in denotational domains.

Preliminaries

Sequences

Let ω be the set of natural numbers. An infinite sequence (or stream) over a set A is map α : ω → A. Streams are the carrier of the final coalgebra for the functor (-) × A in Set [START_REF] Jacobs | A Tutorial on (Co)Algebras and (Co)Induction[END_REF]. We write A ω for the set of streams over A and let α, β, γ, . . . range over streams. A finite sequence (or word) of length n over A is a map p : {0, . . . , n -1} → A. We write A <ω for the set of words over A and let p, q, . . . range over words. Given a stream α and n ∈ ω, the word α↾n is the restriction of α of domain {0, . . . , n -1}.

Seen as relations, streams and words over A are subsets of ω × A. Hence p ⊆ α means that p ∈ A <ω is a finite prefix (and can be though of as a finite approximation) of α ∈ A ω . More generally, given a partial map s : ω ⇀ A (i.e. a subset of ω × A satisfying the following coherence property1 : if (n, a)(n, a ′ ) ∈ s then a = a ′ ), we let [s] be the set of streams approximated by s:

[s] := {α ∈ A ω | s ⊆ α} .

Type 2 Continuity

Let A and B be at most countable. It is generally accepted that a "computable" total map f from A ω to B ω must only need to read a finite part of α ∈ A ω in order to produce a finite part of its answer in B ω . This can be formalized by stating that for any input stream α ∈ A ω and any output index m ∈ ω, there is an input index n ∈ ω such that for any β ∈ A ω approximated by α↾n, we have f (β)(m) = f (α)(m). This precisely means that f is a continuous map from A ω to B ω , where A, B are discrete and A ω , B ω are equipped with the corresponding product topology. It is convenient to reformulate the continuity of f as: for all (m, b) ∈ ω × B and all

α ∈ f -1 [{(m, b)}], there is some p ∈ A <ω such that α ∈ [p] ⊆ f -1 [{(m, b)}] , (1)
where f -1 is the inverse image of f :

f -1 S := {α | f (α) ∈ S} (S ⊆ B ω ) .

Topology

Basic Definitions.

A topological space is a set X together with a collection Ω(X) of subsets of X such that Ω(X) contains both X and the empty set ∅, and is moreover preserved by finite intersections and arbitrary unions. A subset of X is closed if its complement w.r.t. X is open.

As advocated (and made precise in the relevant context) in [START_REF] Smyth | Topology[END_REF] (see also [START_REF] Escardó | Synthetic topology: of data types and classical spaces[END_REF]), the closure under arbitrary unions and finite intersections of opens suggests that "belonging to a given open set" may be through of as a kind of finite observation. Any set X can be endowed with the discrete topology Ω(X) = P(X), meaning that any point of X is observable. In other words, the discrete topology is the finer possible topology on X since it distinguishes all its elements. At the other extreme, the coarsest topology on X contains only ∅ and X. More generally, given two topologies Ω(X) and Ω ′ (X) on X, we say that Ω(X) is coarser than Ω ′ (X) if Ω(X) ⊆ Ω ′ (X).

Given topological spaces (X, Ω(X)) and (Y, Ω(Y )), a map f :

X → Y is continuous if the inverse image by f of any open subset of (Y, Ω(Y )) is open in (X, Ω(X)). If (X i ) i∈I is a family of topological spaces, the set Π i∈I X i of maps f : i ∈ I → f (i) ∈ X i
can be equipped with the product topology, which is the coarsest topology such that all projections

π i : f ∈ Π i∈I X i → f (i) ∈ X i are continuous.
A basis of a topological space (X, Ω(X)) is a collection of sets B such that every open set of X is the union of elements of B (by convention ∅ ∈ Ω(X) is the empty union).

A pre-basis of (X, Ω(X)) is a collection of sets whose finite intersections form a basis of (X, Ω(X)). Note that every basis is a pre-basis. Since inverse images preserve unions and intersections, in order to show that f : (X, Ω(X)) → (Y, Ω(Y )) is continuous, it suffices to check that the inverse images by f of pre-basic opens of (Y, Ω(Y )) are open in (X, Ω(X)).

A Topology on Streams.

As usual (see e.g. [START_REF] Kechris | Classical Descriptive Set Theory[END_REF][START_REF] Thomas | Automata on Infinite Objects[END_REF]), we equip A ω (= Π ω A) with the product topology issued from the discrete topology on A. With this topology, a subset U of A ω is open if and only if for any α ∈ U , there is n ∈ ω such that [α↾n] ⊆ U (see e.g. [START_REF] Kechris | Classical Descriptive Set Theory[END_REF]). This means that only a finite part of α must have been read in order to observe that α belongs to U .

We consider two basis for A ω :

• the set of all sets of the form [p] with p ∈ A <ω ,

• the set of all sets of the form [s] with s a finite partial map from ω to A.

The set of all sets of the form [{(n, a)}] with (n, a) ∈ ω × A is a pre-basis of these two basis.

The two above basis provide two equivalent formulations of the continuity of a stream function f :

A ω → B ω : besides (1) one can equivalently state that for any (m, b) ∈ ω × B and any α ∈ f -1 [{(m, b)}] there is some finite s : ω ⇀ A such that α ∈ [s] ⊆ f -1 [{(m, b)}] . (2)

Domains

We refer to [START_REF] Amadio | Domains and Lambda-Calculi[END_REF] for a more comprehensive treatment. Most of the material we use can also be found in [START_REF] Plotkin | LCF Considered as a Programming Language[END_REF].

Basic Definitions.

We write D → po E for the set of monotone functions from the partial order (D, ⊑ D ) to the partial order (E, ⊑ E ). A subset ∆ of a partial order (D, ⊑) is directed if it is non empty and for all d, d ′ ∈ ∆, there is some e ∈ ∆ such that d, d ′ ⊑ e.

A complete partial order (cpo) is a partial order (D, ⊑) which has a least element ⊥ and such that all directed ∆ ⊆ D have a least upper bound ∆.

A monotone map of cpos g :

D → po E is Scott-continuous if g commutes with lubs of directed sets: {g(d) | d ∈ ∆} = g( ∆) for all directed ∆ ⊆ D. The set D → cpo E is itself a cpo w.r.t. the pointwise ordering: g ⊑ h if g(d) ⊑ E h(d) for all d ∈ D. The discrete (or flat) cpo (X ⊥ , ⊑ X ⊥ ) associated to a set X is defined as X ⊥ := X +{⊥} and d ⊑ X ⊥ e if d = ⊥ or d = e. Note that a directed set ∆ ⊆ X ⊥ is
either a singleton or of the form {⊥, x} with x ∈ X. It follows that any monotone map of flat cpos is Scott-continuous.

An element e of a cpo (D, ⊑) is finitary2 if for all directed ∆ ⊆ D such that e ⊑ ∆, there is some d ∈ ∆ such that e ⊑ d. A cpo (D, ⊑) is algebraic if for any d ∈ D, the set {e | e is finitary and ⊑ d} is directed and its limit is d.

A Domain for Streams.

We write A ω for ω ⊥ → po A ⊥ = ω ⊥ → cpo A ⊥ , where ω ⊥ and A ⊥ are discrete. If s is a partial map from ω to A, then we let s ⊥ be the corresponding element of A ω :

s ⊥ : x ∈ ω ⊥ → s(x) if x ∈ dom(s), ⊥ otherwise. We say that d ∈ A ω is a Scott-approximant of α ∈ A ω if d ⊑ α ⊥ ,
(⊥) = ⊥) and also that d ⊑ d ′ implies [d ′ ] ↑ ⊆ [d] ↑ . Moreover, given s : ω ⇀ A, we have [s] = [s ⊥ ] ↑ . If g : D → E is a map of cpos, we let dom(g) := {d ∈ D | g(d) = ⊥ E }. Lemma 2.1 For any d ∈ A ω , (i) [d] ↑ is closed in A ω , (ii) and moreover open if dom(d) is finite. Proof. (i) If d(⊥) = ⊥, then d ⊑ α ⊥ for no α ∈ A ω . Hence [d] ↑ is empty and thus open. Assume that d(⊥) = ⊥ and let α ∈ A ω such that α / ∈ [d] ↑ . Hence d ⊑ α ⊥ . Since α ⊥ (⊥) = ⊥ = d(⊥), there is some n ∈ ω such that d(n) ∈ A and d(n) = α(n). It follows that d ⊑ β ⊥ for all β ∈ A ω such that β↾(n + 1) = α↾(n + 1). Hence A ω \ [d] ↑ is open and [d] ↑ is closed. (ii) Since dom(d) is finite let m = max(dom(d)) ∈ ω. If α ⊥ ∈ [d] ↑ , then for all β such that β↾(m + 1) = α↾(m + 1) we have d ⊑ β ⊥ , hence β ∈ [d] ↑ .
It is well-known (see e.g. [START_REF] Plotkin | LCF Considered as a Programming Language[END_REF]) that A ω is algebraic, and moreover that if s is a finite partial map from ω to A, then s ⊥ is finitary in A ω . Hence, the [d] ↑ with d ∈ A ω and dom(d) finite form a basis A ω . Since all elements of A ⊥ are finitary, the constant step function ⊥ ⇒ a of value a ∈ A is finitary (see e.g. [START_REF] Plotkin | LCF Considered as a Programming Language[END_REF]). These step functions ⊥ ⇒ a with a ∈ A are the only possible non strict elements of A ω .

Representation

Given f : A ω → B ω and f * : A ω → po B ω , we say that f * represents f if f * (α ⊥ ) = f (α) ⊥ for all α ∈ A ω .
The main question of this paper is: given f : A ω → B ω , is there some f * that represents f , and, if f * represents f , how do their respective continuity properties relate. Trying to be a bit more precise, we could say that we are looking for mappings

(-) * : (A ω → B ω ) → ( A ω → po B ω )
such that f * represents f and such that f * is Scott-continuous iff f is continuous. We are looking for schemes (-) * which are as much as possible independent from the continuity of f . We shall however not to try to axiomatize them.

Representation of Continuous Stream Functions

In this section, we review basic material for the representation of f : A ω → B ω by some Scott-continuous f * : A ω → cpo B ω . The main (and expected) points are that the set of streams approximated by a given Scott-open subset of A ω is open, and therefore that f is continuous if it is represented by a Scott-continuous f * .

3.0.1 Scott Topology. Given a cpo (D, ⊑), a subset U ⊆ D is Scott-open if it is upward closed ((d ∈ U ∧ d ⊑ e)
implies e ∈ U ), and if moreover for any directed ∆ ⊆ D such that ∆ ∈ U , there is some d ∈ ∆ such that d ∈ U . This means that if some limit ∆ belongs to U , then an approximant d ∈ ∆ of ∆ already belongs to U . It is well-known (see e.g. [START_REF] Amadio | Domains and Lambda-Calculi[END_REF]) that a map of cpos is continuous for the Scott topology if and only if it is Scott-continuous (i.e. a monotone map of cpos which commutes with directed limits). Moreover, if (D, ⊑) is algebraic, then the collection of the sets ↑d := {e | d ⊑ e} with d finitary is a basis for the Scott topology.

From Scott-Continuity to Continuity

Lemma 3.1 If U ⊆ A ω is Scott-open, then {α ∈ A ω | α ⊥ ∈ U } is open. Proof. Let α ∈ A ω such that α ⊥ ∈ U . Consider the set S α of all p ⊥ such that p ∈ A <ω approximates α. Then S α is directed and has limit α ⊥ . Since U is Scott-open, it follows that there is some finite p ⊆ α such that p ⊥ ∈ U . Now, if β ∈ [p], then p ⊥ ⊑ β ⊥ , hence β ⊥ ∈ U since U is Scott-open. It follows that α ∈ [p] ⊆ {γ ∈ A ω | γ ⊥ ∈ U }. Lemma 3.1 implies the expected fact that if f is represented by a Scott-continuous f * , then f is continuous. Lemma 3.2 If f * represents f and f * is Scott-continuous then f is continuous. Proof. Let (m, b) ∈ ω × B. We show that f -1 [{(m, b)}] is open in A ω . Since f * rep- resents f , for all α ∈ A ω we have α ∈ f -1 [{(m, b)}] iff α ⊥ ∈ (f * ) -1 ↑{(m, b)} ⊥ . But (f * ) -1 ↑{(m, b)} ⊥ is
Scott-open thanks to the Scott-continuity of f * , and it follows from Lem. 3.

1 that f -1 [{(m, b)}] is open in A ω .

Traces

It is well-known that a Scott-continuous map g : D → cpo E on algebraic cpos (D, ⊑ D ) and (E, ⊑ E ) is completely determined by its values on finitary elements. More precisely, g : D → po E is Scott-continuous if and only if for all d ∈ D we have:

g(d) = {g(d ′ ) | d ′ is finitary and ⊑ d} .
Hence, in order to define f * : A ω → cpo B ω from a continuous f : A ω → B ω , it suffices to specify f * on the finitary elements of A ω . A possibility to analyse this is to look at how f * is generated from a "trace" 3 . We say that τ

⊆ A ω × (ω × B) is a trace of f * : A ω → po B ω if for all d ∈ A ω , f * (d) = {{(m, b)} ⊥ | ∃e, e ⊑ d and (e, (m, b)) ∈ τ } . (3)
We say that τ is finitary if it contains only finitary e ∈ A ω . This gives a necessary and sufficient condition for f * to be Scott-continuous: Proof. The "if" direction is trivial, and the "only if" direction follows from the algebraicity of A ω . Given f : A ω → B ω , the two equivalent definitions of continuity ( 1) and (2) of Sect. 2.3 lead to two possible finitary traces to define an f * :

Proposition 3.3 f * : A ω → po B ω is Scott-continuous if
τ f := {(s ⊥ , (m, b)) | s : ω ⇀ A finite and [s] ⊆ f -1 [{(m, b)}]} τf := {(p ⊥ , (m, b)) | p ∈ A <ω and [p] ⊆ f -1 [{(m, b)}]} (4)
In order to ensure that τ f and τf can indeed be traces of some f * :

A ω → B ω ,
{(m, b) ∈ ω × B | [d] ↑ ⊆ f -1 [{(m, b)}]}
defines a partial map from ω to B.

Proof. If [d] ↑ ⊆ f -1 [{(m, b)}] and [d] ↑ ⊆ f -1 [{(m, b ′ )}], then for all α ∈ [d] ↑ , we have (m, b), (m, b ′ ) ∈ f (α), hence b = b ′ .
The two traces τ f and τf are finitary and hence they both generate a Scott-continuous f * . According to Lem. 3.2, such an f * can not represent a non continuous f . However, f * always under-approximates f .

Lemma 3.6 Let f : A ω → B ω and let f * : A ω → cpo B ω have trace τ f or τf . Then for all α ∈ A ω , we have f * (α ⊥ ) ⊑ B ω f (α) ⊥ .
Actually, we can say more: f * represents f whenever f is continuous.

Proposition 3.7 Let f : A ω → B ω and let f * : A ω → cpo B ω have trace τ f or τf . Then f * represents f if and only if f is continuous.
Proof. Lemma 3.2 implies that f is continuous whenever it is represented by f * . We show the converse for τf . Assume that f : A ω → B ω is continuous and let α ∈ A ω . We only have to show that f (α

) ⊥ ⊑ B ω f * (α ⊥ ). We have f (α) ⊥ (⊥) = ⊥ ⊑ B ⊥ f * (α ⊥ )(⊥) by definition. Let (m, b) ∈ f (α) ⊥ . By continuity of f , there is some p ∈ A <ω such that α ∈ [p] (i.e. p ⊥ ⊑ α ⊥ ) and [p] ⊆ f -1 [{(m, b)}], hence (m, b) ∈ f * (α ⊥ ).

Representation of Arbitrary Stream Functions

The previous section suggests that systematically building f * from a finitary trace may not be the right approach to define f * from f such that f * always represents f and f * is Scott-continuous if and only if f is continuous.

We try to relax the finitary condition on traces, because it fixes the Scott-continuity of f * inside its definition. In this section, given f :

A ω → B ω , we define f * : A ω → po B ω by: f * (d) := {(m, b) ∈ ω × B | [d] ↑ ⊆ f -1 [{(m, b)}]} ⊥ (5)
That f * is indeed a function follows from Prop. 3.5. Its monotony is obvious. The set

{(d, (m, b)) | [d] ↑ ⊆ f -1 [{(m, b)}]}
is a trace for f * . This trace is sufficient in the sense that for all (m, b) ∈ ω × B and all

finitary d ∈ A ω , if [d] ↑ ⊆ f -1 [{(m, b)}] then (m, b) ∈ f * (d).
The scheme (5) satisfies our first requirement on f * .

Lemma 4.1 Given any f : A ω → B ω , the f * defined from f as in ( 5) is monotone and represents f .

Proof. The monotonicity follows from the fact that d

⊑ d ′ implies [d ′ ] ↑ ⊆ [d] ↑ . Let α ∈ A ω . We have [α ⊥ ] ↑ = {α}, and therefore (m, b) ∈ f (α) implies (m, b) ∈ f * (α ⊥ ). It follows that f (α) ⊥ ⊑ f * (α ⊥ ). Conversely, if (m, b) ∈ f * (α ⊥ ), then we have [α ⊥ ] ↑ ⊆ f -1 [{(m, b)}], hence (m, b) ∈ f (α). It follows that f * (α ⊥ ) ⊑ f (α) ⊥ .
However, we show in Sect. 4.1 that the continuity of f does not imply the Scottcontinuity of f * . This does not happen when A ω is (topologically) compact: as shown in Sect. 4.2, if A ω is compact then the continuity of f implies the Scott-continuity of f * . We moreover show that in this case, f * is Scott-continuous whenever it has a sufficient trace and represents a continuous f .

Continuity Does Not Entail Scott-Continuity

We now show that ( 5) can induce a non Scott-continuous f * : A ω → po B ω from a continuous f : A ω → B ω . The surprising point is that this comes from a failure to the converse of Lem. 3.1, namely that when A is infinite, an open U ⊆ A ω can be such that the set of its Scott-approximants

{d ∈ A ω | [d] ↑ ⊆ U } is not Scott-open.
It will be shown in Sect. 4.2, this is not possible when A is finite. We work here with the Baire space N := ω ω .

Lemma 4.2 There is an open

U ⊆ N such that {d ∈ A ω | [d] ↑ ⊆ U } is not Scott-open.
d i (a) := 0 if a ∈ {1, . . . , i + 1}, ⊥ otherwise. The set {d ∈ A ω | [d] ↑ ⊆ U } ⊆ N is not Scott-open since (i) [ {d i | i ∈ ω}] ↑ ⊆ U , (ii) for all i, [d i ] ↑ is not contained in U .

Proofs of the claims (i) and (ii).

(i) Let α ∈ [ {d i | i ∈ ω}] ↑ . For all i ∈ ω we have d i ⊑ α, hence α(i + 1) = 0. It follows that α(α(0) + 1) = 0, so that α ∈ U .
(ii) Let i ∈ ω and define α i as

α i =    0 → i + 1 k → 0 (1 ≤ k ≤ i + 1) k → 1 (k ≥ i + 2)
We have

α i ∈ [d i ] ↑ since α(k) = 0 for all 1 ≤ k ≤ i + 1. But α i / ∈ U since α i (α i (0) + 1) = α i (i + 2) = 1.
Using Lem. 4.2, we can show that (5) gives a non Scott-continuous representation of a suitable continuous f . It suffices for f to test whether its argument belongs to the open set U of Lem. 4.2.

Lemma 4.3 There is a continuous f : N → N such that f * : N → po N defined from ( 5) is not Scott-continuous.

Proof. Consider the open set U of Lem. 4.2 and define f : N → N as [START_REF] Escardó | Synthetic topology: of data types and classical spaces[END_REF]. We claim that:

f (α) = 1 ω if α ∈ U 0 ω otherwise Define f * from f as in
(i) f is continuous, (ii) f * is not Scott-continuous: f * ( {d i | i ∈ ω}) ⊑ {f * (d i ) | i ∈ ω}, where (d i ) i∈ω is defined in the proof of Lem. 4.2.
Proofs of the claims.

(i) We only have to show that N \ U is open. But α / ∈ U iff α(α(0) + 1) = 0 iff α ∈ [{(0, i), (i + 1, k)}] for some i ∈ ω and k ≥ 1. (ii) Since [ {d i | i ∈ ω}] ↑ ⊆ U , for all α ∈ [ i∈ω d i ] ↑ we have f (α) = 1 ω , hence f * ( i∈ω d i ) = (1 ω ) ⊥ = {(n, 1) | n ∈ ω} ⊥ . However, by Claim (ii) of the proof of Lem. 4.2, for all i ∈ ω there is some α in [d i ] ↑ such that f (α) = 0 ω . It follows that for all n ∈ ω, we have (n, 1) / ∈ f (α) ⊥ ⊒ f * (d i ), hence (n, 1) / ∈ i∈ω f * (d i ). Remark 4.4
The point is the definition of f * . In the case of Lem. 4.3, since f is definable in Gödel's system T, it is representable by a (strongly) stable function.

We see no other way in this situation than to use some (to our opinion) more contrived definition of f * , such as: Lemma 4.5 implies that f * is Scott-continuous whenever it has a sufficient trace and represents a continuous f : A ω → B ω with A finite. Recall that if f * is defined from f as in [START_REF] Escardó | Synthetic topology: of data types and classical spaces[END_REF], then f * represents f and has a sufficient trace.

f * (α ⊥ ) := f (α) ⊥ , f * (⊥ ⇒ a) := f (a ω ) ⊥ , f * (d) := {(m, b) | ∃p ∈ A <ω , p ⊥ ⊑ d and [p] ⊆ f -1 [{(m, b)}]} ⊥ otherwise.
Lemma 4.7 Let A be finite set and let f : A ω → B ω be represented by f * : A ω → po B ω . Assume that f * has a sufficient trace:

• for all (m, b) ∈ ω × B and all finitary d ∈ A ω , if [d] ↑ ⊆ f -1 [{(m, b)}] then (m, b) ∈ f * (d).
If f is continuous then f * is Scott-continuous.

Note that if f * represents f then f * (α ⊥ ) is strict by strictness of f (α) ⊥ . Recall that [d] ↑ is empty if and only if d = ⊥ ⇒ a for some a ∈ A, and in this case d is finitary.

Proof. Let ∆ be a directed subset of A ω . Since f * is monotone, it suffices to check that f * ( ∆) ⊑ A ω f * (∆). This is trivial if ∆ is finitary and in particular if [ ∆] ↑ is empty.

We have to show that f * ( ∆)(e) ⊑

An Account in Hypercoherences

We give an account of our preceding results in Ehrhard's Hypercoherences [START_REF] Ehrhard | Hypercoherences: A strongly stable model of linear logic[END_REF]. Our motivation is to check that a trace similar to the "sequential" trace τf of (4) is indeed "sequential". We are thus looking at Strongly Stable maps of Hypercoherences. Maps of Hypercoherences are maps of the underlying qualitative domains [START_REF] Girard | The System F of Variable Types, Fifteen Years Later[END_REF]. At higher type, these maps work on representation of elements by some coding (traces) and not on the "extensional" elements themselves. We will thus represent f by a map f of the corresponding qualitative domains.

Basic Definitions.

We gather here some basic definitions on Hypercoherences. See e.g. [START_REF] Ehrhard | Hypercoherences: A strongly stable model of linear logic[END_REF][START_REF] Ehrhard | Projecting sequential algorithms on strongly stable functions[END_REF] for details. We need some notations. Given two sets A and B, we say that A is a multisection of B (written

A ✁ B) if ∀a ∈ A, ∃b ∈ B, a ∈ b and ∀b ∈ B, ∃a ∈ A, a ∈ b .
Moreover, given S ⊆ X × Y , we let S 1 and S 2 , the two projections of S, be:

S 1 := {x ∈ X | ∃y ∈ Y, (x, y) ∈ S} and S 2 := {y ∈ Y | ∃x ∈ X, (x, y) ∈ S}
An Hypercoherence is a set X together with a collection Γ(X) of non-empty finite subsets of X such that {x} ∈ Γ(X) for all x ∈ X. The set X is called the web of the Hypercoherence (X, Γ(X)).

Let (X, Γ(X)) be an Hypercoherence. The set of states qD(X) of its associated qualitative domain is be the set of all u ⊆ X such that all non-empty finite subset of u belong to Γ(X). The corresponding coherence C(X) is the set of all non-empty finite subset S of qD(X) such that all multisections of S belong to Γ(X). Note that (X, qD(X)) is a cpo whose finitary elements are exactly the finite u ∈ qD(X). Write qD fin (X) for the set of finite u ∈ qD(X).

Given Hypercoherences X and Y , a Strongly Stable function g : X → FS Y is a Scottcontinuous function from (qD(X), ⊆) to (qD(Y ), ⊆) such that for all S ∈ C(X), we have g(S) ∈ C(Y ) and g(S) = g( S). The Hypercoherence associated to X → FS Y has web qD fin (X) × Y and Γ(X → FS Y ) is the set of all non-empty and finite subsets u of qD fin (X) × Y such that if u 1 ∈ C(X), then u 2 ∈ Γ(Y ) and if moreover u 2 is a singleton, then u 1 is a Singleton.

To each g : X → FS Y , we can associate its trace tr(g) ⊆ qD fin (X) × Y : tr(g) := {(u, y) | y ∈ g(u) and u is minimal} , and g can be recovered from its trace as

g(u) = {y | ∃u ′ ⊆ u, (u ′ , y) ∈ tr(g)} .
By Proposition 19 of [START_REF] Ehrhard | Hypercoherences: A strongly stable model of linear logic[END_REF], qD(X → FS Y ) is exactly the set of traces of strongly stable maps from X to Y .

Representation.

Given a set A, its discrete Hypercoherence Γ(A) is the set of singletons {a} with a ∈ A.

Proposition 5.1 If X is a discrete Hypercoherence, then (i) qD(X) = {{x} | x ∈ X} ∪ {∅}, (ii) C(X) = {{{x}} | x ∈ X} ∪ {S ⊆ * fin qD(X) | ∅ ∈ S}.
• We now show that if S ∈ C(ω → FS A), then f (S) = f ( S).

The inclusion (⊇) follows from the monotonicity of f . For the other direction, let S = {d A similar study could have been carried out in domains for finite and infinite lists. There are different possibilities, depending on the strictness conditions imposed on the data type. Typical Haskell lists are fully lazy, and their domain (which contains streams by completeness) contains also approximations with "holes" such as, say, [⊥, 1]. Hence most of the material of Sect. 3 and Sect. 4, and in particular the negative results of Sect. 4.1 should apply to this framework. Another possibility is to use head strict lazy lists, as in e.g. [START_REF] Pitts | A Co-induction Principle for Recursively Defined Domains[END_REF]. In this case, the only possible Scott-approximants are finite lists of non-bottom elements. The negative results of Sect. 4.1 should not apply to this case, but the positive results of Sect. 4.2 should also not apply. Note these both kinds of finite/infinite lists are available in the (strict, call-by-value) language OCaml [START_REF] Leroy | The Objective Caml System Release 3[END_REF] thanks to the Lazy module, as well as in the (lazy) language Haskell [START_REF] Marlow | Haskell 2010[END_REF] thanks to strictness '!' type annotation.

Conclusion.

We have studied the representation of stream functions in Scott domains for the corresponding PCF types. As expected, these domains are well suited for the representation of continuous functions. This is moreover adapted to the framework of Ehrhard's Hypercoherences. However, our results seem to indicate that it is difficult to represent a stream function by a monotone map on the correspond domain, and to require that the representant is Scott-continuous if and only if the represented function is continuous. This kind of modularity fails in the general case for reasons that are not clear to us. Fortunately, things work well in the compact case, which corresponds to one of our motivations.

It is nevertheless unclear how to use this kind of domains to represent backtracking mechanisms used to approximate non-continuous functions (see e.g. [START_REF] Semmes | A Game for the Borel Functions[END_REF]). Further work will concern more concrete and flexible framework such as Hyland-Ong games [START_REF] Hyland | On Full Abstraction for PCF: I, II, and III[END_REF], or game presentations of sequential data structures such as [START_REF] Melliès | Sequential algorithms and strongly stable functions[END_REF].

Remark 3 . 4

 34 Note that (3) is possible for a given d ∈ A ω only when the set {{(m, b)} ⊥ | ∃e, e ⊑ d and (e, (m, b)) ∈ τ } is bounded ( A ω is bounded complete [1, 16]). In this case, (3) is equivalent to f * (d) = {(m, b) | ∃e, e ⊑ d and (e, (m, b)) ∈ τ } ⊥ .

Proposition 3 . 5

 35 we can check that with τ = τ f and τ = τf , the set {(m, b) | ∃e, e ⊑ d and (e, (m, b)) ∈ τ } defines a partial function from ω to B. This follows from a more general result (recall that [s] = [s ⊥ ] ↑ and that d ⊑ d ′ implies [d ′ ] ↑ ⊆ [d] ↑ ): Given f : A ω → B ω and d ∈ A ω , the set

Proof.

  Consider the open set U ⊆ N made of the α ∈ N such that α(α(0) + 1) = 0 . Note that U is the union of the basic open sets [{(0, i), (i + 1, 0)}] for i ∈ ω. Consider now the directed family (d i ) i∈ω ∈ N with

10 4. 2 . 3

 1023 Representation.

  A ⊥ f * (∆)(e) for all e ∈ ω ⊥ . Consider first the case of e = ⊥. If f * ( ∆)(⊥) = ⊥ then we are done. Otherwise,f * ( ∆)(⊥) = b ∈ B. Since [ ∆] ↑ is assumed to be non-empty, let α ∈ [ ∆] ↑ . By monotonicity of f * , we have f * (α ⊥ )(⊥) = b, which contradicts the strictness of f * (α ⊥ ). Consider now the case of e = m ∈ ω. If f * ( ∆)(m) = ⊥ then we are done. So let b ∈ B such that (m, b) ∈ f * ( ∆). We show that there is some d ∈ ∆ such that (m, b) ∈ f * (d). Since [ ∆] ↑ is assumed to be non-empty, let α ∈ [ ∆] ↑ . By monotonicity of f * , we have (m, b) ∈ f * (α ⊥ ) hence (m, b) ∈ f (α) since f * represents f . It follows that [ ∆] ↑ ⊆ f -1 [{(m, b)}]. But f -1 [{(m, b)}] ⊆ A ω isopen by continuity of f . Since A is finite, by Lem. 4.5 there is d ∈ ∆ such that [d] ↑ ⊆ f -1 [{(m, b)}]. If d is finitary, then we are done by assumption on f * . Otherwise, by algebraicity of A ω and since [d] ↑ ⊆ f -1 [{(m, b)}], by Lem. 4.5 again there is a finitary d ′ ⊑ d such that [d ′ ] ↑ ⊆ f -1 [{(m, b)}], and we are done by assumption on f * .

  1 , . . . , d n } ∈ C(ω → FS A) and ({m}, b) ∈ f (S). Hence, for all 1 ≤ i ≤ n there is a minimal p i ∈ A <ω such that (p i ) tr ⊆ d i and (m, b) ∈ f [p i ]. But {(p 1 ) tr , . . . , (p n ) tr } ⊑ {d 1 , . . . , d n }. Reasoning similarly as above, we get that p 1 = • • • = p n (=: p), hence p tr ⊆ S and ({m}, b) ∈ f ( S). 6 Concluding Remarks 6.0.6 Other Possible Domains for Streams.

  and write [d] ↑ for the set of streams which are Scott-approximated by d. Note that this set is never empty if d is strict (d

They correspond exactly to cliques of the coherence space[START_REF] Girard | Linear Logic[END_REF] ω ⊸ A where ω and A are discrete.

In contrast with e.g.[START_REF] Amadio | Domains and Lambda-Calculi[END_REF], we do not call them "compact" in order to avoid confusion with the topological notion of compactness, to be used in Sect 4.2.

By lack of a better name, we depart from the usual terminology (see e.g.[START_REF] Amadio | Domains and Lambda-Calculi[END_REF]) since we do not require any minimality in the trace. This will be regained with Hypercoherences in Sect. 5.

The Compact Case

In this section we show that the problem raised by Lem. 4.2 does not appear when A ω is a compact topological space, which exactly means that A is finite. We thus avoid the counter-example of Lem. 4.3. This implies that f * is Scott-continuous whenever it has a sufficient trace and represents a continuous f .

Topological Compactness.

A subset set C of a topological space (X, Ω(X)) is compact if for any family (A i ) i∈I of open sets such that C ⊆ i∈I A i , there is a finite I 0 ⊆ I such that C ⊆ i∈I 0 A i . We say that (X, Ω(X)) is compact when X is compact in (X, Ω(X)). It is well-known (see e.g. [START_REF] Kechris | Classical Descriptive Set Theory[END_REF]) that a closed subset of a compact set is compact and also that A ω is compact if and only if A is finite.

4.2.2

The Set of Scott-Approximants of an Open is Scott-Open.

We now show that the topological compactness of

The upward closure is trivial, and as suggested by Lem. 4.2, the point is the "finite" observation of limits.

Proof. The set [ ∆] ↑ is closed by Lem. 2.1, and hence compact since A ω is compact. So, we may assume that there are s 1 , . . . , s n finite partial from

We will show that

We proceed by contradiction, by showing that from any α ∈

), contradicting the assumption on the s i 's.

First, note that if (m, a) ∈ S \ ∆, then no (m, b) with b = a belongs to ∆, since (m, a) belongs to some

Proof. (i) First, we have ∅ ∈ qD(X) since the empty set has no non-empty subset. Furthermore, if x ∈ X, then the only non-empty subset of {x} is {x}, and {x} ∈ Γ(X) since X is discrete.

Conversely, assume that s ∈ qD(X) with distinct x, y ∈ s. Then {x, y} is a finite non-empty subset of s which is not in Γ(X).

(ii) If x ∈ X then {{x}} ⊆ * fin qD(X). Moreover, u ✁ {{x}} implies u = {x}, so that u ∈ Γ(X). On the other hand, if S ⊆ * fin qD(X) contains the empty set, then S has no multisection and we are done.

Conversely, if S ∈ C(X) does not contain the empty set, then S is of the form {{x 1 }, . . . , {x n }}. Since {x 1 , . . . , x n } is a multisection of S, we must have {x 1 , . . . , x n } ∈ Γ(X), but this is possible only when n = 1. Proposition 5.1.(i) tells us that given a set X equipped with the discrete Hypercoherence, we can identify (qD(X), ⊆) with the discrete cpo X ⊥ .

The Hypercoherence associated to A ω is the Hypercoherence of ω → FS A, where ω, A are discrete and the function space is the strongly stable one.

It is possible to show that ω → FS A and A ω are isomorphic w.r.t. the pointwise order (which is different from the stable order, corresponding to (qD(ω → FS A), ⊆)). We do not need this generality since it is easy to directly represent any s : ω ⇀ A by its trace: let

Note that this encompasses the cases of p ∈ A <ω and α ∈ A ω .

Proposition 5.2 If s : ω ⇀ A, then s tr ∈ qD(ω → FS A).

Proof. Let S ⊆ (s tr ) fin be non-empty and such that S 1 ∈ C(ω). Since ∅ / ∈ S 1 , we have S 1 = {{n}}, hence S 2 = {a} ∈ Γ(A). Moreover, both S 1 and S 2 are singletons.

We have for f similar properties as for the f * 's of Sect. 3.

Lemma 5.3 f is Scott-continuous and moreover represents f if and only if f is continuous.

Proof. Monotonicity follows from the shape of the definition. Scott-continuity follows from the fact that p tr ∈ qD(ω → FS A) is finite. That f represents f if and only if f is continuous directly follows from the definition of f .

We now show that f is strongly stable. Thanks to Ehrhard's collapse theorem [START_REF] Ehrhard | Projecting sequential algorithms on strongly stable functions[END_REF], this means that f can be "extensionally" represented by a sequential algorithm in the sense of [START_REF] Berry | Sequential Algorithms on Concrete Data Structures[END_REF]. Lemma 5.4 f is strongly stable.

Given sets A and B, we write

It is shown in [START_REF] Ehrhard | Hypercoherences: A strongly stable model of linear logic[END_REF] that if S ∈ C(A) for some Hypercoherence A, and S ′ is a non-empty finite subset of qD(A) such that S ′ ⊑ S, then S ′ ∈ C(A).

Proof. We show that f preserves coherences S ∈ C(ω → FS A) and their intersections.

Let S ∈ C(ω → FS A). Then S is a finite non-empty subset of qD(ω → FS A). Hence S is of the form {d 1 , . . . , d n }. Let

Assume first that ∅ ∈ M 1 . Hence we have x j = ∅ for some j, and it follows that (∅, b j ) ∈ f (d i ) for some i. But this is impossible by definition of f .

It thus follows from Prop. 5.1.(ii) that M 1 = {{k}} for some k ∈ ω, hence that M is of the form {({k}, b 1 ), . . . , ({k}, b m )}.

We show that b

By assumption, for all 1 ≤ j ≤ m, there is some 1

-Assume that we do not have p 1 = • • • = p m . Hence, there is a least l such that there are 1 ≤ j 0 , j 1 ≤ m and a ∈ A such that (l, a) ∈ p j 0 \ p j 1 .

Assume that l ∈ dom(p j ) for all j. Hence {({l}, p 1 (l)), . . . , ({l}, p m (l))} is a finite multisection of {d 1 , . . . , d n }, so that {({l}, p 1 (l)), . . . , ({l}, p m (l))} belongs to Γ(ω → FS A). It follows that p 1 (l) = • • • = p m (l), but this contradicts the assumption that p j 0 (l) = p j 1 (l) for some j 0 , j 1 .

It therefore must be the case that l ∈ dom(p j 0 ) \ dom(p j 1 ) for some j 0 , j 1 .

But by assumption on l, for all l ′ < l we have l ′ ∈ dom(p 1 ) ∩ • • • ∩ dom(p m ) and p 1 (l ′ ) = • • • = p m (l ′ ). Hence p j 1 is a prefix of all the p j 's, and therefore (p j 1 ) tr is contained in all the d i 's. By monotonicity of f (Lem. 5.3), we get ({k}, b j 1 ) ∈ f (d i ) for all 1 ≤ i ≤ n. This implies b j = b j 1 for all 1 ≤ j ≤ m. But then the minimality of the p j 's would imply that p j 0 = p j 1 , contradicting l ∈ dom(p j 0 )\dom(p j 1 ) (note that in this case, we already have b 1 = • • • = b m , which was our primarily goal).

We therefore have