Andrea Condoluci
email: andrea.condoluci@unibo.it

Matteo Manighetti

Admissible Tools in the Kitchen of Intuitionistic Logic

The usual reading of logical implication A → B as " if A then B " fails in intuitionistic logic: there are formulas A and B such that A → B is not provable, even though B is provable whenever A is provable. Intuitionistic rules apparently don't capture interesting meta-properties of the logic and, from a computational perspective, the programs corresponding to intuitionistic proofs are not powerful enough. Such non-provable implications are nevertheless admissible, and we study their behaviour by means of a proof term assignment and related rules of reduction. We introduce V, a calculus that is able to represent admissible inferences, while remaining in the intuitionistic world by having normal forms that are just intuitionistic terms. We then extend intuitionistic logic with principles corresponding to admissible rules. As an example, we consider the Kreisel-Putnam logic KP, for which we prove the strong normalization and the disjunction property through our term assignment. This is our first step in understanding the essence of admissible rules for intuitionistic logic.

Introduction

Proof systems are usually presented inductively by giving axioms and rules of inference, which are respectively the ingredients and the tools for cooking new proofs. For example, when presenting classical propositional logic (CPC) in natural deduction, for each of the usual connectives ∧, ∨, ¬, →, ⊥ one gives a set of standard tools to introduce or remove a connective from a formula in order to obtain a proof.

In their most essential form, we can represent rules as an inference A 1 , . . . , A n / B (read "from A 1 , . . . , A n infer B") where A 1 , . . . , A n , B are schemata of logic formulas. A rule A 1 , . . . , A n / B is said to be admissible in a proof system if it is in a way redundant, i.e. whenever A 1 . . . A n are provable, then B is already provable without using that rule. Adding or dropping rules may increase or decrease the amount of proofs we can cook in a proof system. The effect can be dramatic: for example, classical propositional logic CPC can be obtained by simply adding the rule of double negation elimination (¬¬A / A) to intuitionistic propositional logic IPC. Admissible rules are all the opposite: if we decide to utilize one in order to cook something, then we could have just used our ingredients in a different way to reach the same result.

One appealing feature of CPC is the fact that it is structurally complete: all its admissible rules are derivable, in the sense that whenever A 1 , . . . , A n / B is an admissible rule, then also the corresponding principle [START_REF] Harrop | On disjunctions and existential statements in intuitionistic systems of logic[END_REF] i.e. the system acknowledges that there's no need for that additional tool, so we can internalize it and use the old tools to complete our reasoning. This is not the case in intuitionistic logic: the mere fact that we know that the tool was not needed, doesn't give us any way to show inside the system why is that. On the other hand, IPC has other wonderful features. Relevant here is the disjunction property, fundamental for a constructive system: when a disjunction A ∨ B is provable, then one of the disjuncts A or B is provable as well. Our interest is in these intuitionistic admissible rules that are not derivable, in the computational principles they describe, and in the logic systems obtained by explicitly adding such rules to IPC.

A 1 ∧ • • • ∧ A n → B is provable
Can one effectively identify all intuitionistic admissible rules? The question of whether that set of rules is recursively enumerable was posed by Friedman in 1975, and answered positively by Rybakov in 1984. It was then de Jongh and Visser who exhibited a numerable set of rules (now known as Visser's rules) and conjectured that it formed a basis for all the admissible rules of IPC. This conjecture was later proved by Iemhoff in the fundamental [START_REF] Iemhoff | On the admissible rules of intuitionistic propositional logic[END_REF]. Rozière in his Ph.D. thesis [START_REF] Rozière | Admissible and Derivable Rules in Intuitionistic Logic[END_REF] reached the same conclusion with a substantially different technique, independently of Visser and Iemhoff. These works elegantly settled the problem of identifying and building admissible rules. However our question is different: why are these rules superfluous, and what reduction steps can eliminate them from proofs?

Rozière first posed the question of finding a computational correspondence for his basis of the admissible rules in the conclusion of his thesis, but no work has been done on this ever since. Natural deduction provides a powerful tool to analyse the computational behaviour of logical axioms, thanks to the fact that it gives a simple way to translate axioms into rules and to develop correspondences with λ -calculi. Our plan is therefore to understand the phenomenon of admissibility by equipping proofs with λ -terms and associated reductions in the spirit of the Curry-Howard correspondence. Normalization will show explicitly what role admissible rules play in a proof.

Visser's Basis

The central role in the developement of the paper is played by Visser's basis of rules. The term basis means that any rule that is admissible for IPC is obtainable by combining some of the rules of the family with other intuitionistic reasoning. It consists of the following sequence of rules:

Visser n : (B i → C i ) i=1...n → A 1 ∨ A 2 /                n j=1 ((B i → C i ) i=1...n → B j ) ∨ ((B i → C i ) i=1...n → A 1 ) ∨ ((B i → C i ) i=1...n → A 2 )
This is read as: for every natural number n, whenever the left part of the rule (a n-ary implication) is provable, then the right part (an n + 2-ary disjunction) is provable. It forms a basis in the sense that all other admissible rules of IPC can be obtained from the combination of rules from this family with the usual rules of intuitionistic logic. It is an infinite family, since Visser n+1 cannot be derived from Visser 1 ,. . . ,Visser n [START_REF] Rozière | Admissible and Derivable Rules in Intuitionistic Logic[END_REF].

The importance of Visser's basis is not limited to intuitionistic logic but also applies more generally to intermediate logics, as witnessed by the following: Theorem 1.1 (Iemhoff [START_REF] Iemhoff | Intermediate logics and Visser's rules[END_REF]). If the rules of Visser's basis are admissible in a logic, then they form a basis for the admissible rules of that logic This theorem also gives us a simple argument to prove the structural completeness of CPC: since all the Visser n rules are provable in CPC, they are admissible and therefore they constitute a basis for all the admissible rules of CPC; but since the Visser n are derivable, all admissible rules are derivable.

Contributions and Structure of the Paper

In Section 2 we introduce the natural deduction rules corresponding to Visser's rules, and present the associated λ -calculus V: we show that proofs in the new calculus normalize to ordinary intuitionistic proofs. In the remaining part of the paper, we push further our idea and start adapting our calculus to intermediate logics characterized by axioms derived from admissible rules. In Section 3 we study the well-known Harrop's rule, and more precisely the logic KP obtained by adding Harrop's principle to IPC: we prove good properties like subject reduction, the disjunction property, and strong normalization. In Section 4 we quickly introduce the logic AD (obtained by adding the axiom V 1 to IPC) as a candidate for future study, and possible extensions to arithmetic. Proofs can be found in the appendices at the end of the paper.

2 Proof Terms for the Admissible Rules: V

In this section, we are going to assign proof terms to all the inferences of Visser's basis in a uniform way. First, we give a natural deduction flavor to the Visser rules. Since the conclusion of the left-hand side of the rules is a disjunction, we model the rules as generalized disjunction eliminations ∨ E ; "generalized" because the main premise will be the disjunction in the antecedent of the Visser n , but under n implicative assumptions. Therefore the rules have the form:

[B i → C i ] i=1...n . . . A 1 ∨ A 2 [(B i → C i ) i=1...n → A 1 ] . . . D [(B i → C i ) i=1...n → A 2 ] . . . D [(B i → C i ) i=1...n → B j ] j=1...n . . . . . . D • • • D Visser n D
In order to keep the rules admissible, we need to restrict the usage of the inference: the additional requirement is that the proofs of the main premise (the one on the left with end-formula A 1 ∨ A 2 ) must be closed proofs, i.e. cannot have open assumptions others than the ones discharged by that Visser inference. Otherwise we would be able to go beyond IPC, since for example we would prove all the principles corresponding to the admissible rules (as in system AD, see Section 4). On the other side, it is straightforward to see that our rules directly correspond to rules of Visser's basis, and that they adequately represent admissibility. We now turn to proof terms:

t, s, u ::= x, y, z, . . . ∈ V | t s | λ x.t | efq t (exfalso) | <t, s> (pair) | proj i t (projection) | inj i t (injection) | case[t | | y.s 1 | y.s 2 ] (case) | V n [ x.t | | y.s 1 | y.s 2 | | z. u] (Visser -in V and AD) | hop[ x.t | | y.s 1 | y.s 2 ] (Harrop -in KP) Figure 1: Proof terms
Since the shape of the rules is the elimination of a disjunction, the proof term associated with this inference will be modeled on the case analysis case[-| | -| -]. The difference will be in the number of assumptions that are bound, and in the number of possible cases. We use the vector notation x.t on variables to indicate that a sequence of (indexed) variables x 1 , . . . , x n is bound, and on terms like z. u to indicate a sequence of (indexed) terms u 1 , . . . , u n on each of which we are binding the variable z. The resulting annotation for a Visser inference is then:

