Guillaume Bonfante
email: bonfante@loria.fr

Course of value distinguishes the intentionality of programming languages

Keywords: H.4 [Information Systems Applications]: Miscellaneous; D.2.8 [Software Engineering]: Metrics-complexity measures, performance measures Theory of computing, theory of complexity and recursion Implicit computational complexity, Space and time resource evaluation, program interpretation

In this contribution, we propose to study the transformation of first order programs by course of value recursion. Our motivation is to show that this transformation provides a separation criterion for the intentionality of sets of programs. As an illustration, we consider two variants of the multiset path ordering, for the first, terms in recursive calls are compared with respect to the subterm property, for the second with respect to embedding. Under a quasi-interpretation, both characterize Ptime, the latter characterization being a new result. Once applied the transformation, we get respectively Ptime and Pspace thus proving that the latter set of programs contains more algorithms.

INTRODUCTION

This paper follows a line opened in [START_REF] Bonfante | Observation of implicit complexity by non confluence[END_REF] where we have shown that transformations of languages could be used to compare sets of programs. Let us come back to the key idea. In the field of implicit computational complexity, when characterizing a set of programs, the intentionality measures the 'quantity' of programs, not the 'quantity' of functions. Indeed, one function may be computed by many programs, possibly efficient. Thus, a set of programs may correspond to a small number of functions but with a large choice of programs. The larger choice, the easier to pick up one program. To show the strength of some theory (which defines a set of programs) one usually exhibit some remarkable example. However, the argument is usually rather weak since one has to compare programs, not functions. We point out the work of Asperti [START_REF] Asperti | The intensional content of rice's theorem[END_REF] who considers such complexity cliques, showing their intrinsic undecidability. See also [START_REF] Bonfante | Quasi-interpretation: a way to control ressources[END_REF] where we proved that characterizing programs computable in Ptime is Σ2-complete.

To avoid such direct comparison of programs, we propose to compare sets of programs via some apparel. Let us suppose for the discussion that a program is a rewriting system, in other words, our study focuses on recursion. Let us suppose that we are given two sets S and S of programs, and that these programs compute the same set U of functions. Suppose that under some transformation (of rewriting systems) T , the two sets T (S) and T (S ) of programs yield different function sets V1 = V2, then, T (S) = T (S ) and consequently S and S cannot be equivalent from an implicit computational complexity point of view: indeed, would they be the same, then T (S) = T (S )! The transformation works as a kind of lens, separating thus indistinguishable programs at the first level.

In [START_REF] Bonfante | Observation of implicit complexity by non confluence[END_REF], we have considered the effect of adding non-determinism to programs. We have shown that this transformation does not add some computational strength to constructorfree programs (see Jones [START_REF] Jones | Logspace and ptime characterized by programming languages[END_REF]) which characterize functions in Ptime. On contrary, applying it on programs with a multi-set path ordering termination proof admitting a quasiinterpretation, one obtains a characterization of Pspace. Then, if Pspace is different from Ptime, we have shown the separation between the two sets of programs. We propose in this paper to consider a (kind of) course-of-value recursion transformation.

