Gilles Dowek
email: gilles.dowek@inria.fr

Third Order Matching is Decidable

de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

The higher order matching problem is the problem of determining whether a term is an instance of another in the simply typed λ-calculus i.e. to solve the equation a = b where a and b are simply typed λ-terms and b is ground.

Pattern matching algorithms are used to check if a proposition can be deduced from another by elimination of universal quantifiers or by introduction of existential quantifiers. In automated theorem proving, elimination of universal quantifiers and introduction of existential quantifiers are mixed and full unification is required, but in proof-checking and semi-automated theorem proving, these rules can be applied separately and thus pattern matching can be used instead of unification.

Higher order matching is conjectured decidable in [START_REF] Huet | Résolution d' Équations dans les Langages d[END_REF] and the problem is still open. In [START_REF] Huet | A Unification Algorithm for Typed λ-calculus[END_REF] [6] [START_REF] Huet | Proving and Applying Program Transformations Expressed with Second Order Patterns[END_REF] Huet has given a semi-decision algorithm and shown that in the particular case in which the variables occurring in the term a are at most second order this algorithm terminates, and thus that second order matching is decidable. In [START_REF] Statman | Completeness, Invariance and λ-definability[END_REF] Statman has reduced the conjecture to the λ-definability conjecture and in [START_REF] Wolfram | The Clausal Theory of Types[END_REF] Wolfram has given an always terminating algorithm whose completeness is conjectured.

We prove in this paper that third order matching is decidable i.e. we give an algorithm that decides if a matching problem, in which all the variables are at most third order, has a solution. The main idea is that if the problem a = b has a solution then it also has a solution whose depth is bounded by some integer s depending only on the problem a = b, so a simple enumeration of the substitutions whose depth is bounded by s gives a decision algorithm. This result can also be used to bound the depth of the search tree in Huet's semi-decision algorithm and thus turn it into a always-terminating decision algorithm. It can also be used to design an algorithm which enumerates a complete set of solutions to a third order matching problem and either terminates if the problem has a finite complete set of solutions or keeps enumerating solutions forever if it the problem admits no such set. At last we discuss the problems that occur when we try to generalize the proof given here to higher order matching.

1 Trees and Terms

Trees

Definitions 1 (Following [START_REF] Gorn | Explicit Definitions and Linguistic Dominoes[END_REF]) An occurrence is a list of strictly positive integers α =< s 1 , ..., s n >. The number n is called the length of the occurrence α. A tree domain D is a non empty finite set of occurrences such that if α < n >∈ D then α ∈ D and if also n ̸ = 1 then α < n -1 >∈ D. A tree is a function from a tree domain D to a set L, called the set of labels of the tree.

If T is a tree and D its domain, the occurrence < > is called the root of T and the occurrence α < n > is called the n th son of the occurrence α. The number of sons of an occurrence α is the greatest integer n such that α < n >∈ D. A leaf is an occurrence that has no sons.

Let T be a tree and let α =< s 1 , ..., s n > be an occurrence in this tree, the path of α is the set of occurrences {< s 1 , ..., s p > | p ≤ n}. The number of elements of this path is the length of α plus one.

The depth of the tree T is the length of the longest occurrence in D. This occurrence is, of course, a leaf.

If T is a tree of domain D and α is an occurrence of D, the subtree T /α is the tree T ′ whose domain is D ′ = {β | αβ ∈ D} and such that

T ′ (β) = T (αβ)
By an abuse of language, if α < n > is an occurrence of a tree T , the subtree T /α < n > is also called the n th son of the occurrence α.

If a is a label and T 1 , ..., T n are trees (of domains D 1 , ..., D n ) then the tree of root a and sons T 1 , ..., T n is the tree

T of domain D = {< >} ∪ i {< i > α | α ∈ D i } such that T (< >) = a and T (< i > α) = T i (α)
If T is a tree of domain D, α an occurrence of D and T ′ a tree of domain D ′ then the graft of

T ′ in T at the occurrence α (T [α ← T ′ ]) is the tree T ′′ of domain D ′′ = D-{αβ | αβ ∈ D} ∪ {αβ | β ∈ D ′ } and such that T ′′ (γ) = T ′ (β) if γ = αβ and T ′′ (γ) = T (γ) otherwise
Let T and T ′ be trees and let a be a label such that all the occurrences of a in T are leaves α 1 , ..., α n then the substitution of

T ′ for a in T (T [a ← T ′ ]) is defined as T [α 1 ← T ′ ]...[α n ← T ′ ].
Note that since α 1 , ..., α n are leaves, the order in which the grafts are performed is insignificant.

Types

Definition 2 (Type)

Let us consider a finite set T . The elements of T are called atomic types. A type is a tree whose labels are either the elements of T or → and such that the occurrences labeled with an element of T are leaves and the ones labeled with → have two sons.

Let T be a type, if the root of T is labeled with an atomic type U then T is written U , if the root of T is labeled with → and its sons are written T 1 and T 2 then T is written (T 1 → T 2 ). By convention

T 1 → T 2 → T 3 is an abbreviation for (T 1 → (T 2 → T 3 )).

Definition 3 (Order of a Type)

If T is a type, the order of T is defined by

• o(T ) = 1 if T is atomic, • o(T 1 → T 2 ) = max{1 + o(T 1 ), o(T 2 )}.

Typed λ-terms

Definitions 4 For each type T we consider three sets C T , I T , L T . The elements of C T are called constants of type T , those of I T instantiable variables of type T and those of L T local variables of type T .

We assume that we have in each atomic type at least a constant and that there is a finite number of constants i.e. that the set T C T is finite1 . We assume also that we have an infinite number of instantiable and local variables of each type.

A typed λ-term is a tree whose labels are either App, or < Lam, x > where x is a local variable, or < V ar, x > where x is a constant, an instantiable variable or a local variable such that the occurrences labeled with App have two sons, the occurrences labeled with < Lam, x > have one son and the occurrences labeled with < V ar, x > are leaves.

Let t be a term, if the root of t is labeled with < V ar, x > we write it x, if the root of t is labeled with < Lam, x > and its son is written u then we write it λx : T.u where T is the type of x, if the root of t is labeled with App and its sons are written u and v then we write it (u v). By convention (u v w) is an abbreviation for ((u v) w).

In a term t, an occurrence α labeled with < V ar, x > is bound if there exists an occurrence β in the path of α labeled with < Lam, x >, it is free otherwise.

A term is ground if no occurrence is labeled with a pair < V ar, x > with x instantiable. Let t and t ′ be terms and x be a variable, the substitution of

t ′ for x in t (t[x ← t ′ ]) is defined as t[< V ar, x >← t ′ ].

Definition 5 (Type of a Term)

A term t is said to have the type T if either: • t is a constant, an instantiable variable or a local variable of type T .

• t = (u v) and u has type U → T and v type U for some type U , • t = λx : U.u, the term u has type V and T = U → V .

A term t is said to be well-typed if there exists a type T such that t has type T . In this case T is unique and is called the type of t.

Definition 6 (βη-reduction)

The βη-reduction relation, written £, is defined as the smallest transitive relation compatible with term structure such that (λx :

T.t u) £ t[x ← u] λx : T.(t x) £ t if x is not free in t
We adopt the usual convention of considering terms up to α-conversion (i.e. bound variable renaming) and we consider that bound variables are renamed to avoid capture during substitutions. A rigorous presentation would use, for instance, de Bruijn indices [START_REF] De Bruijn | Lambda Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem[END_REF].

Obviously, if t is a term of type T , x is a variable of type U and u a term of type U then the term t[x ← u] has type T . In the same way if a term t has type T and t reduces to u then u has type T .

Proposition 1 The βη-reduction relation is strongly normalizable and confluent on typed terms, and thus each term has a unique normal form. Proof See, for instance, [START_REF] Hindley | Introduction to Combinators and λ-Calculus[END_REF].

Proposition 2 Let t be a normal well-typed term of type U 1 → ... → U n → U (U atomic), the term t has the form t = λy 1 :

U 1 . ... λy m : U m .(x u 1 ... u p )
where m ≤ n and x is a constant, an instantiable variable or a local variable.

Proof The term t can be written in a unique way t = λy 1 : V 1 . ... λy m : V m .u where u is not an abstraction. The term u can be written in a unique way u = (v u 1 ... u p ) where v is not an application. The term v is not an application by definition, it is not an abstraction (if p = 0 because u is not an abstraction and if p ̸ = 0 because t is normal), it is therefore a constant, an instantiable variable or a local variable. Then since t has type U 1 → ... → U n → U , we have m ≤ n and for all i, V i = U i .

Definition 7 (Head of a Term, Atomic Term) Let t = λy 1 : T 1 . ... λy m : T m .(x u 1 ... u p ) be a normal term. The symbol x is called the head of the term. If m = 0 then t is said to be atomic, it is an abstraction otherwise.

Definition 8 (η-long Form) If t = λy 1 : U 1 . ... λy m : U m .(x u 1 ... u p ) is a term of type T = U 1 → ... → U n → U (U atomic) (m ≤ n)
which is in βη-normal form then we define its β-normal η-long form as the term

t ′ = λy 1 : U 1 . ... λy m : U m .λy m+1 : U m+1 . ... λy n : U n .(x u ′ 1 ... u ′ p y ′ m+1 ... y ′ n )
where u ′ i is the β-normal η-long form of u i and y ′ i is the β-normal η-long form of y i . This definition is by induction on the pair < c 1 , c 2 > where c 1 is the number of occurrences in t and c 2 the number of occurrences in T

In the following all the terms are assumed to be in β-normal η-long form.

Böhm Trees

Definition 9 (Böhm Tree) A (finite) Böhm tree is a tree whose occurrences are labeled with pairs < l, x > such that l is a list of local variables < y 1 , ..., y n > and x is a constant, an instantiable variable or a local variable.

Definition 10 (Type of a Böhm Tree)

Let t be a Böhm tree whose root is labeled with the pair << y 1 , ..., y n >, x > and whose sons are u 1 , ..., u p . The Böhm tree t is said to have the type T if the Böhm trees u 1 , ..., u p have type U 1 , ..., U p the symbol x has type U 1 → ... → U p → U (U atomic) and T = T 1 → ... → T n → U where T 1 , ..., T n are the types of the variables y 1 , ..., y n .

A Böhm tree t is said to be well-typed if there exists a type T such that t has type T . In this case T is unique and is called the type of t.