x : (B i → C i ) i=1...n t : A 1 ∨ A 2 Γ, y : (B i → C i ) i=1...n → A 1 s 1 : D Γ, y : (B i → C i ) i=1...n → A 2 s 2 : D {Γ, z : (B i → C i ) i=1...n → B j u j : D} j=1...n Visser n Γ V n [ x.t | | y.s 1 | y.s 2 | | z. u] : D We call V the
calculus obtained by adding this family of rules of inference to IPC. The syntax of V can be found in Figure 1, and it includes the usual proof terms for intuitionistic logic [START_REF] Heine | Lectures on the Curry-Howard isomorphism[END_REF], plus the proof terms

V -[-| | -| -| | -]
for the Visser family.

We now turn to the reduction rules. First of all, we need to define W contexts: intuitively, contexts are proof terms with a hole, where the hole is denoted by , and E t means replacing the unique hole in the context E with the term t. Definition 2.1 (Weak head IPC contexts). W contexts are defined by the following grammar:

W ::= | W t | proj i W | case[W | | -| -]. Reduction rules for IPC -Beta (λ x.t) s → t{s/x} -Projection proj i <t 1 ,t 2 > → t i -Case case[inj i t | | y.s 1 | y.s 2 ] → s i {t/y} Additional rules for V -Visser-inj V n [ x.inj i t | | y.s 1 | y.s 2 | | z. u] → s i {λ x.t/y} (i = 1, 2) -Visser-efq V n [ x.W efq t | | y.s 1 | y.s 2 | | z. u] → s 1 {(λ x. efq t)/y} -Visser-app V n [ x.W x j t | | y.s 1 | y.s 2 | | z. u] → u j {λ x.t/z} ( j = 1 . . . n) Figure 2: Reduction rules (V)
The reduction rules for the proof terms are given in Figure 2: the first block defines → IPC by means of the usual rules for IPC, and the second block defines → V as → IPC plus additional reduction rules for the new construct

V n [ x.t | | y.s 1 | y.s 2 | | z. u],
depending on different shapes that t might have. Let us explain the intuition. In the first case (Visser-inj), the term is the injection inj i t with possibly free variables x i of type B i → C i for i = 1 . . . n; in that branch one has chosen to prove one of the two disjuncts A 1 or A 2 , and we may just reduce to the corresponding proof s i , in which we plug the proof t but after binding the free variables x. In the second case (Visser-efq), the disjunction is proved by means of a contradiction, and that contradiction may be used to prove any of the cases s 1 , s 2 , u. In the third case (Visser-app), the term contains an application with one of the variables bound by the Visser rule on the left hand side, i.e. the proof uses one of the Visser assumptions to prove the disjunction. We reduce to the corresponding case u j , where λ x.t is substituted for the assumption of type (B i → C i ) i=1...n → B j . The reduction relation → V is obtained as usual as the structural closure of the reduction → V (and similarly for → IPC ).

As expected, V-terms normalize: we prove normalization by providing an evaluation function that reduces V-terms to intuitionistic terms. The idea is to define the evaluator by structural recursion on typed terms, and using normalization for IPC after each recursive call. Theorem A.1 (Normalization for V). V enjoys the normalization property.

The following is a consequence of Lemma A.2: Theorem 2.1. V-terms normalize to IPC-terms.

Beyond IPC: Harrop's Rule and KP

In the previous section we have been expecially careful in imposing the restriction on the open assumptions for the application of our new rules, in order to keep our calculus inside the intuitionistic world and to obtain precisely a characterization of admissibility. At this point, however, one can legitimately ask: what happens if we lift such restriction, and allow one or more admissible principles inside an extended logic? The system of rules we introduced assumes then a different role, that is the role of providing a simple and modular way to obtain Curry-Howard systems for semi-classical logics arising from the addition to IPC of axioms corresponding to admissible principles.

The simplest and oldest studied admissible rule of IPC is the rule of independence of premise, also known as Harrop's rule in its propositional variant [START_REF] Harrop | On disjunctions and existential statements in intuitionistic systems of logic[END_REF]:

¬B → A 1 ∨ A 2 / (¬B → A 1 ) ∨ (¬B → A 2 )
The logic that arises by adding it to IPC has also been studied, and is known as Kreisel-Putnam logic (KP). It was introduced by G. Kreisel and H. Putnam [START_REF] Kreisel | Eine Unableitbarkeitsbeweismethode für den Intuitionistischen Aussagenkalkl[END_REF] to show a logic stronger than IPC that still could satisfy the disjunction property, thus providing a counterexample to the conjecture of Łukasiewicz that IPC was the only such logic.

We now proceed to define a Curry-Howard calculus for KP as an instance of the system we presented in the previous section. It suffices to realize that Harrop's rule is a particular case of Visser 1 where the formula C is taken to be ⊥ (note that the third disjunct in this instance of Visser 1 becomes ¬B → B, that implies both the other hypotheses ¬B → A 1 and ¬B → A 2 ; for this reason we can ignore it). Then we get the following simplified rule in natural deduction:

[¬B]
. . .

A 1 ∨ A 2 [¬B → A 1 ] . . . D [¬B → A 2 ] . . . D Harrop D
The restriction on the assumptions of the main premise is now gone, and open proofs are allowed. In fact Harrop's principle is provable in our system:

[¬B → A 1 ∨ A 2 ] (2) [¬B] (1) A 1 ∨ A 2 [¬B → A 1 ] (1) (¬B → A 1 ) ∨ (¬B → A 2 ) [¬B → A 2 ] (1) (¬B → A 1 ) ∨ (¬B → A 2 ) Harrop (1) (¬B → A 1 ) ∨ (¬B → A 2 ) (2) (¬B → A 1 ∨ A 2 ) → (¬B → A 1 ) ∨ (¬B → A 2 )
The proof term is a simplified version of the proof term for V 1 , where we remove the term corresponding to the trivialized third disjunct:

Γ, x : ¬B t : A 1 ∨ A 2 Γ, y : ¬B → A 1 s 1 : D Γ, y : ¬B → A 2 s 2 : D Γ hop[x.t | | y.s 1 | y.s 2 ] : D
By inspecting the reduction rules for V, we realize that the rule Visser-app has no counterpart in KP: since the Harrop assumptions have negated type, their use in proof terms is completely encapsulated in exfalso terms (see Classification, Lemma B.1 below). Therefore the reduction rules for KP are the ones for IPC (Figure 2) plus the additional rules Harrop-inj and Harrop-efq in Figure 3. We denote with → KP the toplevel reduction for KP, and with → KP its structural closure. We prove for KP the usual properties of subject reduction, classification, and strong normalization. As expected we denote with KP the provability in KP, but we use simply when not ambiguous.

-Harrop-inj hop[x.inj i t | | y.s 1 | y.s 2 ] → s i {λ x.t/y} -Harrop-efq hop[x.W efq t | | y.s 1 | y.s 2 ] → s 1 {(λ x. efq t)/y}
Theorem B.1 (Subject reduction for KP). If Γ KP t : A and t → KP s, then Γ KP s : A.

In order to classify normal forms of KP, we need to consider proof terms with possibly open Harrop assumptions: we denote with Γ ¬ a negated typing context, i.e. of the form Γ ¬ = {x 1 : ¬A 1 , . . . , x n : ¬A n }. We obtain the following classification of normal forms: Lemma B.1 (Classification for KP). Let Γ ¬ KP t : A for t in (weak head) normal form and t ¬neutral:

• Implication: if A = B → C, then t is an abstraction or a variable in Γ ¬ ;

• Disjunction: if A = B ∨C, then t is an injection;

• Conjunction: if A = B ∧C, then t is a pair;

• Falsity: if A = ⊥, then t = x s for some s and some x ∈ Γ ¬ .

We prove that KP enjoys the strong normalization property, i.e. all typable terms are strongly normalizing. We use a modified version of the method of reducibility candidates by Girard-Tait [START_REF] Girard | Proofs and types[END_REF]. The differences with respect to the usual proof are that Harrop and exfalso terms are added to neutral terms, and that the reductions for hop (which involve terms under binders) require special treatment.

Theorem B.2 (Strong normalization of KP).

If Γ KP t : A, then t is strongly normalizing.

The complete proof is on the appendix. We can now prove the disjunction property: Lemma 3.1 (Consistency). KP t : ⊥ for no t.

Proof. Let us assume that there exists t (which we assume in normal form by Theorem B.2) such that KP t : ⊥, and derive a contradiction. We proceed by induction on the size of t. The base case is impossible because by Lemma B.1 t cannot be a variable. As for the inductive case, by Lemma B.1, t is either an exfalso, or x u ∈ Γ ¬ for some x ∈ Γ ¬ . In the former case t = efq s for some s such that KP s : ⊥, and we use the i.h.; the latter case is not possible, since Γ ¬ = / 0.

Conclusions and Future Work