Referring to the study of recursive schema [START_REF] Péter | Rekursive Funktionen[END_REF][START_REF] Rose | Subrecursion[END_REF], it is well known that course-of-values recursion, that is functions defined by equations of the shape: f (0, y) = g(y) f (x + 1, y) = h(x, y, f (j1(x), y), . . . , f (j k (x), y) where g, h, j1, . . . , j k are primitive recursive and ji(x) ≤ x for i ∈ {1, . . . , k} , are themselves primitive recursive. A similar remark holds for recursion with parameter substitu-tions as observed by Leivant and Marion in [START_REF] Leivant | Ramified recurrence and computational complexity II: substitution and poly-space[END_REF]: f (0, y) = g(y) f (x + 1, y) = h(x, y, f (x, j1(y)), . . . , f (x, j k (y)))

Leivant and Marion have proved that restricted to safe recursion, primitive recursion with parameter substitution corresponds to the functions computable within Pspace. We will rediscover a similar characterization with courseof-value recursion in Section 4, Theorem 3 [START_REF] Asperti | The intensional content of rice's theorem[END_REF].

As observed by Leivant, notice that the transformation of such recursive schemas into primitive recursion involves an encoding function which, in other terms, means that one uses the exponential function. For the study of classes of low complexity such as Ptime, it is then reasonable to treat both schema apart.

Actually, in the context of rewriting systems, we define a notion that subsumes both schemas. A program has a course-of-value recursive schema if a recursive call contains an argument which is computed by an other function symbol. In other words, there is a rule of the form f (x1, . . . , xn) = C[f (j1(x1), . . . , jn(xn))] for some context functions f, j1, . . . , jn. A typical example of course-of-value is given by the quick-sort recursion:

qs( ) = insert(qs(first-half( )), qs(second-half( )))
for a non empty list . The functions first-half and second-half respectively compute the first half and the second half of the list (with respect to some pivot). These two functions appear as arguments of qs, the quick-sort function.

To prove the termination of recursive programs, one shows that arguments decrease according to some well-founded order. A very large number of such orders have been considered so far. We consider two of them, one based on the subterm relation and one on embedding. We recall that for the subterm relation, one erases some of the leading symbols, while for embedding, the erasing can be done at any point. For instance t1 = a(a(b(ε))) is a subterm of t2 = c(c(a(a(b(ε))))) but not a subterm of t3 = a(a(c(b(ε)))). But t1 is both embedded in t2 and t3. The subterm relation and the embedding relation are well-founded. Thus, if one or more arguments of a recursive call decrease while the others stay unchanged, the program ends.

Is there a main difference between these two orderings? Let us restrict our attention to programs computing functions of polynomial growth (this will be ensured later by the interpretation). In both cases, for programs terminating by means of the subterm relation or the embedding relation, functions computed are the functions of Ptime. We want to stress the fact that the characterization for the path ordering based on the subterm relation already appeared in [START_REF] Bonfante | Quasi-interpretation: a way to control ressources[END_REF], but the one based on embedding is a new result.

But, if one applies course-of-value, the situation is different. In the first case (based on the subterm relation), either with or without course-of-value recursion we stick to functions in Ptime. In the second case, we reach Pspace. To conclude, we have established the non-equivalence of these two sets of programs.

As a matter of fact, as a by-product of our result, we show that adding course-of-value recursion to product-path ordering based on embedding together with a quasi-interpretation shifts the computed functions from Ptime to Pspace, a characterization closed to the one of Leivant and Marion mentioned above.

Section 2 defines the syntax of programs. The reader familiar with rewriting, interpretation and path ordering may directly jump to Section 3 which provides the new characterization of Ptime, namely given by programs with an additive quasi-interpretation and a proof by product-path-ordering based on embedding. Section 4 deals with the course-ofvalue extension of programs.

PROGRAMMING LANGUAGES

As said above, we consider rewriting systems as a model of functional programs. Apart from Definition 2, all the material is standard. We briefly recall the main definitions, essentially to fix some notations. Dershowitz and Jouannaud's survey [START_REF] Dershowitz | Handbook of Theoretical Computer Science[END_REF] of rewriting is a good entry point for beginners.

Let X denotes a (countable) set of variables. A signature is a set of symbols, that is a pair of a name and a natural number, each symbol is referred to by its name. The number is called the symbol's arity. Given a signature Σ, the set of terms over Σ and X is denoted by T (Σ, X ) and the set of ground terms, that is terms without variables, by T (Σ). The size |t| of a term t is defined as the number of symbols in t. For instance, |f (a, f (a, b))| = 5. The height of a term, written ||t||, is the longest path from the root to a leaf. ||f (a, f (a, b))|| = 2. A position is a word in N * . Given a term t, a position q denotes a sub-term t |q by the equations: t |ε = t for the empty wordε

t |q = ti |q if t = f (t1, . . . , tn) and q = i • q
Finally, as a general notation, we use u as a shorthand to denote sequences of terms u1, . . . , un.

Definition 1 (subterm and embedding relations).

The subterm relation is the smallest binary relation, denoted ¢, on terms such that t ¢ t and t ¢ ui t ¢ f (u1, . . . , un) for all terms t, u1, . . . , un and f an n-ary symbol. The embedding relation, denoted , is the smallest relation verifying: t t t ui t f (u1, . . . , un) (ti ui)i=1,...,n f (t1, . . . , tn) f (u1, . . . , un) for all terms t, t1, . . . , tn, u1, . . . , un and f an n-ary symbol.

From the definition, it is clear that ¢ ⊆ , that is for all terms t, v, t ¢ v ⇒ t v. The inclusion is strict as shown by the example: Example 1. Let us suppose that 1, 2, 3, 4, 5, 6 are unary constructors. Then,

1(3(5(•))) 1(2(3(4(5(6(•)))))) 1(3(5(•))) ¢ 1(2(3(4(5(6(•)))))) 4(5(6(•))) ¢ 1(2(3(4(5(6(•)))))) 4(5(6(•))) 1(2(3(4(5(6(•))))))
A context is a term t whose variables occur only once. t[u1, . . . , un] is a shorthand for t[x1 ← u1, . . . , xn ← un] where x1, . . . , xn are the variables of t given in some a priori order. Actually, from the context, no confusion should arise from the variables.

We say that two contexts t1 and t2 are compatible (t1 |com t2) if either t1 or t2 is a variable or t1 = f (u1, • • • , un), t2 = f (v1, • • • , vn) and for all i ≤ n, ui |com vi.

The extension of two compatible contexts t1 and t2, denoted t1 + t2, is defined by:

x + t = t t + x = t f (u1, • • • , un) + f (v1, • • • , vn) = f (u1 + v1, . . . , un + vn)
where x denotes a variable and f is a symbol. In the definition above, we suppose without loss of generality that t1 and t2 do not share variables.

Example 2. For instance, cons(cons(x, y), z) is compatible with cons(u, cons(v, t)). And cons(cons(x, y), z) + cons(u, cons(v, t)) = cons(cons(x, y), cons(v, t)).

Definition 2 (Compatible extension). Given some terms t 1 , t1, t2 such that t 1 t1 and t1 |com t2, the compatible extension of t 1 w.r.t. t2 is defined as the largest term t such that t t1 + t2 and t |com t 1 . It is defined by the following equations.

• ext(t 1 , t1, x) = t 1 and ext(t 1 , x, t2) = t2 whenever x a variable.

• Otherwise, t1 = f (v1, . . . , vn), t2 = f (w1, . . . , wn) and either

-t 1 = t1, then ext(t1, t1, t2) = t1, -or t 1 vi for some i ≤ n, then ext(t 1 , t1, t2) = ext(t 1 , vi, t2), -or vi
wi for all i ≤ n, then ext(t 1 , t1, t2) = f (ext(u1, v1, w1), . . . , ext(un, vn, wn)).

Example 3. Consider for instance the terms cons(x, z) cons(cons(x, y), z) and cons(u, cons(v, t)). We have: ext(cons(x, z), cons(cons(x, y), z), cons(u, cons(v, t)) = cons(x, cons(v, t)). There are positions p1, . . . , p h and indices j1, . . . , j h ≤ m such that for all terms u1, . . . , un, v1, . . . , vm, if t1[u1, . . . , un] = t2[v1, . . . , vm], then

t = t 1 [ui 1 , . . . , ui k ] = ext(t 1 , t1, t2)[vj 1 |p 1 , . . . , vj h |p h ].
Proof. By induction on the definitions.

Syntax of programs

In this subsection, we briefly present rewriting systems, a simple model of functional programming.

In the sequel of the section, we suppose that we are given an algebra of terms given by a (finite) signature C on which computations are done. These terms are called constructor terms, and accordingly, symbols in the signature are called constructor symbols.

Next, we suppose given a set F of function symbols. A rule is a pair ( , r), next written → r, where:

• = f(p1, • • • , pn) where f ∈ F and pi ∈ T (C, X ) for all i = 1, . . . , n,
• and r ∈ T (C ∪ F, X ) is a term such that any variable occuring in r also occurs in .

Definition 3. A program is a quadruplet f = C, F, f, E such that E
is a finite set of rules. We distinguish among F a main function symbol whose name is given by the program name f.

The set of rules induces a rewriting relation written →. The relation * → is the reflexive and transitive closure of → and t ! → u denotes the fact that t * → u and u is a normal form. All along, when it is not explicitly mentioned, we suppose programs to be confluent, that is, the rewriting relation is confluent.

The domain of the computed functions is the constructor term algebra

T (C). The program f = C, F, f, E com- putes a partial function f : T (C) n → T (C) defined as fol- lows. For every u1, • • • , un ∈ T (C), f (u1, • • • , un) = v iff f(u1, • • • , un) ! → v
and v is a constructor term. The notation is extended to terms by composition.

Example 4. Equality on binary words in {0, 1} * , boolean operations, membership in a list (built on cons, nil) are computed as follows.

ε = ε → tt i(x) = i(y) → x = y with i ∈ {0, 1} i(x) = j(y) → ff with i = j ∈ {0, 1} i(x) = ε → ff with i ∈ {0, 1} ε = i(y) → ff with i ∈ {0, 1} not(tt) → ff not(ff) → tt or(tt, y) → tt or(ff, y) → y and(tt, y) → y and(ff, y) → ff if tt then y else z → y if ff then y else z → z
The definitions of a program induce a partial order on symbols, defined as the smallest transitive relation containing g f for all f, g, such that there is a rule f (p1, • • • , pn) → r and g occurs in r. Let ≺ denotes the strict part of and the equivalence relation induced by . The rank is then the equivalence class of a symbol w.r.t. . We define constructors to be symbols of a rank smaller than any other ranks.

Given a program C, F, f, E , we define E <f to be the subset of E restricted to rules g(p1, • • • , pn) → r such that g ≺ f . The rewriting relation → <f denotes the corresponding restriction to E <f . Given a symbol f , we define f (t1, . . . , tn)

→ f u iff f (t1, . . . , tn) → ! <f f (u1, . . . , un) → r → ! <f u.
This notion is known as relative rewriting relation.

Definition 4 (Call-tree). Suppose we are given a program C, F, f, R . Let be the relation

(f, t1, . . . , tn) (g, u1, . . . , um) ⇔ f (t1, . . . , tn) → C[g(w1, . . . , wm)] ∧ ∀i : wi ! → ui
with f and g some defined symbols, and t1, . . . , tn, u1, . . . , um some constructor terms. Given a term f (t1, . . . , tn), the relation defines a tree whose root is (f, t1, . . . , tn) and η is a daughter of η iff η η . The size of a call-tree is the number of nodes it contains.

Example 5. The call tree of 0(1(ε)) = 0(0(ε)) is

(=, 1(0(1(ε))), 1(0(0(ε)))) (=, 0(1(ε)), 0(0(ε))) (=, 1(ε), 0(ε))

Interpretations of programs

The result presented in the following sections are correct whenever all computed functions have polynomial growth rate. However, to ensure that property (see corollary 1) in an effective way, we propose to use interpretations. Other methods could be used.

Given a signature Σ, a Σ-algebra on R is a mappingwhich associates to every n-ary symbol f ∈ Σ an n-ary function f : R n → R. Finally, we restrict the interpretations over the real numbers to be Max-Poly functions, that is functions obtained by finite compositions of the constant functions, maximum, addition and multiplication. In [START_REF] Bonfante | Synthesis of quasi-interpretations[END_REF], we have proved that it is decidable to compute (if it exists!) an interpretation given a program.

Definition 5. Given a program C, F, f, E , let us con- sider a (C ∪ F)-algebra -on R.
The generalized geography game suppose that we are given a direct acyclic graph g, a node r ∈ g. Alternatively, player and opponent play a successor of the current node (player begins with r). The first who can't play (there is no more successors) looses. The question is: "does player has a winning strategy 1 ? Even if the graph is binary, that is each node has at most two successors, the problem is known to be Pspace-complete. The problem is solved by the following program.

1 That is, he cannot loose if playing properly.

Example 6. player(g) → if snd(g) = ε then if fst(g) = ε then ff else not(opp(rem1(g))) else not(and(opp(rem1(g)), opp(rem2(g)))) opp(g) → if snd(g) = ε then if fst(g) = ε then ff else not(opp(rem1(g)))
else not(and(player(rem1(g)), player(rem2(g))))

fst(cons(T (x), )) → fst( )

fst(cons(V (x, y, z), ) → y fst(cons(i(x), )) → fst( ) fst(nil) → ε snd(cons(T (x), )) → snd( ) snd(cons(V (x, y, z), ) → z snd(cons(i(x), )) → snd( ) snd(nil) → ε rem1(g) → goto(rem(g), fst(g)) rem2(g) → goto(rem(g), snd(g)) rem(cons(T (x), )) → cons(T (x), rem( )) rem(cons(V (x, y, z), )) → cons(x, ) rem(cons(i(x), )) → cons(i(x), rem( )) rem(nil) → ε goto(cons(T (V (x, y, z)), , m)) → if m = x then cons(V (x, y, z), ) else cons(T (V (x, y, z)), goto( , m)) goto(cons(V (x, y, z), ), m) → ε goto(cons(i(x), ), m) → cons(i(x), goto( , m)) goto(nil, m) → ε Such a program admits a quasi-interpretation. Set nil = ε = ff = tt = = 1 T (x) = i (x) = = x + 1 cons (x, y) = x + y + 1 V (x, y, z) = x + y + z + 1 with i ∈ {0, 1}. All other n-ary symbols f are mapped to f (x1, . . . , xn) = max(x1, . . . , xn).
At the beginning of the computation, the graph is given by an adjacent list of the form cons(e, ) where denotes the rest of the list and e = T (V (x, y, z)) denotes the (not yet visited) node x with two successors y and z. 2 In the computation process, the current node is denoted by e = V (x, y, z) and a visited node by e = x. Finally, at the beginning of the computation, the root node is supposed to be denoted by V (r, y, z) with y and z its successors.

Few notes on the program. fst(g) (respectively snd) computes the first (resp. second) successor of the current node. goto(g, m) puts m as the current node of g, rem1(g) removes the current node and puts its first successor as the current node. rem2(g) is analogous. rem(g) marks the current node as a visited node. Definition 6. The interpretation of a symbol f is said to be additive if it has the shape i xi + c for some constant c ≥ 1. A program with an interpretation is said to be additive when its constructors are additive.

For instance, the program given in Example 6 is additive. We recall a proposition and a corollary taken from [START_REF] Bonfante | Quasi-interpretation: a way to control ressources[END_REF]: Proposition 3. Let C, F, f, E be a program with an additive quasi-interpretation. Then, there is a constant K > 0 such that t ≤ K × |t| for all constructor terms t ∈ T (C).

Given a program with an additive quasi-interpretation, suppose that u1, . . . , un ∈ T (C). Whenever t[u1, . . . , un] * → v with v ∈ T (C), then |v| ≤ t(u1, . . . , un) . So, the size of the outputs of programs is directly linked to the value of the initial interpretation. For additive programs, Proposition 3 leads to |v| ≤ t (K|u1|, . . . , K|un|). Consequently, Corollary 1. The output of additive program has a polynomial size w.r.t. to its corresponding input.

Termination proofs

Proving the termination of a program is a very common issue of software engineering. Many methods have been considered so far, and we are considering one of the most simple, namely path orderings which are decidable simplification orderings. The proof of the well-foundedness of ≺mpo is due to Dershowitz [START_REF] Dershowitz | Orderings for term-rewriting systems[END_REF] and Kamin and Levy [START_REF] Kamin | Attempts for generalising the recursive path orderings[END_REF] and relies on Kruskal theorem. An formalized proof of the wellfoundedness of the multiset path ordering by Coupet-Grimal and Delobel can be found in [START_REF] Coupet-Grimal | An effective proof of the well-foundedness of the multiset path ordering[END_REF].

A precedence F (strict precedence ≺F ) is a quasi-ordering (strict partial ordering) on a given set F of function symbols. We define the equivalence relation ≈F as f ≈F g iff f F g and g F f. This precedence F on function symbols extends canonically to C ∪F with the following relations ∀f ∈ F , ∀c ∈ C, c ≺F f. Definition 7. Given an ordering ≺ on terms, its product extension ≺ over sequences (of equal length) is defined by:

(m1, • • • , m k ) ≺ (n1, • • • , n k ) if and only if (i) ∀i ≤ k, mi ni and (ii) ∃j ≤ k such that mj ≺ nj.
It is clear that if the ordering ≺ on terms is well-founded, then its extension to sequences is also well-founded. This is the core point of the following ordering. Definition 8. Given a program C, F, f, E and a precedence F , we define the subterm product path ordering ≺ ¢ mpo by the rules of Figure 1. A program is ordered by ≺ ¢ mpo iff there is a precedence F such that for each rule l → r, the inequality r ≺ ¢ mpo l holds.

Remark 1. The product path ordering is closed under substitutions and context.

Example 7. The program of Example 4 can be ordered by product path ordering. Set ≺ to be or ≺ and ≺ not ≺=≺ it-the-else ≺ in.

However, Example 6 cannot be ordered by the ordering. As we will see later, this is due to the rule player(g) → if snd(g) = ε then if fst(g) = ε then ff else not(opp(rem1(g))) else not(and(opp(rem1(g)), opp(rem2(g)))).

Definition 9. The embedding product path ordering ≺ mpo is defined in exactly the same manner, but with constructors compared as in Figure 2.

Since the subterm relation is included in the embedding relation, it is clear that programs ordered by P P O ¢ are ordered by P P O .

The main difference between P P O ¢ and P P O is that t ≺ ¢ mpo u iff t ¡ u for all constructor terms t, u. For P P O , we get a larger set t ≺ mpo u iff t u. As a consequence, a rule such as:

f (1(0(x))) → f (1(x))
is not compatible with ≺ ¢ mpo but it is compatible with ≺ mpo.

CHARACTERIZATIONS OF PROGRAMS

In this section, we address the following problem. Is there a fundamental difference between the two product path orderings? We answer to the question by a characterization of the functions computed by means of the two orderings. Let us begin recalling the following theorem, Theorem 1. [Bonfante, Marion and Moyen [START_REF] Bonfante | Quasi-interpretation: a way to control ressources[END_REF]] Functions computed by programs with an additive quasi-interpretation and a termination proof by P P O ¢ are exactly Ptime functions.

Actually, it is safe to replace P P O ¢ by P P O as shown by the Theorem: Theorem 2. Functions computed by programs with an additive quasi-interpretation and a termination proof by P P O are exactly Ptime functions.

Since programs ordered by P P O ¢ are ordered by P P O , it is immediate that Ptime functions can be computed by programs ordered by P P O with an additive quasi-interpretation. So, the issue is to prove that the converse holds.

The main issue with the embedding relation is that the set of terms Ut = {u | u ≺ mpo t} does not have a polynomial size w.r.t. the size of the constructor term t. This property is a key feature used in the proof of [START_REF] Bonfante | Quasi-interpretation: a way to control ressources[END_REF] to apply memoisation. For the embedding relation, one may observe that all the sequences of booleans of size n verify:

{0, 1} n ⊂ U 01 • • • 01 n times . Thus, |U 01 • • • 01 n times
| ≥ 2 n leads to an exponential lower bound. This is bad news.

The remaining of the Section is devoted to the proof of Theorem 2. The core point of the proof is to show that actually, when evaluating f (t1, . . . , tn) for some constructor terms t1, . . . , tn, not all the terms f (u1, . . . , un) with u1 t1, . . . , un tn will be evaluated, only a polynomial number of them. This is Proposition 6. After this crucial step, the proof follows the line of the proof of Theorem 1 in [START_REF] Bonfante | Quasi-interpretation: a way to control ressources[END_REF].

s t s ≺ ¢ mpo t s, t ∈ T (C) s ¢ mpo ti s ≺ ¢ mpo f (. . . , ti, . . .) f ∈ F C ∀i ≤ n : si ≺ ¢ mpo f (t1, • • • , tn) g ≺F f g(s1, • • • , sm) ≺ ¢ mpo f(t1, • • • , tn) g ∈ F C, f ∈ F (s1, • • • , sn) ≺ ¢ mpo (t1, • • • , tn) f ≈F g g(s1, • • • , sn) ≺ ¢ mpo f(t1, • • • , tn) g, f ∈ F Figure 1:
The subterm product path ordering 1. For each constructor terms t and s, s ≺ mpo t iff s t.

s t s ≺ mpo t s, t ∈ T (C) s mpo ti s ≺ mpo f (. . . , ti, . . .) f ∈ F C ∀i ≤ n : si ≺ mpo f (t1, • • • , tn) g ≺F f g(s1, • • • , sm) ≺ mpo f(t1, • • • , tn) g ∈ F C, f ∈ F (s1, • • • , sn) ≺ mpo (t1, • • • , tn) f ≈F g g(s1, • • • , sn) ≺ mpo f(t1, • • • , tn) g, f ∈ F
2. If t is a constructor term and u contains a function symbol, then u ≺ mpo t.

Proof. The proof is by induction on the definition of the path ordering.

Proposition 5. For all rules f (p1, • • • , pn) → r, there is a context C such that

• r = C[f1( u1), . . . , f k ( u k )],
• C does not contain any symbol of rank of f , • f1, . . . , f k have the rank of f ,

• the ui's are constructor terms.

Proof. We define C to be the largest context such that r = C[t1, . . . , tn] and

• C does not contain any symbol of rank of f

• for all i, ti = fi( ui) with fi of rank of f .

The key point is to verify that the ui's are actually sequences of constructor terms. Let us remind that the patterns p1, . . . , pn are themselves constructor terms. Notice also that for all i ≤ n, since ti = fi( ui) mpo r ≺ mpo f (p1, • • • , pn), it is necessarily the case that ( ui) ≺ mpo ( p). Then, by definition ui pi for all i ≤ n and consequently, by Proposition 4 (2), the ui's contain no function symbols. Proposition 6. There is a finite set of terms Θ such that:

• for all symbol f ∈ F ,

• for all constructor terms t1, . . . , tn,

• for all constructor terms u1, . . . , u k ,

• for all function symbol g of rank of f such that f (t1, . . . , tn)

* → C[g(u1, . . . , u k )],
• for all i ≤ k, there is an element e ∈ Θ, some positions q1, . . . , q h and some indices i1, . . . , i h such that ui = e[ti 1 |q 1 , . . . , ti h |q h ].

Proof. Let Θ be the following set.

• x ∈ Θ,
• for all f (p1, • • • , pn) → r, for all i ≤ n, pi ∈ Θ,

• for all q, r ∈ Θ, for all p q, ext(p, q, r) ∈ Θ.

This set is finite. Indeed, the height ||ext(p, q, r)

|| ≤ max(||p||, ||r||), so that Θ ⊆ {v | ||v|| ≤ d} with d = max{||pi|| | f (p1, • • • , pn) → r ∈ R}.
Now, we proceed by induction on the length of the derivation.

For the base case, f (t1,

• • • , tn) * → f (t1, • • • , tn), the result is trivial (take e = x, q = ε). Otherwise, f (t1, • • • , tn) * → C[g(u1, • • • , un)] → C[C [h(v1, • • • , vn)]] af- ter application of the rule g(p1, • • • , pn) → C [h(s1, • • • , sn)]
with the substitution σ. That is, ui = piσ and vi = siσ with i ≤ n. By Proposition 4, si pj for some j and vi = si[σ(xj 1 ), . . . , σ(xj )] for the set xj 1 , . . . , xj of the variables of si, that is a subset of the variable of pi. By induction, we can state that ui = pi[σ(x1), . . . , σ(x )] = e[ti 1 |q 1 , . . . , ti h |q h ] for some e ∈ Θ and some positions q1, . . . , q h and indices i1, . . . , i h . Notice that pi ∈ Θ, and since si pi, ext(si, pi, e) ∈ Θ. According to Proposition 2, there are positions r1, . . . , r h and indices j1, . . . , j h such that: vi = ext(si, pi, e)[tj 1 |q j 1 .r 1 , . . . , tj h |q j h .r h ] Since ext(si, pi, e) ∈ Θ), we have the desired property.

Corollary 2. Given a program C, F, f, E ordered by P P O , f ∈ F and constructor terms t1, . . . , tn, we denote by T (f,t 1 ,...,tn) the call tree rooted by (f, t1, . . . , tn) and by R (f,t 1 ,...,tn) the subset of nodes (g, u1, . . . , um) ∈ T (f,t 1 ,...,tn) such that g f . There is a polynomial P such that: |R (f,t 1 ,...,tn) | ≤ P (max(|t1|, . . . , |tn|)).

Proof. As seen above, if (g, u1, . . . , um) ∈ R (f,t 1 ,...,tn) , then for all i ≤ m, ui = e[ti 1 |q 1 , . . . , ti h |q h ] for some e ∈ Θ as defined above. One may observe that the number of positions for each qi is bounded by i |ti|. Let d be the maximal arity of the contexts e ∈ Θ. Without loss of generality, we suppose d to be greater than the arity of any symbols in F. We conclude, taking

P (x) = |F| × |Θ| × (d × x) 2d .
Lemma 1. Let f be a functional program with an additive quasi-interpretation. Then, there is a polynomial Qf such that for any equation → r and all e r, | e (t1, . . . , tn)| ≤ Q(max(|t1|, . . . , |tn|)) with t1, . . . , tn constructor terms.

Proof. It is proved by induction on the structure of e, using Corollary 1.

Proof Theorem 2. A naive implementation would lead to an exponential number of function calls. This issue is easily skipped if we switch from a call-by-value semantics to a call-by-value semantics with cache, see Figure 3. In the definition, we set S to be the set of substitutions whose range is a subset of constructor terms. This technique is very common in algorithmic studies, it is known as dynamic programming, a technique inspired from Andersen and Jones' rereading (cf. [START_REF] Andersen | Generalizing cook's transformation to imperative stack programs[END_REF]) of a simulation technique over 2 way push-down automata by Cook (see [START_REF] Cook | Characterizations of pushdown machines in terms of time-bounded computers[END_REF]) also known as memoization.

Our general purpose is to show that the size of the cache remains polynomial w.r.t. the size of the input, that is

• there is a polynomial number of entries and

• each entry has polynomial size, in other words:

the size of the arguments of calls are polynomial the size of output terms is polynomial Since each step of the call-by-value semantics with cache can be performed in polynomial (actually linear) time w.r.t. the size of the cache, the items above are sufficient to ensure that the computation can be done in polynomial time.

Actually, one must also note that functions computed by additive program have output of polynomial size w.r.t. their inputs (Corollary 1). Consequently, to ensure that the cache has polynomial size, one only need to verify that arguments of function calls in the cache have polynomial size.

We will proceed by induction on the rank of symbols, and consequently, we provide a polynomial P f to bound the size of the cache of the function f , depending only on the rank of f . Without loss of generality, we can suppose that

P f ≥ Pg if g ≺ f .
First, let us define D to be the maximal arity of functions, A to be the number of function symbols and R to be the maximal size of the right-hand side of a rule. Finally, let us suppose we want to compute f (t1, . . . , tn). Elements in the cache will be terms g(u1, . . . , um) such that f (t1, . . . , tn) * → C[g(u1, . . . , um)]. Consequently, g has rank smaller or equal to the rank of f .

Base case.

Consider the evaluation of functions with minimal rank. Let us consider such a function f . Suppose that we are given a term f (t1, . . . , tn). Consider a term g(u1, . . . , um) in the cache, since g has rank equivalent to the one of f , by Corollary 2, there are at most PD(max(|t1|, . . . , |tn|)) such nodes. Due to Proposition 4(1), each of these argument has size bounded by max(|t1|, . . . , |tn|). We set accordingly the polynomial P f (x) = x × PD(x).

Induction step.

Now, suppose f being of a higher rank. Suppose we want to compute f (t1, . . . , tn). Consider its call-tree T f (t 1 ,...,tn) . There is actually a bijection between the set S (f,t 1 ,...,tn) = {(g, v1, . . . , vn) | (g, v1, . . . , vn) ∈ T (f,t 1 ,...,tn) } and the set of entries in the cache Cache f (t 1 ,...,tn) . Each element of the cache (g, v1, . . . , v k , v) ∈ Cache (f,t 1 ,...,tn) corresponds to some node (g, v1, . . . , v k ) ∈ T (f,t 1 ,...,tn) . To sum up, it is sufficient to count the number of elements in S (f,t 1 ,...,tn) verifying that their arguments have polynomial size.

Suppose that f (t1, . . . , tn) * → C[g(u1, . . . , um)] with g of equal rank to the one of f . Again, by Proposition 2, there are only P (max(|t1|, . . . , |tn|)) entries in the cache for some polynomial P . Each of these arguments having size smaller than max(|t1|, . . . , |tn|) by embedding.

So, the main issue is to evaluate the number of entries in the cache involving functions of smaller rank. Let Y f be the following binary relation. (g, v1, . . . , v k ) Y f (h, w1, . . . , wm) holds iff g has the rank of f and there exists some function symbol h ≺ f and some terms w 1 , . . . , w k such that

(g, v1, . . . , v k ) Y (h , w 1 , . . . , w k ) Y * (h, w1, . . . , w ).
One may observe that (g, u) Y f (h, v) implies that h ≺ f . Let D (g,u 1 ,...,u k ) = {(h, w1, . . . , w ) | (g, v1, . . . , v k ) Y f (h, w1, . . . , w )}. The elements in S (f,t 1 ,...,tn) splits as follows: S (f,t 1 ,...,tn) = R (f,t 1 ,...,tn) ∪ (g, u)∈R (f,t 1 ,...,tn) D (g, u) .

(

) 1
Let us compute the size of D (g,u 1 ,...,um) for some node (g, u1, . . . , um) ∈ R (f,t 1 ,...,tn) . The relation Y f can be reformulated as (g, u1, . . . , um) Y f (h, w1, . . . , w k ) iff one of the two statement holds:

(g, u) Y (h, w) ∧ h ≺ f (2) (g, u) Y (h , u ) Y f (h, w) with h ≺ f (3)
Let G (g,u 1 ,...,um) denotes the set of nodes verifying Equation [START_REF] Asperti | The intensional content of rice's theorem[END_REF]. Let us consider a node (h, w1, . . . , w k ) ∈ G (g,u 1 ,...,um) . Let us make the hypothesis (which we prove a little bit further) that there is a polynomial Q such that for all i ≤ k, we have |wi| ≤ Q(max(|t1|, . . . , |tn|)). Then, by induction, the cache corresponding to the computation of h(w1, . . . , w k ) is bounded by P h (Q(max(|t1|, . . . , |tn|))). Consequently, the size of D (g,u 1 ,...,um) is bounded by (h,w 1 ,...,w k )∈G (g,u 1 ,...,um ) P h (Q(max(|t1|, . . . , |tn|))).

Recall that |G (g,u 1 ,...,um) | ≤ R. Consequently, taking PH a polynomial bounding P h for all such h, we get the bound Recalling Equation ( 1), we can state that the cache of f (t1, . . . , tn) is bounded by

|D (g,u 1 ,...,um) | ≤ R × PH (Q(max(|t1|, . . . , |tn|))). (Constructor) c ∈ C Ci-1, ti ⇓c Ci, vi C0, c(t1, • • • , tn) ⇓c Cn, c(v1, • • • , vn) (Read) Ci-1, ti ⇓c Ci, vi (f, v1, • • • , vn, v) ∈ Cn C0, f(t1, • • • , tn) ⇓c Cn, v (Update) Ci-1, ti ⇓c Ci, vi f(p1, • • • , pn) → r ∈ E σ ∈ S piσ = vi Cn, rσ ⇓c C, v C0, f(t1, • • • , tn) ⇓c C ∪ (f, v1, • • • , vn, v), v
P (max(|t1|, . . . , |tn|)) × (1 + R × PH (Q(max(|t1|, . . . , |tn|))))
which is a polynomial in max(|t1|, . . . , |tn|), thus completing the induction.

So, it remains to prove the existence of Q as defined above. Recalling the definition of Y, for all (h, w1, . . . , w k ) ∈ G (g,u 1 ,...,um) , we have g(u1, . . . , um) → rσ = C[h(e1, . . . , e k )]σ for some context C and some terms ei with eiσ ! → wi. Observe that terms in the range of σ have size bounded by max(|u1| . . . , |um|), themselves bounded by max(|t1|, . . . , |tn|). So, employing Lemma 1, we can state that eiσ has size polynomially bounded by Qe i (max(|t1|, . . . , |tn|)). Since there are only finitely many (there are finitely many rules) such ei, the proof is done.

COURSE OF VALUE EXTENSION

In this section, we suppose that we have a well-founded partial ordering < on terms which is closed by substitution and context, think of < has ≺ ¢ mpo or ≺ mpo. 3 Let us suppose that a theory T is defined as the set of program such that for all rules → r, > r. The ordering being closed by context and substitution, u → v implies u > v thus leading to termination.

Definition 10. The course-of-value (cov) extension of T induced by a relation > is the set of programs such that for all terms u1, . . . , un, f (u1, . . . , un) → f r implies f (u1, . . . , un) > r.

By induction on the rank of symbols, it is easy to prove that such a property provides termination (one may observe that the property is actually a weak form of termination proof by dependency pairs. A good complexity analysis in the context of depedency pairs has been done by Hirokawa and Moser [START_REF] Hirokawa | Automated complexity analysis based on the dependency pair method[END_REF]).

We can presently state our second main theorem:

Theorem 3.

1. Functions computed by cov-programs with an additive quasi-interpretation and a termination proof by P P O ¢ are exactly Ptime functions.

3 A reminder for the reader: Remark 1.

2. Functions computed by cov-programs with an additive quasi-interpretation and a termination proof by P P O are exactly Pspace functions.

The theorem can be interpreted as follows. Even if P P O ¢ and P P O characterize the same class of functions (namely Ptime), they contain different algorithms. In other words, we gave an indirect proof of an essential difference between the two program sets.

One may observe first that the program of the generalized geography given in Example 6 cannot be proven terminating within P P O ¢ . The issue comes from the rule4 player(g) → if snd(g) = ε then if fst(g) = ε then ff else not(opp(rem1(g))) else not(and(opp(rem1(g)), opp(rem2(g)))).

It cannot be ordered by P P O ¢ even with course-of-value extension. Indeed, player(g) cannot be compared to opp(rem1(g)).

But even rem1 (g) cannot be compared to the term g whatever the constructor term g. Consider for instance the term rem1(cons(T (V (1(ε), ε, ε)), cons(V (0(ε), 1(ε), ε), nil))). We have

rem1 (cons(T (V (1(ε), ε, ε)), cons(V (0(ε), 1(ε), ε), nil))) = cons(V (1(ε), 0(ε), ε), cons(0(ε), nil)) but cons(V (1(ε), 0(ε), ε), cons(0(ε), nil)) ¢ cons(T (V (1(ε), ε, ε)), cons(V (0(ε), 1(ε), ε), nil)).
However, it is clear that

cons(V (1(ε), 0(ε), ε), cons(0(ε), nil)) cons(T (V (1(ε), ε, ε)), cons(V (0(ε), 1(ε), ε), nil))
and more generally speaking, it is obvious that rem1 (g) is embedded in g! Thus, the relation →player can be ordered by P P O . More generally, we will see that the program can be ordered by cov-P P O .

Proof of Theorem 3

The end of the section is devoted to the proof of the Theorem.

Since program with an additive quasi-interpretation and a termination proof by P P O ¢ are part of cov-programs with an additive quasi-interpretation and a termination proof by P P O ¢ , it is clear that these latter program contain at least all Ptime functions. Thus, the first item of the Theorem is a direct corollary of the following proposition: Proposition 7. Functions computed by cov-programs with an additive quasi-interpretation and a termination proof by P P O ¢ can be computed in polynomial time.

Proof. The proof goes by induction on the rank of symbols. It is actually an adaptation of the Lemma 44 in [START_REF] Bonfante | Quasi-interpretation: a way to control ressources[END_REF]. The main issue is to prove that the number of entries in the cache remain polynomial. Consider a rule application f (p1, • • • , pn)σ → rσ with a constructor substitution σ. Let us consider g of rank of f such that r = C[g(q1, . . . , qn)]. According to the ordering, qiσ ! → v implies that v ≺ ¢ mpo piσ. Thus, recursive calls corresponding to symbols of rank of f are done on terms which are subterms of the input terms.

At that point, we essentially recovered the properties we had for programs with a standard proof of termination by P P O ¢ . We recall that there are at most i=1,...,n |ti| constructor terms that are subterms of t1, . . . , tn. Thus, there are at most ( i=1,...,n |ti|) d entries in the cache where d is the maximal arity of symbols. We define S(x) = (d × x) d . One may observe that there are at most S(max(|t1|, . . . , |tn|)) entries in R (f,t 1 ,...,tn) with the notation R as in the section above.

Function calls corresponding to symbols of lower ranks can be treated as in [START_REF] Bonfante | Quasi-interpretation: a way to control ressources[END_REF]. Due to the subterm property, we can state that f (t1, . . . , tn) * → C[g(u1, . . . , um)] for some constructor terms t1, . . . , tn, u1, . . . , um implies the inequality g(u1, . . . , um) ≤ f (t1, . . . , tn) . Then, |g(u1, . . . , um)| ≤ f (t1, . . . , tn) ≤ P f (max(|t1|, . . . , |tn|)) where the latter inequality comes from Proposition 3. Thus, inputs of subcalls have polynomial size with respect to the size of the inputs, say Q(x).

To end the induction, suppose that the function calls of symbols of lower rank needs a cache of size P (x) where x is the size of the input. Then, each of the calls fired by symbols of rank of f can be performed in P (Q(x)) which is a polynomial. To sum up, the tree has size S(x) × P (Q(x)) where x denotes the size of the input.

For the second statement of the Theorem 3, we define T to the be set of programs with a termination proof by P P O having a quasi-interpretation. The easiest part is to prove the completeness with respect to Pspace. To justify this, let us observe that the program of the generalized geography given in Example 6 is actually a cov-program with an additive quasi-interpretation and a termination proof by P P O . Indeed, it has a quasi-interpretation. And clearly, the fact that rem1 (g) g shows that the program is catched by P P O . Set the precedence to be the rank relation on symbols.

From this completeness result, the fact that Ptime functions can be computed in T , that T is closed by composition, it is tedious, but not difficult to prove that all Pspace predicates can be computed by cov-program with an additive quasi-interpretation and a termination proof by P P O .

In the other direction, the proof is done by induction on the rank of symbols. The principle is to show that the height of the call tree is bounded by a polynomial. Thus, the evaluation can be performed by a Parallel Random Access Machine (PRAM) running in polynomial time. Then, following Chandra, Kozen and Stockmeyer [START_REF] Chandra | [END_REF], we can state the the computation can be done in polynomial space.

Consider, within some computation, a rule application f (p1, • • • , pn)σ → C[g(u1, . . . , um)]σ with g of rank of f and σ a constructor substitution. Consider the normal forms uiσ ! → vi. By definition of the ordering, for all i ≤ n, vi piσ and for one of them vj piσ. Consequently, the size of one of the inputs is decreased by at least one, the other being not bigger. Consequently, the depth of the function calls of rank of f is bounded linearly by the size of the input.

We can actually go back to the proof of Theorem 2 and do exactly the same induction on symbol's rank, but replacing the size of the call tree by its depth. For symbols of lower rank, we use the trick above: these calls are polynomial and involve arguments of polynomial size. It is then routine to verify that globally the call tree has polynomial depth.

CONCLUSION

At first sight, we could have concluded that termination proofs by sub-term or embedding correspond to the same set of algorithms. This can be justified by Theorems 1 and 2. But, as Theorem 3 shows it, this is only a partial view on sets of programs. One knows that there are several ways to compute functions, by a lot of programs. The skill of programmers is to find the right one. Thus, it is important that tools performing resource analysis are as wide as possible. We have shown that a tool based on embedding is more powerful than a tool based on the subterm relation. It would be nice to draw a general map of termination tools with such methods. To discriminate two sets of programs, we shifted the problem from a direct comparison of two programs to an indirect one. It seems that the latter is much easier in practice.

Figure 2 :

 2 Figure 2: The embedded product path ordering

Figure 3 :

 3 Figure 3: Call-by-value interpreter with Cache of C, F, f, E .

  Given a term t 1 t1, let xi 1 , . . . , xi k be the subset of variables in t 1 occuring in t1.

	Proposition 1. Given a term t and two contexts t1[x1, . . . , xn],
	t2[y1, . . . , ym] such that t = t1[u1, . . . , un] = t2[v1, . . . , vm],
	then t1 and t2 are compatible.
	Proof. By induction on the definition.
	Proposition 2. Let us suppose given two compatible con-
	texts t1[x1, . . . , xn], t2[y1, . . . , ym].

If x has one successor, z is supposed to be ε, if it has zero successor, then y = z = ε.

Which is typically a course-of-value/parameter substitutions recursion schema.

* Work partially supported by project ANR-08-BLANC-0211-03 (COMPLICE) and by EA Cristal.


Olha Nahorna

Frédéric Berthommier
email: frederic.berthommier@gipsa-lab.grenoble-inp.fr

Jean-Luc Schwartz

Binding and unbinding the McGurk effect in audiovisual speech fusion: Follow-up experiments on a new paradigm

Keywords: Audio : Video : Audio Coherent McGurk effect, binding, multisensory fusion, audiovisual speech perception, audiovisual scene analysis

The McGurk effect demonstrates the existence of a fusion process in audiovisual speech perception: the combination of the sound "ba" with the face of a speaker who pronounces "ga" is frequently perceived as "da". We assume that in the upstream of this phonetic fusion process, there is a "binding" process, which controls the combination of image and sound, and can block or reduce it in the case of audiovisual incoherencies (conditional binding process), as in the case of a dubbed film. To test and explore this binding hypothesis, we designed various experiments in which a coherent or incoherent audiovisual context is placed before McGurk stimuli, and we show that the incoherent contextual stimulus can significantly reduce the McGurk effect.

INTRODUCTION

In the McGurk effect, fusion between the sound and the image has long been considered as automatic [START_REF] Massaro | Speech perception by ear and eye[END_REF] [START_REF] Soto-Faraco | Assessing automaticity in audiovisual speech integration: evidence from the speeded classification task[END_REF]. This is now questioned in recent experiments showing that imposing high demands on the attention system decreases the amount of audiovisual fusion [START_REF] Alsius | Audiovisual integration of speech falters under high attention demands[END_REF] [START_REF] Bibliography Alsius | Attention to touch weakens audiovisual speech integration[END_REF] While evidence for the non-automaticity of the fusion mechanism stays compatible with a one-stage architecture, some data suggest that audiovisual interactions could intervene at various stages in the speech decoding process [START_REF] Grant | The use of visible speech cues for improving auditory detection of spoken sentences[END_REF] [START_REF] Kim | Investigating the audiovisual detection advantage[END_REF]) (van Wassenhove, Grant, & Poeppel, 2005) [START_REF] Bernstein | Audiovisual speech binding: convergence or association?[END_REF] [START_REF] Bernstein | Spatiotemporal dynamics of audiovisual speech processing[END_REF] [START_REF] Bernstein | Auditory speech detection in noise enhanced by lipreading[END_REF]. Actually, audiovisual fusion could be conceived as a two-stage process, beginning by binding together the appropriate pieces of audio and video information, followed by integration per se [START_REF] Berthommier | A phonetically neutral model of the low-level audiovisual interaction[END_REF]. The binding stage would occur early in the audiovisual speech processing chain enabling the listener to extract and group together the adequate cues in the auditory and visual streams, exploiting coherence in the dynamics of the sound and sight of the speech input.

PRELIMINARY EXPERIMENTS

In a preliminary experiment presented in AVSP 2010 [START_REF] Nahorna | Binding and unbinding in audiovisual speech fusion: Removing the McGurk effect by an incoherent preceding audiovisual context[END_REF], we proposed an original paradigm to test this idea and attempt to show the existence of a binding process able to modulate audiovisual fusion. In this paradigm, incongruent "McGurk" targets (A/ba/ + V/ga/) or congruent "ba" (A/ba/ + V/ba/) targets are preceded by coherent or incoherent audiovisual contexts (Fig. 1).

Figure 1: Experimental paradigm

Two contextual audiovisual stimuli (either coherent or not) precede two target audiovisual stimuli (a congruent audiovisual " ba " or a McGurk stimulus combining an audio " ba " with a visual " ga "). The coherent context consists of a sequence of 5, 10, 15 or 20 syllables randomly selected within {" pa ", " ta ", " va ", " fa ", " za ", " sa ", " ka ", " ra ", " la ", " ja ", " cha ", " ma ", " na "}. In the incoherent context, the auditory content is the same, but the visual content is replaced by a series of sentences matched in global duration. The results showed the almost complete elimination of the McGurk effect in the case of incoherent contexts (Fig. 2).

A second experiment aimed to check if a short 200-ms audiovisual alert introduced in the coherent or incoherent contexts just before (280 ms) "McGurk" targets could result in focusing the attention of the subject and hence remove the effect of the incoherent context and reset the McGurk effect at its initial stage. It appeared that the alert had actually no effect at all: the effect of the incoherent context remained exactly the same whether the alert was present or not (Fig. 3).

CONTROL EXPERIMENTS AND VALIDATION

OF THE EFFECT

In the preparation of Experiments 1 and 2 we controlled congruent "ba" and incongruent "McGurk" stimuli in terms of labial dynamics and acoustical intensity, but we had not checked by perception tests if there could exist fine differences in stimuli whether they were extracted from the coherent or incoherent material. Particularly, the visual "ga" stimulus incorporated in the "McGurk" targets was extracted, in the incoherent context case, from sentence material, and in the coherent context case, from sequences of syllables. Therefore we designed a third experiment assessing the perceptual content of pure targets without context. The congruent "ba" and incongruent "McGurk" targets used in experiment 1 and 2, trimmed 80ms before burst onset, were presented to the subjects in random order. It appeared that though "McGurk" targets produced a strong McGurk effect whatever the stimuli (either coming from the coherent, or from the incoherent context), there were small but significant differences between the targets recorded after coherent or incoherent contexts. Indeed, the McGurk effect was slightly less with targets coming from the incoherent context material, which could have influenced the validity of our conclusions after Experiments 1 and 2.

Therefore we prepared a fourth experiment, where we used only targets recorded with coherent contexts. For this aim, we exploited the finding of Experiment 2 showing that the context effect seemed to resist an alert pointing to the target location in time. In Experiment 4, we used exactly the same contextual stimuli as in Experiment 1, but targets consisted of "ba" and "McGurk" stimuli extracted only from the coherent context (that is, corresponding in the visual stream to sequences of syllables, as in the audio stream). For this purpose, a fixed set of target stimuli (comprising "ba" and "McGurk" stimuli) was cut and placed at the end of the coherent and incoherent context sequences of Experiment 1. Since there was no more continuity between the end of the context stimulus and the onset of the target stimulus, we introduced a 200-ms transition stimulus between context and target, considering that this transition, possibly providing a visible "alert", would probably not remove the potential unbinding effect with incoherent contexts. The same set of target stimuli was used for both contexts and for all context durations. The results confirmed that an incoherent context reduces the McGurk effect (Fig. 4), though reduction was not complete in this case, either because of a better control of the targets, or because of the mounting procedure, which could, in spite of the results of Experiment 2, have slightly decreased the "unbinding" effect produced by the incoherent context.

Coherent context

FURTHER EXPERIMENTS ON THE ROLE OF

CONTEXT

Now it seems clear that an incoherent context decreases the amplitude of the McGurk effect. In a last experiment, we attempted to better understand what kind of incoherence was necessary to produce this reduction in the McGurk effect. For this aim, we tested smaller kinds of incoherencies, in which the audio and visual contents of incoherent contexts were both made of syllables (while the visual content of the incoherent context was made of sentences in Experiments 1, 2 and 3). We kept intact the visual track, and we applied various modifications on the audio track in the context material.

In a first manipulation (phonetically inconsistent context, P), we permutated the audio content from one syllable to the other. To maximize the chance that the audio-visual incoherence would indeed be perceivable for each context syllable, syllables were firstly organised in five groups known to be visually rather distinguishable (visemes), then the audio content of each syllable was permutated with the content of a syllable from a different group.

In a second manipulation (temporally incoherent context, T), we slightly advanced or delayed each audio syllable at random from 30ms audio lead to 170ms audio lag. This was aimed at staying within an "integration window" (Van Wassenhove, Grant, & Poeppel, 2007) in which the McGurk effect has been shown to hardly vary. In the last incoherent context (PT), both phonetic and temporal manipulations were applied, in exactly the same way respectively as the two previous contexts.

The results are displayed in Fig. 5. They show a reduction in the McGurk effect in the P context and to a lesser extent in the T context, and an even larger reduction in the PT context. A three-factor ANOVA was computed with the factors "subject", "target" and "context". The three factors produce highly significant effects (p<0.0001).

Focussing on the stimuli of interest that are the McGurk targets (the congruent ones being only a control), a second three-factor ANOVA was computed with the factors "subject", "phonetic incoherence" and "temporal incoherence", considering that the four contexts (coherent, P, T and PT) could be decomposed into these two factors. The results show that the three factors are significant, and particularly the phonetic incoherence (p<0.0001) and the temporal incoherence (p<0.02), with no interaction between the two factors (p>0.8). Percentage of " ba " responses for " ba " (in dark grey) and " McGurk " (in light grey) stimuli, in the coherent (C) vs. phonetically incoherent (P), temporally incoherent (T) and phonetically and temporally incoherent (PT) contexts.

Coherent

DISCUSSION

All these experiments converge to show that McGurk fusion depends on the previous audiovisual context. This suggests that the coherence vs. incoherence of the audio and video streams could lead the subject to selectively increase vs. decrease the role of the visual input in the fusion process.

The existence of a two-stage process has long been introduced in auditory perception through "Auditory Scene Analysis", with a first binding stage grouping together the auditory components of a given acoustic source, before categorisation processes could be applied on this source [START_REF] Bregman | Auditory scene analysis[END_REF]. The present paper extends this idea towards "Audiovisual Speech Scene Analysis". It is classically considered that the Auditory Scene Analysis process involves a default grouping stage followed by a possible build-up of auditory segregation. The present data are consistent with the hypothesis of a default state of the binding mechanism in which audio and video components are fused together (leading to the McGurk effect), followed by an "unbinding" process when evidence for different auditory and visual sources accumulates.

Let us come back to the models of audiovisual fusion available in the literature. One-stage models consider that phonetic decision operates at a given representational stage, and produces an integrated percept combining auditory and visual cues in a given way, possibly mediated by general attentional mechanisms (Fig. 6a). The present data suggest that an additional computational stage should be incorporated before decision operates [START_REF] Berthommier | A phonetically neutral model of the low-level audiovisual interaction[END_REF]. This involves online computation of some assessment of the coherence/incoherence of the auditory and visual inputs (C in Fig. 6b). Local coherence may also help the subject to better process the auditory and visual streams and extract adequate information [START_REF] Schwartz | Seeing to hear better: Evidence for early audio-visual interactions in speech identification[END_REF]. Though instantaneous evidence for incoherence does not suffice to unbind the auditory and visual inputs, as displayed by the McGurk effect, accumulation of such evidence may modulate the decision process. This is displayed in Fig. 6b by a bottom-up arrow (a). The effect of phonetic incoherence, displayed in Experiment 2, suggests that the decision stage itself could intervene in the computation of the coherence measure: this motivates the top-down arrow (b). The coherence evaluation C could result in decreasing the weight of the visual stream in the decision output if it suggests that the audio and video streams are incoherent, as happens in the various cases of incoherent contexts explored in this paper.

van Wassenhove, V., Grant, K., & Poeppel, D. (2005). Visual speech speeds up the neural processing of auditory speech. PNAS 102 , 1181-1186.

Van Wassenhove, V., Grant, K., & Poeppel, D. (2007). Temporal window of integration in bimodal speech. Neuropsychologia 45 , 598-607.

Figure 2 :

 2 Figure 2: Results of Experiment 1 Percentage of " ba " responses for " ba " (in dark grey) and " McGurk " (in light grey) stimuli, in the coherent (left) vs. incoherent (right) contexts.

Figure 3 :

 3 Figure 3: Results of Experiment 2 (a) For each box, percentage of " ba " responses for " ba " (in dark grey) and " McGurk " (in light grey) stimuli, in the coherent (left) vs. incoherent (right) contexts. Left box: without alert stimulus. Right box: with alert stimulus.

Figure 4 :

 4 Figure 4: Results of Experiment 4 Percentage of " ba " responses for " ba " (in dark grey) and " McGurk " (in light grey) stimuli, in the coherent (left) vs. incoherent (right) contexts.

Figure 5 :

 5 Figure 5: Results of Experiment 5

Figure 6 :

 6 Figure 6: One-stage vs. two-stage model for audiovisual fusion in speech perception (a) Left: A possible one-stage model (b) Right: A possible two-stage model

ACKNOWLEDGEMENTS

This work was supported by the French National Research Agency (ANR) through funding of the MULTISTAP project (MULTISTability and binding in Audition and sPeech: ANR-08-BLAN-0167 MULTISTAP)