Paul Brunet

Damien Pous

A formal exploration of Nominal Kleene Algebra

Keywords: 1998 ACM Subject Classification F.1.1 Models of Computation, F.4.3 Formal Languages, F.4.1 Mathematical Logic Keywords and phrases Nominal sets, Kleene algebra, equational theory, Coq 1

An axiomatisation of Nominal Kleene Algebra has been proposed by Gabbay and Ciancia, and then shown to be complete and decidable by Kozen et al. However, one can think of at least four different formulations for a Kleene Algebra with names: using freshness conditions or a presheaf structure (types), and with explicit permutations or not. We formally show that these variations are all equivalent.

Then we introduce an extension of Nominal Kleene Algebra, motivated by relational models of programming languages. The idea is to let letters (i.e., atomic programs) carry a set of names, rather than being reduced to a single name. We formally show that this extension is at least as expressive as the original one, and that it may be presented with or without a presheaf structure, and with or without syntactic permutations. Whether this extension is strictly more expressive remains open.

All our results were formally checked using the Coq proof assistant.

Introduction

Gabbay and Ciancia introduced a nominal extension of Kleene algebra [START_REF] James | Freshness and name-restriction in sets of traces with names[END_REF], as a framework for trace semantics with dynamic allocation of resources. The associated semantics extends formal languages into nominal languages, where words have a nominal structure. Kozen et al. recently proved the completeness of the proposed axiomatisation [START_REF] Dexter Kozen | Completeness and incompleteness in Nominal Kleene Algebra[END_REF], and proposed a coalgebraic treatment [START_REF] Dexter Kozen | Nominal Kleene Coalgebra[END_REF] yielding decidability of the equational theory.

They use the following syntax for nominal regular expressions:

e, f ∶∶= a ∈ Σ 0 1 e + f e ⋅ f e ⋆ νa.e , where Σ is the alphabet, and νa.e makes it possible to generate a fresh letter (or name) a before continuing as e. For instance, the expression νa.νb.(a⋅b) denotes the language of all words of length two consisting of two distinct letters. While such a syntax is natural from a nominal point of view, other choices are possible. For instance, one might expect expressions to be typed or classified according to their set of free names. Similarly, name permutations, which are available in any model, can be reified at the syntactic level. We first list four axiomatisations of the corresponding presentations-one of them corresponding to Gabbay and Ciancia's axiomatisation, and we prove that all choices are in fact equivalent. For the sake of the proofs, we need to introduce the positive fragments, where the constant 0 denoting the empty language is excluded; these fragments are interesting 22:2 NKA in Coq because they are stable: any proof of an equality whose members belong to the fragment only uses expressions from that fragment. Kleene algebra are known to be complete not only with respect to language models, but also relational models. There, the letters from the alphabet are interpreted as binary relations, and the regular operations correspond to standard operations on binary relations: union, composition, reflexive transitive closure. This makes it possible to interpret imperative programs, seen as state transformers: binary relations between memory states. Kozen actually designed an extension of Kleene algebra, Kleene algebra with tests [START_REF] Kozen | Kleene algebra with tests[END_REF], which makes it possible to represent not only the control flow of such programs, but also the tests and conditions appearing in while loops and branching statements.

Extending Kleene algebra with names seems appropriate to model imperative programs with local variables, where parts of the memory is visible only locally. The previous notion of nominal Kleene algebra is however not really appropriate for this purpose: letters of the alphabet (i.e., atomic programs, instructions) are equated with names bound by the νa.e construct (i.e., memory locations). In contrast, the instruction x ← y that assigns to variable x the value of variable y should be an elementary construction depending on the names x and y. For this reason, we provide an extension of the syntax where letters carry a list of names. (We could use arbitrary nominal sets, but we restrict to a concrete representation in this work for the sake of simplicity.) The typed version of this extension is more appropriate for modelling imperative programs with local variables; like above for plain nominal Kleene algebra, we show that the various presentations are equivalent. We moreover show that the extension is conservative: plain nominal Kleene algebra can be encoded into the extended ones. Whether a converse encoding is possible remains open.

Outline.

We define the various theories in Section 2 and we compare them in Section 3. In Section 4 we provide a relational interpretation for our extended model. We conclude in Section 5.

Notation.

We write f (A) for the set of finite subsets of A. The set of natural numbers is written N.Composition of two functions f and g is written f ○ g; it maps x to f (g (x)).

2

Expressions and proofs

Atoms and letters

Let A be an infinite set of atoms with decidable equality. We consider in this paper finitely supported permutations of atoms, simply called permutations in the following. They are bijections π such that there is a finite set

A ⊆ A such that a ∉ A ⇒ π (a) = a.
The inverse of a permutation π is written π -1 . The identity permutation is denoted by ⎧ ⎩ ⎫ ⎭ , and the permutation exchanging a and b, and leaving every other atom unchanged, is written ⎧ ⎩ a b ⎫ ⎭ . Finally, if π is a permutation and A is a finite set of atoms, π (A) ∶= {π (a) a ∈ A} is the image of A under π.

We consider as letters an arbitrary nominal set L [START_REF] Gabbay | A new approach to abstract syntax involving binders[END_REF][START_REF] Andrew | Nominal Sets: Names and Symmetry in Computer Science[END_REF], which we assume to be decidable. Such a set is specified through the data of its set of elements, a function ♮ () ∶ L → f (A) mapping every element to its support, and an action of the group of permutations on L.

These functions must satisfy the following axioms:

∀x ∈ L, ∀π, (∀a ∈ ♮ (x) , π(a) = a) ⇒ π (x) = x.
(1)

∀x ∈ L, ∀π, ♮ (π (x)) = π (♮ (x)) . (2) ∀x ∈ L, ∀π, π ′ , π (π ′ (x)) = π ○ π ′ (x) . ( 3
)

Expressions and sets of expressions

We define a single type for expressions, containing all possible operators, and we define several fragments of it afterwards. Doing so makes it possible to share several definitions, enabling important code-reuse in our proof scripts.

▸ Definition 1 (Expressions). The set E of expressions is composed of terms formed over the following syntax, where the letter A is a finite set of atoms, π denotes a permutation, a is an atom and l is a letter:

e, f ∶= 0 1 e + f e ⋅ f e ⋆ ν a .

e l a ⟨π⟩ e

A id A w a .e.

Product (⋅), sum (+) and Kleene star (⋅ ⋆ ) are the regular operations, together with the associated constants 0 and 1, ν a is name restriction. Variables can be either letters l or atoms a. We include a syntactic construction for explicit permutations ⟨π⟩. The remaining entries ( A , id A , and w a ) are for the presheaf presentation; we discuss them in Section 2.2.2

Untyped expressions

▸ Definition 2 (Untyped expression). An expression e is untyped if it neither contains the operator w a nor the constants A and id A . The set of untyped expressions is written U.

We define freshness only for untyped expressions:

▸ Definition 3 (Freshness). An atom a is fresh for e if the judgement a # e can be inferred in the following system.

a # 1 a # 0 a ∉ ♮ (l) a # l a ≠ b a # b a # e a # f a # e + f a # e a # f a # e ⋅ f a # e a # e ⋆ a # ν a .e a # e a # ν b .e π -1 (a) # e a # ⟨π⟩ e .
Accordingly, the support of an untyped expression e, written ♮ (e), is the unique set such that ∀a, a # e ⇔ a ∉ ♮ (e).

Typed expressions

For the presheaf approach, we replace freshness assumptions with type derivations. In order to enforce uniqueness of types, we replace the constants 0 and 1 from the untyped syntax by the annotated constants A and id A , and we use explicit weakenings (w a ).

▸ Definition 4 (Typed expressions). For any e ∈ E and A ∈ f (A), e has the type A if the judgement e ∶ A can be inferred in the following system:

id A ∶ A A ∶ A l ∈ L l ∶ ♮ (l) a ∈ A a ∶ {a} e ∶ A f ∶ A e + f ∶ A e ∶ A f ∶ A e ⋅ f ∶ A e ∶ A e ⋆ ∶ A e ∶ A ∪ {a} a ∉ A ν a .e ∶ A e ∶ A ∖ {a} a ∈ A w a .e ∶ A e ∶ π -1 (A) ⟨π⟩ e ∶ A M F C S 2 0 1 6
22:4

NKA in Coq

If this is the case, then e is typed. The set of typed expressions is written T.

▸ Remark. This type system is syntax directed and yields a simple decision procedure.

Expressions over letters or atoms

A significant motivation for this work was to study the differences between having atoms or letters as variables in expressions. Hence we define two other subsets.

▸ Definition 5 (Atomic expressions, literate expressions). An expression e is called atomic (respectively literate) if it does not contain letters (respectively atoms) as variables. The set of atomic expressions is E ⟨A⟩, and the set of literate expressions is E ⟨L⟩.

Intuitively, there are two main differences between having atoms or letters as variables. First, a letter may depend on many atoms. Second, two letters with the same support can still be different, whereas the following equivalence holds :