Our system provides a meaningful explanation of the admissible rules in terms of normalization of natural deduction proofs. In addition, by simply lifting the condition of having closed proofs on the main premise, we can study intermediate logics characterized by the axioms corresponding to some admissible rules; the study of the Kreisel-Putnam logic exemplifies this approach.

We believe that our presentation is well-suited to continue the study of admissibility in intuitionistic systems, a subject that is currently mostly explored with semantic tools. We devised powerful proofs of normalization for our systems KP and V, and we will try to extend these results to other similarly obtained systems. We conclude with some remarks on future generalizations.

The Logic AD

Now that we have shown the potential of our system in analysing the extension of IPC with axioms corresponding to admissible rules, we might wonder what could happen when we try to add several of them. We can be even more ambitious: what if we want to add all the Visser rules to IPC? A theorem by Rozière greatly simplifies our task: Theorem 4.1 (Rozière [START_REF] Rozière | Admissible and Derivable Rules in Intuitionistic Logic[END_REF]). All Visser rules are derivable in the logic AD, obtained by adding the V 1 axiom schema to IPC.

Clearly, since the Visser rules are derivable in AD they are also admissible; as we know from Theorem 1.1 this means that they form a basis for all the admissible rules of AD, and since they are derivable we obtain: Corollary 4.1. The logic AD is structurally complete. However, we also know from Iemhoff [START_REF] Iemhoff | A(nother) characterization of intuitionistic propositional logic[END_REF] that IPC is the only logic that has the Visser rules as admissible rules and satisfies the disjunction property. This means that AD cannot satisfy the disjunction property. This was also proved with different techniques by Rozière, who also showed that AD is still weaker than CPC. Given these properties, AD seems the best candidate to be studied with our technique.

Arithmetic