Definition 11 (Böhm Tree of a Normal Term) Let t = λy 1 : T 1 . ... λy n : T n .(x u 1 ... u p ) be a λ-term in normal (η-long) form. The Böhm tree of t is inductively defined as the tree whose root is the pair < l, x > where l =< y 1 , ..., y n > is the list of the variables bound at the top of this term, x is the head symbol of t and sons are the Böhm trees of u 1 , ..., u p .

Remark Normal (η-long) well-typed terms and well-typed Böhm trees are in one-to-one correspondence. Moreover if t is a normal (η-long) term and t is its Böhm tree then occurrences in t labeled with a constant, an instantiable variable or a local variable and occurrences in t are in one-to-one correspondence. So we will use the following abuse of notation: if α is an occurrence in the Böhm tree of t we write (t/α) for the normal (η-long) term corresponding to the Böhm tree ( t/α) and t[α ← u] for the term t[α ′ ← u] where α ′ is the occurrence of a variable or a constant in t corresponding to α. Notation Let t be a term, we write |t| for the depth of the Böhm tree of the normal (η-long) form of t.

Proposition 3 In each type T there is a ground term t such that |t| = 0. Proof Let T = U 1 → ... → U n → U with U atomic and let c be a constant of type U . The term t = λx 1 : U 1 . ... λx n : U n .c has type T and |t| = 0.

Substitution

Definition 12 (Substitution)

A substitution is a finite set of pairs < x i , t i > where x i is an instantiable variable and t i a term of the same type in which no local variable occurs free such that if < x, t > and < x, t ′ > are both in this set then t = t ′ . The variables x i are said to be bound by the substitution.

Definition 13 (Substitution applied to a Term)

If σ is a substitution and t a term then we let

σt = t[α 1 1 ← t 1 ]...[α p 1 1 ← t 1 ]...[α 1 n ← t n ]...[α pn n ← t n ]
where α 1 i , ..., α p i i are the occurrences of x i in t. Note that since the α j i are leaves, the order in which the grafts are performed is insignificant.

Definition 14 (Composition of Substitutions) Let σ and τ be two substitutions the substitution τ • σ is defined by

τ • σ = {< x, τ t > | < x, t >∈ σ} ∪ {< x, t > | < x, t >∈ τ and
x not bound by σ} Proposition 4 Let σ and τ be two substitutions and t is a term, we have

(τ • σ)t = τ (σt)
Proof By decreasing induction on the depth of an occurrence α in t we prove that we have

(τ • σ)(t/α) = τ (σ(t/α)) 2

Definition 16 (Third Order Matching Problem)

A third order matching problem is a matching problem Φ = {a 1 = b 1 , ..., a n = b n } such that the types of the instantiable variables that occur in a 1 , ..., a n are of order at most three.

Definition 17 (Solution)

Let Φ = {a 1 = b 1 , ..., a n = b n } be a matching problem. A substitution σ is a solution of this problem if and only if for every i, the normal form of the terms σa i and b i are identical up to α-conversion.

Remark Usual unification terminology distinguishes variables (here instantiable variables) and constants. The need for local variables comes from the fact that we want to transform the problem λy : T.x = λy : T.y (where x is an instantiable variable of type T ) into the problem x = y by dropping the common abstraction. The symbol y cannot be an instantiable variable (because it cannot be instantiated by a substitution), it cannot be a constant because, if it were, we would have the solution x ← y to the second problem which is not a solution to the first. So we let y be a local variable and the solution x ← y is now forbidden in both problems because no local variable can occur free in the terms substituted for variables in a substitution. In Huet's unification algorithm [START_REF] Huet | A Unification Algorithm for Typed λ-calculus[END_REF] [6] these local variables are always kept in the head of the terms in common abstractions. In Miller's mixed prefixes terminology [START_REF] Miller | Unification Under a Mixed Prefix[END_REF], constants are universal variables declared to the left hand side of the instantiable variables and local variables are universal variables declared to the right hand side of all the instantiable variables.

Remark In an alternative definition of matching problems, the terms b 1 , ..., b n do not need to be ground. The method of this paper can be adapted to such problems using the standard technique of variable freezing [START_REF] Huet | Résolution d' Équations dans les Langages d[END_REF].

Definition 18 (Ground Solution)

Let Φ = {a 1 = b 1 , ..., a n = b n } be a problem and let σ be a solution to Φ. The solution σ is said to be ground if for each instantiable variable that has an occurrence in some a i , the term σx is ground.

Proposition 5 If a matching problem has a solution then it has a ground solution. Proof Let Φ = {a 1 = b 1 , ..., a n = b n } be a matching problem and let σ be a solution to this problem. Let y 1 : T 1 , ..., y n : T n be the instantiable variables occurring in the term σx for some x instantiable variable occurring in some a i . Let u 1 , ..., u n be ground terms of the types T 1 , ..., T n . Let τ = {< y 1 , u 1 >, ..., < y n , u n >}, and σ ′ = τ • σ. Obviously, for each instantiable variable x of a, the term σ ′ x is ground and σ ′ is a solution to Φ.

Definition 19 (Complete Set of Solutions)

Obviously if σ is a solution to a problem Φ then for any substitution τ , τ • σ is also a solution to Φ. A set S of solutions to a problem Φ is said to be complete if for every substitution θ that is a solution to this problem there exists a substitution σ ∈ S and a substitution τ such that θ = τ • σ. So in contrast with second order matching [6] [START_REF] Huet | Proving and Applying Program Transformations Expressed with Second Order Patterns[END_REF] there is no (always terminating) algorithm that enumerates a complete set of solutions to a third order matching problem.

We consider now algorithms that take as an input a matching problem and either give one solution to the problem or fail if it does not have any.

A Bound on the Depth of Solutions

All the problems considered in the rest of the paper are third order.

To prove the decidability of third order matching we are going to prove that the depth of the term t substituted to a variable x by a solution σ to a problem Φ can be bounded by an integer s depending only on the problem Φ. Of course the previous example shows that a matching problem may have solutions of arbitrary depth, but to design a decision algorithm we do not need to prove that all the solutions are bounded by s but only that at least one is. To show this result we take a problem Φ that has a solution σ (by proposition 5, we can consider without loss of generality that this solution is ground) and we build another solution σ ′ whose depth is bounded by an integer s depending only on the problem Φ.

The proof is divided into two parts. In the first part,we focus on a particular case in which the problem Φ is a an interpolation problem i.e. set of equations of the form (x c 1 ... c n ) = b such that x is an instantiable variable and c 1 , ..., c n and b are ground terms. Then, in the second part, we reduce the general case to this particular case.

Consider now an equation (x c 1 ... c n ) = b and a substitution σ solution to this equation. Let us write t = σx = λy 1 : T 1 . ... λy n : T n .u (u atomic). We have

σ(x c 1 ... c n ) = (λy 1 : T 1 . ... λy n : T n .u c 1 ... c n ) This term reduces to u[y 1 ← c 1 , ..., y n ← c n ] whose normal form is b.
The terms c i are at most second order. In the key lemma, we prove that, in the general case, when we substitute a second order term c to a variable y in a term u and we normalize the term u[y ← c], we get a term with a depth larger than or equal to the one of u. If this were true in all the cases, we would know that the depth of t (the solution) has to be less than or equal to the depth of b (the right hand side of the equation). A simple enumeration of the terms t whose depth is less than or equal to |b| would give a decision procedure.

Actually, the key lemma shows that the depth of the normal form of u[y ← c] can be less than the depth of u in two cases : when c is a non relevant term and when |c| = 0. When such cases happen, solutions may have an arbitrary depth. In these cases, we show that if the problem Φ has a solution σ then it has also another solution σ ′ whose depth is bounded by some integer s depending only on the problem Φ.

Interpolation Problems

Definition 20 (Interpolation Problem)

An interpolation problem is a set of equations of the form (x c 1 ... c n ) = b such that x is an instantiable variable and c 1 , ..., c n and b are ground terms. (2) If α is an occurrence in the Böhm tree of u such that no occurrence in the path of α is labeled with y, then α is also an occurrence in the normal form of u[y ← c] and has the same label in the Böhm tree of u and in the Böhm tree of the normal form of u[y ← c].

(3) If α =< s 1 , ..., s n > is an occurrence in the Böhm tree of u such that for each occurrence β =< s 1 , ..., s k > in the path of α, β ̸ = α, labeled with y, the term c is relevant in its r th argument where r is the position of the son of β in the path of α i.e. r = s k+1 , then there exists an occurrence α ′ of the Böhm tree of the normal form of u[y ← c] such that all the labels occurring in the path of α, except y, occur in the path of α ′ and the number of times they occur in the path of α ′ is greater than or equal to the number of times they occur in the path of α. Moreover if the occurrence α is labeled with a symbol different from y, then the occurrence α ′ is labeled with this same symbol.

(4) Moreover if |c| ̸ = 0 then the length of α ′ is greater than or equal to the length of α. Proof By induction on the number of occurrences of y in u. We substitute these occurrences one by one and we normalize the term. Let β be the occurrence in the Böhm tree of u corresponding to the occurrence of y in u we substitute. Let us write c = λz 1 : U 1 . ... λz p : U p .d

The term (u/β) has the form λv 1 : V 1 . ... λv q : V q .(y e 1 ... e p ). When we substitute y by the term c in (y e 1 ... e p ) we get (c e 1 ... e p ) and when we normalize this term we get the term d[z 1 ← e 1 , ..., z p ← e p ] which is normal because the type of the e i are first order.

Let us consider the occurrences in the Böhm tree of u, while substituting the occurrence of y corresponding to β, we have removed all the occurrences β < i > γ where i is an integer (i ≤ p) and γ is an occurrence in the Böhm tree of e i . We have added all the occurrences βδ where δ is an occurrence of the Böhm tree of c labeled with a symbol different from z 1 , ..., z p and all the occurrences βδγ where δ is a leaf occurrence in the Böhm tree of c labeled with a z i and γ is an occurrence of the Böhm tree of e i . (2) When an occurrence β of y is substituted by c all the occurrences removed have the form β < i > γ. So if no occurrence in the path of α is labeled with y, the occurrence α remains in the normal form of u[y ← c].

(3) If the occurrence β is not in the path of α then the occurrence α is still an occurrence in the normal form of u[y ← c], we take α ′ = α.

If β = α then the occurrence β is an occurrence of the Böhm tree of the normal form of u[y ← c]. We take α ′ = β = α.