∀a, b ∈ A, a = b ⇔ (∀c ∈ A, c # a ⇔ c # b) .

Positive expressions

For the sake of proofs, we also define the classes of expressions without 0 or A as a subexpression. A motivation for excluding these is that in any reasonable system 0 ≡ 0 ⋅ e. Hence if there is an atom a not fresh for e, we would have two equivalent expressions with different sets of fresh variables.

▸ Definition 6 (Positive expression). An expression e is positive if it does not contain 0 nor

A as a sub-expression. The set of positive expressions is E + .

For concision, we write E + ⟨L⟩ for E ⟨L⟩ ∩ E + , and E + ⟨A⟩ for E ⟨A⟩ ∩ E + .

Explicit permutations

Our syntax includes for explicit permutations ⟨π⟩, while permutations are usually considered as external operations. This allows one to manipulate permutations inside the expressions, and we shall see that this addition does not raise the complexity of the problem.

Nevertheless, we need to formally define the semantics of permutations on expressions.

▸ Definition 7 (Action of a permutation on an expression). Let e ∈ E be an expression and π a permutation. The action of π on e, written π e, is defined as follows:

π 1 ∶= 1 π 0 ∶= 0 π (w a .e) ∶= w π(a) . (π e) π id A ∶= id π(A) π A ∶= π(A) π (ν a .e) ∶= ν π(a) . (π e) π a ∶= π (a) π l ∶= π (l) π (⟨π ′ ⟩ e) ∶= ⟨ ⎧ ⎩ ⎫ ⎭ ⟩ (π ○ π ′ ) e π (e ⋆ ) ∶= (π e) ⋆ π (e ⋅ f ) ∶= π e ⋅ π f π (e + f ) ∶= π e + π f
Expressions without explicit substitutions are called clean.

▸ Definition 8 (Clean expressions). An expression e is clean if it never uses the operator ⟨π⟩.

The set of clean expressions is C.

Applying permutations preserves all classes we have listed so far:

Ax ⊢ f = e Ax ⊢ e = f Ax ⊢ e = f Ax ⊢ f = g Ax ⊢ e = f Ax ⊢ e = f (e, f ) ∈ Ax (a)
Equivalence and axiom rules.

Ax ⊢ 0 = 0 Ax ⊢ 1 = 1 Ax ⊢ id A = id A Ax ⊢ A = A Ax ⊢ l = l Ax ⊢ a = a Ax ⊢ e = g Ax ⊢ f = h Ax ⊢ e + f = g + h Ax ⊢ e = g Ax ⊢ f = h Ax ⊢ e ⋅ f = g ⋅ h Ax ⊢ e = f Ax ⊢ e ⋆ = f ⋆ Ax ⊢ e = f Ax ⊢ ν a .e = ν a .f Ax ⊢ e = f Ax ⊢ w a .e = w a .f Ax ⊢ e = f Ax ⊢ ⟨π⟩ e = ⟨π⟩ f (b) Congruence rules. Ax ⊢ e + f = f + e Ax ⊢ e + (f + g) = (e + f ) + g Ax ⊢ e + e = e Ax ⊢ e ⋅ (f + g) = (e ⋅ f ) + (e ⋅ g) Ax ⊢ (e + f ) ⋅ e = (e ⋅ g) + (f ⋅ g) Ax ⊢ e ⋅ (f ⋅ g) = (e ⋅ f ) ⋅ g Ax ⊢ f + e ⋅ g ⩽ g Ax ⊢ e ⋆ ⋅ f ⩽ g Ax ⊢ f + g ⋅ e ⩽ g Ax ⊢ f ⋅ e ⋆ ⩽ g (c)
Constant-free Kleene algebra axioms. (Note the equivalence in the first point, which is why we keep a residual empty permutation when we apply a permutation to an expression of the shape ⟨π⟩ e.)

Proofs

A generic framework for proofs

We now describe a generic framework for defining equational theories over E. Given a relation Ax ⊆ E × E, we define the judgement Ax ⊢ e = f to hold if it can be inferred in the system displayed in Table 1 (where Ax ⊢ e ⩽ f is a shorthand for Ax ⊢ e + f = f ). Notice that we have "hardwired" some laws of Kleene Algebra (KA) in this system, on the basis that they should hold for any reasonable equational system for Nominal Kleene Algebra. However, as we have two sets of constants, we cannot put inside the generic system the Kleene Algebra laws dealing with them. For instance when we consider expressions over the untyped syntax, the fact that e ⋅ 1 = e will be stated inside Ax. It is a simple matter to check that whatever Ax, the relation Ax ⊢ _ = _ is an equivalence relation and Ax ⊢ _ ⩽ _ is a preorder.

M F C S 2 0 1 6

22:6

NKA in Coq

Sets of axioms

In Tables 23456, we present a number of possible sets of axioms, which may be combined to axiomatise the different subsets we consider. All the axioms displayed here are implicitly universally quantified.

The first groups of axioms correspond to the axioms of KA for 1, declined in a typed and an untyped fashion. We then do the same for 0 and A , first with the KA axioms, and then for its interactions with ⟨π⟩, ν a and w a , always separating between the typed and untyped cases. These sets of axioms for constants are presented in Tables 2 and3.

We then introduce sets of axioms to handle permutations. The axiom propagating w a is set apart, as it only makes sense for typed expressions. This group is displayed in Table 4. Notice that no law speaks about zeros, as it already has been dealt with in (3a).

The sets of axioms in Table 5 are simple distributive laws of the restriction and weakening operators. The next group, displayed in Table 6, constitutes the core of the nominal theory of expressions. The untyped axioms are mostly the classic nominal axioms, taken from [START_REF] Dexter Kozen | Completeness and incompleteness in Nominal Kleene Algebra[END_REF]. The only new axiom here is (6b), where we use syntactic permutations rather than semantic ones. The typed axioms are for the most part straightforward reformulations of the previous ones. Notice that in the typed case, we do not need to use freshness conditions, but rather typing statements. The last law of the set (6f) reflects the fact that for an untyped expression e, if a ≠ b then a # e ⇔ a # ν b .e.

Theories

A theory is given by a relation Ax, listing the axioms, and a set S from which we take expressions. As expressions may be typed or untyped, atomic or literate, clean or not and positive or not, there are 16 theories, listed in Table 7.

Notice that every subset of expressions mentioned in this table is associated with a single theory. In the following, for concision, we may refer to a theory by simply giving its base set. It is also worth mentioning that for every set S, the theories for E ⟨L⟩ ∩ S and E ⟨A⟩ ∩ S use the same set of axioms.

The theory E ⟨A⟩ ∩ U ∩ C corresponds precisely to the axiomatisation of NKA given in [START_REF] Dexter Kozen | Completeness and incompleteness in Nominal Kleene Algebra[END_REF]. In our view, the best theory for defining the interpretation of a program would be

E + ⟨L⟩ ∩ U ∩ C, but a relational interpretation is best defined in E + ⟨L⟩ ∩ T.
A difficulty is that if we have a theory (S, Ax), with two expressions e, f ∈ S such that Ax ⊢ e = f , it may be the case that the proof uses expressions outside of S. This is generally what happens in systems with 0 (or A ): if e ∉ S and 0 ∈ S, then:

Ax ⊢ 0 = 0 ⋅ e Ax ⊢ 0 ⋅ e = 0 Ax ⊢ 0 = 0
This is a bad property when one wants to prove results by structural induction on proofs. This phenomenon disappears with stable theories: A ⋅ e =e (if e ∶ A) . ⟨π⟩ e

▸
⟨π⟩ A = π(A) ν a . A = A∖{a} (if a ∈ A) w a . A = A∪{a} (if a ∉ A) (b) Typed zero axioms
⟨π⟩ ⟨π ′ ⟩ e = ⟨π ○ π ′ ⟩ e ⟨π⟩ 1 =1 ⟨π⟩ id A =id π(A) ⟨ ⎧ ⎩ ⎫ ⎭ ⟩ e =e ⟨π⟩ a =π (a) (if a ∈ A) ⟨π⟩ l =π (l) (if l ∈ L) (
+ ⟨L⟩ ∩ U (2a) (4a) (5b) (6b) (6e) NKAspu E + ⟨A⟩ ∩ U NKAnmpu E + ⟨L⟩ ∩ U ∩ C (2a) (5b) (6a) (6e) NKAnspu E + ⟨A⟩ ∩ U ∩ C NKAmu E ⟨L⟩ ∩ U (2a) (3a) (4a) (5b) (6b) (6e) NKAsu E ⟨A⟩ ∩ U NKAnmu E ⟨L⟩ ∩ U ∩ C (2a) (3a) (5b) (6a) (6e) NKAnsu E ⟨A⟩ ∩ U ∩ C NKAmpt E + ⟨L⟩ ∩ T (2b) (4a) (4b) (5a) (5b) (6d) (6f) NKAspt E + ⟨A⟩ ∩ T NKAnmpt E + ⟨L⟩ ∩ T ∩ C (2b) (5a) (5b) (6c) (6f) NKAnspt E + ⟨A⟩ ∩ T ∩ C NKAmt E ⟨L⟩ ∩ T (2b) (3b) (4a) (4b) (5a) (5b) (6d) (6f) NKAst E ⟨A⟩ ∩ T NKAnmt E ⟨L⟩ ∩ T ∩ C (2b) (3b) (5a) (5b) (6c) (6f) NKAnst E ⟨A⟩ ∩ T ∩ C
E + ⟨L⟩ ∩ T E + ⟨L⟩ ∩ U E ⟨L⟩ ∩ T E ⟨L⟩ ∩ U E + ⟨L⟩ ∩ T ∩ C E + ⟨L⟩ ∩ U ∩ C E ⟨L⟩ ∩ T ∩ C E ⟨L⟩ ∩ U ∩ C E + ⟨A⟩ ∩ T E + ⟨A⟩ ∩ U E ⟨A⟩ ∩ T E ⟨A⟩ ∩ U E + ⟨A⟩ ∩ T ∩ C E + ⟨A⟩ ∩ U ∩ C E ⟨A⟩ ∩ T ∩ C E ⟨A⟩ ∩ U ∩ C Figure 1
The two cubes as sets 3 Ordering theories

Definitions

We define two preorders to compare theories. The first one is the strongest one:

▸ Definition 11 (Embedding preorder). A theory (S, Ax) can be embedded into (S ′ , Ax ′ ), written (S, Ax) ≼ (S ′ , Ax ′ ) if there is a function φ such that for any e ∈ S, φ (e) ∈ S ′ , and for any e, f ∈ S, Ax ⊢ e = f ⇔ Ax ′ ⊢ φ (e) = φ (f ). In that case we say that φ is an embedding of (S, Ax) into (S ′ , Ax ′ ).

When a theory can be embedded into a second one, then every model of the latter one gives rise to a model former one. However, some intuitively equivalent theory cannot be compared using this preorder. For instance, E + ⟨A⟩ ∩ T cannot be embedded into E + ⟨A⟩ ∩ U. Indeed, while the typed expressions id {a} and id {a,b} are not equal (they have different types), they have the same untyped behaviour and both of them should be mapped to the untyped constant 1. To this end, we introduce a slightly weaker preorder:

▸ Definition 12 (Reduction preorder). A theory (S, Ax) reduces to (S ′ , Ax ′ ), which we denote by (S, Ax) ≪ (S ′ , Ax ′ ), if for any pair (e, f ) ∈ S × S there is a pair of expressions (e ′ , f

′ ) ∈ S ′ such that Ax ⊢ e = f ⇔ Ax ′ ⊢ e ′ = f ′ .
▸ Lemma 13. If (S, Ax) ≪ (S ′ , Ax ′ ) and if (S ′ , Ax ′ ) is decidable, then so is (S, Ax).

▸ Remark. This lemma assumes an effective proof of (S, Ax) ≪ (S ′ , Ax ′ ): there must be a way to build the pair e ′ , f ′ from the pair e, f . Our (Coq) proofs below have this property.

Embeddings

We summarise the results we obtained using Coq on Figure 1. (The scripts are available online [START_REF] Brunet | Web appendix to this abstract[END_REF]). A plain arrow is drawn between two theories if the source of the arrow can be embedded into the target of the arrow, and a dashed arrow when the source reduces to the target. Thanks to the decidability result for E ⟨A⟩ ∩ U ∩ C [START_REF] Dexter Kozen | Nominal Kleene Coalgebra[END_REF], this ensures that all atomic theories are decidable. We discuss in more details how we obtained some of these results.

Reducing to positive fragments

The first step consists in getting rid of the constants 0 and A , so that we can focus on stable theories (Definition 10). We only present here the untyped case. In other words we choose a ▸ Definition 14. If e is an untyped expression, extract (e) is the unique normal form of e with respect to the following confluent rewriting system:

e + 0 → e 0 + f → f e ⋅ 0 → 0 0 ⋅ f → 0 ν a .0 → 0 ⟨π⟩ 0 → 0 0 ⋆ → 1.
The interesting property of this function is that if Ax ⊢ e = 0, then extract (e) is syntactically equal to 0, and extract (e) ∈ E + otherwise. Furthermore, for every e ∈ S, Ax ⊢ extract (e) = e.

The formal proof then relies on two key observations:

1. If (e, f ) ∈ Ax ∖ (3a), then Ax ∖ (3a) ⊢ extract (e) = extract (f ). 2. If (e, f ) ∈ (3a), then extract (e) = extract (f ).
This allows to prove by induction on proofs that:

Ax ⊢ e = f ⇒ Ax ∖ (3a) ⊢ extract (e) = extract (f ) .
Because the positive axiomatisation is included in Ax, we also get:

Ax ∖ (3a) ⊢ extract (e) = extract (f ) ⇒ Ax ⊢ extract (e) = extract (f ) .
The fact that extract (e) is provably equal to e with the axioms Ax allows to close the proof of equivalence, with the entailment:

Ax ⊢ extract (e) = extract (f ) ⇒ Ax ⊢ e = f.
However, if Ax ⊢ e = 0 then extract (e) ∉ E + . This means that we cannot directly use extract () as an embedding between theories. We obtain the reduction as follows: when given the pair e, f , we compute extract (e) and extract (f ). If both of these are equal to zero, then when map the pair to equal positive expressions, say 1, 1. If both of them are non-zero, then we produce extract (e) , extract (f ). Otherwise we produce different positive expressions, say 1, a in the atomic case and 1, l in the literate case.

From presheaves to freshness, and back

Let (S, Ax) be a positive untyped theory, meaning S ⊆ E + ∩ U, and (S ′ , Ax ′ ) be the corresponding positive typed theory. We show here how to transport S into S ′ , and vice versa. This corresponds to the vertical arrows on Figure 1. The key tools in this case are the erasure and retyping functions.

▸ Definition 15 (Erasure). The erasure of e ∈ T, written ⌊e⌋, is the expression obtained from e by removing all weakenings (w a ), and replacing all id A with 1 and all A with 0.

▸ Lemma 16. If e ∈ S ′ then ⌊e⌋ ∈ S, and if e ∶ A then ♮ (⌊e⌋) ⊆ A.

▸ Definition 17 (Retyping). Let e ∈ U, we define the retyping of e, written ⌈e⌉, by structural induction: (6f ) (5a) (4b) ⊢ e = w A∖♮(⌊e⌋) . ⌈⌊e⌋⌉ .

⌈0⌉ ∶= ∅ ⌈1⌉ ∶=id ∅ ⌈e + f ⌉ ∶=w ♮(f )
Furthermore, if S ⊆ C, we may remove the axiom (4b).

From this lemma, we obtain that the retyping function is an embedding of S into S ′ . But it also shows a problem for the other direction. For instance the expressions e and w a .e have different types, and are thus different, but they will be mapped to the same expression. For this reason, we cannot use the erasure function to embed S ′ into S. Nevertheless, we can use it to show that S ′ is simpler than S. Given a pair of expressions e, f ∈ S ′ , if e and f have the same type, then we produce the pair ⌊e⌋ , ⌊f ⌋ which is equiprovable. If it is not the case, we purposely produce different expressions, as in the previous section.

From atomic to literate

We assume there is an atom α ∈ A and an element λ ∈ L with ♮ (λ) = {α}. We show the transformation from E + ⟨A⟩ ∩ U to E + ⟨L⟩ ∩ U, which corresponds to the central horizontal top arrow on Figure 1. Let NKApu be the set of axioms (2a), (4a), (5b), (6b), (6e) corresponding to the theory of these sets.

▸ Definition 20 (From atoms to letters.). Given an expression e ∈ E + ⟨A⟩ ∩ U, we obtain the expression ⇃e⇂ ∈ E + ⟨L⟩ ∩ U by replacing every atomic variable a by ⟨ ⎧ ⎩ a α ⎫ ⎭ ⟩ λ. We write ⇃E + ⟨A⟩ ∩ U⇂ for the set of expressions f ∈ E + ⟨L⟩ ∩ U, such that there is an expression e ∈ E + ⟨A⟩ ∩ U such that f = ⇃e⇂.

For any expression e, e ∈ ⇃E + ⟨A⟩ ∩ U⇂ if and only if each literate variable in e has the identifier x. It is also worth noting that ⇃_⇂ preserves freshness: a # e ⇔ a # ⇃e⇂. As for typed and untyped expressions, we define an inverse operation.

▸ Definition 21 (Going back). The inverse operation is only defined on literate expressions whose variables carry the identifier x, and thus have a singleton support. The expression ↿e↾ is then obtained by replacing every variable by the single atom in its support.

The function ↿_↾ is the inverse of ⇃_⇂, ⇃_⇂ preserves NKApu-equality, and ↿_↾ preserves NKApu-equality on the image of ⇃_⇂.

▸ Lemma 22. ∀e ∈ E + ⟨A⟩ ∩ U, NKApu ⊢ e = ↿⇃e⇂↾. ▸ Lemma 23. ∀e, f ∈ E + ⟨A⟩ ∩ U, NKApu ⊢ e = f ⇒ NKApu ⊢ ⇃e⇂ = ⇃f ⇂. ▸ Lemma 24. ∀e, f ∈ E + ⟨L⟩ ∩ U ∩ ⇃E + ⟨A⟩ ∩ U⇂, NKApu ⊢ e = f ⇒ NKApu ⊢ ↿e↾ = ↿f ↾.
By putting all together, we obtain that ⇃_⇂ is an embedding of E + ⟨A⟩ ∩ U into E + ⟨L⟩ ∩ U.

Relational interpretation of literate expressions

Our main motivation for developing the typed syntax was to define a relational interpretation of expressions. As explained in the introduction, the classical way of interpreting a program as a relation is to consider memory states as functions, associating values to memory cells. A M F C S 2 0 1 6

22:12

NKA in Coq

program is then simply a relation between memory states. Furthermore, in most high level programming languages, one cannot access every part of the memory: a variable should be declared before it is used. There are also constructs allowing one to declare a local variable, which is hidden from the rest of the program. Both of these considerations can be encoded by considering functions with a finite domain: the set of memory locations that are visible in the current scope.

Let us be more precise. Consider that the set A of atoms corresponds to memory locations, and that locations may contain values from an arbitrary set V. A memory state of domain A ∈ f (A) is then a function from A to V, and an expression of type A will be interpreted as a binary relation over memory states of domain A (whence the presheaf structure).

Regular operations are interpreted using the standard operations on binary relations; in particular, id A is interpreted as the identity relation on V A . To interpret letters, we need to fix an equivariant map φ that assign to a letter x a relation between memory states with domain ♮ (x). Several choices are possible for the operations of restriction (ν a ) and weakening (w a ), yielding slightly different theories. Here is a possibility which gives rise to a model of our theory: if R is a relation over V A , then we define

ν a .R ∶= {(f ↾ A , g↾ A ) (f, g) ∈ R} ; (if a ∈ A) w a .R ∶= {(f, g) (f ↾ A , f ↾ A ) ∈ R and f (a) = g(a)} . (if a ∉ A)
(Where f ↾ A is the restriction of a function f ∈ V B for some superset B of A.) Note that this model is not free: for all relations R, S we have ν a .(R ⋅ S) ⊆ (ν a .R) ⋅ (ν a .S), which is not an inequation provable from the axioms.

Example.

Consider the program swap (x, y) that exchanges the contents of the variables x and y. The natural implementation of this program is the following: let t in t ← x; x ← y; y ← t.

The instruction x ← y may be represented by a nominal element assign (x, y) with support {x, y}, and such that π (assign (x, y)) = assign (π (x) , π (y)). Accordingly, the program swap is represented by the following expression, where the location is hidden using a top-level restriction. ν t . (assign (t, x) ⋅ assign (x, y) ⋅ assign (y, t)) .

Alternatively, one can obtain an expression with a single letter using explicit permutations: let a 1 and a 2 be two atoms, and set a ∶= assign (a 1 , a 2 ). The instruction x ← y may be represented by ⟨ ⎧ ⎩ x a 1 ⎫ ⎭ ⎧ ⎩ y a 2 ⎫ ⎭ ⟩ a, and the program swap by

ν t . (⟨ ⎧ ⎩ t a 1 ⎫ ⎭ ⎧ ⎩ x a 2 ⎫ ⎭ ⟩ a) ⋅ (⟨ ⎧ ⎩ x a 1 ⎫ ⎭ ⎧ ⎩ y a 2 ⎫ ⎭ ⟩ a) ⋅ (⟨ ⎧ ⎩ y a 1 ⎫ ⎭ ⎧ ⎩ t a 2 ⎫ ⎭ ⟩ a).

Future work

We leave two questions for future work. First, is it possible to reduce the literate theory of nominal Kleene algebra to that of atomic nominal Kleene algebra? If not, is there a free language theoretic model for which we could obtain decidability? Second, is there a free relational model for our literate theory?

Table 4

 4 a) General permutation axioms ⟨π⟩ (w a .e) =w π(a) . ⟨π⟩ e (b) Permutation vs. wa Permutation axioms w a . (e + f ) =w a .e + w a .f w a . (e ⋆ ) = (w a .e ⋆ ) w a . (e ⋅ f ) =w a .e ⋅ w a .f w a . (id A ) =id A∪{a} (if a ∉ A) w a . (w b .e) =w b . (w a .e) (a) Weakening ν a . (e + f ) =ν a .e + ν a .f ν a . (ν b .e) =ν b . (ν a .e) (b) Restriction

  theory (S, Ax), with S taken from the set {E ⟨A⟩ ∩ U, E ⟨A⟩ ∩ U ∩ C, E ⟨L⟩ ∩ U, E ⟨L⟩ ∩ U ∩ C}, the corresponding positive theory being (S ∩ E + , Ax ∖ (3a)).

Table 1

 1 Modular deduction system

▸ Lemma 9. For any subset of expressions S chosen from {T, U, E ⟨A⟩ , E ⟨L⟩ , E + , C}, for any permutation π, and for any expression e ∈ E, e ∈ S ⇔ π e ∈ S. Furthermore, if e has the type A then π e ∶ π (A), and if a is fresh for e then π (a) # π e.

Table 2

 2 Identity axioms

	e ⋅ 1 =e 1 ⋅ e =e 1 + e ⋅ e ⋆ ⩽e ⋆ 1 + e ⋆ ⋅ e ⩽e ⋆ (a) Untyped identity axioms e ⋅ id A =e (if e ∶ A) id A ⋅ e =e (if e ∶ A) id e + 0 =e e ⋅ 0 =e 0 ⋅ e =e ⟨π⟩ 0 =0 ν a .0 =0 (a) Untyped zero axioms e + A =e (if e ∶ A) (if e ∈ U) (if e ∈ U) e ⋅ A =e (if e ∶ A)

Definition 10. A theory (S, Ax) is stable if for any expressions e, f ∈ E such that Ax ⊢ e = f , e ∈ S if and only if f ∈ S. All of our positive theories (those included in E + ) are stable. A + e ⋅ e ⋆ ⩽e ⋆ (if e ∶ A) id A + e ⋆ ⋅ e ⩽e ⋆ (if e ∶ A) (b) Typed identity axioms

Table 3

 3 Zero axioms

⟨π⟩ (e + f ) = ⟨π⟩ e + ⟨π⟩ f ⟨π⟩ (e ⋅ f ) = ⟨π⟩ e ⋅ ⟨π⟩ f ⟨π⟩ (e ⋆ ) = (⟨π⟩ e) ⋆ ⟨π⟩ (ν a .e) =ν π(a)

Table 5

 5 Distributive laws of νa, wa

	M F C S 2 0 1 6

b .e ∶ A and a ∉ A) (c) Typed α-conversion with ν b .e =ν a .⟨ ⎧ ⎩ a b ⎫ ⎭ ⟩ e (if ν b .e ∶ A and a ∉ A) (d) Typed α-conversion with ⟨π⟩ ν a .e =e (if a # e) ν a .f ⋅ e =ν a . (f ⋅ e) (if a # e) e ⋅ ν a .f =ν a . (e ⋅ f ) (if a # e) (e) Untyped nominal axioms ν a .w a .e =e (if ν a .w a .e ∶ A) (ν a .f ) ⋅ e =ν a . (f ⋅ w a .e) e ⋅ (ν a .f ) =ν a . (w a .e ⋅ f ) ν b .w a .e =w a .ν b .e (if a ≠ b) (f) Typed nominal axioms

Table 6

 6 Nominal axioms

	Name	Set	Axioms
	NKAmpu	E

Table 7 Theories

 7

	P. Brunet & D. Pous

  The notation w A .e is justified by the law w a .w b .e = w b .w a .e, holding in every typed theory.▸ Lemma 18. e ∈ S entails ⌈e⌉ ∈ S ′ . Furthermore, ⌈e⌉ has the type ♮ (e). These functions allow one to go back and forth between S and S ′ : ▸ Lemma 19. If e ∈ S, then e = ⌊⌈e⌉⌋. If e ∶ A, then:

			∖♮(e) . ⌈e⌉ + w ♮(e)∖♮(f ) . ⌈f ⌉
	⌈a⌉ ∶=a	⌈l⌉ ∶=l	⌈e ⋅ f ⌉ ∶=w ♮(f )∖♮(e) . ⌈e⌉ ⋅ w ♮(e)∖♮(f ) . ⌈f ⌉
	⌈e ⋆ ⌉ ∶= ⌈e⌉ ⋆		⌈ν a .e⌉ ∶=ν a . ⌈e⌉	(if a ∈ ♮ (e))
	⌈⟨π⟩ e⌉ ∶= ⟨π⟩ ⌈e⌉		⌈ν a .e⌉ ∶=ν a .w a . ⌈e⌉	(if a ∉ ♮ (e))

Acknowledgements.

We would like to thank Daniela Petrisan and Alexandra Silva for the discussions that have led to this work.

* This author was funded by the European Research Council (ERC) under the European Union's Horizon 2020 programme (CoVeCe, grant agreement No 678157); this work has also been supported by the project ANR 12IS02001 PACE.


domain: sdv spi spi.gproc

text:
Isabelle Déléris
email: isabelle.deleris@grignon.inra.fr

Anne Saint-Eve

Aurélie Saglio

Ioan Isabelle Souchon
email: isabelle.souchon@grignon.inra.fr

Cristian Trelea
email: cristian.trelea@agroparistech.fr

INSIGHTS IN AROMA COMPOUND RETENTION BY MUCOSA DURING CONSUMPTION THROUGH MATHEMATICAL MODELLING

Keywords: aroma release, wetted mucosa, saliva, persistence, interaction, dynamic modelling Chemical compounds studied ethyl propanoate (PubChem CID: 7749), 2-nonanone

Highlights

-Aroma compound persistence after gaseous sample inhalation was modelled.

-Both physiological and physicochemical parameters were included in the model.

-The respective contributions of wetted mucosa and saliva on release kinetics were assessed.

-The major role of mucosa partition coefficients of molecules was confirmed.

Introduction

Olfactory perception is known to largely contribute to overall perception of foods and, consequently, to consumer choice and preferences. A better understanding of this specific perception is therefore of great importance and requires the identification of the main mechanisms at the origin of aroma compound release during food consumption. Several studies have notably focused on orthonasal and retronasal perceptions to highlight the origin of the main differences between these two perception pathways (Espinosa Diaz, 2004;[START_REF] Halpern | Retronasal and orthonasal smelling[END_REF][START_REF] Heilman | A new method for comparing orthonasal and retronasal olfaction[END_REF][START_REF] Hummel | Retronasal perception of odors[END_REF][START_REF] Hummel | Perceptual differences between chemical stimuli presented through the ortho-or retronasal route[END_REF][START_REF] Sun | Identification of air phase retronasal and orthonasal odorant pairs[END_REF][START_REF] Visschers | Cross-Modality of Texture and Aroma Perception Is Independent of Orthonasal or Retronasal Stimulation[END_REF][START_REF] Welge-Lüssen | Swallowing Is Differentially Influenced by Retronasal Compared with Orthonasal Stimulation in Combination with Gustatory Stimuli[END_REF]. The large number and the variety of mechanisms (physical, chemical, physiological, neurobiological, cognitive, etc.) that can be involved at different space and time scales largely contribute to the complexity of perception. Among them, the release dynamics of aroma compounds have long been known to be among key factors to explain aromatic perceptions [START_REF] Barron | Impact of crema on the aroma release and the in-mouth sensory perception of espresso coffee[END_REF][START_REF] Biasioli | Correlation of PTR-MS spectral fingerprints with sensory characterisation of flavour and odour profile of "Trentingrana" cheese[END_REF][START_REF] Déléris | The dynamics of aroma release during the consumption of candies with different structures. Relationship with temporal perception[END_REF][START_REF] Gierczynski | Aroma perception in dairy products: the roles of texture, aroma release and consumer physiology. A review[END_REF][START_REF] Heenan | Characterization of fresh bread flavour: Relationships between sensory characteristics and volatile composition[END_REF]. Numerous studies in the literature have focused on the identification of the main factors that can impact release kinetics, either related to the physicochemical properties of the molecules, to product characteristics (composition, structure), to individual physiology (saliva composition and flow rate, breath flow rate) or to oral processing (chewing efficiency, product coating, etc.) [START_REF] Benjamin | Tongue Pressure and Oral Conditions Affect Volatile Release from Liquid Systems in a Model Mouth[END_REF][START_REF] Buettner | Chemical input -Sensory output: Diverse modes of physiology-flavour interaction[END_REF]Foster et al., 2011;Frank et al., 2012;[START_REF] Gierczynski | Aroma perception in dairy products: the roles of texture, aroma release and consumer physiology. A review[END_REF][START_REF] Heath | The oral management of food: the bases of oral success and for understanding the sensations that drive us to eat[END_REF][START_REF] Heenan | PTR-TOF-MS monitoring of in vitro and in vivo flavour release in cereal bars with varying sugar composition[END_REF]. The existence of aroma compound retention by wetted mucosa has often been proposed to explain specific release behaviours, but little is known about the origin of this phenomenon. However, several mechanisms have been suggested in the literature: the interaction of aroma compounds with the constituents of the mucus layer (mucins, enzymes, antioxidants, ionic compounds), with saliva and/or with the mucosa tissues themselves [START_REF] Buettner | Chemical input -Sensory output: Diverse modes of physiology-flavour interaction[END_REF]; the role of the contact area between nasal mucus and air [START_REF] Keyhani | A numerical model of nasal odorant transport for the analysis of human olfaction[END_REF]; the role of the physicochemical properties of aroma compounds (Ferreira et al., 2006;[START_REF] Tromelin | Retention-release equilibrium of aroma compounds in polysaccharide gels: Study by quantitative structureactivity/property relationships approach[END_REF]; and the role of breath and/or salivary flow rates [START_REF] Buettner | Investigation of the Retronasal Perception of Strawberry Aroma Aftersmell Depending on Matrix Composition[END_REF][START_REF] Hodgson | In vivo studies on the long term persistence of volatiles in the breath[END_REF].

Performing in vivo experiments and developing appropriate experimental set-ups constitute the main difficulties involved in exploring this topic and in validating or not the assumptions.

A previous study proposed various simple protocols to explore and quantify in vivo aroma release and persistence from gaseous samples, depending on the exposed physiological cavities (nose, mouth or pharynx) [START_REF] Déléris | Experimental approaches to better understand the retention of aroma compounds in oro-naso-pharyngeal cavities in[END_REF]. Results confirmed the main role of aroma compound properties and highlighted the possible occurrence of different types of mechanisms, either physical or biochemical, to explain release behaviours. The global nature of the approach and the complexity of the phenomena involved did not allow the authors to clearly identify the relative contribution of each mechanism.

The difficulty of dissociating all of the phenomena that occur during in vivo experiments generally prevents from determining the respective contribution of product properties or of consumer characteristics to aroma release. Due to these experimental issues, the modelling approach (in silico) can be a useful tool to improve the understanding. It has been largely used in the fields of pharmacokinetics and toxicology: Quantitative Structure-Activity Relationships (QSAR) (Geerts and Heyden, 2011), Physiologically-Based Pharmaco-Kinetic (PB-PK) [START_REF] Corley | Comparative Computational Modeling of Airflows and Vapor Dosimetry in the Respiratory Tracts of Rat, Monkey, and Human[END_REF][START_REF] Medinsky | Advances in biologically based models for respiratory-tract uptake of inhaled volatiles[END_REF][START_REF] Morris | Biologically-based modeling insights in inhaled vapor absorption and dosimetry[END_REF] and Theoretical Passive Absorption (TPAM) [START_REF] Obata | Prediction of oral drug absorption in humans by theoretical passive absorption model[END_REF][START_REF] Takano | Oral absorption of poorly water-soluble drugs: Computer simulation of fraction absorbed in humans from a miniscale dissolution test[END_REF] models have helped to better understand drug and toxic vapour absorption. In the field of olfaction, the QSAR approach has also been largely used to identify the main interactions between aroma compounds and olfactory receptors at the origin of perception [START_REF] Anker | Quantitative structure-retention relationship studies of odor-active aliphatic compounds with oxygen-containing functional groups[END_REF][START_REF] Chastrette | Structure-minty odour relationships: Suggestion of an interaction pattern[END_REF][START_REF] Kraft | Odds and trends: Recent developments in the chemistry of odorants[END_REF][START_REF] Rognon | Structure-odor relationships -a highly predictive tridimensional interaction-model for the bell-pepper note[END_REF][START_REF] Sanz | Relationships between molecular structure and perceived odor quality of ligands for a human olfactory receptor[END_REF]. Some of these models clearly highlighted the need to consider absorption/solubilisation phenomena in tissues of the respiratory tract and/or in the mucus layer to correctly represent the availability of aroma compounds for olfactory receptors. It was demonstrated that the transport of odorant molecules in nasal mucosa clearly differs from the one within an aqueous layer [START_REF] Kurtz | Experimental and numerical determination of odorant solubility in nasal and olfactory mucosa[END_REF]. The main limitation of modelling approaches remains the lack of experimental data, notably concerning the air/mucosa partition or diffusion properties of aroma compounds within the mucus layer, or mucosa characteristics depending on its location (nasal, oral or pharyngeal cavity).

In food science, some mechanistic models describing volatile release have been proposed and sometimes compared to experimental in vivo data [START_REF] Buffo | Persistence of aroma compounds in human breath after consuming an aqueous model aroma mixture[END_REF][START_REF] Harrison | Mathematical models of release and transport of flavors from foods in the mouth to the olfactory epithelium[END_REF][START_REF] Harrison | Mathematical model of flavor release from liquids containing aroma-binding macromolecules[END_REF][START_REF] Hodgson | Aroma release and delivery following the consumption of beverages[END_REF][START_REF] Normand | Modeling the Kinetics of Flavour Release during Drinking[END_REF][START_REF] Wright | Modelling flavour release from a chewed bolus in the mouth: Part II. The release kinetics[END_REF]. These models, based on physical, chemical and physiological parameters, led to more or less good predictions of the release kinetics of aroma compounds, but only for liquid food products. Only the models of [START_REF] Wright | Modelling flavour release from a chewed bolus in the mouth: Part II. The release kinetics[END_REF] and [START_REF] Normand | Modeling the Kinetics of Flavour Release during Drinking[END_REF] included a term representing possible interactions between aroma compounds and mucosa and/or salivary constituents. Even though many publications exist on molecular mechanisms that explain interactions between aroma compounds and proteins in the mucus of the nasal cavity of rats (Odorant Binding Proteins, OBPs), results cannot be directly used to explain in vivo release kinetics in humans [START_REF] Borysik | Rapid Odorant Release in Mammalian Odour Binding Proteins Facilitates Their Temporal Coupling to Odorant Signals[END_REF][START_REF] Yabuki | Dynamics of Odorant Binding to Thin Aqueous Films of Rat-OBP3[END_REF]. All of these studies constitute a first step in describing the phenomena involved but do not yet provide a clear understanding. In a previous publication, a mathematical model was proposed to predict in vivo aroma release from masticated food products that considered food properties and the physiological characteristics of the individuals (Doyennette et al., 2014). Comparison between experimental and predicted kinetics highlighted the possible specific retention of one hydrophobic aroma compound by wetted mucosa and mucus in the naso-oro-pharyngeal cavities. This model thus needs to be further developed to propose a satisfactory quantitative description of the retention phenomenon at the origin of aroma persistence.

In this context, the main goal of the present study is to better understand the mechanisms underlying aroma release and persistence. The originality of the proposed approach is to combine: (i) in vivo aroma release measurements (using controlled protocols to ensure aroma supply by flavoured air inhalation, without the interference of any food product); with (ii) the detailed mechanistic modelling of mass transfer to investigate the key mechanisms responsible for the release profiles and/or retention of aroma compounds.

Material and methods

Even if this study was not performed in the field of medical research, a detailed research protocol containing the relevant information in agreement with the World Medical Association Declaration of Helsinki was done. Only single-use materials were used with panellists. Aroma compounds were all food grade and their liquid concentrations were adjusted to limit gaseous concentration and ensure panellist comfort and avoid sensory saturation. Only one session (45 minutes) per week was planned for each panellist and the number of samples during one session was limited to five. Samples were coded to protect the privacy of panellist and the confidentiality of their personal information. Subjects were clearly informed of the observational nature of this study, gave their free and informed consent and received compensation for their participation.

Aroma compounds

Food grade quality aroma compounds (ethyl propanoate, 2-nonanone and (Z)-3-hexen-1-ol) were purchased from Sigma Aldrich (France) (Table 1).

They were selected since they belong to several chemical classes and present different physicochemical properties and different release behaviours in terms of persistence [START_REF] Déléris | Experimental approaches to better understand the retention of aroma compounds in oro-naso-pharyngeal cavities in[END_REF]. Concentrated stock solutions were prepared in polypropylene glycol (Sigma Aldrich, France) and used throughout the study. Diluted solutions were prepared extemporaneously.

Gaseous sample preparation

An aroma compound mixture was used to reduce the number of experimental sessions.

Gaseous samples were prepared as previously described [START_REF] Déléris | Experimental approaches to better understand the retention of aroma compounds in oro-naso-pharyngeal cavities in[END_REF]. The concentrations of aroma compounds in the liquid phase were high enough to be detected during PTR-MS measurements, while being acceptable from a sensory point of view for the panellists: 1000 mg/kg for (Z)-3-hexen-1-ol, 150 mg/kg for ethyl propanoate and 100 mg/kg for 2-nonanone.

Twenty-five mL of flavoured aqueous solution were stored at ambient temperature for 4 hours before measurements in 250-mL flasks (Schott, France), closed by caps equipped with valves (equilibrium establishment). To control the inhaled volume of gaseous sample (and, therefore, the amount of inhaled aroma compounds) between the different assays, a specific set-up was developed to prepare gaseous samples (Figure 1): a manual pump was connected to one of the cap valves and used to push some fresh air into the flasks. By way of this procedure, flavoured air was introduced into a balloon positioned on the other valve of the flask cap.

Three pump strokes were needed to prepare 200 mL of gaseous sample, which was considered as appropriate to be inhaled by panellists in one breath. Once inflated, balloons were closed with plastic pliers.

The study of the variation of aroma concentration within balloons during storage highlighted the fact that this preparation had to be done less than 30 s before measurement to avoid any loss of aroma compounds (not shown). Even if some interactions between aroma compounds and balloon material could occur, they were assumed to always be the same and to not influence the results since all conditions were controlled.

Panellists

Eight panellists (four men and four women, 22-45 years old) were recruited for the study.

They were instructed not to smoke, eat, drink or use any persistent-flavoured product for at least one hour before Proton Transfer Reaction-Mass Spectrometry (PTR-MS) or saliva collection sessions.

When dealing with aroma release and food oral processing, lots of studies in literature largely highlighted the key role that anatomy and physiology can have on the dynamics of phenomena [START_REF] Buettner | Chemical input -Sensory output: Diverse modes of physiology-flavour interaction[END_REF]Féron et al., 2014;Foster et al., 2011;Repoux et al., 2012b). Some physiological measurements were thus performed on panellists who participated to this study to define the range of variation of these parameters for the panel.

The volumes of the oral, nasal and pharyngeal cavities of the subjects were measured with the Eccovision Acoustic Rhinopharyngometer (Sleep Group Solutions, North Miami Beach, FL, USA). Software was developed to automatically calculate the air/product areas of the oral and pharyngeal cavities for each individual (Doyennette et al., 2011). The tidal volume of each individual was measured with a spirometer (Pulmo System II, MSR, Rungis, France) (Repoux et al., 2012a).

Non-stimulated saliva was collected by asking volunteers to swallow the saliva in their mouth before starting and to then spit each 30 s for 5 min into ice-chilled vessels. The final saliva weight was measured and the flow rate was calculated as g/min. Whole saliva samples were centrifuged at 13400×g for 5 min at 4°C to remove cellular debris (Eppendorf, model 5415 R, Germany). The supernatants were frozen and stored at -80°C before analysis. Protein concentration (expressed in mg/mL) was obtained by standard Bradford protein assay Quick Start (Bio-Rad, France) using bovine serum albumin (Sigma-Aldrich, France) as the standard calibration. The lipolytic (lipolysis), proteolytic (proteolysis), lysozymal (lysozyme) and amylolytic (amylase) activities of individual salivas (expressed in U/mL) were determined as previously described [START_REF] Neyraud | Variability of human saliva composition: Possible relationships with fat perception and liking[END_REF].

Three replicates per physiological parameter and per panellist were performed. The minimal, median and maximal values of physiological characteristics and associated quartiles are summarized in Table 2. 2.4. Determination of aroma in vivo release kinetics using PTR-MS measurements Release kinetics were obtained using the reference protocol previously defined (referred to as the Nose, Mouth, Swallowing protocol, or N.M.S.) [START_REF] Déléris | Experimental approaches to better understand the retention of aroma compounds in oro-naso-pharyngeal cavities in[END_REF]: sample inhalation was performed through the panellist's mouth in one short breath and the measurement of aroma release was made within the panellist's nasal cavity.

During a session, subjects started with the analysis of a blank sample to get used to the protocol and then tested five samples. The measurement procedure was similar to the one previously described [START_REF] Déléris | Experimental approaches to better understand the retention of aroma compounds in oro-naso-pharyngeal cavities in[END_REF]: room and breath analyses for 10 s and 30 s, respectively, followed by sample inhalation and release measurement. During the assay, panellists were allowed to swallow. Between each sample, panellists cleaned their mouth with mineral water (Evian, Danone) and their breath was retested before each new measurement. Some differences with the previous study should be mentioned. First, swallowing events were imposed: 20 s after sample inhalation for the first swallow, and then every 30 s until the end of measurement. Secondly, the sample volume was standardised, allowing the quantitative comparison between protocols. Three sessions of 45 min were planned to obtain three replicates of the five samples for each subject. All the measurements were performed within a 21-day period.

The High-Sensitivity Proton Transfer Reaction-Mass Spectrometer (PTR-MS) (Ionicon Analytik, Innsbruck, Austria) was operated at a drift tube temperature, voltage and pressure of 60°C, 600.1 (0.4) V and 2.0 (0.01) mbar, respectively (E/N=151.4 (1.4) Td). Nose-space was sampled via two inlets of a stainless nosepiece placed in both nostrils of the assessors.

The inlet of the PTR-MS instrument was connected to the sampling device via a 1/16" PEEK ™ tube maintained at 110°C. Measurements were performed using the Multiple Ion Detection (MID) mode. For a mass/charge ratio (m/z) of 21 (H 3 O + ) and 37 (H 2 O-H 3 O + ), the dwell time per mass was fixed to 0.05 s. The mean signal for H 3 O + was 7.8×10 6  0.8×10 6 counts per second (cps) and its day-to-day variation along the measurement period was 10%.

The signal for H 2 O-H 3 O + did not exceed 4% of the one of m/z 21 (in agreement with equipment specifications).

Using the fragmentation patterns of individual compounds (Table 1), the molecules studied were monitored at m/z 83 ((Z)-3-hexen-1-ol), m/z 75 and 103 (ethyl propanoate) and m/z 143 (2-nonanone). For these four specific masses, a dwell time per mass of 0.1 s was selected as a compromise between sensitivity for aroma compound detection and appropriate sampling frequency with regard to phenomena to be measured. In addition, m/z 59 and 93 were monitored with a dwell time per mass of 0.05 s as markers of panellists' breath [START_REF] Weel | Flavor Release and Perception of Flavored Whey Protein Gels: Perception Is Determined by Texture Rather than by Release[END_REF] and of balloon material, respectively. With these settings, exhaled air was sampled every 0.6 s, which was assumed to be appropriate regarding the mean duration of the breathing cycle (Doyennette et al., 2011;[START_REF] Sherwood | Fundamentals of physiology: a human perspective[END_REF][START_REF] Tortora | Principles of anatomy and physiology Harper-Collins[END_REF].

Mean signal-to-noise ratios varied between 2.0 and 38.0 (depending on the ions), meaning that responses during sample analysis sufficiently exceeded the baseline. These measurements led to the determination of molecule release kinetics, i.e., intensity I t = f(time t), for each panellist. Since solution composition was precisely known, aroma compounds were unambiguously detected at the stated m/z ratio. For this reason and to facilitate text readability, compound names rather than their m/z ratio are used hereafter.

For data handling, experimental release curves were divided into three main periods: (i) the phase before the product was inhaled (phase 0); (ii) the phase before the first swallow (phase 1); and (iii) the phase after the first swallow (phase 2). For each sample, the mean PTR-MS signal measured during phase 0 was subtracted from the PTR-MS signals obtained during phases 1 and 2. Some quantitative release parameters were extracted from each individual release curve and for each phase of product consumption: maximal intensities (I max1 and I max2 ), which indicate the maximum concentration reached by a compound; and areas under the curve (AUC 1 and AUC 2 ), which are related to the total amount of molecule that is released). The ratios between areas under the curve before and after swallowing were also calculated (AUC 1 /AUC 2 ). Some temporal release parameters such as times at which I max occurred (t max1 and t max2 ) and initial release rates (Rate 1 and Rate 2 , calculated by dividing the I max values with the t max times) were also determined. Peak widths for each phase were obtained as the difference between the two times at which the intensity was 20% of I max (after and before release peak) (t 20%_1 and t 20%_2 ). The difference between the time at which the intensity was 50% of I max after the peak and t max (t 50%-t max ) was also extracted. In addition, standardised release kinetics were obtained by dividing each intensity value of the curve by the corresponding I max (I t_stand =I t /I max ). Standardised areas under the curve (AUC stand. ), determined from these standardised kinetics, were used as an indication of persistence behaviour. Because the objective was to compare the persistence of aroma release between molecules, the use of arbitrary units for aroma concentration data was sufficient for data analysis. Since the two ions related to ethyl propanoate behaved in the same way, only the result of m/z 75 is presented in the text.

Non-parametric descriptive analysis was carried out on datasets and comparative analysis was performed using Kruskal-Wallis tests and the Conover-Iman procedure (multiple paired comparisons) to highlight differences in in vivo release kinetics between molecules. The level of significance was set at p<0.05.

Modelling

Principles of the model

The aroma release model presented in this study was developed to describe aroma release after one inhalation of a gaseous sample through the mouth. It is based on equations that describe mass transfers that occur between the different physiological cavities (mouth, nose, pharynx), considered as interconnected reactors that vary in volume and that exchange matter.

A schematic representation of the four physiological cavities involved in the model design, as well as their connections and the mechanisms responsible for aroma release, are given in Figure 2. A schematic representation of mass transfer between air, saliva and mucosa within a physiological cavity is presented in Figure 3. All variables and parameters required for the model simulation are specified in these figures and described in Tables 3 and4, respectively.

The model describes the steps of the experimental protocol: sample inhalation through the mouth, exposure period to the sample until the first swallow, and post-swallow release.

Except for the first inhalation, breathing occurs through the nose. Each swallowing step is known to be very short [START_REF] Martin-Harris | Coordination of respiration and swallowing[END_REF] compared to persistence phenomena [START_REF] Hodgson | In vivo studies on the long term persistence of volatiles in the breath[END_REF][START_REF] Normand | Modeling the Kinetics of Flavour Release during Drinking[END_REF]. Swallowing events are thus described as quick simultaneous contractions of the oral cavity and of the pharynx, leading to air expulsion, followed by relaxation and filling with fresh air (Doyennette et al., 2014).

Two compartments in the mouth and in the pharynx (mucosa and saliva) and one compartment in the nose (mucosa) were included in the model to introduce a reservoir effect (Figure 2). In each cavity, the air phase was assumed to be in contact with mucosa and/or saliva layers. The proportions of these contact areas can be changed in the model to evaluate the respective contributions of saliva and mucosa. The volumes of the layers involved in the interaction with aroma compounds were expressed as products between compartment areas and layer thicknesses (Eq. (A.12) to Eq. (A.16) in the Appendix A). Similarly to Doyennette et al. (2014), transfer resistances on the air side (1/k Oa , 1/k Fa and 1/k Na ) were assumed to be negligible when compared to the transfer resistance on the wetted mucosa or saliva sides (1/k Om , 1/k Fm , 1/k Nm and 1/k Os , 1/k Fs , respectively).

To improve the readability of the paper, only generic equations describing phenomena are given in the text. They were written specifically for each compartment to obtain the complete description of aroma release. The details of all model equations are given in the Appendix A.

Air flow rates

By convention, the air flow rates indicated in Figure 2 are positive if they follow the direction of the arrow. With this convention, air flow rates in the different cavities Q Oa , Q OFa , Q Na and Q NFa are positive (or null, depending on whether breathing occurs through the nose or the mouth) during inhalation, and negative (or null) during exhalation. Conversely, air flow rate from the trachea Q Ta is negative during inhalation and positive during exhalation.

Air flow rate in the trachea due to breathing was assumed sinusoidal (Eq. (A.33)). According to Figure 2 and to the experimental protocol, the air flow rate in the mouth is given by the breathing flow rate during the first inhalation and is null afterwards (Eq. (A.34)). The opposite was considered for the air flow rate in the nasal cavity (Eq. (A.35)). According to Figure 2, the air balance in the pharynx at any time is given by the equality of inlet and outlet fluxes (Eq. (A.36)).

Saliva in oral cavity

The volume of saliva in the oral cavity gradually increases due to the salivary flow rate Q Os and abruptly decreases after swallowing. A minimal residual volume of saliva V Osmin was assumed to remain in the mouth after swallowing (Doyennette et al., 2014).

Mathematical description of interfacial conditions and fluxes

Air/mucosa and air /saliva interfaces

The interfacial aroma compound concentrations at air/mucosa or air/saliva interfaces were obtained from the partition conditions at the interfaces, using the following generic equations:

Eq. 1

Recall that transfer resistances on the air side were assumed negligible, hence, in the air, bulk and interfacial concentrations are identical. Specifically, the air/mucosa interfacial aroma compound concentrations are described by Eq. (A.17), Eq. (A.18) and Eq. (A.19) in oral, nasal or pharyngeal cavities, respectively. The air/saliva interfacial aroma compound concentrations are given by Eq. (A.20) and Eq. (A.21) in the oral or pharyngeal cavities, respectively.

Volatile mass fluxes and between the air and the other compartments (mucosa or saliva) are determined by the resistances located on the mucosa and saliva sides, respectively.

They are given by the difference between the mucosa (C m ) or saliva (C s ) concentrations and the interfacial concentrations ( ) or ( ) and are calculated using the following generic equations:

Eq. 2 Specifically, in the oral cavity these fluxes are given by Eq. (A.26) and Eq. (A.29), in the pharynx by Eq. (A.28) and Eq. (A.30) and in the nose by Eq. (A.27).

Mucosa/saliva interface

Since the mucosa was assumed to be partially wetted by the saliva, aroma partition and flux between mucosa and saliva compartments was also considered in the oral and pharyngeal cavities. Transfer resistances were considered in both saliva and mucosa layers since they are expected to be of comparable magnitude. Interfacial aroma compound concentrations at mucosa/saliva interface were obtained from the partition conditions at the interfaces, using the following generic equation (Figure 3):

Eq. 3

The mucosa/saliva interfacial aroma compound concentrations are described by Eq. (A.22) and Eq. (A.24) in oral or pharyngeal cavities, respectively. The partition coefficients between mucosa and saliva were calculated based on partition coefficients with the air phase (Eq.

(A.23) and Eq. (A.25)):

Eq. 4

Since the mucosa was assumed to be partially wetted by the saliva, a volatile flux between saliva and mucosa was also considered (Eq. (A.31) in the oral cavity and Eq. (A.32) in the pharyngeal cavity):

Eq. 5 with being the equivalent mass transfer coefficients between saliva and wetted mucosa, with saliva taken as reference. It includes resistances in both phases in contact and the partition between them [START_REF] Marin | Volatile release from aqueous solutions under dynamic headspace dilution conditions[END_REF]:

Eq. 6

Volatile mass balances

According to Figure 2, in each considered cavity the air may exchange aroma compounds with mucosa, saliva and air of connected cavities, as applicable. The generic volatile mass balance for the air in a cavity has the following form, where the term "source" denotes cavities which supply air to the cavity under consideration:

Eq. 7

For the first inhalation, the variation of aroma concentration in the air in the oral cavity C Oa is due to the volatile flux from the inhaled air sample and also to contact with the mucosa and saliva layers (Eq. (A.37)). For the following breathing cycles (through the nose), the mouth is closed (Eq. (A.38)). The mass balance in the air of the nasal cavity is given by Eq. (A.39), with no saliva layer present and the possible source of volatile compounds being the pharynx, during expiration. The pharynx has both saliva and mucosa layers and can exchange air with the mouth (first inhalation) nose (subsequent breathing) and trachea, as described by Eq.

(A.40).

Saliva layers in mouth (Eq. (A.41)) and pharynx (Eq. (A.42)) exchange aroma compounds with air and mucosa, according to the generic mass balance:

Eq. 8

with the saliva in the oral cavity being additionally diluted by the fresh saliva flow rate.

Mucosa layers are in contact with air and saliva (except in the nose) and the mass balance for these layers was written on the basis of Eq. 9 (developed as (Eq. A.43), (Eq. A.44) and (Eq.

A.45) in the oral, nasal and pharyngeal cavities, respectively):

Eq. 9

Reference values of the parameters

The reference values of parameters used for simulations are given in Table 4. Some were taken from experimental data or from the literature, and were estimated when little information was available. For instance, the contact area between air and mucosa in the nose A Nam was set to 150 cm² [START_REF] Levitzky | Pulmonary physiology[END_REF]. Concerning air/mucosa partition properties, values comprised between 5.6×10 -5 and 4.8×10 -1 were found for the air/mucus partition coefficient of butanol and octanol in bullfrog [START_REF] Hornung | Olfactory Mucosa-Air Partitioning of Odorants[END_REF]. Thus, a typical reference value of 1×10 -3 was selected in this case. Concerning the mucosa layer thickness, values between 500 and 800 µm in the mouth and 100 to 200 µm for the gingival mucosa were reported [START_REF] Patel | Modeling the oral cavity: In vitro and in vivo evaluations of buccal drug delivery systems[END_REF][START_REF] Shojaei | Buccal mucosa as a route for systemic drug delivery: a review[END_REF]. It is expected, however, that aroma compounds will not necessarily have time to diffuse in the whole epithelium thickness, so these values were considered as upper limits for the mucosa layer thickness involved in aroma retention.

Sensitivity analysis

The model contains a total of 27 independent parameters (Table 4), i.e. which cannot be calculated based on other ones (such as a volume being the product of an area and a layer thickness). To assess the importance of these parameters for the prediction of the volatile compound concentration in the nasal cavity (model output) a global Monte Carlo sensitivity analysis was performed as follows. The model output was the relative volatile concentration in the nasal cavity ( ), i.e. the predicted concentration ( ) of the aroma compound divided by its maximum value. For a given value p j of each parameter p, the relative local sensitivity was defined as:

Eq. ( 10)

where is the output of the model calculated for time with the considered parameter value set to p j and is a perturbation of the parameter, taken as 10% of its minimum value indicated in Table 4. Thus represents an approximation of the partial derivative of the nasal concentration with respect to the considered parameter, taken in absolute value and averaged over time. To make sensitivities dimensionless, of order of unity and hence comparable among various parameters, the right-hand side scaling factor was introduced, based on the reference value of the parameter given in Table 4.

The global sensitivity of a parameter was calculated as an average of local sensitivities across a large number of samples taken in the parametric space:

Eq. ( 11)

The parametric space was defined by the range of variation of each parameter indicated in Table 4 and sampled according to a multidimensional "Latin hypercube" method to ensure a uniform representation of all parameter values. Parameters whose range of variation spanned more than one order of magnitude were evenly sampled on a logarithmic rather than linear scale.

Automatic sensitivity analysis gives global information on the relative importance of various parameters for the nasal concentration prediction, but provides little insight in the involved phenomena. A manual sensitivity analysis was also performed by varying some of the parameters (specified in the results section) one by one while keeping the others at their reference values. Parameters whose possible variation range was large (sometimes several orders of magnitude) were included in the manual sensitivity analysis, while those relatively well known from the experimental protocol and physiological measurements were kept constant.

Model fitting

To test the ability of the model to reproduce release curves observed for different molecules, some of the least well known parameters were estimated based on release data. The number of estimated parameters was kept at a minimum, however. Volumes, contact areas, respiratory frequency and deglutition times were either known from physiological measurements or imposed by the experimental protocol; these parameters were kept fixed to their reference values indicated in Table 4. Partition coefficients between air and saliva ( ) were experimentally determined for the three aroma compounds; these values were used without change. The estimated parameters, assumed to be the same in all cavities, were the transfer coefficient in the saliva ( , the same for all molecules) because in vivo hydrodynamic conditions are poorly known, and parameters related to the mucosa layer: thickness ( , common to all molecules), transfer coefficient ( , also common to all molecules) and air/mucosa partition coefficients ( ),

expected to vary strongly with the physico-chemical properties of the studied compounds and hence specific to each molecule.

Model fitting was thus performed simultaneously using data from release experiments with the three molecules, the partition coefficients being specific to each molecule but common to all cavities and the other abovementioned parameters common to all molecules and all cavities. The fitting criterion was the sum of the absolute values of the errors between model predictions and experimental measurements of the compound concentration in the nasal cavity, both normalised by their respective maximum values ( ), because measured data was only available in arbitrary units. Since possible ranges of some of the parameters span up to 4 orders of magnitude (Table 4) a "global" optimisation procedure based on genetic programming was used, namely the "ga" implementation in the Matlab® Global Optimization Toolbox, with default settings (e.g. population of 40 individuals, convergence tolerance 10 -6 )

and the maximum number of generations increased to 200. Parameters whose search range (Table 4) spanned more than one order of magnitude were sampled on a logarithmic scale, i.e.

the logarithm of the parameter was actually searched for by the optimisation algorithm. Since the considered optimisation algorithm is stochastic, several (~10) optimisation runs were performed and the one with the best fit was selected. Consistent convergence to similar values of the parameters (usually within ±15%) was observed in most runs.

Results and discussion

Molecule specific effects on aroma release kinetics

As previously highlighted [START_REF] Déléris | Experimental approaches to better understand the retention of aroma compounds in oro-naso-pharyngeal cavities in[END_REF], significant differences between aroma compounds in terms of release descriptors were observed (Figure 4).

Differences in I max1 and I max2 and in AUC 1 and AUC 2 were explained by differences in inhaled gaseous concentrations of molecules due to different aqueous concentrations and air/water partition properties. They were thus not shown nor discussed here.

Before swallowing (Figure 4-a), no difference between molecules was observed concerning t max . Yet, the peak width t 20%_1 of 2-nonanone was the largest and those of ethyl propanoate the narrowest. After swallowing, differences in release behaviours were more pronounced since some temporal parameters were significantly different between molecules: ethyl propanoate was released the most rapidly and with a quite narrow peak, whereas (Z)-3-hexen-1-ol had the most delayed release, with the largest peak at 50% of I max (t 50%-t max ), and 2-nonanone had the largest peak at 20% of I max t 20%_2 ) (Figure 4-b). Initial release rates were molecule-dependent both before and after swallowing (Figure 4-c). Ethyl propanoate was released faster than (Z)-3-hexen-1-ol (before and after swallowing) and 2-nonanone (only before swallowing).