Since its inception with Harrop [START_REF] Harrop | On disjunctions and existential statements in intuitionistic systems of logic[END_REF], the motivation for studying admissible rules of IPC was to understand arithmetical systems. A famous theorem of de Jongh states that the propositional formulas whose arithmetical instances are provable in intuitionistic arithmetic (HA) are exactly the theorems of IPC, and many studies of the admissible rules of HA (like Visser [START_REF] Visser | Substitutions of Σ 0[END_REF], Iemhoff and Artemov [START_REF] Artemov | From de Jongh's theorem to intuitionistic logic of proofs[END_REF]) originated from it. In particular Visser shows that the propositional admissible rules of HA coincide with those of IPC, and that Σ 0 1 rules are also related. Harrop's principle, that we have investigated in this paper, is also known as the propositional Independence of Premise principle. Its first order version:

(¬A → ∃x. B(x)) → ∃x. (¬A → B(x)) (IP)
corresponds to an admissible rule of HA that has an important status in the theory of arithmetic, and was given a constructive interpretation for example by Gödel [START_REF] Gödel | Über eine bisher noch nicht bentzte Erweiterung des finiten Standpunktes[END_REF] with his well known Dialectica interpretation.

We can assign to IP a proof term and two reduction rules that act in the same way as the ones introduced for Harrop's rule: that is, we will distinguish the two cases where there is an explicit proof of the existential in the antecedent, and where an exfalso reasoning has been carried on. We believe that a more advanced study of other admissible rules of HA can be carried on similar grounds.

• (∨ I ) t is an injection, and we conclude.

• (∨ E ) and t = case[s | | -| -] with Γ → s : D ∨ D .
Because t is in normal form, s cannot be an injection. By i.h. s is →neutral, and therefore t is →neutral. • (∧ I ) t is a pair, and we conclude.

• (∧ E ) and t = proj i s with Γ → s : D ∧ D . Because t is in normal form, s cannot be a pair. By i.h. s is →neutral, and therefore t is →neutral.

• (Visser n ) not possible. Assume t = V n [ x.s | | -| -| | -] with x : (A i → B i ) i=1...n s : A 1 ∨ A 2
by inversion, and derive a contradiction. By i.h. s is →neutral or an injection, but both cases contradict the hypothesis that t is a normal form.

In order to prove normalization, we define an evaluation function eval(•), mapping each typable term in V to its normal form. We first assume a corresponding function for IPC: Definition A.1 (eval IPC (•)). We call eval IPC (•) the function mapping each term typable in IPC to its normal form. Definition A.2 (eval(•)). Let t a term typable in V. We define its evaluation eval(t) by structural induction: eval(x) := x eval(t s)

:= eval IPC (eval(t) eval(s)) eval(λ x.t) := λ x. eval(t) eval(efq t) := efq (eval(t)) eval( t, s ) := eval(t), eval(s) eval(proj i t) := eval IPC (proj i (eval(t))) eval(inj i t) := eval IPC (inj i (eval(t))) eval(case[t | | y.s 1 | y.s 2 ]) := eval IPC (case[ eval(t) | | y. eval(s 1 ) | y. eval(s 2 )]) eval(V n [ x.t | | y.s 1 | y.s 2 | | z. u]) :=      eval IPC (eval(s i ){λ x.t /y}) if eval(t) = inj i t eval IPC (eval(s 1 ){λ x. efq t /y}) if eval(t) = W efq t eval IPC (eval(u j ){λ x.t /z}) if eval(t) = W x j t
Note: the three cases in the definition of eval(•) on Visser terms are exhaustive by inspection of the normal forms of type disjunction (Lemma A.1) since it holds by inversion that Γ → t :

A 1 ∨ A 2 with dom(Γ → ) = x. Lemma A.2 (eval(•) well-defined). For every V-term t s.t. Γ V t : A: 1. Γ IPC eval(t) : A, 2. eval(t) is normal, 3. t → * V eval(t).
Proof. The three points can be proved mutually, by induction on the type derivation Γ V t : A: 1. follows by i.h. and by subject reduction for IPC;

2. follows by i.h. and from the fact that the output of eval IPC (•) are only normal forms;

3. follows by i.h. and from the fact that IPC is a subcalculus of V.

It easily follows: Theorem A.1 (Normalization for V). V enjoys the normalization property.

B Theorems on KP

Theorem B.1 (Subject reduction for KP). If Γ KP t : A and t → KP s, then Γ KP s : A.

Proof. By the definition of reduction as the closure of → KP under evaluation contexts, we just prove the statement when t → KP s; the general case t → KP s follows because substitution preserves types.

The cases of the usual intuitionistic reductions are standard (see for example [START_REF] Heine | Lectures on the Curry-Howard isomorphism[END_REF]); we just prove the cases of the reduction rules associated with hop.

For the case of the left injection hop[x.inj • Implication: if A = B → C, then t is an abstraction or a variable in Γ ¬ ;

• Disjunction: if A = B ∨C, then t is an injection;

• Conjunction: if A = B ∧C, then t is a pair;

• Falsity: if A = ⊥, then t = x s for some s and some x ∈ Γ ¬ .

Proof. By induction on the type derivation of t:

• (ax) and t is a variable in Γ ¬ : by definition of Γ ¬ , the type of t is an implication, and we conclude.

• (→ I ) and t is an abstraction: trivial.

• (→ E ) and t = s u with Γ ¬ s : B → A. Because t is in normal form, s cannot be an abstraction. By i.h., s is either a variable in Γ ¬ or a ¬neutral term. In the first case, note that we have that A = ⊥ and t = xs, and the thesis holds; in the second case, t is ¬neutral and the thesis holds.

• (∨ I ) and t is an injection: trivial.

• (∨ E ) and t = case[s | | -| -] with Γ ¬ s : D 1 ∨ D 2 .
By i.h. s is either an injection or ¬neutral. The first case is not possible because t is in normal form; in the second case, t is ¬neutral as required.

• (∧ I ) and t is a pair: trivial.

• (∧ E ) and t = proj i s with Γ ¬ s : D 1 ∧ D 2 . By i.h. s is either a pair or ¬neutral, but the first case contradicts the hypothesis that t is in normal form. Therefore s is ¬neutral, and also t is ¬neutral.

• (⊥ E ) then t is immediately ¬neutral. (∧ E ) Let Γ s : A 1 ∧ A 2 , and by i.h. sσ ∈ A 1 ∧ A 2 for every σ ∈ Γ . We need to prove that (proj 1 s)σ ∈ A 1 and (proj 2 s)σ ∈ A 2 for every σ ∈ Γ . There are two cases:

sσ SN n ∈ Ne: then proj i (sσ ) SN proj i n and we conclude by Lemma B.4(2) and Lemma B.4(3) because that term is neutral.

uσ SN <t 1 ,t 2 > for some t 1 ∈ A 1 and t 2 ∈ A 2 : therefore proj i (uσ ) → * SN proj i <t 1 ,t 2 > → SN t i ∈ A i . Conclude by Lemma B.4(3) since (proj i u)σ = proj i (uσ ).

(∨ I ) We discuss the case of inj 1 ; the case of inj 2 is symmetric. Let Γ t : A, and by i.h. tσ ∈ A for every σ ∈ Γ . We show that also (inj 1 t)σ ∈ A ∨ B for every σ ∈ Γ . Note that (inj 1 t)σ = inj 1 (tσ ), and conclude by i.h. and Definition B.5 [START_REF] Harrop | On disjunctions and existential statements in intuitionistic systems of logic[END_REF].

(∨ E ) This case is just a simplified version of the following argument for the Harrop rule. tσ SN inj i u i for u i ∈ A i : then also hop[x.tσ | | y.s 1 σ | y.s 2 σ ] → * SN s i σ {λ x. u i /y}. In order to be able to use the i.h. we need to show that σ ∪{λ x. u i /y} ∈ Γ, y : ¬B → A i , i.e. that λ x. u i ∈ ¬B → A i , that by definition holds iff for every t ∈ ¬B , u i {t /x} ∈ A i . In order to show the latter, take σ := σ ∪ {t /x}: then by i.h. tσ ∈ A 1 ∨ A 2 ⊆ SN, and therefore by Lemma B. [START_REF] Iemhoff | A(nother) characterization of intuitionistic propositional logic[END_REF] Proof. By Lemma B.6, tσ ∈ A for every σ ∈ Γ . We now take σ as the identity substitution, mapping the variables in Γ to themselves. Note that this is an allowed substitution since variables are neutral terms and therefore are contained in the denotation of every proposition (Lemma B.4(2)). It follows that t = tσ ∈ A , and we conclude because A contains only SN terms by Lemma B.4(1).

Figure 3 :

 3 Figure 3: Reduction rules (KP)

(

  Harrop) We need to prove that (hop[x.t | | y.s 1 | y.s 2 ])σ ∈ D for every σ ∈ Γ . We first note that (hop[x.t | | y.s 1 | y.s 2 ])σ = hop[x.tσ | | y.s 1 σ | y.s 2 σ ] (assuming by renaming that x and y do not occur in σ ). Let σ := σ ∪ {x/x}. tσ = tσ and by i.h. tσ ∈ A 1 ∨ A 2 . There are three cases:

  1 t | | y.s 1 | y.s 2 ] → s 1 {λ x.t/y}, by inversion we have Γ, y : ¬B → A 1 s 1 : D and Γ, x : ¬B inj 1 t : A 1 ∨A 2 for some A 1 , A 2 , B, D. Again by inversion Γ, x : ¬B x : A 1 , and by → I we obtain Γ λ x.t : ¬B → A 1 . By substitutivity we get the desired result Γ s 1 {λ x.t/y} : D. The case of the right injection is analogous. Finally, if hop[x.W efq t | | y.s 1 | y.s 2 ] → s 1 {λ x. efq t/y}, by inversion we have Γ, y : ¬B → A 1 s 1 : D and Γ, x : ¬B W efq t : A 1 ∨ A 2 for some A 1 , A 2 , B, D. It is easy to see, by induction on the definition of weak head contexts and by inversion, that Γ, x : ¬B t : ⊥; by ⊥ E we obtain Γ, x : ¬B efq t : A 1 . By → I we obtain Γ λ x. efq t : ¬B → A 1 , and by substitutivity we get the desired result Γ s 1 {λ x. efq t/y} : D. We say that a term is ¬neutral if it has the form W efq t . Lemma B.1 (Classification for KP). Let Γ ¬ KP t : A for t in (weak head) normal form and t not ¬neutral:

•

  (Harrop) not possible. Assume t = hop[x.s | | -| -] with Γ ¬ , x : ¬B s : D 1 ∨ D 2 , and derive a contradiction. By i.h. s is an injection or a ¬neutral term, but both cases contradict the hypothesis that t is in normal form. • hop[x.inj i t | | y.s 1 | y.s 2 ] → s i {λ x.t/y}. By renaming, x, y ∈ fv(σ ), dom(σ ). Then hop[x.inj i t | | y.s 1 | y.s 2 ]σ = hop[x.inj i (tσ ) | | y.s 1 σ | y.s 2 σ ] → s i σ {λ x.tσ /y}. We conclude because s i σ {λ x.tσ /y} = (s i {λ x.t/y})σ . • hop[x.W efq t | | y.s 1 | y.s 2 ] → s 1 {λ x. efq t/y}. By renaming, x, y ∈ fv(σ ), dom(σ ). Then hop[x.W efq t | | y.s 1 | y.s 2 ]σ = hop[x.W efq tσ | | y.s 1 σ | y.s 2 σ ] for some SN context W . We have hop[x.W efq tσ | | y.s 1 σ | y.s 2 σ ] → s 1 σ {λ x. efq (tσ )/y}, and we conclude because s 1 σ {λ x. efq (tσ )/y} = s 1 {λ x. efq t/y}σ . Lemma B.6 (Fundamental lemma). If Γ t : A and σ ∈ Γ , then tσ ∈ A . Proof. By induction on the type derivation. The base case is the axiom, and instantiated variables belong to the corresponding denotations by the definition of Γ . Let us now proceed by cases on the rules of inference: By Definition B.5(2), λ x.tσ ∈ A → B iff for all s ∈ A , tσ {s/x} ∈ B . By taking σ := σ ∪ {s/x}, this follows from the i.h. and from the hypothesis on σ . Note that n(sσ ) is neutral, and we conclude by Lemma B.4(2) and Lemma B.4(3).

	Conclude by Lemma B.4(3).

(→ I ) Assume that for all σ ∈ Γ, x : A , tσ ∈ B ; we need to prove that for all σ ∈ Γ , (λ x.t)σ ∈ A → B . Let σ ∈ Γ , and by renaming x ∈ dom(σ ) ∪ fv(σ ). Then (λ x.t)σ = λ x.tσ . (→ E ) We need to prove that for all σ ∈ Γ , (t s)σ ∈ B . Note that (t s)σ = (tσ )(sσ ). By i.h. tσ ∈ A → B , and therefore by Definition B.5(2), either: tσ SN n ∈ Ne: then (tσ )(sσ ) → * SN n(sσ ) since sσ ∈ SN (by i.h. and Lemma B.4(1))tσ SN λ y. u: then (tσ )(sσ ) → * SN (λ y. u) (sσ ) → SN u{sσ /y} ∈ B by Definition B.5(2). (⊥ I ) By the hypothesis, for every σ ∈ Γ , tσ ∈ ⊥ . We need to prove that (efq t)σ ∈ A . By Lemma B.4(1) tσ ∈ SN, and since (efq t)σ = efq (tσ ), (efq t)σ is a neutral term. Conclude by Lemma B.4(2). (∧ I ) Let Γ t 1 : A 1 and Γ t 2 : A 2 : we need to prove that for every σ ∈ Γ , <t 1 ,t 2 >σ ∈ A 1 ∧ A 2 . Since <t, s>σ = <tσ , sσ >, the claim follows from Definition B.5(3) and the i.h. tσ ∈ A and sσ ∈ B .

  tσ = tσ {t /x} → * SN inj i (u i {t /x}) SN inj i u i for u i {t /x} SN u i . By Definition B.5(4) u i ∈ A i , but also u i {t /x} by Lemma B.4(3), and we conclude. tσ SN W efq u ∈ Ne: then also hop[x.tσ | | y.s 1 σ | y.s 2 σ ] → * SN s 1 σ {λ x. efq u/y}. As above, in order to use the i.h. and conclude we only need to prove that (λ x. efq u) ∈ ¬B → A 1 . By Definition B.5(2), this is the case if and only if for all u ∈ ¬B , (efq u){u /x} ∈ A 1 . This is proved similarly as the point above, and it follows by Lemma B.5 and the definition of inert terms. tσ SN K z ∈ Ne: we conclude as usual because hop[x.K z | | y.s 1 σ | y.s 2 σ ] is neutral as well. Theorem B.2 (Strong normalization of KP). If Γ KP t : A, then t is strongly normalizing.

A Theorems on V

First some definitions. We denote with V the provability in V (but we use when not ambiguous). We denote with Γ → an implicative typing context, i.e. of the form Γ → = {x 1 : A 1 → B 1 , . . . , x n : A n → B n }. We say that a term is →neutral if it has the form W x s or W efq s .

Lemma A.1 (Classification for V). Let Γ → V t : A for t in normal form, and t not →neutral:

• Implication: if A = B → C, then t is either an abstraction or a variable in Γ → ;

Proof. By induction on the type derivation of t:

• (ax) t is a variable in Γ → . By definition of Γ → , the type of t is an implication, and we conclude.

• (→ I ) t is an abstraction, and we conclude.

• (→ E ) and t = s u with Γ → s : B → C. Because t is in normal form, s cannot be an abstraction. By i.h., s is either a variable in Γ → or is →neutral; in both cases t is →neutral.

B.1 Strong Normalization

In this section, we prove the strong normalization property for KP by means of an adapted version of Girard's method of candidates [START_REF] Girard | Proofs and types[END_REF].

Definition B.1 (Weak head KP contexts).

Let SN be the set of strongly normalizing terms of KP. By abuse of notation, we say that a context -be it an IPC context W or a KP context K -is strongly normalizing if all its "internal" λ -terms are strongly normalizing. Definition B.2 (Weak head reduction → SN , SN ). We define → SN as the "strongly normalizing" closure of → KP (Figure 2) under weak head contexts: We are now ready to define the semantics of formulas:

1. p := SN for every p atomic (also p = ⊥),

In fact, we note that our definition produces candidates of reducibility:

Lemma B.4 (Denotations are candidates). For every A, its denotation:

1. contains only strongly normalizing terms: A ⊆ SN 2. contains all neutral terms: Ne ⊆ A 3. is backward closed: if t ∈ A and s → SN t, then s ∈ A . Proof. First note that if t = K t and tσ ∈ SN, then tσ = K t σ for some SN context K . Therefore, we assume that K t → SN K s with t → s , and we prove that t σ → s σ by cases on the reduction rules:

• (λ y. s) u → s{u/y}. By renaming, y ∈ fv(σ ), dom(σ ). Then ((λ y. s) u)σ = (λ y. sσ ) (uσ ) → sσ {uσ /y}, with s{u/y}σ = s{u/y}σ . We conclude because sσ {uσ /y} = s{u/y}σ and sσ , uσ ∈ SN by the hypothesis that tσ ∈ SN.

• proj i <t 1 ,t 2 > → t i . Then (proj i <t 1 ,t 2 >)σ = proj i <t 1 σ ,t 2 σ > → t i σ , and t 1 σ ,t 2 σ ∈ SN by hypothesis.

• case[inj i t | | y.s 1 | y.s 2 ] → s i {t/y}. By renaming, y ∈ fv(σ ), dom(σ ). Similar to the case below.


Ana Sofia Dias

Marianna Pirone

Gianfranco Urciuoli

Review on the Methods for Evaluation of Root Reinforcement in Shallow Landslides

Keywords: Root cohesion, Root mechanical reinforcement, Shallow landslides, Slope stability

Recently geotechnical engineers aim to adopt more environmental-friendly solutions (not harmful to the environment), therefore the interest on the use of vegetation as a measure to improve slope stability is increasing. The mechanical reinforcement due to roots against shallow landslides occurs when the fibres intersect the shear surface, usually at depths lower than 2 m. In the literature, the presence of roots is often taken into account by modelling the soil as an equivalent composite material: 'the root-permeated soil', by including an additional cohesion term in the Mohr-Coulomb equation. The models used to estimate the root additional cohesion are presented in the first part of the paper. In some cases, root cohesion is calculated based on the resistant properties of the fibres and assuming an order for the progressive roots failure, either breaking, slipping out or buckling. On the other hand, some authors used structural models of the roots investigating not only the stresses in the roots, but also in the surrounding soil to obtain a better estimation of the root cohesion. In the second part of the paper, the calculation of the root reinforcement is used to assess the safety factor (SF) of the slope. Both Limit Equilibrium analyses (LE) and Finite Element Methods (FEM) are discussed, stressing the limitations of both the approaches.

Introduction

The shallow landslide's failure surface reaches depths of up to 2 m and it can intersect roots, which provide an increase of soil resistance. Therefore, the introduction of vegetation in a slope is an appealing measure to increase the slope safety.

The way roots influence the behaviour of the composite material (root-permeated soil) was investigated by [START_REF] Graf | Effects of vegetation on the angle of internal friction of a moraine[END_REF] and [START_REF] Zhang | Triaxial compression test of soil-root composites to evaluate influence of roots on soil shear strength[END_REF], however, the root reinforcement is usually modelled as an additional cohesion term [START_REF] Wu | Investigation of landslides on Prince of Wales Island, Alaska[END_REF]). Nevertheless, the type of root failure cannot be neglected because the ultimate load taken by a root depends on the rupture mechanism [START_REF] Wu | Study of soil-root interaction[END_REF][START_REF] Schwarz | Root reinforcement of soils under compression[END_REF].