If β is in the path of α and β ̸ = α, β =< s 1 , ..., s k > then let r be the position of the son of β in the path of α i.e. r = s k+1 . Let γ be such that α = β < r > γ. By hypothesis z r has an occurrence in d, let δ be such an occurrence. The occurrence βδγ is an occurrence in the Böhm tree of the normal form of u[y ← c]. We take α ′ = βδγ.

In all the cases, all the labels occurring in the path of α, except y, occur in the path of α ′ and the number of times they occur in the path of α ′ is greater than or equal to the number of times they occur in the path of α.

If the occurrence α is labeled with a symbol different from y, then the occurrence α ′ is labeled with the same symbol as α. • if one of the terms c i is not relevant in one of its arguments, • if one of the terms c i is such that |c i | = 0. So solutions may have an arbitrary depth. When this happens, we compute another solution to the problem whose depth is bounded by an integer s depending only on the initial problem.

This new substitution is constructed in two steps. In the first step we deal with non relevant terms and in the second with terms of depth 0. Let us consider the Böhm tree of t. The set of the occurrences of the Böhm tree of t accessible with respect to the equation (x c 1 ... c n ) = b is inductively defined as:

• the root of the Böhm tree of t is accessible,

• if α is an accessible occurrence labeled with y i and c i is relevant in its j th argument then the occurrence α < j > (the j th son of α) is accessible,

• if α is an accessible occurrence labeled with a symbol different from all the y i then all the sons of α are accessible.

Definition 23 (Occurrence Accessible with Respect to an Interpolation Problem) An occurrence is accessible with respect to an interpolation problem if it is accessible with respect to one of the equations of this problem.

Definition 24 (Term Accessible with Respect to an Interpolation Problem)

A term is accessible with respect to an interpolation problem if all the occurrences of its Böhm tree which are not leaves are accessible with respect to this problem.

Definition 25 (Accessible Solution Built from a Solution)

Let Φ be an interpolation problem and let σ be a solution to this problem. For each instantiable variable x occurring in the equations of Φ we consider the term t = σx. In the Böhm tree of t, we prune all the occurrences non accessible with respect to the equations of Φ in which x has an occurrence and put Böhm trees of ground terms of depth 0 of the expected type as leaves. The tree obtained that way is the Böhm tree of some term t ′ . We let σx = t ′ . We prove by decreasing induction on the depth of the occurrence α of the Böhm tree of u that if α is accessible with respect to the equation (x c 1 ... c n ) = b then α is also an occurrence of the Böhm tree of u ′ and (u

′ /α)[y 1 ← c 1 , ..., y n ← c n ] = (u/α)[y 1 ← c 1 , ..., y n ← c n ]
and then since the root of u is accessible with respect to this equation we have

u ′ [y 1 ← c 1 , ..., y n ← c n ] = u[y 1 ← c 1 , ..., y n ← c n ] i.e. ((σx) c 1 ... c n ) = b
So σ is a solution to Φ.

Proposition 7 Let Φ be an interpolation problem and let σ be a solution to Φ. Let h be the maximum depth of the right hand side of the equations of Φ. Let σ the accessible solution built from σ. Let t = σx = λy 1 : T 1 . ... λy n : T n .u (u atomic). There are at most h + 1 occurrences of symbols not in {y 1 , ..., y n } on a path of the Böhm tree of t. Proof Let α be an occurrence in the Böhm tree of t such that there are more than h+1 occurrences of symbols not in {y 1 , ..., y n } in the path of α.

Let β be the (h+1)-th occurrence of such a symbol. Since there are more that h+1 occurrences of symbols not in {y 1 , ..., y n } in the path of α, the occurrence β is not a leaf, so it is accessible with respect to some equation (x c 1 ... c n ) = b of Φ. Also, since this occurrence is not a leaf, it is labeled with a symbol f whose type is not first order.

For each occurrence γ =< s 1 , ..., s k > in the path of β labeled with y i , let r be the position of the son of this occurrence in this path (i.e. r = s k+1 ). Since the occurrence β is accessible with respect to the equation (x c 1 ... c n ) = b, the term c i is relevant in its r th argument. So using n times the part (3) of the key lemma there exists an occurrence β ′ in the Böhm tree of the normal form of the term b = (σx c 1 ... c n ) such that the path of β ′ contains at least h + 1 occurrences. Thus, the length of this occurrence is at least h. This occurrence is labeled with the symbol f whose type is not first order, so it has a son β ′′ whose length is at least h + 1.

So the depth of b is greater than or equal to h + 1 which is contradictory.

Definition 26 (Compact Term) A term t = λy 1 : T 1 . ... λy n : T n .u (u atomic) is compact with respect to an interpolation problem Φ if no variable y i has more than h + 1 occurrences in a path of its Böhm tree, where h is the maximum depth of the right hand side of the equations of Φ.

Proposition 8 Let Φ be an interpolation problem and let σ be an accessible solution to Φ. Let h be the maximum depth of the right hand side of the equations of Φ. Let us consider an instantiable variable x and t = σx = λy 1 : T 1 . ... λy n : T n .u (u atomic). Let us consider a variable y i and an occurrence α of the Böhm tree of t such that there are more than h + 1 occurrences on the path of α labeled with the variable y i . We consider all the equations (x c 1 ... c n ) = b of Φ such that the (h + 2) -th occurrence of y i is accessible with respect to this equation. Then there exists an integer j such that for every such equation we have

c i = λz 1 : U 1 . ... λz p : U p .z j
Proof Let β be the first occurrence of y i in the path of α. Let j be the integer such that α = β < j > β ′ . Let (x c 1 ... c n ) = b be an equation of Φ such that the (h + 2) -th occurrence of y i on the considered path is accessible with respect to this equation. If the head of c i is a symbol different from a z k then |c i | ̸ = 0. Using part (3) of the key lemma when we substitute c 1 , ..., c i-1 , c i+1 , ..., c n we have an occurrence α ′ that has more than h + 1 occurrences of y i on its path. Then using part (4) of the key lemma, when we substitute c i we have an occurrence α ′′ whose length is greater than or equal to h + 1 so

h + 1 ≤ |u[y 1 ← c 1 , ..., y n ← c n ]| i.e. h + 1 ≤ |b| which is contradictory. So we have c i = λz 1 : U 1 . ... λz p : U p .z k Since h+2 > 1 the occurrence β < j > is accessible with respect to the equation (x c 1 ... c n ) = b.
Thus as the occurrence β is labeled with y i and the occurrence β < j > is accessible with respect to this equation, the term c i is relevant in its j th argument. Therefore k = j and

c i = λz 1 : U 1 . ... λz p : U p .z j
Definition 27 (Compact Accessible Solution Built from an Accessible Solution)

Let Φ be an interpolation problem and let σ be an accessible solution to this problem. Let h be the maximum depth of a right hand side of the equations of Φ. We let σx = t = λy 1 : T 1 . ... λy n : T n .u

For each α, occurrence in t labeled with y i such that the corresponding occurrence α ′ in the Böhm tree of t has more than h + 1 occurrences labeled with y i in its path, we have c i = λz 1 : U 1 . ... λz p : U p .z j in all the equations (x c 1 ... c n ) = b of Φ such that α ′ is accessible with respect to this equation. We substitute the occurrence α by the term λz 1 : U 1 . ... λz p : U p .z j . We get that way a term t ′ . We let σ ′ x = t ′ . This solution is accessible but not compact. The first occurrence of f is accessible with respect to both equations, but the second and third occurrences are accessible only with respect to the second one. We have h = 0, so we substitute the second and third occurrences of f by the term λy : T.λz : T.z and we get the substitution and for all i such that z has an occurrence in (σx σd 1 ... σd i-1 z σd i+1 ... σd n ) by induction hypothesis we have σ Definition 29 Let Ψ be a third order matching problem and let σ be a solution to Ψ. We let Φ(Ψ, σ) be the following third order interpolation problem:

′ d i = σd i , so c i = σ ′ d i . Therefore (σ ′ x c 1 ... c n )[z i ← σ ′ d i ] = b[z i ← σ ′ d i ] (σ ′ x c 1 ... c n )[z i ← σ ′ d i ] = b (σ ′ x σ ′ d 1 ... σ ′ d n ) = b σ ′ a = b
Φ(Ψ, σ) = a=b∈Ψ Φ(a = b, σ)
Proposition 14 Let Ψ be a third order matching problem and let σ be a solution to Ψ. Let h be the maximum of the depth of the right hand side of the equations of Ψ. Then σ is a solution to the problem Φ(Ψ, σ), each substitution σ ′ solution to the problem Φ(Ψ, σ) is a solution to Ψ and if

a ′ = b ′ ∈ Φ(Ψ, σ) then |b ′ | ≤ h.
Proof By propositions 12 and 13. Lemma 4 Let Ψ be third order matching problem. Let h be the maximum of the depth of the the right hand side of the equations of Ψ. If this problem has a solution σ then it also has a solution σ ′ such that for every instantiable variable x, σx has a depth less than or equal to (n + 1)(h + 1) -1 where n the arity of x. Proof The substitution σ is a solution to the problem Φ(Ψ, σ), thus, by lemma 3, this problem has a solution σ ′ such that for every instantiable variable x, σ ′ x has a depth less than or equal to (n + 1)(h + 1) -1. This solution σ ′ is a solution to the problem Ψ.

Remark This method, in which an interpolation problem Φ(Ψ, σ) is constructed from a pair < Ψ, σ > where Ψ is an arbitrary problem and σ a solution to Ψ, can be compared to the one used in the completeness proof of [START_REF] Snyder | Higher-Order Unification Revisited: Complete Sets of Transformations[END_REF] in which a problem in solved form is constructed from such a pair.

A Decision Procedure

Theorem Third Order Matching is Decidable Proof A decision procedure is obtained by considering the problem Φ and enumerating all the ground substitutions such that the term substituted for x has a depth less than or equal to (n + 1)(h + 1) -1, where h maximum depth of b for a = b ∈ Φ and n is the arity of x. If one of these substitutions is a solution then success else failure. This decision procedure is obviously sound. By lemma 4, it is complete.

Remark A more efficient decision algorithm is obtained by enumerating the nodes of the tree obtained by pruning Huet's search tree [START_REF] Huet | A Unification Algorithm for Typed λ-calculus[END_REF] [6] at each node corresponding to a substitution whose depth is larger than (n + 1)(h + 1) -1. This tree is obviously finite and thus this algorithm terminates. It is obviously sound. By lemma 4, it is complete.