AUC stand , which can be associated with molecule persistence, also reflected differences in release behaviour: the highest value was obtained for 2-nonanone, highlighting quite persistent release behaviour for this molecule (Figure 4-d). In contrast, ethyl propanoate presented the lowest values of AUC stand . The AUC 1 /AUC 2 ratios were higher than 1 for all molecules, meaning that a greater amount was released before swallowing than after.

However, a 30-fold increase in AUC 1 /AUC 2 ratio was observed between 2-nonanone and ethyl propanoate, meaning that the latter was mainly released before swallowing, whereas 2-nonanone was released during both phases.

All these results were in agreement with previous observations and confirmed the probable existence of retention phenomena for some aroma compounds. To get insight in the exact nature of these interactions, notably in the respective roles of the physicochemical properties of the molecules, of saliva and/or of mucosa characteristics, model simulations and sensitivity analysis were used.

We could also mention that from these results, no clear relationship between aroma release and anatomical or physiological parameters was observed

Simulations of aroma compound release kinetics

One of the advantages of using a modelling approach is the possible determination of the time variation of variables that could not be experimentally determined, providing insight in the involved mechanisms. Examples of simulated release kinetics obtained with the model in the different compartments of the naso-oro-pharyngeal cavities are presented in Figure 5.

As a starting point, model parameters were fixed to their reference values, determined either from data in the literature or experimentally (Table 4). Air/mucosa contact areas in the mouth A Oam and in the pharynx A Fam were fixed at 10% of the total area of the mouth A O and the pharynx A F , respectively, meaning that 90% of the mouth and pharynx surfaces were wetted and 5-g, respectively). The saliva volume in the mouth followed a cyclic variation, with a linear increase due to the saliva flow rate between each swallowing event and a sudden decrease when swallowing occurred.