Soil-root interaction models for the quantification of such reinforcement are presented in this paper. One approach can be the estimation of the maximum reinforcement by bundle of roots as a sum of the resistance provided each individual [START_REF] Wu | Investigation of landslides on Prince of Wales Island, Alaska[END_REF][START_REF] Pollen | Estimating the mechanical effects of riparian vegetation on stream bank stability using a fiber bundle model[END_REF]Schwarz et al. 2010a[START_REF] Schwarz | Modelling root reinforcement using a root-failure Weibull survival function[END_REF]. Some other authors used numerical models, which consider the root and soil influence on each other [START_REF] Mao | Evaluation of root reinforcement models using numerical modelling approaches[END_REF][START_REF] Liang | Modelling the seismic performance of rooted slopes from individual root-soil interaction to global slope behaviour[END_REF].

Moreover, the root reinforcement for stability of shallow landslides can be evaluated by either a macro model or a soil-root interaction model [START_REF] Wu | Root reinforcement of soil: review of analytical models, test results, and applications to design[END_REF][START_REF] Cazzuffi | Geosynthetic engineering and vegetation growth in soil reinforcement applications[END_REF]). The first is preferable in the case of roots with small dimensions and spacing. The rooted soil is represented by a homogeneous material with given resistant properties obtained from tests on root-permeated soil. The second is more convenient when roots are large and disperse, so that they are investigated as soil-embedded elements allowing the estimation of the stresses in the fibre.

The objective of the paper is to present the approaches adopted in the literature to analyse root reinforcement and its use on assessing slope stability. The advantages and disadvantages of the methods, as well as theirs limitations, concerns and future work projections are discussed.

Roots Effect on Soil Shear Resistance

The root-permeated soil is a composite material whose shear strength is described by (1) [START_REF] Veylon | Quantification of mechanical and hydric components of soil reinforcement by plant roots[END_REF]. This way, the shear stress at failure (𝑠 𝑓 ) is a sum of the effective shear strength of the soil matrix given by Mohr-Coulomb criterion (𝑠 𝑠 ), shear strength component due to matric suction (𝑠 𝜓 ) and shear strength component due to the root system (𝑠 𝑟 ).

𝑠 𝑓 = 𝑠 𝑠 + 𝑠 𝜓 + 𝑠 𝑟

(1) In the majority of the literature, roots are considered to provide increase of cohesion to the soil. The works stating that roots influence the composite material's friction angle are very scarce. Triaxial tests were performed by [START_REF] Graf | Effects of vegetation on the angle of internal friction of a moraine[END_REF] and [START_REF] Zhang | Triaxial compression test of soil-root composites to evaluate influence of roots on soil shear strength[END_REF] reporting opposite conclusions regarding the roots effect on the soil resistance. [START_REF] Graf | Effects of vegetation on the angle of internal friction of a moraine[END_REF] performed consolidated-undrained (CU) triaxial tests on vegetated soil (clayey gravel with sand) in saturated conditions applying confining pressures of 50, 75 and 100 kPa to represent the low stresses of surface soil. The results showed that roots provide an increase of internal friction angle of up to 5° (from 34.3° to 39.4°) but no additional cohesion. Therefore, [START_REF] Graf | Effects of vegetation on the angle of internal friction of a moraine[END_REF] showed dissatisfaction about considering the effect of roots as an additional cohesion, as typically is assumed, as the effect of roots should rather be a stress-dependent term.

In the results of direct shear tests of Fig. 1, the parallel displacement of shear envelopes suggested that fibres do not affect the frictional properties of the soil (sand). Yet, it is interesting to notice that for the range of normal stresses used by [START_REF] Graf | Effects of vegetation on the angle of internal friction of a moraine[END_REF], Fig. 1 shows an increase of the internal friction angle [START_REF] Gray | Mechanics of fiber reinforcement in sand[END_REF].

Fig. 1 Influence of fibres with different orientations on the shear strength envelope (1ksf = 47.9 kN/m 2 ) [START_REF] Gray | Mechanics of fiber reinforcement in sand[END_REF] On the other hand, the consolidated-drained (CD) triaxial tests performed by [START_REF] Zhang | Triaxial compression test of soil-root composites to evaluate influence of roots on soil shear strength[END_REF] on rooted soil (sand) with different water contents and roots in different directions showed that roots increased soil shear strength by increasing cohesion.

In the works of [START_REF] Graf | Effects of vegetation on the angle of internal friction of a moraine[END_REF] and [START_REF] Zhang | Triaxial compression test of soil-root composites to evaluate influence of roots on soil shear strength[END_REF], macro models of root-permeated soil were obtained according with the classification of [START_REF] Wu | Root reinforcement of soil: review of analytical models, test results, and applications to design[END_REF] because the stresses in the roots were not investigated.