Remark This result can be used to design an algorithm which enumerates a complete set of solutions to a third order matching problem and either terminates if the problem has a finite complete set of solutions or keeps enumerating solutions forever if it the problem admits no such set. Such an algorithm is got by enumerating the nodes of the tree obtained by pruning Huet's search tree [START_REF] Huet | A Unification Algorithm for Typed λ-calculus[END_REF] [6] at each node labeled with a problem that has no solution (by the theorem above, it is decidable if such a problem has a solution or not). Obviously, this algorithms still produces a complete set of solutions.

Let us show now that when a matching problem has a finite complete set of solutions then this algorithm terminates. Recall that a set of substitutions is called minimal if no substitution of this set is an instance of another and that Huet's algorithm applied to a matching problem produces a minimal complete set of solutions [START_REF] Huet | Résolution d' Équations dans les Langages d[END_REF]. It is routine to verify that if a a problem has a finite complete set of solutions then any minimal complete set of solutions is also finite. So, if a problem has a finite complete set of solutions then Huet's tree for this problem has a finite number of success nodes and thus a finite number of nodes labeled with a problem that has a solution. The pruned tree is therefore finite and the algorithm obtained by enumerating its nodes terminates.

Remark This decidability result can be compared with the decidability of the equations of the form P (x 1 , ..., x n ) = b where P is a polynomial whose coefficients are natural numbers and b is a natural number.

If this equation has a solution < a 1 , ..., a n > then it has a solution < a ′ 1 , ..., a ′ n > such that a ′ 1 ≤ b. Indeed either Q(X) = P (X, a 2 , ..., a n ) is not a constant polynomial and for all n, Q(n) ≥ n, so a 1 ≤ b, or the polynomial Q is identically equal to b and < 0, a 2 , ..., a n > is also a solution. So a simple induction on n proves that if the equation has a solution then it also has a solution in {0, ..., b} n and an enumeration of this set gives a decision procedure.

Conclusion: Towards Higher Order Matching

The proof given here is based on the fact that if t is a third order term then when we reduce the term (t c 1 ... c n ), in the general case, we get a term deeper than t (or, at least, if it is not, the depth loss can bounded). This gives a bound (in terms of the depth of b) on the depth of the solutions of the equation (x c 1 ... c n ) = b. In the particular cases in which the depth loss is greater than the bound, some part of the term t is superfluous and that we can construct a smaller term t ′ such that (t ′ c 1 ... c n ) = (t c 1 ... c n ).

Generalizing this property of reduction to the full λ-calculus would give the decidability of higher order matching. To get the normal form of the term (t c 1 ... c n ) we have followed the strategy hinted by the weak normalization theorem and reduced first all the second order redexes, then all the first order redexes. So a generalization of this proof to higher order should require an induction on the maximal order of a redex. In the proof for the third order case, we quickly get the normal form of the term (t c 1 ... c n ) and we do not need to define the depth of a non-normal term. It seems that the generalization of this result to higher order requires such a definition.

  Pattern Matching Definition 15 (Matching Problem) A matching problem is a set Φ = {< a 1 , b 1 >, ..., < a n , b n >} of pairs of terms of the same type such that the terms b 1 , ..., b n are ground. A pair < a, b > is frequently written as an equation a = b.

Lemma 1

 1 Some problems have no finite complete set of solutions. Proof (Example 1) Consider an atomic type T and an instantiable variable x : T → (T → T ) → T and the problem λa : T.(x a λz : T.z) = λa : T.a The substitutions x ← λo : T.λs : T → T.(s ... (s o) ... ) are solutions to this problem and they cannot be obtained as instances of a finite number of solutions. Remark In [6] [12], the similar examples (x λz : T.z) = a and (x λz : T.z) = b(a) are considered.

3. 1 . 1

 11 Key Lemma Definition 21 (Relevant Term) Let c = λz 1 : U 1 . ... λz p : U p .d (d atomic) be a normal term and i an integer, i ≤ p. We say that c is relevant in its i th argument if z i has an occurrence in the term d. Lemma 2 (Key Lemma) Let us consider a normal term u, a variable y of type T of order at most two and a normal ground term c of type T . (1) If y has an occurrence in u then |c| ≤ |u[y ← c]|.

( 1 )

 1 Let β be an outermost occurrence of y in the Böhm tree of u. For each occurrence δ in the Böhm tree of c, βδ is an occurrence in the Böhm tree of the normal form of u[y ← c]. So |c| ≤ |u[y ← c]|.

( 4 )

 4 If δ =< > then c = λz 1 : U 1 . ... λz p : U p .z r and |c| = 0. So if |c| ̸ = 0 then δ ̸ =< > and the length of α ′ is greater than or equal to the length of α. Corollary Let us consider a normal term u, a variable y of type T of order at most two and a ground term c of type T . If c is relevant in all its arguments and |c| ̸ = 0 then |u| ≤ |u[y ← c]|. Proof We take for α the longest occurrence in the Böhm tree of u. When we substitute one by one the occurrences of y, by part (4) of the key lemma, we get occurrences that are at least long. So there is an occurrence in the Böhm tree of the normal form of u[y ← c] which is at least long as α. So |u| ≤ |u[y ← c]|.

3. 1 . 2

 12 Computing the Substitution σ ′ Let us consider an equation (x c 1 ... c n ) = b. Let σ be a solution to this equation and let t = σx. Let us write t = λy 1 : T 1 . ... λy n : T n .u. The normal form of the term σ(x c 1 ... c n ) is the normal form of u[y 1 ← c 1 , ..., y n ← c n ]. If all the c i are relevant in their arguments and |c i | ̸ = 0 then using the corollary of the key lemma we have |t| ≤ |(t c 1 ... c n )|, so |t| ≤ |b| and this gives a bound on the depth of t. But the depth of t may decrease when applied to the terms c i and normalized in two cases:

Example 2

 2 Let x be an instantiable variable of type T → (T → T ) → T . Consider the problem (x a λz : T.b) = b The variable z has no occurrence in b so this problem has solutions of arbitrary depth x ← λo : T.λs : T → T.(s t) where t is an arbitrary term of type T . In this example we will compute the substitution x ← λo : T.λs : T → T.(s c) where c is a constant. Example 1 (continued) The term λz : T.z has depth 0, so we have solutions of an arbitrary depth. In this example we will compute the substitution x ← λo : T.λs : T → T.(s o) Definition 22 (Occurrence Accessible with Respect to an Equation of the Form (x c 1 ... c n ) = b) Let us consider an equation (x c 1 ... c n ) = b and the term t = σx = λy 1 : T 1 . ... λy n : T n .u

Example 2 (

 2 continued) From the solution x ← λo : T.λs : T → T.(s t) where t is an arbitrary term, we compute the substitution x ← λo : T.λs : T → T.(s c) where c is a constant. Proposition 6 Let Φ be an interpolation problem and let σ be a solution to Φ, then the accessible solution σ built from σ is a solution to Φ. Proof Let us consider an equation (x c 1 ... c n ) = b of Φ and the terms σx = t = λy 1 : T 1 . ... λy n : T n .u and σx = t ′ = λy 1 : T 1 . ... λy n : T n .u ′

Example 1 (Example 3

 13 continued) We build the substitution x ← λo : T.λs : T → T.(s o) Consider an instantiable variable x of type (T → T → T ) → T . And the problem (x λy : T.λz : T.y) = a (x λy : T.λz : T.z) = b We have the solution x ← λf : T → T → T.(f a (f c (f d b)))

xProposition 11

 11 ← λf : T → T → T.(f a b) Note that we must not substitute the first occurrence of f by λy : T.λz : T.z, because we would get the substitution x ← λf : T → T → T.b which is not a solution to the first equation. Definition 28 Let a = b be an equation and let σ be a (ground) solution to this equation. By induction on the number of occurrences of a we construct an interpolation problem Φ(a = b, σ). • If a = λx : T.d then since σ is a solution to the problem a = b we have b = λx : T.e and σ is a solution to the problem d = e. We let Φ(a = b, σ) = Φ(d = e, σ) • If a = (f d 1 ... d n ) with f a constant or a local variable then since σ is a solution to a = b we have b = (f e 1 ... e n ) and σ is a solution to the problems d i = e i . We let Φ(a = b, σ) = i Φ(d i = e i , σ)• If a = (x d 1 ... d n ) with x instantiable then for all i such that z has an occurrence in the normal form of the term (σx σd 1 ... σd i-1 z σd i+1 ... σd n ) we let c i = σd i andH i = Φ(d i = σd i , σ) (obviously σ is a solution to d i = σd i ). Otherwise we let c i z i where z i is a new local variable and H i = ∅. We let Φ(a = b, σ) = {(x c 1 ... c n ) = b} ∪ i H i Let t = (x d 1 ... d n )be a term and let σ be a substitution. Let c i = σd i if z has an occurrence in (σx σd 1 ... σd i-1 z σd i+1 ... σd n ) and c i = z i where z i is a new local variable of the same type as d i otherwise. The variables z i do not occur in the normal form of (σx c 1 ... c n ). Proof Let us assume that some of these variables have an occurrence in the normal form of (σx c 1 ... c n ) and consider an outermost occurrence of such a variable z i in the Böhm tree of the normal form of (σx c 1 ... c n ). By part (2) of the key lemma, the variable z i has also an occurrence in the normal form of term (σx c 1 ... c n )[z j ← σd j | j ̸ = i] i.e. in the normal form of the term (σx σd 1 ... σd i-1 z i σd i+1 ... σd n ), which is contradictory.Proposition 12 Let a = b be an equation and let σ be a solution to this equation,• the substitution σ is a solution to Φ(a = b, σ),• conversely, if σ ′ is a solution to Φ(a = b, σ) then σ ′ is also a solution to the equation a = b.Proof• By induction on the number of occurrences of a. When a is an abstraction a = λx : T.d (resp. an atomic term whose head is a constant or local variable a = (f d 1 ... d n )) then b is also an abstraction b = λx : T.e (reps. an atomic term with the same head b = (f e 1 ... e n )) and by induction hypothesis σ is a solution to all the equations of the set Φ(d = e, σ) (resp. Φ(d i = e i , σ)), so it is a solution to all the equations of Φ(a = b, σ).When a = (x d 1 ... d n ) then by induction hypothesis σ is a solution to all the equations of the sets H i and using the previous proposition the variables z i have no occurrences in the term (σx c 1 ... c n ) so we have (σxc 1 ... c n ) = (σx c 1 ... c n )[z i ← σd i ] (σx c 1 ... c n ) = (σx σd 1 ... σd n ) = bSo σ is a solution to the equation (x c 1 ... c n ) = b. • By induction on the number of occurrences of a. Let σ ′ be a substitution solution to Φ(a = b, σ). If a is an abstraction a = λx : T.d (resp. an atomic term whose head is a constant or a local variable a = (f d 1 ... d n )) then b is also an abstraction b = λx : T.e (reps. an atomic term with the same head b = (f e 1 ... e n )) and by induction hypothesis we have σ ′ d = e (resp. σ ′ d i = e i ) and so σ ′ a = b. If a = (x d 1 ... d n ) then we have (σ ′ x c 1 ... c n ) = b