Sensitivity analysis of the model to physicochemical and physiological parameters

Modelling makes it possible to easily test the effect of parameters that govern mass transfers, notably those that cannot be modified when performing in vivo studies. Such a sensitivity analysis can contribute to the determination of the nature of the key factors underlying aroma release and persistence.

Global sensitivity analysis

Based on the results of the global sensitivity analysis performed as described in section 3.7.2, model parameters were arbitrarily divided in three groups, according to their influence on the shape of the nasal concentration release curve (recall that nasal concentration was always normalized by its maximum value). The first group included 3 most influential parameters, with global relative sensitivities comprised between 0.4 and 0.2: the air/mucosa partition coefficients in the nose (K Nam ) and in the pharynx (K Fam ) and the respiratory frequency (F R ). The second group included 5 moderately influential parameters, with sensitivities between 0.1 and 0.025: air/mucosa partition coefficient in the mouth (K Oam ), air/saliva partition coefficient in the mouth (K Oas ) and pharynx (K Fas ), mass transfer coefficient in the mouth (k Os ) and the tidal volume (V C ). The other parameters listed in Table 4 had sensitivities less than 0.025.

Overall, these results support the central assumption underlying this work, namely that in absence of any food product, volatile persistence in consumer's exhaled air is mainly related to the interaction between the aroma compound and subject's mucosa, quantified in the model via the air/mucosa partition coefficients. A second important factor, already pointed out in presence of non masticated [START_REF] Tréléa | Mechanistic mathematical model for in vivo aroma release during eating of semi-liquid foods[END_REF] and masticated (Doyennette et al., 2014) food products, is the consumer's breath via the respiratory frequency and current breath volume.