Root Cohesion

As generally accepted, the root shear resistance 𝑠 𝑟 of ( 1) is an additional cohesion. However, roots are elements with low bending and shear resistance, and [START_REF] Wu | Investigation of landslides on Prince of Wales Island, Alaska[END_REF] proposed the following soil-root interaction model (Fig. 2). The shearing on the sliding surface causes the elongation of the roots, which are subjected to tensile stress and act on the unstable volume as stabilizing external forces. The normal component of the root tensile stress (Tn) increases the confining stress on the failure plane, thereby mobilizing additional shear resistance in the soil, whereas the tangential component (Tt) directly resists shear. The increase of shear strength provided by the root 𝑠 𝑟 may be translated by ( 2), where 𝜃 is the shear distortion of the root (Fig. 2) and 𝑡 𝑟 is the root tensile resistance per unit area of soil.

𝑠 𝑟 = (𝑠𝑖𝑛 𝜃 + 𝑐𝑜𝑠 𝜃 𝑡𝑎𝑛 𝜙 ′ )𝑡 𝑟 = 𝑘 ′ 𝑡 𝑟 (2) The value of the angle 𝜃 is difficult to quantify, so [START_REF] Wu | Investigation of landslides on Prince of Wales Island, Alaska[END_REF] suggested the use of a coefficient 𝑘 ′ that takes the value of 1.2. Indeed, the approximation proposed by [START_REF] Wu | Investigation of landslides on Prince of Wales Island, Alaska[END_REF] is generally accepted because it was observed in laboratory and field investigations that 𝑘 ′ ranges between 1.0 and 1.3. However, [START_REF] Thomas | Modelling root-reinforcement with a fiber-bundle model and Monte Carlo simulation[END_REF] recommended the use of a 𝑘 ′ close to 1.0 since that the parameter 𝑘 ′ also intends to take into account the initial angle between the root and the shear surface because the root is tensioned when it is inclined towards the movement direction. When the roots are inclined opposing the movement of the upper layer, the root is subjected to compression providing less resistance. [START_REF] Wu | Study of soil-root interaction[END_REF], [START_REF] Abe | Effect of tree roots on a shear zone: modelling reinforced shear stress[END_REF] and [START_REF] Belfiore | Analisi Del Contributo Meccanico Delle Radici Alla Resistenza Del Terreno[END_REF] also made some considerations on the simplification proposed by [START_REF] Wu | Investigation of landslides on Prince of Wales Island, Alaska[END_REF] because the angle 𝜃 is the parameter that directly controls the tension in the roots, on which depends the root elongation. Improvements have been done to this formulation mainly to take into account the soil-root surface interaction, root inclination and deformation.

In order to compute the root reinforcement in the form of root additional cohesion, the model presented in Fig. 2 needs the tensile resistance of the roots present in the bundle, i.e. 𝑡 𝑟 , as an input.

Several authors proposed models to quantify this parameter. The main difference among them is the order by which roots fail, which leads to different values of root reinforcement. This models are referred as root "breaking" models (BM) in this paper. The term "breaking" regards to the failure of the root, either by breakage, slippage or buckling. Some other authors used numerical models to obtain the reinforcement of the roots also in terms of additional cohesion [START_REF] Mao | Evaluation of root reinforcement models using numerical modelling approaches[END_REF][START_REF] Liang | Modelling the seismic performance of rooted slopes from individual root-soil interaction to global slope behaviour[END_REF]). In the following both "breaking" models and numerical ones will be discussed.

Root "Breaking" Models

W&W Model

The model commonly called W&W was first formulated by [START_REF] Wu | Investigation of landslides on Prince of Wales Island, Alaska[END_REF]. It is assumed that all the roots break simultaneously and pull out does not occur. Therefore, the tensile strength of root fibres per unit area of soil 𝑡 𝑟 is given by (3), representing the sum of the maximum tensile strength of each individual root. For simplification, the roots are grouped in 𝑁 diameter classes so that the value of 𝑡 𝑟,𝑛 is the average tensile strength of the root class, 𝑅𝐴𝑅 𝑛 is the root area ratio of the entire class 𝑛 (the root area ratio is the fraction of a given control area that is occupied by roots).

𝑡 𝑟 = ∑ 𝑡 𝑟,𝑛 • 𝑅𝐴𝑅 𝑛 𝑁 𝑛=1 (3)
This model tends to overestimate the root reinforcement because roots do not break simultaneously [START_REF] Pollen | Estimating the mechanical effects of riparian vegetation on stream bank stability using a fiber bundle model[END_REF][START_REF] Thomas | Modelling root-reinforcement with a fiber-bundle model and Monte Carlo simulation[END_REF]. Better estimations are obtained for grass root systems because the root diameters are more homogeneous [START_REF] Thomas | Modelling root-reinforcement with a fiber-bundle model and Monte Carlo simulation[END_REF]. The value obtained from (3) is substituted into (2) to compute the root reinforcement.

Fibre Bundle Model

In order to avoid some limitations of the W&W model, [START_REF] Pollen | Estimating the mechanical effects of riparian vegetation on stream bank stability using a fiber bundle model[END_REF] introduced the Fibre Bundle Model (FBM). The maximum load withstood by the bundle of fibres is less than the sum of each of their individual strengths because roots break at different instants depending on the way the load is distributed by all the fibres. Therefore the maximum value of tensile strength provided by the bundle not to be the same as if all the roots provided their maximum strength at the same instant.

It is assumed in the FBM that all fibres have the same elastic properties, the complexity of root tortuosity is not considered and all roots break rather than pull out of the soil. The computation of the breakage sequence in the FBM follows the flowchart presented in Fig.

3 [START_REF] Mao | Engineering ecological protection against landslides in diverse mountain forests: choosing cohesion models[END_REF].

Fig. 3 Flowchart for the FBM computation

The load can be distributed by the roots according to three different criteria as a function of the cross section area of the roots, as a function of the root diameter or equally distributed by all the intact roots [START_REF] Mao | Engineering ecological protection against landslides in diverse mountain forests: choosing cohesion models[END_REF]). Thomas and Pollen-Bankhead (2010) suggested that the load distribution by roots in FBM models should be made equally by all the roots (third criteria) because it showed to be more conservative in the estimation of soil shear strength reinforcement. In fact, different load partition methods varied the peak root-reinforcement value by up to 60%.

When a root breaks, the load is redistributed by the remaining unbroken roots. It can follow two approaches: Global load sharing (GLS), in which the load is evenly distributed by the remaining roots; or Local load sharing (LLS), in which the load is redistributed by the neighbouring roots. The first is preferable because it requires less data, even though the real behaviour is somewhere between those two [START_REF] Thomas | Modelling root-reinforcement with a fiber-bundle model and Monte Carlo simulation[END_REF].

Equation ( 4) is used to calculate additional root cohesion assuming that the load (force) is equally distributed by all the roots. First, the roots are ordered from the strongest to the weakest (1 to N), so that the breakage sequence upon loading is known. The index 𝑗 represents the weakest root that is still intact upon loading of the root bundle of N roots. Therefore, 𝑅𝐴𝑅 𝑗 refers to the RAR of the root 𝑗 and 𝑡 𝑟,𝑗 is the strength of the weakest intact root. Therefore, the bundle resistance is equal to the resistance of weakest root multiplied by the number of intact roots (also represented by 𝑗). The value obtained from ( 4) is substituted into (2) to obtain the root reinforcement.

𝑡 𝑟 = 𝑚𝑎𝑥(𝑡 𝑟,𝑗 • 𝑅𝐴𝑅 𝑗 • 𝑗) (4)

Root Bundle Model

The Root Bundle Model (RBM), proposed by Schwarz et al. (2010b), is an FBM extension in which a strain step loading approach is used. In this way a more realistic implementation of root mechanical effects in numerical models for slope stability calculations is provided [START_REF] Vergani | Effects of root tensile force and diameter distribution variability on root reinforcement in the Swiss and Italian Alps[END_REF]). The displacements are imposed equally in all N roots composing the bundle (Schwarz et al. 2010b). For each displacement increment, the load taken by the bundle is the sum of the stresses in all the roots, as long as the tension in each individual root does not exceed the maximum tensile strength. Root pull out is also admitted in the first formulation of this model.

The total force in the bundle (𝐹 𝑡𝑜𝑡 ) is a function of displacement ∆𝑥 given by ( 5), where 𝐹 𝑖 (∆𝑥) is the maximum pull out force allowed in the root belonging to the diameter class 𝑖, 𝑁 is the number of diameter classes and 𝑛 𝑖 is the number of roots of diameter class 𝑖.

𝐹 𝑡𝑜𝑡 (∆𝑥) = ∑ 𝐹 𝑖 (∆𝑥) • 𝑛 𝑖 𝑁 𝑖=1