Proposition 13

 13 Let a = b be an equation and let σ be a solution to this equation, if a ′ = b ′ is an equation of Φ(a = b, σ) then |b ′ | ≤ |b|. Proof By induction on the number of occurrences of a. When a is an abstraction a = λx : T.d (reps. an atomic term whose head is a constant or a local variable a = (f d 1 ... d n )) then b is also an abstraction b = λx : T.e (reps. an atomic term with the same head b = (f e 1 ... e n )) and by induction hypothesis |b ′ | ≤ |e| (resp. |b ′ | ≤ |e i |) so |b ′ | ≤ |b|. When a = (x d 1 ... d n ) and the considered equation is (x c 1 ... c n ) = b then we have b ′ = b so |b ′ | ≤ |b|. When the considered equation is in one of the sets H i , the set H i is non empty so z has an occurrence in the normal form of the term (σx σd 1 ... σd i-1 z σd i+1 ... σd n ) and (σx σd 1 ... σd i-1 z σd i+1 ... σd n )[z ← σd i ] = b so using part (1) of the key lemma we have |σd i | ≤ |b| and by induction hypothesis |b ′ | ≤ |σd i | so |b ′ | ≤ |b|.

This technical restriction is in fact superfluous, because a matching problem expressed in a language with an infinite number of constants can always be reduced to one expressed in the language with a finite number of constants obtained by considering only the constants occurring in the problem and one constant in each atomic type.

Acknowledgments

The author would like to thank Gérard Huet, Richard Statman and Gopalan Nadathur for many very helpful discussions on this problem and remarks on previous drafts of this paper. This research was partly supported by ESPRIT Basic Research Action "Logical Frameworks".

Proposition 9 Let Φ be an interpolation problem and let σ be a solution to Φ. Let σ the accessible solution built from σ and σ ′ the compact accessible solution built from σ. Then σ ′ is a solution to Φ. Proof We consider an equation (x c 1 ... c n ) = b and we let σx = t = λy 1 : T 1 . ... λy n : T n .u

The term u ′ is obtained by substituting in the term u some occurrences (say β 1 , ..., β k ) by some terms (say e 1 , ..., e k ). If α is an occurrence of u then we define u ′ α as the term obtained by substituting in the term u/α the occurrence γ i by the term e i if β i = αγ i .