Mass transfer and geometry (volumes, contact areas) appear to play a smaller role in volatile persistence than in release from food products.

Manual sensitivity analysis

When dealing with mass transfer, the main factors governing molecule transports are the contact area, the driving force (dependent, in particular, on the partition properties of the molecules) and the mass transfer coefficient of the molecules. Simulations were thus performed to evaluate their influence on release kinetics. The ranges of variation of model parameter values were chosen to be in agreement with physicochemical or physiological values (Table 4). Only the effects of these modifications on the simulated release kinetics in the nasal cavity are explained since they correspond to what can be experimentally determined. The variation of aroma concentrations in other compartments were simulated but are not discussed here.

First, to better understand the respective roles of the saliva and mucosa compartments, some simulations were performed without any saliva compartment (air/mucosa contact areas in the mouth and in the pharynx were equal to the total surfaces of the mouth and the pharynx, respectively, so contact areas with saliva were equal to zero, Table 4) .

The absence of saliva as well as the modification of mucosa thickness (10-fold variation factor) did not have an impact on the shape of release kinetics of aroma compounds within the nasal cavity. Differences were mainly observed on mucosa concentration and unloading rates (not shown). For example, mucosa concentrations in the mouth and in the pharynx were 5 to 9-fold higher, respectively, without saliva than with saliva, and 10-fold higher or lower when the thickness decreased or increased, respectively. Mucosa compartments also unloaded more rapidly when saliva was not considered or when mucosa thicknesses were lower.