(5) [START_REF] Schwarz | Modelling root reinforcement using a root-failure Weibull survival function[END_REF] proposed changes in the previous RBM in order to take into account the strength variability within a root diameter class using a statistical approach by introducing a Weilbull survival function. This function is a complementary cumulative distribution function that captures the failure probability of a complex system beyond a threshold. This other model is referred as RBMw. [START_REF] Schwarz | Modelling root reinforcement using a root-failure Weibull survival function[END_REF] assumed that the probability of a root to survive 𝑆(∆𝑥 * ) is given by ( 6):

𝑆(∆𝑥 * ) = 𝑒𝑥𝑝 [-( ∆𝑥 * 𝜆 * ) 𝜔 ] ( 6
)
where The tensile force of a bundle of roots 𝐹 𝑡𝑜𝑡 (∆𝑥) at each incremental displacement ∆𝑥 is obtained by summing the force contribution of each root class 𝐹(𝜙 𝛷 , ∆𝑥), given by ( 7), multiplied by the number of roots of that class 𝑛 𝛷 and by the survival function 𝑆(∆𝑥 𝛷 * ), as in (8). Considering the force in a bundle as a sum of forces on individual roots accepts the assumption that the roots in the bundle do not interact with each other, which is considered an acceptable approximation by [START_REF] Giadrossich | Mechanical interactions between neighbouring roots during pullout tests[END_REF].

𝐹(𝜙 𝛷 , ∆𝑥) = 𝑟𝜋𝐸 0 4𝐿 0 𝜙 𝛷 2+𝛽-𝛾 𝛥𝑥 (7) 𝐹 𝑡𝑜𝑡 (∆𝑥) = ∑ 𝑛 𝛷 𝐹(𝜙 𝛷 , ∆𝑥)𝑆(∆𝑥 𝛷 * ) 𝛷 𝑚𝑎𝑥 𝛷=1 (8)
In these equations, 𝛽 and 𝐸 0 are calibration parameters associated to the Young's modulus of the root material relation with diameter, 𝛾 and 𝐿 0 are calibration parameters associated to the root length relation with diameter, 𝑟 is the reduction coefficient to take into account the root tortuosity, 𝛷 is the mean root diameter of each root class, 𝛷 𝑚𝑎𝑥 is the maximum considered diameter and ∆𝑥 𝛷 * is the normalized displacement. Apparently, RBM provides an additional force. But this force can be considered by unit area, providing this way an additional cohesion value. Indeed, switching from load increments to displacement increments provides important information for the calculation of root reinforcement. The peak root reinforcement does not generally occur at the same displacement as the soil peak strength, but for larger strain values [START_REF] Nakamura | Reinforcement of tree roots in slope stability: a case study from the Ozawa slope in Iwate Prefecture, Japan. Eco-Ground Bio-Eng Use Veg Improve Slope Stab[END_REF][START_REF] Schwarz | Root reinforcement of soils under compression[END_REF]. As a consequence, an increase of the displacement of the peak resistance and an increase of the residual resistance is observed as in Fig. 5 [START_REF] Gray | Mechanics of fiber reinforcement in sand[END_REF][START_REF] Abe | Effect of tree roots on a shear zone: modelling reinforced shear stress[END_REF]. Also, it opened a way for the development of constitutive laws to describe the root-permeated soil.

Discussion on the Root "Breaking" Models

Roots are loaded in different manners along the failure surface of a shallow landslide. At the crest, roots are subjected to pull out forces as a result of the tension cracks that may appear. Along the base of the unstable layer, shear actions are applied to the roots leading to pull out, breakage or buckling, depending on the orientation of the root. Finally, at the toe of the slope roots are under compression, failing by buckling [START_REF] Schwarz | Root reinforcement of soils under compression[END_REF]. Each type of root failure is described in more detail in [START_REF] Dias | A review on the types of root failures along the failure surface of a shallow landslide[END_REF], whose distinction is necessary in order to consider the resistance that the roots actually provide.

Not all the BMs were initially proposed to take into account different root failure mechanisms and for sure that the model by [START_REF] Wu | Investigation of landslides on Prince of Wales Island, Alaska[END_REF] in Fig. 2 does not represent all the presented situations. However, a clear and positive evolution of the root reinforcement calculation methods was observed in this regard. In this discussion section, it is highlighted the flexibility of the BMs and their potential.

As previously mentioned, the BMs provide the maximum reinforcement of a root bundle based on the resistance of each individual. This means that any critical load (breakage, slippage or buckling) can be used to study the root additional cohesion. Therefore, to have the tensile reinforcement mobilized in tension cracks, the pull out resistance of the roots is considered as input of the BMs, considering or not the slip out of the root (Schwarz et al. 2010a). To calculate the shear reinforcement, the previous results are applied to (2), in which the possibility of the root being under tension or compression is already considered in the parameter 𝑘′. Finally, to obtain the reinforcement at the toe of the slope, the BM's input is the critical buckling load [START_REF] Schwarz | Root reinforcement of soils under compression[END_REF].

Numerical Models

Numerical methods have been used to estimate root reinforcement in the composite material. Yet, the description of root-soil interface and root large displacements are some of the limitations reported in the literature. The disadvantages of these methods are mainly related with the occurrence of fractures, as well as root breakage and slip out [START_REF] Tiwari | New numerical scheme in the finite-element method for evaluating the root-reinforcement effect on soil slope stability[END_REF]).

In the work of [START_REF] Mao | Evaluation of root reinforcement models using numerical modelling approaches[END_REF], three-dimensional direct shear tests were simulated using both FEM and DEM models. Three different structural elements were used to simulate the roots and their interaction with the surrounding soil. The beam type roots presented tensile, compressive and bending resistance, the truss type presented tensile and compressive resistance and the cable type only mobilized tensile resistance. The calibration of these models is based on the results of direct shear tests on root-permeated soil.

Liang et al. ( 2015) produced an analytical model of a root and its soil interaction using existing p-y curves for piles in a problem beam on elastic foundation under lateral loading. The study was executed for a shear zone at different depths by imposing displacements to the springs above the shear zone to simulate soil deformation, which is simpler from a computational point of view than using a continuum media. The ultimate resistance of the adopted p-y curve depends on the embedded depth of the root. [START_REF] Liang | Modelling the seismic performance of rooted slopes from individual root-soil interaction to global slope behaviour[END_REF] found large relative soil-root deformations even for relatively small global slip of the rooted soil. In fact, at shallow depths, the soil that is pressed against the root move upward forming a wedge due to the low confining pressures. When the confining pressure increases, soil tends to contour the root. This way, the ultimate resistance of the soil surrounding the root is reached before the critical state of the soil. The beam model was validated by comparing the increase shear strength provided by roots based on direct shear tests and on the analytical model. The additional shear force was obtained from the numerical model of the beam by integrating the reaction force along the root.