We prove by decreasing induction on the depth of the occurrence α of the Böhm tree of u that if α is accessible with respect to the equation (

Thus for the root we get

So σ ′ is a solution to all the equations of Φ.

Proposition 10 Let Φ be an interpolation problem and let σ be a solution to Φ. Let σ be the accessible solution built from σ and σ ′ the compact accessible solution built from σ. Let h be the maximum depth of the right hand side of the equations of Φ. For every instantiable variable x of arity n, σ ′ x has a depth less than or equal to (n + 1)(h + 1) -1.

Proof In a path of the Böhm tree of σ ′ x each y i has at most h + 1 occurrences and there are at most h + 1 occurrences of other symbols, so there are at most (n + 1)(h + 1) occurrences. Therefore the depth of σ ′ x is bounded by (n + 1)(h + 1) -1.

Lemma 3 Let Φ be a third order interpolation problem. If Φ has a solution σ then it also has a solution σ ′ such that for every instantiable variable x, σx has a depth less than or equal to (n + 1)(h + 1) -1, where h is maximum of the depths of the right hand side of the equations and n the arity of x.

Proof The compact accessible solution σ ′ built from the accessible solution built from the solution σ is a solution and for every instantiable variable x, σ ′ x has a depth less than or equal to (n + 1)(h + 1) -1. This bound is met, for instance by the example 3.

General Case


Fadi Badra

Julien Cojan

Amélie Cordier

Jean Lieber

Thomas Meilender

Alain Mille

Pascal Molli

Emmanuel Nauer

Amedeo Napoli

Hala Skaf-Molli

Yannick Toussaint

Knowledge Acquisition and Discovery for the Textual Case-Based Cooking system WIKITAAABLE

Keywords: textual case-based reasoning, case-based cooking, semantic wiki, opportunistic knowledge acquisition

The textual case-based cooking system WIKITAAABLE participates to the second Computer cooking contest (CCC). It is an extension of the TAAABLE system that has participated to the first CCC. WIKITAAABLE's architecture is composed of a semantic wiki used for the collaborative acquisition of knowledge (recipe, ontology, adaptation knowledge) and of a case-based inference engine using this knowledge for retrieving and adapting recipes. This architecture allows various modes of knowledge acquisition for case-based reasoning that are studied within the TAAABLE project. In particular, opportunistic adaptation knowledge discovery is an approach for interactive and semi-automatic learning of adaptation knowledge triggered by a feedback from the user.

Introduction

As final result from last year did not make us good cooks, we decided to keep on doing research. Hence, for the second edition of the Computer Cooking Contest (CCC), the TAAABLE system has evolved towards a new architecture called WIKITAAABLE. This year, we focused our efforts on two intertwined aspects: knowledge and reasoning. Concerning reasoning, we worked on the inference engine improvement to enhance the adaptation ability of the system. Concerning knowledge we set up advanced knowledge acquisition facilities to support the evolution of the system during its life-cycle.

This paper describes the innovations developed in WIKITAAABLE, whose architecture is described in section 2 and discusses current research issues. One innovation this year is that the system is embedded within a semantic wiki and that the collaborative aspects are also of main concern mainly for document and knowledge edition and update.

The remainder of the paper shows how knowledge is manipulated within the system. Section 3 presents knowledge acquisition and representation within the semantic wiki. Section 4 illustrates how knowledge is used by the inference engine. Section 5 describes an opportunistic acquisition strategy guiding the evolution of the system knowledge. Finally, section 6 draws some conclusions and points out ongoing and future work. For qualification purpose, a restricted interface of the system is available online. This interface only allows users to ask queries to the system. The full application with embedded knowledge acquisition features will be available for the contest.

2 Architecture of WIKITAAABLE In a CBR system, results strongly depend on the quality of available knowledge. As a consequence, continuous improvement of knowledge is required to progressively enhance the obtained results.

The previous version of TAAABLE [START_REF] Badra | Taaable: Text Mining, Ontology Engineering, and Hierarchical Classification for Textual Case-Based Cooking[END_REF] suffered from different problems making maintenance and evolution of the system knowledge difficult. For example, there was no way to capture user feedback and to reuse it for maintenance. Besides, knowledge was organized in several files of heterogeneous formats that were difficult to update. As a consequence, the evolutions of the system knowledge were tedious tasks, even for the designers of TAAABLE.

In WIKITAAABLE [START_REF] Cordier | Wikitaaable: A semantic wiki as a blackboard for a textual case-based reasoning system[END_REF] we decided to use a semantic wiki (Semantic Media Wiki [START_REF] Völkel | Semantic Wikipedia[END_REF]) as a central module to manage all data and knowledge used in the system. Making use of a semantic wiki has two major advantages: it enables humans and machines to rely on the same tool for representing and reasoning on shared knowledge and it provides users with user-friendly interfaces for browsing and editing knowledge.

Figure 1 gives an overview of the WIKITAAABLE architecture. Each component has been designed to work with the others and the components are strongly intertwined. For example, knowledge has not been represented at a general level but for reasoning purpose. The semantic wiki module manages knowledge of the system. The wiki is accessible for the users through a graphical interface and for the system through bots1 that automates several tasks. Section 3 details this module. The inference engine includes the CBR core and is able to reason on the knowledge available in the wiki. It is described in section 4. In order to facilitate knowledge acquisition, the architecture of WIKITAAABLE is designed in such a way that it enables as much interactions as possible. Opportunistic knowledge acquisition process developed in WIKITAAABLE is discussed in section 5.

A Semantic Wiki for Collaborative Acquisition of Cooking Knowledge

In [START_REF] Cordier | Wikitaaable: A semantic wiki as a blackboard for a textual case-based reasoning system[END_REF], Semantic Media Wiki (SMW [START_REF] Völkel | Semantic Wikipedia[END_REF]) is used as a blackboard for WIKITAAABLE knowledge management. WIKITAAABLE gathers the whole knowledge body required by the application.

To import knowledge of the first version of the TAAABLE system [START_REF] Badra | Taaable: Text Mining, Ontology Engineering, and Hierarchical Classification for Textual Case-Based Cooking[END_REF] into WIKI-TAAABLE, we wrote several bots that use mediawiki API. Recipes, ontologies, and specific adaptation knowledge are now represented as a graph of semantic wiki pages. Each page can be freely read an updated by humans and by bots. Hence, TAAABLE is now maintained and improved by a collaboration between users and machines.

Domain Ontology

The domain ontology contains four hierarchies: ingredients, dish moments, dish types, and dish origins. For adapting a recipe by substituting some ingredients by other ingredients, the CBR engine requires knowledge stating similarity between ingredients. Therefore, ingredients are organized in the ingredient hierarchy. This hierarchy is used by the CBR engine to compute the cost of a substitution: the closer the ingredients, the lower the cost; e.g., orange is closer to lemon than apple. 2 In order to characterize recipes, three other hierarchies define and organize dish moments (appetizer, dessert), dish types (cake, pizza), and dish origins (Mediterranean, Chinese). The original acquisition of the hierarchies is described in [START_REF] Badra | Taaable: Text Mining, Ontology Engineering, and Hierarchical Classification for Textual Case-Based Cooking[END_REF].

The four hierarchies are imported into WIKITAAABLE by using the Category/Sub-Category relation of Semantic MediaWiki [START_REF] Völkel | Semantic Wikipedia[END_REF]. For example, there is a page for orange and another page for citrus and the two pages are linked by this relation. For instance, the figure 2 shows the imported ingredient hierarchy.

Adaptation knowledge

To adapt a recipe, the CBR engine uses the ontology and a set AK of substitutions. A substitution σ ∈ AK states that, in a given context, some ingredients may be substituted by other ones. For instance, the following substitution states that, for the context of a salad without potato, vinegar may be substituted by lemon juice and salt.

σ = context salad no potato from vinegar by lemon juice salt ( 1
)
Each substitution is represented in a semantic wiki page. For instance, figure 3 shows the wiki page of the above substitution. The acquisition of substitutions is detailed in section 5.

Recipes

The recipes are also imported into WIKITAAABLE, where a wiki page is created for each recipe. Then, a bot crawls all the recipe pages, parses ingredient information, sets dish types, moments, and origins. It updates recipe pages with this information encoded as semantic annotations. Figure 4 shows a recipe page in WIKITAAABLE. We used the n-ary relationship of Semantic Media Wiki to represent an ingredient line, for example, (1, c, Category:rice) represents 1 c rice, the first ingredient line in figure 4. The parsing of ingredient information and setting types is described in [START_REF] Badra | Taaable: Text Mining, Ontology Engineering, and Hierarchical Classification for Textual Case-Based Cooking[END_REF]. O is the domain ontology represented by a set of axioms of the form a ⇒ b where a and b are two variables representing recipe classes. For example, lemon (resp., citrus) represents the class of recipes with lemon (resp., with citrus) and the axiom lemon ⇒ citrus states that any recipe with lemon is a recipe with citrus. In fact, every ingredient name X such as lemon is interpreted here as "class of the recipes with ingredient X".

Recipes is the set of recipes given by the CCC organizers, and consequently the case base of the CBR system TAAABLE. A recipe R ∈ Recipes cannot be directly handled by the CBR inference engine: the engine requires a formal representation whereas R is for the largest part written in natural language. Therefore, only the formalized part of the recipe R is used: its index idx(R), which is expressed by a conjunction of literals (the indexing process of the recipes coincides with the annotation process mentioned in section 3.3). For example

idx(R) = lettuce ∧ vinegar ∧ olive_oil ∧ tomato ∧ Nothing else (2)
is a formal representation of a recipe R having ingredients lettuce, vinegar, olive oil, and tomato. A closed world assumption is associated to idx(R) stating that if a prop- erty cannot be deduced from the recipe description and from the ontology then it is considered as false. Formally, if idx(R) O a then "Nothing else" contains the conjunct ¬a. It can be noticed that the substitution given by a triple (context, from, by) in the wiki pages (cf. equation ( 1)) are rewritten context ∧ from context ∧ by to suit the CBR engine formalism.

The CBR inference is based on substitutions, either taken from AK or built with the help of ontology O (see below for details). The choice of substitutions is made according to the problem-solving context and to a cost function cost : σ → cost(σ) > 0; substitution σ is preferred to substitution τ when cost(σ) < cost(τ ). Therefore, the cost function (and its parameters) constitutes an additional knowledge container.

CBR Inference

Let Q be a query. For example

Q = endive ∧ lemon_juice ∧ ¬onion (4)
is a query for a recipe with endive and lemon juice and without onion. The CBR inference consists in (1) retrieving recipes matching exactly or approximately Q and (2) adapting the retrieved recipes. Retrieval aims at choosing indexes idx(R) matching the query Q. An exact match corresponds to idx(R) O Q. If no index exactly matches Q, the query Q is progressively relaxed into Γ (Q) such that idx(R) O Γ (Q), for some idx(R). The relaxation of Q is obtained by applying generalizations g k according to O:

g k = a k b k is a substitution such that (a k ⇒ b k ) ∈ O. Thus Γ (Q) = g n (. . . (g 1 (Q)) . . .). Therefore, retrieval provides a similarity path idx(R) O Γ (Q) gn ←-. . . g1 ←-Q (5)
This similarity path is built according to a best-first search minimizing k cost(g k ).

For example, retrieval can give the following result

Q = endive ∧ lemon_juice ∧ ¬onion Γ (Q) = green_salad ∧ ⊤ ∧ ¬onion ≡ green_salad ∧ ¬onion idx(R) = lettuce ∧ vinegar ∧ olive_oil ∧ tomato ∧ Nothing else
(Γ consists in generalizing endive into green_salad and in removing lemon_juice from the query by generalizing it in several steps to ⊤, the hierarchy top).

Adaptation is composed of two sub-steps. Let R be a retrieved recipe, with index idx(R). The first subset of adaptation is matching, that aims at building an adaptation path from idx(R) to Q of the form

idx(R) σ1 -→ . . . σp -→ Σ(idx(R)) O Γ (Q) γq ←-. . . γ1 ←-Q (6)
where σ i ∈ AK (i = 1 . . . p) and substitutions γ j (j = 1 . . . q) correspond to axioms of the ontology: γ j = a j b j with (a j ⇒ b j ) ∈ O. Such an adaptation path is built according to a best-first search in a state space minimizing i cost(σ i ) + j cost(γ j ).

The second sub-step of adaptation consists in "following" the adaptation path: first R is adapted successively in σ 1 (R), σ 2 (σ 1 (R)), . . . σ p (. . . (σ 2 (σ 1 (R)) . . .) = Σ(R). Then, ingredients of Σ(R) are substituted by other ingredients according to a generalization-specialization process (generalization corresponds to the relation O and specialization to the substitutions γ -1 q , . . . , γ -1 1 ). For example, let idx(R) and Q be the example presented above. Matching may provide the following adaptation path:

idx(R) σ -→ Σ(idx(R)) O Γ (Q) γ ←-Q
where σ is defined by ( 3) and γ = endive green_salad. Thus, the adaptation of R consists in replacing vinegar by lemon juice and salt (cf. σ) and by substituting lettuce by endive (cf. O and γ -1 ).

It can be noticed that retrieval provides a first matching: a similarity path is a kind of adaptation path involving no σ ∈ AK. Thus, the retrieved recipe R can be adapted following this similarity/adaptation path. However, during adaptation, some substitutions σ ∈ AK may be used and, if they do, the resulting adaptation requires less effort. 45 Opportunistic Knowledge Acquisition and Discovery WIKITAAABLE has been designed to facilitate continuous knowledge acquisition through interactions with its users: it is a reflexive and perpetually evolving system. However, due to the heterogeneity of knowledge acquisition situations that can be envisioned, setting up such a process is a complex task. This diversity of situations is explained by several factors:

-The various types of knowledge (ontology, adaptation knowledge, substitutions costs, recipes) that can be acquired. -The different interaction modalities such as simple user feedback, direct modification on wiki pages, interaction through dedicated interfaces, use of external knowledge discovery methods, etc. -The provenance of knowledge that is acquired: single users, community of users, experts, other sources of data (web sites), or local knowledge from which new knowledge in inferred.

In the following, a particular scenario of opportunistic knowledge discovery is detailed. In WIKITAAABLE, substitutions σ ∈ AK are acquired at problem-solving time through interactions with the user. The knowledge discovery process CABAMAKA [START_REF] D'aquin | Case base mining for adaptation knowledge acquisition[END_REF] is used to assist the user in the formulation of new pieces of knowledge. Its role is to generate a set of substitutions σ ∈ AK "on the fly" from the comparison of two sets of recipes of the case base. The generated substitutions can be used by the system to repair a failed adaptation. Each time a substitution is validated by the user, it is stored for future reuse. In the following, the main principles of the approach are illustrated on an example. More details on the proposed approach can be found in [START_REF] Badra | Opportunistic adaptation knowledge discovery[END_REF].

In section 4, the user wanted a salad recipe with lemon juice but without onion, which was modeled by the query Q defined by [START_REF] D'aquin | Case base mining for adaptation knowledge acquisition[END_REF]. The substitution σ ∈ AK defined by (3) was used to adapt the retrieved recipe R by replacing vinegar by lemon juice and salt. Such a substitution cannot be obtained from the ontology O, so let us assume in this scenario that σ is not available to the system. Thus, to perform adaptation, the system relies solely on the ontology O from which it generates the substitution vinegar lemon_juice. Now, in our scenario, the user is not satisfied with the proposed solution and gives this feedback to the system. Therefore, the knowledge discovery process is triggered: a set of substitutions is learned from the case base by comparing salad recipes with vinegar and salad recipes with lemon juice. Among the learned substitutions is the substitution σ learned = vinegar lemon_juice ∧ salt, which suggests to replace vinegar by lemon juice in the retrieved recipe R and to add salt. The user is satisfied with the adaptation resulting from the application of this substitution, so the latter is stored for future reuse. At this point, the user is encouraged to specify the condition of application of the substitution σ learned . The user states that vinegar can be replaced by lemon juice and salt in salad recipes that do not contain potato, which is modeled by the substitution context salad∧¬potato. Combining the learned substitution σ learned and its application context gives the substitution σ defined by [START_REF] Cordier | Wikitaaable: A semantic wiki as a blackboard for a textual case-based reasoning system[END_REF].

In WIKITAAABLE, the wiki is used as a gateway enabling to centralize knowledge used in the system. It provides functionalities to facilitate acquisition and maintenance of knowledge and enables to progressively add new acquisition features, allowing the evolution of the whole system. However, setting up a complex knowledge acquisition process raises several issues. For example, tools for ensuring consistency of knowledge used in the system must be developed. Another issue is to handle updates from multiple users. What happens when one believes that an avocado is to be eaten as a starter whereas someone else reckon that it has to be eaten as a dessert? Is the system supposed to converge towards a "commonly accepted" knowledge base or should it be able to deal with user's preferences?

A strength of the architecture of WIKITAAABLE is that it will enable to progressively address these issues. A future work is to allow users to add their own recipes to the system. This functionality requires to be able to dynamically annotate new recipes within WIKITAAABLE in order to make them usable by the CBR inference engine. One of the advantages of such a functionality, combined with the benefits of a wiki, is that communities of users will be able to share their recipes and to collaborate in order to improve the global knowledge of the system. Next, we would like to tackle the multi-user issue which is a prerequisite for envisioning a collaborative building of the knowledge base of TAAABLE.

Conclusion, Ongoing Work, and Future Work

The textual case-based cooking system WIKITAAABLE participates to the second CCC. It is an extension of the TAAABLE system that has participated to the first CCC. WI-KITAAABLE's architecture is composed of a semantic wiki used for the collaborative acquisition of knowledge (recipe, ontology, adaptation knowledge) and of a CBR inference engine using this knowledge for retrieving and adapting recipes. This architecture allows various modes of knowledge acquisition for CBR that are studied within the TAAABLE project. In particular, opportunistic adaptation knowledge discovery is an approach for interactive and semi-automatic learning of adaptation knowledge triggered by a feedback from the users.

The first ongoing work is the improvement of the WIKITAAABLE system (user interface, inference engine, knowledge base encoded in wiki pages, and links between these components). Another work planned for the next weeks is the development of tools within WIKITAAABLE for knowledge acquisition triggered by user feedbacks. Such a knowledge acquisition leads to a continuous evolution of the knowledge base and thus, of the behavior of the system. It is important to ensure that these evolutions are improvements and that the integrity of the knowledge is preserved. We plan to use non regression and consistency tests for this purpose. Today, only the compulsory task of the CCC is addressed by WIKITAAABLE but we plan to have also the two challenges addressed by the system for the day of the contest.

Currently, wiki pages are accessed and maintained by a limited community: the TAAABLE project members. These pages encode the knowledge that have been acquired on the basis of a consensus. A long term objective is to have several open semantic wikis with cooking knowledge, each of them corresponding to a user community, the consensus being only realized at the level of a community.

Fig. 1 .

 1 Fig. 1. Overview of the WIKITAAABLE architecture.

Fig. 2 .

 2 Fig. 2. WIKITAAABLE ingredient ontology.

Fig. 3 .

 3 Fig. 3. A substitution semantic wiki page.

Fig. 4 .

 4 Fig. 4. indexed recipe of "Arroz dulce".

3

 3 For example, this closed world assumption enables to deduce that idx(R) O ¬meat ∧ ¬fish, i.e., that R is a vegetarian recipe. The indexes idx(R) are used to access recipes through a hierarchy H idx , according to the partial ordering O : for C, D ∈ H idx , C O D iff there is a directed path in H idx from C to D. The indexes idx(R) are leaves of the H idx . Adaptation knowledge has two parts. The first part is included in ontology O. The second part is the set AK of substitutions (cf. section 3.2). Any σ ∈ AK may be considered as a domain specific inference rule R is a good recipe σ(R) is a good recipe . The substitutions have the form C D where C and D are conjunctions of literals. Applying C D to a conjunction of literals (such as an index or a query) consists in replacing the literals of C by literals of D. For example, the substitution σ described in figure 3 is written as follows σ = salad ∧ ¬potato ∧ vinegar salad ∧ ¬potato ∧ lemon_juice ∧ salt (3)

A bot is a piece of software for doing automated repetitive tasks.

This closeness can be measured by a weighted length of the shortest path between ingredients in the hierarchy.

If f and g are two propositional formulas, f O g means that f implies g, given the ontology O. More precisely: if I satisfies both O and f then I satisfies g.

If the cost function is an estimation of the adaptation effort, then the adapted recipe should be better by following (6) then by following[START_REF] Völkel | Semantic Wikipedia[END_REF]. Indeed, since adding new substitutions (the ones of AK) only adds new ways to connect indexes to queries, it comes that P i cost(σi) + P j cost(γj) ≤ P k cost(g k ).

Acknowledgments

The participants of the TAAABLE project wish to thank the organizers of the CCC for providing this benchmark, that entails many interesting problems, and the need to collaborate with researchers in various domains on knowledge engineering.


Romane Hélie
email: romane.helie@math.unistra.fr

Philippe Helluy
email: philippe.helluy@unistra.fr

Stable second order boundary conditions for kinetic approximations

Keywords: Boundary conditions, Lattice Boltzmann, Entropy stability

. The method ensures entropy stability of the resulting approximation but also high order accuracy.

Introduction

The vectorial kinetic approach is a general method for approximating hyperbolic systems of conservation laws. It has been introduced by Bouchut in [START_REF] Bouchut | Construction of BGK models with a of kinetic entropies for a given system of conservation laws[END_REF] and Aregba and Natalini in [START_REF] Aregba | Discrete kinetic schemes for multidimensional systems of conservation laws[END_REF]. It consists in representing any system of conservation laws by a finite set of transport equations coupled through a stiff relaxation term. This representation has several advantages: it allows rigorous mathematical analysis [START_REF] Bouchut | Construction of BGK models with a of kinetic entropies for a given system of conservation laws[END_REF][START_REF] Aregba | Discrete kinetic schemes for multidimensional systems of conservation laws[END_REF][START_REF] Dubois | Simulation of strong nonlinear waves with vectorial lattice boltzmann schemes[END_REF]. Associated with time splitting techniques, it leads to the construction of very efficient schemes [START_REF] Baty | A robust and efficient solver based on kinetic schemes for magnetohydrodynamics (mhd) equations[END_REF].

We first describe the one-dimensional framework, but it can be generalized to higher dimensions. We consider a system of m conservation laws

∂ t w + ∂ x q(w) = 0, (1)
where the unknown conservative variable w(x, t) ∈ R m depends on a space variable x ∈ [L, R] and a real time variable t ≥ 0. The system (1) is supplemented with an initial condition and boundary conditions at x = L and x = R. We assume that (1) admits a Lax entropy s : R m → R, associated to an entropy flux g : R m → R. This means that s is strictly convex and that s ′ q ′ = g ′ . A weak solution w to (1) is admissible if the entropy is decreasing

∂ t s(w) + ∂ x g(w) ≤ 0.

Kinetic approximation

The system of conservation laws is approximated by the following system of 2m kinetic equations

∂ t f + Λ∂ x f = 1 ε (f eq (w) -f ), (2)
where:

the kinetic vector

f (x, t) = f 1 (x, t) f 2 (x, t) ∈ R 2m , f 1,2 (x, t) ∈ R m ,
the matrix Λ is defined by (I is the identity matrix of size m × m)

λ = λI 0 0 -λI , λ > 0,
the parameter ε > 0. The equilibrium f eq is defined below, the conservative data are related to the kinetic data thanks to the m × 2m matrix P = (I, I), and w = P f. This kinetic model is consistent with the conservation laws (1) when ε → 0 as soon as P f eq (w) = w, P Λf eq (w) = q(w).

The consistency conditions (3) lead to a unique possibility for the equilibrium data

f eq (w) = w 2 + q(w) 2λ w 2 -q(w) 2λ .
For the numerical resolution of (2) we use a Lattice Boltzmann Method (LBM). For a given integer N > 0, we define the space step h = (R -L)/N , the grid points x i = L + ih + h/2, 0 ≤ i < N and the time step τ = h/λ. The solution is approximated by f n i ≃ f (x i , nτ ). For going from time step n -1 to time step n, we first solve the free transport equation ∂ t f + Λ∂ x f = 0 exactly, which is possible by simple shift operations, thanks to the choice of the time step. We get

f n,- i = f n-1 1,i-1 f n-1 2,i+1 , w n i = P f n,- i . (4)
Then we apply a relaxation procedure for staying close to equilibrium

f n i = ωf eq (w n i ) + (1 -ω)f n,- i . (5)
The choice ω = 1 consists in returning to equilibrium at the end of each step. The resulting time marching scheme is first order accurate. The over-relaxation choice ω = 2 results in a second order accurate time scheme [START_REF] Paul | An interpretation and derivation of the lattice boltzmann method using strang splitting[END_REF]. We observe that the LBM is particularly simple and efficient: it is made of independent shift operations followed by independent local relaxations. It is highly parallelizable and the second order extension has no additional cost. It is clear that the shift algorithm (4) needs to be adapted at the boundaries, when i = 0 or i = N -1. At the left point, the value f n-1 1,-1 is missing, and at the right point, the value f n-1 2,N is missing. The boundary conditions are given by two "ghost cell" functions b L and b R whose role is to reconstruct the missing values from the first and last cell values:

f n-1 1,-1 = b L (f n-1 1,0 , f n-1 2,0 ), f n-1 2,N = b R (f n-1 1,N -1 , f n-1 2,N -1 ).
We propose below a general strategy to apply the boundary conditions on the kinetic scheme. We shall test it on the very simple transport conservation law at constant velocity v. In this case, we thus have m = 1 and

q(w) = vw. (6)
Let us explicit the kinetic model in this case. We find

P = (1, 1), w = f 1 + f 2 , f eq (w) = w( 1 2 + v 2λ ) w( 1 2 -v 2λ )
.

The chosen entropy and entropy flux are

s(w) = w 2 2 , g(w) = v w 2 2 .
3 Entropy stability and boundary conditions

Stability analysis

For constructing the kinetic model we follow [START_REF] Bouchut | Construction of BGK models with a of kinetic entropies for a given system of conservation laws[END_REF][START_REF] Dubois | Simulation of strong nonlinear waves with vectorial lattice boltzmann schemes[END_REF]. We assume that it is possible to find convex kinetic entropies s k such that

s(w) = min w=f1+f2 s 1 (f 1 ) + s 2 (f 2 ) = s 1 (f eq 1 ) + s 2 (f eq 2 ). ( 7
)
For the simple transport equation ( 6) that we consider, we can take

s 1 (f 1 ) = λ λ + v (f 1 ) 2 , s 2 (f 2 ) = λ λ -v (f 2 ) 2 .
These two kinetic entropies are convex under the sub-characteristic condition

|v| < λ.
For a general system of conservation laws with a Lax entropy, it is also possible to compute s k . The practical calculations can be done thanks to the Legendre transform [START_REF] Dubois | Simulation of strong nonlinear waves with vectorial lattice boltzmann schemes[END_REF][START_REF] Guillon | Stability analysis of the vectorial Lattice-Boltzmann Method[END_REF].

Once the consistency (3) and the kinetic entropy property [START_REF] Dubois | Simulation of strong nonlinear waves with vectorial lattice boltzmann schemes[END_REF] are ensured, the lattice Boltzmann scheme (4-5) is entropy dissipative for ω ∈ [START_REF] Aregba | Kinetic approximation of a boundary value problem for conservation laws[END_REF][START_REF] Aregba | Discrete kinetic schemes for multidimensional systems of conservation laws[END_REF]. Indeed, the shift step (4) preserves the kinetic entropy exactly and the relaxation step (5) makes it decrease, by design. This reasoning has to be adapted at the boundaries.

For establishing the entropy dissipative kinetic boundary condition, we assume that the initial condition is constant outside an

interval [a, b] ⊂]L, R[ w(x, 0) = w, if x < a or x > b.
Without loss of generality, we can assume that s(w) = 0 and g(w) = 0, because the properties of the entropy are not modified by the addition of affine functions. Then the boundary entropy condition simply states that, in the shift step (4), the kinetic entropy that enters the domain should be smaller than the kinetic entropy that leaves the domain. We obtain

s 1 (b L (f 1 , f 2 )) ≤ s 2 (f 2 ), s 2 (b R (f 1 , f 2 )) ≤ s 1 (f 1 ). ( 8
)

First order stable boundary conditions

We consider the simple transport case q(w) = vw. We assume that w = 0 and v > 0. It is then mandatory to impose w = 0 at the left boundary. A condition is missing at the right boundary. As in [START_REF] Drui | An analysis of over-relaxation in a kinetic approximation of systems of conservation laws[END_REF] we apply a null boundary condition on the flux error y, defined by

y = λf 1 -λf 2 -q(f 1 + f 2 ) = (λ -v)f 1 -(λ + v)f 2 .
This quantity vanishes when f k = f eq k . The boundary conditions are thus

f 1 + f 2 = 0 at x = L, λf 1 -λf 2 -q(f 1 + f 2 ) = 0 at x = R.

This allows to deducing the ghost cell functions b

L and b R b L (f 1 , f 2 ) = -f 2 , b R (f 1 , f 2 ) = λ -v λ + v f 1 . (9)
The kinetic entropy condition (8) is then satisfied, because v > 0.

The boundary conditions (9) are thus stable. However, we have observed that the right outgoing condition is only first order accurate, even when ω = 2.

Stabilized second order boundary conditions

As proposed in [START_REF] Drui | An analysis of over-relaxation in a kinetic approximation of systems of conservation laws[END_REF] we replace the right Dirichlet boundary condition by a Neumann boundary condition, because it was experimentally observed a better second order accuracy with w(L, t) = 0, ∂ x y(R, t) = 0. The spatial derivative is approximated by

∂ x y(R, nτ ) ≃ y n N -1 -y n N -2 h = 0.
But with this approximation, the right ghost cell boundary function now depends on the kinetic data in cell N -1 and cell N -2:

f n-1 2,N = b R (f n-1 1,N -1 , f n-1 2,N -1 , f n-1 1,N -2 , f n-1 2,N -2 ). ( 10
)
It is then generally not possible to ensure directly [START_REF] Guillon | Stability analysis of the vectorial Lattice-Boltzmann Method[END_REF]. We thus propose the following nonlinear correction at the right boundary:

-Compute f n-1 2,N with formula (10). -If the right entropy inequality is not satisfied, i.e. if s 2 (f n-1 2,N ) > s 1 (f n-1 1,N -1 ), then replace f n-1 2,N by the closest value f n-1 2,N such that

s 2 ( f n-1 2,N ) = s 1 (f n-1 1,N -1
). This construction ensures the decrease of entropy, with a minimal adjustment. It is expected that it will remain a second order accurate approximation. Similar ideas are exposed for instance in [START_REF] Aregba | Kinetic approximation of a boundary value problem for conservation laws[END_REF] (see also included references) in the FV framework.

Extension to higher dimension

The above construction can be extended to higher dimensions. Let us comment a two-dimensional example. We solve the transport equation

∂ t w + ∇ • q(w) = 0, q i (w) = v i w.
The unknown w(x 1 , x 2 , t) depends on a two-dimensional variable (x 1 , x 2 ) in a square Ω ⊂ R 2 . The velocity vector v = (v 1 , v 2 ) T . In this case, we can consider the D2Q4 model with four kinetic unknowns f k , 1 ≤ k ≤ 4. The kinetic velocities are (λ is a positive parameter)

c 1 = λ 1 0 , c 2 = λ -1 0 , c 3 = λ 0 1 , c 4 = λ 0 -1 .
The kinetic equations read

∂ t f k + c k • ∇f k = 1 ε (f eq k -f k ).
The equilibrium is given by

f eq k (w) = w 4 + v • c k w 2λ 2 , w = 4 k=1 f k .
We also define the flux error by

y =   λ(f 1 -f 2 ) -v 1 (f 1 + f 2 ) λ(f 3 -f 4 ) -v 2 (f 3 + f 4 ) λ 2 (f 1 + f 2 -f 3 -f 4 )   .
As in the D1Q2 model, the flux error vanishes when f = f eq . The kinetic entropy is given by

Σ(f ) = 1 λ + 2v 1 f 2 1 + 1 λ -2v 1 f 2 2 + 1 λ + 2v 2 f 2 3 + 1 λ -2v 2 f 2 4 .
Its convexity implies the sub-characteristic condition 2 max(|v

1 | , |v 2 |) < λ.
We summarize two boundary condition strategies in Table 1 ((n 1 , n 2 ) is the normal vector to the considered boundary): 5 Numerical results

D1Q2 model

For our tests, the initial data is the compact support function w(x, 0) = 0 if r(x) > 1, (1 -r(x) 2 ) 5 otherwise, where r(x) = |x-x0| σ , with σ = 0.2. We consider several test cases corresponding to different initial positions x 0 of the peak: in test case 1, x 0 = -1/2; in test case 2, x 0 = 0 and in test case 3, x 0 = 1/2. In Figure 1 we check the accuracy and the stability of the second order boundary condition.

D2Q4 model

We choose a square geometry, aligned with the kinetic velocities: Ω = [0, 1] × [0, 1]. We initialize w with a compact support function

w(x 1 , x 2 , t) = 0 if r(x 1 , x 2 ) > 1, (1 -r(x 1 , x 2 ) 2 ) 5 otherwise. with r(x 1 , x 2 ) = √ (x1-x1,0) 2 +(x2-y2,0) 2 σ
and σ = 0.4. We consider several test cases in Table 5.2, corresponding to different initial positions of the peak and several velocities (v 1 , v 2 ).

We first check in Figure 2 the second order accuracy and the instability of the boundary condition described in the second column of Table 1. Finally, we check in Figure 2 the improvement given by the projection strategy.

5 - √ 2/4 - √ 2/4 √ 2/2 √ 2/2 6 √ 2/4 √ 2/4 - √ 2/2 - √ 2/2 7 0 0 √ 2/2 √ 2/2

Conclusion

In this short paper, we have described a general strategy for imposing boundary conditions on a vectorial kinetic approximation. The difficulty is that the number of necessary boundary conditions is different between the kinetic model and the approximated conservation laws. With our method, it is possible to rigorously stabilize boundary schemes that are accurate but slightly unstable. In future works, we will extend the approach to nonlinear systems of conservation laws and more complex boundary geometries. 5.2. Second order is achieved for all the tests for short times. Right: entropy evolution for test case 1. The scheme is unstable on the long time. 5.2. Second order is achieved for all the tests. Right: entropy evolution for test case 1. The scheme is now stable thanks to the entropy limiting procedure.

Fig. 1 .

 1 Fig. 1. Second order boundary condition for the D1Q2 model (Dirichlet on w at the left boundary and Neumann on y at the right boundary). Left: error rates in the L 2 norm for the three test cases. Second order is achieved for all the tests. Right: entropy evolution for test case 1. Once the peak has entered the domain, the entropy decreases.

Fig. 2 .

 2 Fig. 2. Second order boundary condition for the D2Q4 model, without entropy limiting. Left: error rates in the L 2 norm for the test cases of Table5.2. Second order is achieved for all the tests for short times. Right: entropy evolution for test case 1. The scheme is unstable on the long time.

Fig. 3 .

 3 Fig. 3. Second order boundary condition for the D2Q4 model, with entropy limiting. Left: error rates in the L 2 norm for the test cases of Table5.2. Second order is achieved for all the tests. Right: entropy evolution for test case 1. The scheme is now stable thanks to the entropy limiting procedure.

Table 1 .

 1 Two different boundary condition strategies for the D2Q4 model. Left: It is possible to prove that this boundary condition is entropy dissipative, but first order accurate. Right: second order boundary condition, but not stable for long time simulations. By projecting this second-order boundary condition on the space of the decreasing entropy boundary conditions, we obtain stability and second-order accuracy.

Table 2 .

 2 Parameters of the test cases for the D2Q4 model.


Bouteiller, Bosilca, Faverge, Dongarra Wu

Keywords: gitlabpages.inria.fr/ 7 High-Performance Computing Classical parallel programming, threads High-Performance Computing Classical parallel programming, threads Classical parallel programming Classical parallel programming Classical parallel programming Classical parallel programming Classical parallel programming Classical parallel programming Classical parallel programming « Hierarchical DAG Scheduling for Hybrid Distributed Systems »,

Performance (Gflop/s) CPU Saturation GPU Saturation C2070 GPU Saturation K40c cuBLAS SGEMM K40c cuBLAS SGEMM C2070 8 Core CPU MKL SGEMM 1. Performance of compute kernels on CPU and GPU dep lem granularity

How big should a task be?

Tuning the tile size?

• B = "big" tile size, for GPUs

[0][0], inout:B[1][0]) TRSM(A[0][0], B[1][0]) #pragma omp task \ depend(in:A[1][0], in:B[0][0], inout:B[0][1]) GEMM(A[1][0], B[0][0], B[0][1])
...

NumPEx project

•

  of compute kernels on CPU and GPU dep lem granularity How big should a task be? GPUs • Have thousands for cores to feed • Newer generations require yet larger sizes • Can run several kernels at the same time • Still limited https://starpu.gitlabpages.inria.frCan use parallel implementations (e.g. from MKL) • But better have subtasks to interleave them How big should a task be? How size does not fit all Gwenolé Lucas experimented with Chameleon • Cholesky inversion • 2 NVIDIA V100 • 2 Xeon Gold 6142 • Different matrix tile sizes : 2880 / 960 / 320 https://starpu.gitlabpages.inria.fr

•Figure 5 .

 5 Figure 5. Performance for different tile size parameters (DPOTRF, using 1 GPU on Bunsen).

FromFigure 6 .

 6 Figure 6. Performance of h-PaRSEC Cholesky and QR com when both employ the same tile size for kernels executed on

From PARSEC : « Hierarchical DAG Scheduling for Hybrid Distributed Systems », Wu, Bouteiller, Bosilca, Faverge, Dongarra

https://starpu.

How big should a task be?

From CEA : « A hierarchical fast direct solver for distributed memory machines with manycore nodes », Augonnet, Goudin, Kuhn, Lacoste, Namyst, Ramet core (2,620 seconds). We can thus compare the speedup obtained within a KNL in Figure 20. We obtain a parallel ef ciency of 78.2% instead of 49.9% on 64 cores. It is also worth noting that this is very challenging testcase because there is only 56MB of data per core in average when using 64 threads. On the distributed memory side, Figure 22 shows the strong scalability of a sphere testcase with 867000 unknowns on several nodes of TERA1000-1. In addition to the ideal scaling line, three other lines depict the time performances