The mass transfer coefficient of aroma compounds in mucosa had a greater impact on the release kinetics in the nasal cavity when it increased than when it decreased (not shown).

With an increased mass transfer coefficient in mucosa, mucosa loading and unloading rates were higher. Since air flow rate remained constant between simulations, mucosa compartments were more rapidly unloaded and the gaseous concentration in the nose was thus lower and decreased more rapidly. The effects with decreased values of mass transfer coefficients were less obvious: below a value of 10 -6 m/s, very slow aroma transport prevents any significant amount of aroma compound to be loaded into the mucosa, so there is almost no impact on aroma concentration in the nose.

Decreasing the air/mucosa partition properties had a big impact on the nasal concentration of aroma compounds and the shape of release kinetics. A low air/mucosa partition means high affinity of the aroma compound for the mucosa compartment. Most of the aroma compound was thus retained within the mucosa and released very slowly in tiny amounts according to breathing cycles. Persistence was thus long but the actual concentration in the nasal cavity was low. A 100-fold increase in the air/mucosa partition from 10 -3 had less effect on the aroma concentration in the nose than a 100-fold decrease, due to the fact that the amounts of aroma compound loaded into the mucosa became negligible.

These results revealed which parameters related to mucosa had an impact on release kinetics.

However, except in the nasal cavity, mucosa is always wetted by a saliva film. Mucosa parameters were thus fixed to their reference values and saliva parameters were modified to evaluate their influence on aroma release kinetics. As a reference, it was assumed that saliva covered 90% of the mouth and pharynx surfaces.