Other FEM models of roots have been developed recently, such as [START_REF] Dupuy | A generic 3D finite element model of tree anchorage integrating soil mechanics and real root system architecture[END_REF] and [START_REF] Fourcaud | Understanding the impact of root morphology on overturning mechanisms: a modelling approach[END_REF], however to study root anchorage when the plant is subjected to overturning actions (e.g. wind). [START_REF] Dupuy | A generic 3D finite element model of tree anchorage integrating soil mechanics and real root system architecture[END_REF] produced a FEM model with the real root geometry represented by 2-node linear beam elements. A great computational effort was necessary to produce such analysis and it is unthinkable to extend such analyses for an entire slope. The interaction between the structural element and the soil is considered rigid based on field observations [START_REF] Dupuy | A generic 3D finite element model of tree anchorage integrating soil mechanics and real root system architecture[END_REF]). Therefore, it is assumed that root slippage does not directly occur at the root-soil interface but in the nearest neighbouring soil around the roots (Mickovski et al. 2011;[START_REF] Mao | Evaluation of root reinforcement models using numerical modelling approaches[END_REF].

Application of Root Reinforcement to Slope Stability

The calculation of the root reinforcement previously presented is then applied to access the safety factor (SF) associated to a slope. Two main approaches are the following ones: limit equilibrium (LE) and finite element method (FEM). In the following examples of application of those methods are presented.

Limit Equilibrium [START_REF] Greenwood | SLIP4EX-a program for routine slope stability analysis to include the effects of vegetation, reinforcement and hydrological changes[END_REF] presented a software for the calculation of SF using LE analysis by the method of slices. The software allows a comparison of different computation methods, such as Bishop, Janbu, Fellenius, Simple and Greenwood. The inclusion of the vegetation effect is made by means of a force applied to the base of the slices and it is recommended by the author the lowering of the groundwater table by 10 cm.

Even though [START_REF] Greenwood | SLIP4EX-a program for routine slope stability analysis to include the effects of vegetation, reinforcement and hydrological changes[END_REF] has suggested this software for preliminary analysis, some researchers, such as [START_REF] Danjon | Using three-dimensional plant root architecture in models of shallow-slope stability[END_REF][START_REF] Genet | The influence of plant diversity on slope stability in a moist evergreen deciduous forest[END_REF] and [START_REF] Sonnenberg | Centrifuge modelling of soil slopes reinforced with vegetation[END_REF], have been using it to investigate the influence of vegetation on slope stability for being user-friendly. Nevertheless, [START_REF] Stokes | Desirable plant root traits for protecting natural and engineered slopes against landslides[END_REF] highlighted that this method tends to overestimate the SF.

Other commercial software based on the slices method, such as GeoSlope, have been used to calculate the safety factor, as in the work of Tardio and Mickovsli (2015), where a surface soil layer is introduced in the model with the mechanical properties of a rooted soil. [START_REF] Bischetti | Quantifying the effect of brush layering on slope stability[END_REF] investigated the effect of brush layering on slope stability using an infinite slope model where a resistant force is provided by each brush live cutting inserted in the soil. In the work of [START_REF] Nakamura | Reinforcement of tree roots in slope stability: a case study from the Ozawa slope in Iwate Prefecture, Japan. Eco-Ground Bio-Eng Use Veg Improve Slope Stab[END_REF], where roots were modelled according to [START_REF] Nghiem | Analysis of root reinforcement at slip surface[END_REF], the reinforcement provided by the roots is introduced in the infinite slope model with planar failure surface and the 𝑆𝐹 is given by ( 9), where 𝑤 represents the soil weight of the slice per unit area, 𝑢 is the pore pressure at the base of the slice per unit area, 𝑐 is the soil cohesion, 𝛥𝑆 𝑅𝑐 is the increment of cohesion resultant from the presence of roots and 𝛼 is the inclination of the slope. This is the simplest model.

𝑆𝐹 = (𝑤 𝑐𝑜𝑠 𝛼 -𝑢) 𝑡𝑎𝑛 𝜙 + (𝑐 + 𝛥𝑆 𝑅𝑐 ) 𝑢 𝑠𝑖𝑛 𝛼 (9)
However, it is known that roots reinforcement is only mobilized for greater displacements than the yielding strain of the soil [START_REF] Gray | Mechanics of fiber reinforcement in sand[END_REF]. Considering LE analysis seems, for this reason an approach which is not appropriate.

Finite Element Method

Root reinforcement is always represented as an increase of cohesion in the surface soil layer [START_REF] Tiwari | New numerical scheme in the finite-element method for evaluating the root-reinforcement effect on soil slope stability[END_REF] or in the regions where vegetation is present [START_REF] Genet | Root reinforcement in plantations of Cryptomeria japonica D. Don: effect of tree age and stand structure on slope stability[END_REF][START_REF] Mao | Evaluation of root reinforcement models using numerical modelling approaches[END_REF][START_REF] Liang | Modelling the seismic performance of rooted slopes from individual root-soil interaction to global slope behaviour[END_REF]. However, the method of calculation of such cohesion differs. In the case of [START_REF] Liang | Modelling the seismic performance of rooted slopes from individual root-soil interaction to global slope behaviour[END_REF], the root reinforcement is obtained from a numerical model. On the other hand, [START_REF] Genet | Root reinforcement in plantations of Cryptomeria japonica D. Don: effect of tree age and stand structure on slope stability[END_REF] used "breaking" models. [START_REF] Genet | Root reinforcement in plantations of Cryptomeria japonica D. Don: effect of tree age and stand structure on slope stability[END_REF] produced a FEM model using a commercial software to investigate how the root cohesion could influence the SF of the slope in unsaturated conditions. The root cohesion was calculated as a function of the depth and distance from the stem using W&W. Similarly, [START_REF] Liang | Modelling the seismic performance of rooted slopes from individual root-soil interaction to global slope behaviour[END_REF] used blocks of root-permeated soil material with increasing cohesion in depth in a 2D FEM model of the slope to investigate the root influence on the behaviour of a slope. In this case, the computation of the roots additional cohesion required the analyses of p-y curves for different depths of the failure surface, root diameters and group effect of a bundle of roots by comparing direct shear tests performed on spread roots. [START_REF] Mao | Evaluation of root reinforcement models using numerical modelling approaches[END_REF] produced a slope stability analysis using a 3D FEM software. The displacements and stresses at each node as well as the SF were calculated to access the influence of different roots densities and distributions on slope stability. The influence of the roots was considered as an additional root cohesion calculated using different root "breaking" models. However, the innovation in this work was that the properties of the soil were assigned individually to each node of the mesh using an algorithm allowing the root cohesion varying vertically and horizontally.

Even though developments have been made on the estimation of the root cohesion, researchers insist on using W&W, which is known to overestimate root reinforcement. Moreover, FEM enables the gradual mobilization of the root reinforcement with increasing displacement, but in the examples here presented root influence takes the form of an additional cohesion, which means that the full potential of FEM has not yet been used.

Conclusions

Roots are loaded in different manners along a failure surface of a shallow landslide. At the crest, tension cracks may appear and roots are subjected to pull out forces. Along the base of the unstable layer, shear actions are applied to the roots. At the foot of the slope, roots are under compression, failing by buckling [START_REF] Schwarz | Root reinforcement of soils under compression[END_REF]. Due to mobilization of roots tensile strength, an increase of cohesion occurs into the soil, even though as influence on the frictional term for low confining pressures has been observed.

Most of the proposed methods to evaluate root reinforcement only assume root breakage, which leads to overestimation of the root reinforcement. Nevertheless, these methods are flexible enough to consider other types of root failure depending on what the ultimate resistance is considered to be. The evolution of these root "breaking" models lead to formulations that include the root resistance variability, as well as the possibility of investigating the displacement at which roots fail and its correspondent root reinforcement value.

Numerical models also have been used to study the effects of roots on the resistance of rootpermeated soil by using structural elements to represent the fibres. The advantage of such approach is in considering soil-root interaction, whose representation can still be improved.

Finally, a slope stability analysis can be produced considering the root reinforcement. The representation of this reinforcement can be through macro models or root-soil interaction models. The representation of a root system with structural elements is rather complex and computationally demanding, so the representation of the roots is made using an equivalent material with the same properties of root-permeated soil. LE and FEM models were used. In LE models, that tend to overestimate the SF, the root reinforcement is considered as an additional cohesion or resistant force at the base of the sliding layer is used. In the case of FEM, blocks or layers of soil are represented where the effect of the presence of roots is incorporated by an additional cohesion, not taking advantage of the full potential of the method.

Fig. 2

 2 Fig. 2 Scheme of the stresses in the root during shear

  𝜔 is the Weibull exponent, 𝜆 * is the scaling factor and ∆𝑥 * is the normalized displacement. The exponent 𝜔 represents the relative variability of root strength in relation to an optimized root diameter[START_REF] Schwarz | Modelling root reinforcement using a root-failure Weibull survival function[END_REF][START_REF] Vergani | Effects of root tensile force and diameter distribution variability on root reinforcement in the Swiss and Italian Alps[END_REF]. High 𝜔 values (e.g. 𝜔 = 100) represent low variability of root mechanical behaviour resulting into displacement-force relations with sharp peaks correspondent to the failure of each root diameter class, as in Fig.4. Decreasing values of 𝜔 traduce increasing variability of root strength within a diameter class and consequently a lower maximum force. Details on the calibration of the survival function can be found in[START_REF] Schwarz | Modelling root reinforcement using a root-failure Weibull survival function[END_REF].

Fig. 4

 4 Fig. 4 Scheme of the RBM and RBMw outputs of a root bundle of three diameter classes

Fig. 5

 5 Fig.5Shear stress-displacement curves for soil samples with and without roots[START_REF] Cazzuffi | Geosynthetic engineering and vegetation growth in soil reinforcement applications[END_REF] An analysis performed by[START_REF] Vergani | Effects of root tensile force and diameter distribution variability on root reinforcement in the Swiss and Italian Alps[END_REF] showed that the characterization of mechanical properties and root distribution is fundamental for the quantification of root reinforcement. Great variability in the estimated values were obtained by this author, that highlighted that the Weibull exponent applied to a general force-displacement curve leads to the estimation of conservative peak reinforcement values. Therefore,[START_REF] Vergani | Effects of root tensile force and diameter distribution variability on root reinforcement in the Swiss and Italian Alps[END_REF] stated that the use of the RBMw is an important improvement in the estimation of root reinforcement.

Acknowledgements

The authors wish to acknowledge the support of the European Commission via the Marie Skłodowska-Curie Innovative Training Networks (ITN-ETN) project TERRE 'Training Engineers and Researchers to Rethink geotechnical Engineering for a low carbon future' (H2020-MSCA-ITN-2015-675762).