Simulations were performed by increasing this percentage up to 100% without any significant effect (not shown). When saliva is considered, mucosa concentrations are lower due to: (i) the reduced contact area between air and mucosa and, consequently, lower loading rates of mucosa compartments in the mouth and in the pharynx; and (ii) the fact that part of the aroma compound was captured by saliva instead of mucosa. Nevertheless, there was no impact on nasal concentration and release kinetics.

100-fold variations in the mass transfer coefficients of molecules in saliva did not affect release kinetics in the nasal cavity (not shown). The only consequences were modifications of aroma concentrations in saliva.

Concerning the modifications of air/saliva partition properties, only a 100-fold decrease significantly modified release kinetics as a consequence of a higher affinity of aroma compounds for saliva. Saliva becomes the main aroma reservoir, supplying aroma compounds to the air in the nasal cavity until the first swallow at 20 s. Aroma concentrations increased in saliva (50-fold and 60-fold factors in the pharynx and the mouth, respectively) and decreased in mucosa (6-fold and 3-fold factors in the pharynx and the mouth, respectively) (not shown).

Simulations were also performed by varying mouth and pharynx volumes and the salivary flow rate (in the range of experimental values, determined on panellists), but no significant difference was obtained between simulations (not shown), confirming the absence of effect of these parameters in the range of variation that was tested.

On the basis of these results, it can be concluded that both saliva and mucosa had an impact on aroma release when the affinity of aroma compounds for these compartments was sufficiently high. Mechanistic modelling provided insight into the relative time distributions of the aroma compound among these compartments.

Adjustment of simulated release kinetics to experimental data

To validate model assumptions, model simulations were fitted to experimental data. Three experimental kinetics were used, each one representing specific release behaviour (related to specific aroma compounds). Several parameters were used as degrees of freedom: the effective mucosa thickness participating to aroma retention, the mass transfer coefficients of aroma compounds in saliva and in mucosa and the air/mucosa partition coefficients of aroma compounds. For these parameters, values were assumed to be the same in all physiological cavities (mouth, pharynx and nose). (1 panellist, 1 replicate) and simulated release kinetics of ethyl propanoate, (Z)-3-hexen-1-ol and 2-nonanone, respectively.

Concerning fitted parameters, the final value of mucosa thickness was modified (26 µm) but remained in a realistic order of magnitude. In a first approach, it was set at a similar value for all physiological cavities (nose, pharynx and mouth) since sensitivity analysis did not show a significant influence of this parameter on release kinetic shape. For further studies, it could perhaps be interesting to more accurately study the impact of this parameter since the nose, mouth and pharynx mucosa are clearly physiologically different.

The values of the mass transfer coefficients of aroma compounds reached 6.0×10 -5 m/s in saliva and 4.9×10 -5 m/s in mucosa. They were on the order of magnitude of the one used as a reference for simulations and were the same for the three molecules. This result is in agreement with the fact that these coefficients mainly depend on the hydrodynamics in the system and little on molecule properties [START_REF] Marin | Volatile release from aqueous solutions under dynamic headspace dilution conditions[END_REF]. The fact that the mass transfer coefficient in saliva was higher than the one in mucosa was quite expected and can be explained by the difference in viscosity between saliva and mucus. Yet, the absolute values of these mass transfer coefficients in mucosa and saliva were quite high in comparison with the data in the literature (3×10 -6 m/s) [START_REF] Marin | Volatile release from aqueous solutions under dynamic headspace dilution conditions[END_REF]. The high degree of mixing that probably exists in the naso-oro-pharyngeal cavities can account for this discrepancy (the data in the literature were related to in vitro studies).

The air/mucosa partition properties of aroma compounds ranged between 4.7×10 -4 (2nonanone) and 6.9×10 -3 (ethyl propanoate), the one of (Z)-3-hexen-1-ol being intermediate. In the case of ethyl propanoate, the air/mucosa partition coefficient increased by a factor of 7 compared to reference values, so that the model correctly predicted the experimental release kinetics. It thus appeared that this molecule has limited interaction with saliva and mucosa.

The shape of release kinetics in this case is therefore mainly explained by the pulse of the aroma compound due to sample inhalation and air renewal in the mouth at swallowing (Figure 6-a). Concerning 2-nonanone, the 2-fold decrease in the air/mucosa partition value suggests that 2-nonanone interacts more with mucosa than the other two compounds. For (Z)-3-hexen-1-ol, the value of air/mucosa partition properties after model fitting was only slightly modified in comparison to the reference values and remained thus in the same order of magnitude than the air/saliva partition coefficient.

On the basis of these results, we could argue that both air/mucosa and air/saliva partition properties are, at least partly, at the origin of the release behaviours that were observed for the molecules: the ones with the lower affinity for saliva and/or mucosa (highest partition coefficients) had the least persistent behaviour.

All these results confirmed that in vivo release behaviours were strongly molecule-dependent and highlighted the fact that different types of interactions with mucosa and/or saliva were involved, depending on the molecule's properties. These simulations were in agreement with previous experimental data, which notably showed the limited retention of ethyl propanoate and the specific retention of 2-nonanone in the oral and pharyngeal cavities [START_REF] Déléris | Experimental approaches to better understand the retention of aroma compounds in oro-naso-pharyngeal cavities in[END_REF]. To improve simulations, further development of the model could be foreseen, notably concerning assumptions on mucosa. This will require experimental determination of mucosa properties.

Conclusions

In conclusion, it appears that the proposed model adequately simulated aroma release and retention after the inhalation of a gaseous flavoured sample by panellists. The simulation of the time variation of concentrations that cannot be determined experimentally helped to better understand the involved phenomena. The sensitivity analysis contributed to distinguish the respective roles of saliva and mucosa on aroma retention phenomena. No clear effect of cavity volumes or saliva flow rate on aroma release kinetics was highlighted in the range of variation of parameters that was tested. But results confirmed the particular role of wetted mucosa can play, depending on aroma compound properties. This study constitutes a first step in understanding aroma persistence and further work is needed to clarify the relationships between the properties of molecules and the type of interactions that are involved. a Global sensitivity index: +++ means a highly influent parameter (sensitivity index between 0.4 and 0.2); ++ means a moderately influent parameter (sensitivity index between 0.1 and 0.025); + was used for parameters with sensitivity index below 0.025.

Appendix

Figure captions

V Na V Fm V Fs Vc Fr V Fa V Nm Q Ta Q NFa Q Na Q OFa f Nam f Fam f Fas f Fms C Om C Os V Om V Os Q Oa C Oa V Oa f Oam f Oas

  by saliva. The resulting kinetics were considered as a reference. The inset on each figure illustrates the first 3 seconds of the release to better understand initial phenomena. Just after sample inhalation through the mouth, the gaseous concentrations of aroma compounds in the pharynx C Fa and in the mouth C Oa increased respectively). In parallel, molecules accumulated within mucosa and saliva layers both in the mouth (Figures 5-e and 5f, respectively) and in the pharynx respectively). When the mouth was closed (at 2 s), aroma compound gaseous concentration in the air in the mouth started to decrease, as well as in the pharynx. In the mouth, the slow decrease in the gaseous concentration of aroma compounds after 2s was due to adsorption on mucosa and saliva layers. In the pharynx, the expiration flow rate accounts for the much faster decrease since it was responsible for the transport of aroma compounds from the pharynx to the nose (increase in aroma compound concentration in the nose C Na (Figure5-g) and, therefore, a decrease in aroma compound concentration in the pharynx C Fa (Figure5-a). The adsorption of aroma compounds on mucosa is also probably involved in this decrease. The pulse in aroma concentration in the nasal cavity led to an increase in aroma concentration within the nasal mucosa layer C Nm (Figure5-h). Yet, aroma compound concentration in the nose air rapidly decreased to zero since air from the lungs was aroma-free and the aroma transfer from the nasal mucosa to the air in the nose (which occurred as aroma concentration in the nasal mucosa progressively decreased; Figure5-h) was not rapid enough to compensate for the dilution by the breath flow rate. Similar conclusions can be drawn concerning the variation of concentrations in pharynx compartments.The first swallow occurred at 20 s. It led to a sudden decrease in saliva volume in the mouth V Os (Figure5-i), as well as decreases in aroma compound concentrations in the air within the mouth (C Oa , Figure5-d) and in saliva in the mouth C Os (Figure5-f) and in the pharynx C Fs (Figure5-c). In all mucosa compartments, concentrations C Fm , C Om and C Nm progressively decreased, highlighting the unloading of these compartments (Figures5-b, 5-e and 5-h, respectively). These mass transfers were probably the limiting steps since aroma concentrations in the different air phases C Fa , C Oa and C Na did not increase

Figures 6

 6 Figures 6-a, 6-b and 6-c indicate the good fit that was obtained between experimental

Fam g/cm 3

 3 Aroma concentration at the air/wetted mucosa interface in the pharynx C * Fas g/cm 3 Aroma concentration at the air/saliva interface in the pharynx C * Fms g/cm 3 Aroma concentration at the wetted mucosa/saliva interface in the pharynx, 3 Aroma concentration at the wetted mucosa/saliva interface in the pharynx, on the saliva side C Oa g/cm 3 Aroma concentration in the air in the oral cavity C Om g/cm 3 Aroma concentration in the wettedd mucosa in the oral cavity C Os g/cm 3 Aroma concentration in saliva in the oral cavity C * Oam g/cm 3 Aroma concentration at the air/wetted mucosa interface in the oral cavity C * Oas g/cm 3 Aroma concentration at the air/saliva interface in the oral cavity C * Oms g/cm 3 Aroma concentration at the wetted mucosa/saliva interface in the oral cavity, on the mucosa side C * Osm g/cm 3 Aroma concentration at the wetted mucosa/saliva interface in the oral cavity, on the saliva side C Na g/cm 3 Aroma concentration in the air in the nose C Nm g/cm 3 Aroma concentration in the mucosa in the nose C * Nam g/cm 3 Aroma concentration at the air/mucosa interface in the nose C Ta g/cm 3 Aroma concentration in the trachea Q Na cm 3 /s Air flow rate into the nasal cavity Q NFa cm 3 /s Air flow rate from the nasal cavity to the pharynx Q Oa cm 3 /s Air flow rate into the oral cavity (1 st inhalation) Q OFa cm 3 /s Air flow rate from the oral cavity to the pharynx Q Ta cm 3 /s Air flow rate from the trachea t Volatile mass flux between the air and the wetted mucosa in the pharynx  Fas g/s Volatile mass flux between the air and the saliva in the pharynx  Fms g/s Volatile mass flux between the wetted mucosa and the saliva in the pharynx  Nam g/s Volatile mass flux between the air and mucosa in the nasal cavity  Oam g/s Volatile mass flux between the air and the wetted mucosa in the oral cavity  Oas g/s Volatile mass flux between the air and the saliva in the oral cavity  Oms g/s Volatile mass flux between the wetted mucosa and the saliva in the oral cavity

Fig. 1 :Fig. 2 :

 12 Fig. 1: Schematic representation of the experimental set-up for the preparation of gaseous

Fig. 3 :

 3 Fig. 3: Schematic representation of the balances between the different compartments. Bold

Fig. 6 :

 6 Fig. 6: Comparison between individual experimental and simulated release kinetics of: (a)

Figure 1 .Figure1Figure 2 .

 12 Figure 1. Schematic representation of the experimental set-up for the preparation of gaseous

Figure2Figure 3 .Figure3Figure 4 .Figure4Figure 5 .Figure5Figure 6 .

 3456 Figure2

Figure6

  Figure6

Table 1 :

 1 Physicochemical properties of aroma compounds used in the present study. 870 1 : estimation with EPI Suite TM programme 871 2 : PTR-MS: Proton Transfer Reaction-Mass Spectrometry

	688		A: model equations
			Oral cavity	Nasal cavity	Pharynx
		Volumes
		wetted	Eq. (A.12)	Eq. (A.13)	Eq. (A.14)
		mucosa
		saliva	Eq. (A.15)	n. a.	Eq. (A.16)
		Interfacial concentrations
		air/mucosa	Eq. (A.17)	Eq. (A.18)	Eq. (A.19)
		air/saliva	Eq. (A.20)	n. a.	Eq. (A.21)
		mucosa/sal	Eq. (A.22)	n. a.	Eq. (A.24)
		iva	Eq. (A.23)		Eq. (A.25)
		Volatile mass fluxes
		air/mucosa	Eq. (A.26)	Eq. (A.27)	Eq. (A.28)
		air/saliva	Eq. (A.29)		Eq. (A.30)
		mucosa/sal iva	Eq. (A.31)		Eq. (A.32)
		Air flow
		rates
		breathing		Eq. (A.33)
			Eq. (A.34)	Eq. (A.35)	Eq. (A.36)
		Volatile mass balances
		air	Eq. (A.37)	Eq. (A.39)	Eq. (A.40)
			Eq. (A.38)
		saliva	Eq. (A.41)	n. a.	Eq. (A.42)
		mucosa	(Eq. A.43)	(Eq. A.44)	(Eq. A.45)
	689	n. a.: not applicable

Table 2 :

 2 Minimal, median and maximal values of the physiological characteristics of panellists and associated quartiles.

			Physiological parameters	min	Q1	median	Q3	max
	parameters Salivary	rest at	V C (L) V nose (cm 3 ) V mouth (cm 3 ) V pharynx (cm 3 ) Salivary flux (g/min) Antioxidant (eq mM Trolox) Lipolysis (mU/mL) Amylase (U/mL) Proteolysis (U/mL) Lysozyme (U/mL) Proteins (mg/mL)	0.49 5.8 33.1 16.8 0.32 75.4 0.04 67.4 1.6 313.2 332.2 413.9 0.54 0.80 9.5 11.1 35.5 39.3 24.3 27.4 0.44 0.54 90.7 105.7 0.08 0.15 88.7 124.8 1.9 4.1 0.46 0.55 0.81	0.86 13.1 56.7 30.2 0.66 127.5 0.19 148.6 4.8 444.1 0.94	0.93 16.8 69.8 34.8 0.87 137.3 0.27 196.0 11.2 462.1 1.15

Table 3 :

 3 Definition of model variables 877

	Symbol Unit Definition
	C Fa	g/cm 3 Aroma concentration in the air in the pharynx
	C Fm	g/cm 3 Aroma concentration in the wetted mucosa in the pharynx
	C Fs	g/cm 3 Aroma concentration in saliva in the pharynx
	C *

Table 4 :

 4 Definition, reference values and range of variations used for simulations of model 878

	879	parameters.
							Global sensitivity
	Symbol Unit	Definition	Reference value	Range of variation	analysis) a index (from Monte-Carlo	Source
	A F	cm²		Total area of the pharynx	65	32.5 ... 130	+	(Doyennette et al., 2014)
	A Fam	cm²	Air/mucosa contact area in pharynx			+	-
	A Fas	cm²	Air/saliva contact area in pharynx		/	+	-
	A Fms	cm²	Mucosa/saliva contact area in pharynx		/	+	-
	A Nam	cm²	Air/mucosa contact area in nose	150	75 ... 300	+	(Levitzky, 2003)
	A O	cm²		Total area in oral cavity	116	58 ... 232	+	(Doyennette et al., 2014)
	A Oam	cm²	Air/mucosa contact area in oral cavity			+	-
	A Oas	cm²	Air/saliva contact area in oral cavity		/	+	-
	A Oms	cm²	Mucosa/saliva contact area in oral cavity		/	+	-
	C ext µg/cm 3	Aroma concentration in air	1	0.5 ... 2	+	Experimental value
	e Fm	cm	Thickness of wetted mucosa in pharynx	5 10 -3	5 10 -4 ... 5 10 -2	+	(Shojaei, 1998)
	e Fs	cm	Thickness of saliva layer in pharynx	=V Fs /A Fas	-	/	-
	e Om	cm	Thickness of wetted mucosa in oral cavity	5 10 -3	5 10 -4 ... 5 10 -2	+	(Shojaei, 1998)
	e Os	cm	Thickness of saliva layer in oral cavity	=V Os /Ao Fas	/	/	-
	e Nm	cm	Thickness of mucosa in nasal cavity	5 10 -3	5 10 -4 ... 5 10 -2	+	(Shojaei, 1998)
	F R	Cycle/s	Respiratory frequency	0.24	0.12 ... 0.48	+++	(Doyennette et al., 2014)
	K Fam		Air/wetted mucosa partition coefficient in pharynx	10 -3	10 -5 ... 10 -1

Acknowledgments

We gratefully acknowledge the panellists for their contribution to in vivo and sensory measurements. We also thank Gilles Feron from UMR 1324 INRA/AgroSup Dijon/CNRS/Université de Bourgogne Centre des Sciences du Goût et de l'Alimentation (CSGA) for the characterisation of saliva samples, and Gail Wagman for revising the English version of the manuscript.

Doyennette, M., De Loubens, C., Déléris, I., Souchon, I., Tréléa, I.C., (2011). Mechanisms explaining the role of viscosity and post-deglutitive pharyngeal residue on in vivo aroma release: A combined experimental and modeling study Food Chemistry, 128(2), 380-390. Doyennette, M., Déléris, I., Féron, G., Guichard, E., Souchon, I., Tréléa, I.C., (2014). Main individual and product characteristics influencing in-mouth flavour release during eating masticated food products with different textures: mechanistic modelling and experimental validation. Journal of theoretical biology, 340, 209-221. Espinosa Diaz, M., (2004). Comparison between orthonasal and retronasal flavour perception at different concentrations. Flavour and Fragrance Journal, 19(6), 499-504. Féron, G., Ayed, C., Qannari, E.M., Courcoux, P., Labouré, H., Guichard, E., (2014).

Understanding Aroma Release from Model Cheeses by a Statistical Multiblock Approach on Oral Processing. Plos One, 9(4), e93113. Ferreira, V., Petka, J., Cacho, J., (2006). Intensity and persistence profiles of flavor compounds in synthetic solutions. Simple model for explaining the intensity and persistence of their aftersmell. Journal of Agricultural and Food Chemistry, 54(2), 489-496.

Foster, K.D., Grigor, J.M.V., Cheong, J.N., Yoo, M.J.Y., Bronlund, J.E., Morgenstern, M.P., (2011). The Role of Oral Processing in Dynamic Sensory Perception. Journal of Food Science, 76(2), R49-R61.

Frank, D.C., Eyres, G.T., Piyasiri, U., Delahunty, C.M., (2012). Effect of food matrix structure and composition on aroma release during oral processing using in vivo monitoring.

Flavour and Fragrance Journal, 27(6), 433-444. Geerts, T., Heyden, Y.V., (2011). In Silico Predictions of ADME-Tox Properties: Drug Absorption. Combinatorial Chemistry & High Throughput Screening, 14(5), 339-361. [START_REF] Hornung | Olfactory Mucosa-Air Partitioning of Odorants[END_REF]

K Fas

Air/saliva partition coefficient in pharynx 5 10 -3 5 10 -4 ... 5 10