Frédéric Blanqui

Guillaume Genestier

Olivier Hermant

Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting

Keywords: 2012 ACM Subject Classification Theory of computation → Equational logic and rewriting; Theory of computation → Type theory Termination, Higher-Order Rewriting, Dependent Types, Dependency Pairs Digital Object Identifier 10.4230/LIPIcs

Dependency pairs are a key concept at the core of modern automated termination provers for first-order term rewriting systems. In this paper, we introduce an extension of this technique for a large class of dependently-typed higher-order rewriting systems. This extends previous results by Wahlstedt on the one hand and the first author on the other hand to strong normalization and non-orthogonal rewriting systems. This new criterion is implemented in the type-checker Dedukti.

Introduction

Termination, that is, the absence of infinite computations, is an important problem in software verification, as well as in logic. In logic, it is often used to prove cut elimination and consistency. In automated theorem provers and proof assistants, it is often used (together with confluence) to check decidability of equational theories and type-checking algorithms.

This paper introduces a new termination criterion for a large class of programs whose operational semantics can be described by higher-order rewriting rules [START_REF]Term rewriting systems[END_REF] typable in the λΠ-calculus modulo rewriting (λΠ/R for short). λΠ/R is a system of dependent types where types are identified modulo the β-reduction of λ-calculus and a set R of rewriting rules given by the user to define not only functions but also types. It extends Barendregt's Pure Type System (PTS) λP [3], the logical framework LF [START_REF] Harper | A framework for defining logics[END_REF] and Martin-Löf's type theory. It can encode any functional PTS like System F or the Calculus of Constructions [START_REF] Cousineau | Embedding pure type systems in the λΠ-calculus modulo[END_REF].

Dependent types, introduced by de Bruijn in Automath, subsume generalized algebraic data types (GADT) used in some functional programming languages. They are at the core of many proof assistants and programming languages: Coq, Twelf, Agda, Lean, Idris, . . . Our criterion has been implemented in Dedukti, a type-checker for λΠ/R that we will use in our examples. The code is available in [START_REF] Genestier | SizeChangeTool[END_REF] and could be easily adapted to a subset of other languages like Agda. As far as we know, this tool is the first one to automatically check termination in λΠ/R, which includes both higher-order rewriting and dependent types.

This criterion is based on dependency pairs, an important concept in the termination of first-order term rewriting systems. It generalizes the notion of recursive call in firstorder functional programs to rewriting. Namely, the dependency pairs of a rewriting rule f (l 1 , . . . , l p ) → r are the pairs (f (l 1 , . . . , l p ), g(m 1 , . . . , m q )) such that g(m 1 , . . . , m q ) is a subterm of r and g is a function symbol defined by some rewriting rules. Dependency pairs have been introduced by Arts and Giesl [2] and have evolved into a general framework for termination [START_REF] Giesl | The dependency pair framework: combining techniques for automated termination proofs[END_REF]. It is now at the heart of many state-of-the-art automated termination

Outline

The main result is Theorem 11 stating that, for a large class of rewriting systems R, the combination of β and R is strongly normalizing on terms typable in λΠ/R if, roughly speaking, there is no infinite sequence of dependency pairs.

The proof involves two steps. First, after recalling the terms and types of λΠ/R in Section 2, we introduce in Section 3 a model of this calculus based on Girard's reducibility candidates [START_REF] Girard | Proofs and types[END_REF], and prove that every typable term is strongly normalizing if every symbol of the signature is in the interpretation of its type (Adequacy lemma). Second, in Section 4, we introduce our notion of dependency pair and prove that every symbol of the signature is in the interpretation of its type if there is no infinite sequence of dependency pairs.

In order to show the usefulness of this result, we give simple criteria for checking the conditions of the theorem. In Section 5, we show that plain function passing systems belong to the class of systems that we consider. And in Section 6, we show how to use size-change termination to obtain the termination of the dependency pair relation.

Finally, in Section 7 we compare our criterion with other criteria and tools and, in Section 8, we summarize our results and give some hints on possible extensions.

For lack of space, some proofs are given in an appendix at the end of the paper.

Terms and types

The set T of terms of λΠ/R is the same as those of Barendregt's λP [3]:

t ∈ T = s ∈ S | x ∈ V | f ∈ F | ∀x : t, t | tt | λx : t, t
where S = {TYPE, KIND} is the set of sorts1 , V is an infinite set of variables and F is a set of function symbols, so that S, V and F are pairwise disjoint. Furthermore, we assume given a set R of rules l → r such that FV(r) ⊆ FV(l) and l is of the form f l. A symbol f is said to be defined if there is a rule of the form f l → r. In this paper, we are interested in the termination of

→ = → β ∪ → R
where → β is the β-reduction of λ-calculus and → R is the smallest relation containing R and closed by substitution and context: we consider rewriting with syntactic matching only. Following [START_REF] Blanqui | Termination of rewrite relations on λ-terms based on Girard's notion of reducibility[END_REF], it should however be possible to extend the present results to rewriting with matching modulo βη or some equational theory. Let SN be the set of terminating terms and, given a term t, let →(t) = {u ∈ T | t → u} be the set of immediate reducts of t.

A typing environment Γ is a (possibly empty) sequence x 1 : T 1 , . . . , x n : T n of pairs of variables and terms, where the variables are distinct, written x : T for short. Given an environment Γ = x : T and a term U , let ∀Γ, U be ∀ x : T , U . The product arity ar(T ) of a term T is the integer n ∈ N such that T = ∀x 1 : T 1 , . . . ∀x n : T n , U and U is not a product. Let t denote a possibly empty sequence of terms t 1 , . . . , t n of length | t| = n, and FV(t) be the set of free variables of t.

For each f ∈ F, we assume given a term Θ f and a sort s f , and let Γ f be the environment such that Θ f = ∀Γ f , U and

|Γ f | = ar(Θ f ).
The application of a substitution σ to a term t is written tσ. Given a substitution σ,

let dom(σ) = {x|xσ = x}, FV(σ) = x∈dom(σ) FV(xσ) and [x → a, σ] ([x → a] if σ is the identity) be the substitution {(x, a)} ∪ {(y, b) ∈ σ | y = x}. Given another substitution σ , let σ → σ if there is x such that xσ → xσ and, for all y = x, yσ = yσ .
The typing rules of λΠ/R, in Figure 1, add to those of λP the rule (fun) similar to (var). Moreover, (conv) uses ↓ instead of ↓ β , where ↓ = → * * ← is the joinability relation and → * the reflexive and transitive closure of →. We say that t has type T in Γ if Γ t : T is derivable. A substitution σ is well-typed from ∆ to Γ, written Γ σ : ∆, if, for all (x : T ) ∈ ∆, Γ xσ : T σ holds.

The word "type" is used to denote a term occurring at the right-hand side of a colon in a typing judgment (and we usually use capital letters for types). Hence, KIND is the type of TYPE, Θ f is the type of f , and s f is the type of Θ f . Common data types like natural numbers N are usually declared in λΠ as function symbols of type TYPE: Θ N = TYPE and s N = KIND.

The dependent product ∀x : A, B generalizes the arrow type A ⇒ B of simply-typed λ-calculus: it is the type of functions taking an argument x of type A and returning a term whose type B may depend on x. If B does not depend on x, we sometimes simply write A ⇒ B.

A : s x / ∈ dom(Γ) Γ, x : A x : A (weak) Γ A : s Γ b : B x / ∈ dom(Γ) Γ, x : A b : B (prod) Γ A : TYPE Γ, x : A B : s Γ ∀x : A, B : s (abs) Γ, x : A b : B Γ ∀x : A, B : s Γ λx : A.b : ∀x : A, B (app) Γ t : ∀x : A, B Γ a : A Γ ta : B[x → a] (conv) Γ a : A A ↓ B Γ B : s Γ a : B (fun) Θ f : s f f : Θ f
Typing induces a hierarchy on terms [START_REF] Blanqui | Théorie des types et récriture[END_REF]Lemma 47]. At the top, there is the sort KIND that is not typable. Then, comes the class K of kinds, whose type is KIND: K = TYPE | ∀x : t, K where t ∈ T. Then, comes the class of predicates, whose types are kinds. Finally, at the bottom lie (proof) objects whose types are predicates.

Example 1 (Filter function on dependent lists). To illustrate the kind of systems we consider, we give an extensive example in the new Dedukti syntax combining type-level rewriting rules (El converts datatype codes into Dedukti types), dependent types (L is the polymorphic type of lists parameterized with their length), higher-order variables (fil is a function filtering elements out of a list along a boolean function f), and matching on defined function symbols (fil can match a list defined by concatenation). Note that this example cannot be represented in Coq or Agda because of the rules using matching on app. And its termination can be handled neither by [38] nor by [START_REF] Blanqui | Definitions by rewriting in the calculus of constructions[END_REF] because the system is not orthogonal and has no strict decrease in every recursive call. It can however be handled by our new termination criterion and its implementation [START_REF] Genestier | SizeChangeTool[END_REF]. For readability, we removed the & which are used to identify pattern variables in the rewriting rules. symbol plus: Nat ⇒ Nat ⇒Nat set infix 1 " + " := plus rule zero + q → q rule ( s p ) + q → s ( p + q ) symbol List: Set ⇒ Nat ⇒ TYPE symbol nil: ∀a , List a zero symbol cons:∀a , El a ⇒ ∀p , List a p ⇒ List a ( s p ) symbol app: ∀a p , List a p ⇒ ∀q , List a q ⇒ List a ( p + q ) rule app a _ ( nil _ ) q m → m rule app a _ ( cons _ x p l ) q m → cons a x ( p + q ) ( app a p l q m ) symbol len_fil: ∀a , ( El a ⇒ Bool ) ⇒ ∀p , List a p ⇒ Nat symbol len_fil_aux: Bool ⇒ ∀a , ( El a ⇒ Bool ) ⇒ ∀p , List a p ⇒ Nat rule len_fil a f _ ( nil _ ) → zero rule len_fil a f _ ( cons _ x p l ) → len_fil_aux ( f x ) a f p l rule len_fil a f _ ( app _ p l q m ) → ( len_fil a f p l ) + ( len_fil a f q m ) rule len_fil_aux true a f p l → s ( len_fil a f p l ) rule len_fil_aux false a f p l → len_fil a f p l symbol fil: ∀a f p l , List a ( len_fil a f p l ) symbol fil_aux: ∀b a f , El a ⇒ ∀p l , List a ( len_fil_aux b a f p l ) rule fil a f _ ( nil _ ) → nil a rule fil a f _ ( cons _ x p l ) → fil_aux ( f x ) a f x p l rule fil a f _ ( app _ p l q m ) → app a ( len_fil a f p l ) ( fil a f p l ) ( len_fil a f q m ) ( fil a f q m ) rule fil_aux false a f x p l → fil a f p l rule fil_aux true a f x p l → cons a x ( len_fil a f p l ) ( fil a f p l )

Assumptions: Throughout the paper, we assume that → is locally confluent (←→ ⊆ ↓) and preserves typing (for all Γ, A, t and u, if Γ t : A and t → u, then Γ u : A).

Note that local confluence implies that every t ∈ SN has a unique normal form t↓. These assumptions are used in the interpretation of types (Definition 2) and the adequacy lemma (Lemma 5). Both properties are undecidable in general. For confluence, Dedukti can call confluence checkers that understand the HRS format of the confluence competition. For preservation of typing by reduction, it implements an heuristic [START_REF] Saillard | Type checking in the Lambda-Pi-calculus modulo: theory and practice[END_REF].

Interpretation of types as reducibility candidates

We aim to prove the termination of the union of two relations, → β and → R , on the set of well-typed terms (which depends on R since ↓ includes → R ). As is well known, termination is not modular in general. As a β step can generate an R step, and vice versa, we cannot expect to prove the termination of → β ∪ → R from the termination of → β and → R . The termination of λΠ/R cannot be reduced to the termination of the simply-typed λ-calculus either (as done for λΠ alone in [START_REF] Harper | A framework for defining logics[END_REF]) because of type-level rewriting rules like the ones defining El in Example 1. Indeed, type-level rules enable the encoding of functional PTS like Girard's System F, whose termination cannot be reduced to the termination of the simply-typed λ-calculus [START_REF] Cousineau | Embedding pure type systems in the λΠ-calculus modulo[END_REF]. So, following Girard [START_REF] Girard | Proofs and types[END_REF], to prove the termination of → β ∪ → R , we build a model of our calculus by interpreting types into sets of terminating terms. To this end, we need to find an interpretation having the following properties: Because types are identified modulo conversion, we need to be invariant by reduction: if T is typable and T → T , then we must have T = T . As usual, to handle β-reduction, we need a product type ∀x : A, B to be interpreted by the set of terms t such that, for all a in the interpretation of

A, ta is in the interpretation of B[x → a], that is, we must have ∀x : A, B = Πa ∈ A . B[x → a] where Πa ∈ P. Q(a) = {t | ∀a ∈ P, ta ∈ Q(a)}.
First, we define the interpretation of predicates (and TYPE) as the least fixpoint of a monotone function in a directed-complete (= chain-complete) partial order [START_REF] Markowsky | Chain-complete posets and directed sets with applications[END_REF]. Second, we define the interpretation of kinds by induction on their size.

Definition 2 (Interpretation of types). Let I = F p (T, P(T)) be the set of partial functions from T to the powerset of T. It is directed-complete wrt inclusion, allowing us to define I as the least fixpoint of the monotone function

F : I → I such that, if I ∈ I, then:

The domain of F (I) is the set D(I) of all the terminating terms T such that, if T reduces to some product term ∀x : A, B (not necessarily in normal form), then A ∈ dom(I) and, for all a ∈ I(A), B[x → a] ∈ dom(I).

If T ∈ D(I) and the normal form 2 of T is not a product, then

F (I)(T ) = SN. If T ∈ D(I) and T↓ = ∀x : A, B, then F (I)(T ) = Πa ∈ I(A). I(B[x → a]).
We now introduce D = D(I) and define the interpretation of a term T wrt to a substitution σ, T σ (and simply T if σ is the identity), as follows:

s σ = D if s ∈ S, ∀x : A, K σ = Πa ∈ A σ . K [x →a,σ] if K ∈ K and x / ∈ dom(σ), T σ = I(T σ) if T / ∈ K ∪ {KIND} and T σ ∈ D, T σ = SN otherwise. A substitution σ is adequate wrt an environment Γ, σ |= Γ, if, for all x : A ∈ Γ, xσ ∈ A σ . A typing map Θ is adequate if, for all f , f ∈ Θ f whenever Θ f : s f and Θ f ∈ s f . Let C be the set of terms of the form f t such that | t| = ar(Θ f ), Θ f : s f , Θ f ∈ s f and, if Γ f = x : A and σ = [ x → t], then σ |= Γ f .

(Informally, C is the set of terms obtained by fully applying some function symbol to computable arguments.)

We can then prove that, for all terms T , T satisfies Girard's conditions of reducibility candidates, called computability predicates here, adapted to rewriting by including in neutral terms every term of the form f t when f is applied to enough arguments wrt R [START_REF] Blanqui | Definitions by rewriting in the calculus of constructions[END_REF]:

Definition 3 (Computability predicates). A term is neutral if it is of the form (λx : A, t)u v, x v or f v with, for every rule f l → r ∈ R, | l| ≤ | v|.
Let P be the set of all the sets of terms S (computability predicates) such that (a) S ⊆ SN, (b) →(S) ⊆ S, and (c) t ∈ S if t is neutral and →(t) ⊆ S.

Note that neutral terms satisfy the following key property: if t is neutral then, for all u, tu is neutral and every reduct of tu is either of the form t u with t a reduct of t, or of the form tu with u a reduct of u.

One can easily check that SN is a computability predicate. Note also that a computability predicate is never empty: it contains every neutral term in normal form. In particular, it contains every variable.

We then get the following results (the proofs are given in Appendix A):

Lemma 4. (a) For all terms T and substitutions σ, T σ ∈ P.

(b) If T is typable, T σ ∈ D and T → T , then T σ = T σ . (c) If T is typable, T σ ∈ D and σ → σ , then T σ = T σ . (d) If ∀x : A, B is typable and ∀x : Aσ, Bσ ∈ D, then ∀x : A, B σ = Πa ∈ A σ . B [x →a,σ] . (e) If ∆ U : s, Γ γ : ∆ and U γσ ∈ D, then U γ σ = U γσ . (f) Given P ∈ P and, for all a ∈ P , Q(a) ∈ P such that Q(a ) ⊆ Q(a) if a → a . Then, λx : A, b ∈ Πa ∈ P. Q(a) if A ∈ SN and, for all a ∈ P , b[x → a] ∈ Q(a).
We can finally prove that our model is adequate, that is, every term of type T belongs to T , if the typing map Θ itself is adequate. This reduces the termination of well-typed terms to the computability of function symbols.

Lemma 5 (Adequacy).

If Θ is adequate, Γ t : T and σ |= Γ, then tσ ∈ T σ .

2 Because we assume local confluence, every terminating term T has a unique normal form T↓.

F. Blanqui, G. Genestier and O. Hermant XX:7

Proof. First note that, if Γ t : T , then either T = KIND or Γ T : s [4, Lemma 28]. Moreover, if Γ a : A, A ↓ B and Γ B : s (the premises of the (conv) rule), then Γ A : s [4, Lemma 42] (because → preserves typing). Hence, the relation is unchanged if one adds the premise Γ A : s in (conv), giving the rule (conv'). Similarly, we add the premise Γ ∀x : A, B : s in (app), giving the rule (app'). We now prove the lemma by induction on Γ t : T using (app') and (conv'):

Dependency pairs theorem

Now, we prove that the adequacy of Θ can be reduced to the absence of infinite sequences of dependency pairs, as shown by Arts and Giesl for first-order rewriting [2].

Definition 6 (Dependency pairs). Let f l > g m iff there is a rule f l → r ∈ R, g is defined and g m is a subterm of r such that m are all the arguments to which g is applied. The relation > is the set of dependency pairs. Let > = → * arg > s be the relation on the set C (Def. 2), where f t → arg f u iff t → prod u (reduction in one argument), and > s is the closure by substitution and left-application of >: f t 1 . . . t p > gu 1 . . . u q iff there are a dependency pair f l 1 . . . l i > gm 1 . . . m j with i ≤ p and j ≤ q and a substitution σ such that, for all k ≤ i, t k → * l k σ and, for all k ≤ j, m k σ = u k .

In our setting, we have to close > s by left-application because function symbols are curried. When a function symbol f is not fully applied wrt ar(Θ f ), the missing arguments must be considered as potentially being anything. Indeed, the following rewriting system: ( s p ) + q > p + q D: app a _ ( cons _ x p l ) q m > p + q E: app a _ ( cons _ x p l ) q m > app a p l q m F:len_fil a f _ ( cons _ x p l ) > len_fil_aux ( f x ) a f p l G:len_fil a f _ ( app _ p l q m ) > ( len_fil a f p l ) + ( len_fil a f q m ) H:len_fil a f _ ( app _ p l q m ) > len_fil a f p l I:len_fil a f _ ( app _ p l q m ) > len_fil a f q m J: len_fil_aux true a f p l > len_fil a f p l K: len_fil_aux false a f p l > len_fil a f p l

In [2], a sequence of dependency pairs interleaved with → arg steps is called a chain. Arts and Giesl proved that, in a first-order term algebra, → R terminates if and only if there are no infinite chains, that is, if and only if > terminates. Moreover, in a first-order term algebra, > terminates if and only if, for all f and t, f t terminates wrt > whenever t terminates wrt →. In our framework, this last condition is similar to saying that Θ is adequate.

We now introduce the class of systems to which we will extend Arts and Giesl's theorem.

Definition 8 (Well-structured system). Let be the smallest quasi-order on F such that f g if g occurs in Θ f or if there is a rule f l → r ∈ R with g (defined or undefined) occurring in r. Then, let = \ be the strict part of . A rewriting system R is well-structured if: (a) is well-founded; (b) for every rule f l → r, | l| ≤ ar(Θ f ); (c) for every dependency pair f l > g m, | m| ≤ ar(Θ g ); (d) every rule f l → r is equipped with an environment ∆ f l→r such that, if Θ f = ∀ x : T , U and π = [ x → l], then ∆ f l→r f l r : U π, where f l is the restriction of defined in Fig. 2. Condition (a) is always satisfied when F is finite. Condition (b) ensures that a term of the form f t is neutral whenever | t| = ar(Θ f ). Condition (c) ensures that > is included in >.

The relation f l corresponds to the notion of computability closure in [START_REF] Blanqui | Definitions by rewriting in the calculus of constructions[END_REF], with the ordering on function calls replaced by the dependency pair relation. It is similar to except that it uses the variant of (conv) and (app) used in the proof of the adequacy lemma; (fun) is split in the rules (const) for undefined symbols and (dp) for dependency pairs whose left-hand side is f l; every type occurring in an object term or every type of a function symbol occurring in a term is required to be typable by using symbols smaller than f only.

The environment ∆ f l→r can be inferred by Dedukti when one restricts rule left hand-sides to some well-behaved class of terms like algebraic terms or Miller patterns (in λProlog).

One can check that Example 1 is well-structured (the proof is given in Appendix B). Finally, we need matching to be compatible with computability, that is, if f l → r ∈ R and lσ are computable, then σ is computable, a condition called accessibility in [START_REF] Blanqui | Definitions by rewriting in the calculus of constructions[END_REF]:

Γ ≺f A : s x / ∈ dom(Γ) Γ, x : A f l x : A (weak) Γ ≺f A : s Γ f l b : B x / ∈ dom(Γ) Γ, x : A f l b : B (prod) Γ f l A : TYPE Γ, x : A f l B : s Γ f l ∀x : A, B : s (abs) Γ, x : A f l b : B Γ ≺f ∀x : A, B : s Γ f l λx : A, b : ∀x : A, B (app') Γ f l t : ∀x : A, B Γ f l a : A Γ ≺f ∀x : A, B : s Γ f l ta : B[x → a] (conv') Γ f l a : A A ↓ B Γ ≺f B : s Γ ≺f A : s Γ f l a : B (dp) ≺f Θg : sg Γ f l γ : Σ Γ f l g yγ : V γ (Θg = (∀ y : U , V ), Σ = y : U , g yγ < f l) (const) ≺f Θg : sg f l g : Θg (g undefined)
and ≺f is defined by the same rules as , except (fun) replaced by: Proof. Since R is well-structured, is well-founded by condition (a). We prove that, for all f ∈ F, f ∈ Θ f , by induction on . So, let f ∈ F with Θ f = ∀Γ f , U and Γ f = x 1 : T 1 , . . . , x n : T n . By induction hypothesis, we have that, for all g ≺ f , g ∈ Θ g .

(fun ≺f ) ≺f Θg : sg g ≺ f ≺f g : Θg
Since → arg and > terminate on C and → arg > ⊆ >, we have that → arg ∪ > terminates. We now prove that, for all f t ∈ C, we have f t ∈ U θ where θ = [ x → t], by a second induction on → arg ∪ >. By condition (b), f t is neutral. Hence, by definition of computability, it suffices to prove that, for all u ∈ →(f t), u ∈ U θ . There are 2 cases: The above example is not PFP because f:Nat⇒Ord is not argument of ordrec. Yet, it is accessible if one takes for Ord the least fixpoint of the monotone function F (S) = {t ∈ SN |if t → * lim f then f ∈ Nat ⇒ S, and if t → * suc u then u ∈ S} [START_REF] Blanqui | Definitions by rewriting in the calculus of constructions[END_REF].

u = f v with t → prod v.
Similarly, the following encoding of the simply-typed λ-calculus is not PFP but can be proved accessible by taking

T c = if c↓ = arrow a b then {t ∈ SN | if t → * lamf then f ∈ T a ⇒ T b } else SN Example 15 (Simply-typed λ-calculus).

Size-change termination

In this section, we give a sufficient condition for > to terminate. For first-order rewriting, many techniques have been developed for that purpose. To cite just a few, see for instance [START_REF] Hirokawa | Tyrolean Termination Tool: techniques and features[END_REF][START_REF] Giesl | Mechanizing and improving dependency pairs[END_REF]. Many of them can probably be extended to λΠ/R, either because the structure of terms in which they are expressed can be abstracted away, or because they can be extended to deal also with variable applications, λ-abstractions and β-reductions.

As an example, following Wahlstedt [38], we are going to use Lee, Jones and Ben-Amram's size-change termination criterion (SCT) [START_REF] Lee | The size-change principle for program termination[END_REF]. It consists in following arguments along function calls and checking that, in every potential loop, one of them decreases. First introduced for first-order functional languages, it has then been extended to many other settings: untyped λ-calculus [START_REF] Jones | Termination analysis of the untyped lambda-calculus[END_REF], a subset of OCaml [START_REF] Sereni | Termination analysis of higher-order functional programs[END_REF], Martin-Löf's type theory [38], System F [START_REF] Lepigre | Practical subtyping for System F with sized (co-)induction[END_REF].

We first recall Hyvernat and Raffalli's matrix-based presentation of SCT [START_REF] Hyvernat | Improvements on the "size change termination principle" in a functional language[END_REF]:

Definition 16 (Size-change termination). Let be the smallest transitive relation such that f t 1 . . . t n t i when f ∈ F. The call graph G(R) associated to R is the directed labeled graph on the defined symbols of F such that there is an edge between f and g iff there is a dependency pair f l 1 . . . l p > gm 1 . . . m q . This edge is labeled with the matrix (a i,j ) i≤ar(Θ f ),j≤ar(Θg) where: if l i m j , then a i,j = -1; if l i = m j , then a i,j = 0; otherwise a i,j = ∞ (in particular if i > p or j > q). R is size-change terminating (SCT) if, in the transitive closure of G(R) (using the min-plus semi-ring to multiply the matrices labeling the edges), all idempotent matrices labeling a loop have some -1 on the diagonal.

XX:12 Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting

C + p q + s p -1 ∞ q ∞ 0 len_fil len_fil_aux El app + A,B C D E F G H,I J,K TC 1 TC 2
We add lines and columns of ∞'s in matrices associated to dependency pairs containing partially applied symbols (cases i > p or j > q) because missing arguments cannot be compared with any other argument since they are arbitrary.

The matrix associated to the dependency pair C: (s p) + q > p + q and the call graph associated to the dependency pairs of Example 7 are depicted in Figure 3. The full list of matrices and the extensive call graph of Example 1 can be found in Appendix B.

Lemma 17. > terminates if F is finite and R is SCT.

Proof. Suppose that there is an infinite sequence χ = f 1 t 1 >f 2 t 2 > . . . Then, there is an infinite path in the call graph going through nodes labeled by f 1 , f 2 , . . . Since F is finite, there is a symbol g occurring infinitely often in this path. So, there is an infinite sequence g u 1 , g u 2 , . . . extracted from χ. Hence, for every i, j ∈ N * , there is a matrix in the transitive closure of the graph which labels the loops of g corresponding to the relation between u i and u i+j . By Ramsey's theorem, there is an infinite sequence (φ i ) and a matrix M such that M corresponds to all the transitions g u φi , g u φj with i = j. M is idempotent, indeed g u φi , g u φi+2 is labeled by M 2 by definition of the transitive closure and by M due to Ramsey's theorem, so M = M 2 . Since, by hypothesis, R satisfies SCT, there is j such that M j,j is -1. So, for all i, u (j) φi (→ * ) + u (j) φi+1 . Since → ⊆ → and → arg is well-founded on C, the existence of an infinite sequence contradicts the fact that is well-founded.

By combining all the previous results, we get: Theorem 18. The relation → = → β ∪ → R terminates on terms typable in λΠ/R if → is locally confluent and preserves typing, F is finite and R is well-structured, plain-function passing and size-change terminating.

The rewriting system of Example 1 verifies all these conditions (proof in the appendix).

Implementation and comparison with other criteria and tools

We implemented our criterion in a tool called SizeChangeTool [START_REF] Genestier | SizeChangeTool[END_REF]. As far as we know, there are no other termination checker for λΠ/R. If we restrict ourselves to simply-typed rewriting systems, then we can compare it with the termination checkers participating in the category "higher-order rewriting union beta" of the termination competition: Wanda uses dependency pairs, polynomial interpretations, HORPO and many transformation techniques [START_REF] Kop | Higher order termination[END_REF]; SOL uses the General Schema [START_REF] Blanqui | Termination of rewrite relations on λ-terms based on Girard's notion of reducibility[END_REF] and other techniques. As these tools implement various techniques and SizeChangeTool only one, it is difficult to compete with them. Still, there are examples that are solved by SizeChangeTool and not by one of the other tools, demonstrating that these tools would benefit from implementing our new technique. For instance, the problem Hamana_Kikuchi_18/h17 is proved terminating by SizeChangeTool but not by Wanda because of the rule: rule map f ( map g l ) → map ( comp f g ) l

And the problem Kop13/kop12thesis_ex7.23 is proved terminating by SizeChangeTool but not by Sol because of the rules:3 rule f h x ( s y ) → g ( c x ( h y )) y rule g x y → f (λ_ , s 0) x y

One could also imagine to translate a termination problem in λΠ/R into a simply-typed termination problem. Indeed, the termination of λΠ alone (without rewriting) can be reduced to the termination of the simply-typed λ-calculus [START_REF] Harper | A framework for defining logics[END_REF]. This has been extended to λΠ/R when there are no type-level rewrite rules like the ones defining El in Example 1 [START_REF] Jouannaud | Termination of Dependently Typed Rewrite Rules[END_REF]. However, this translation does not preserve termination as shown by the Example 15 which is not terminating if all the types Tx are mapped to the same type constant.

In [START_REF] Roux | Refinement Types as Higher-Order Dependency Pairs[END_REF], Roux also uses dependency pairs for the termination of simply-typed higher-order rewriting systems, as well as a restricted form of dependent types where a type constant C is annotated by a pattern l representing the set of terms matching l. This extends to patterns the notion of indexed or sized types [START_REF] Hughes | Proving the correctness of reactive systems using sized types[END_REF]. Then, for proving the absence of infinite chains, he uses simple projections [START_REF] Hirokawa | Tyrolean Termination Tool: techniques and features[END_REF], which can be seen as a particular case of SCT where strictly decreasing arguments are fixed (SCT can also handle permutations in arguments).

Finally, if we restrict ourselves to orthogonal systems, it is also possible to compare our technique to the ones implemented in the proof assistants Coq and Agda. Coq essentially implements a higher-order version of primitive recursion. Agda on the other hand uses SCT.

Because Example 1 uses matching on defined symbols, it is not orthogonal and can be written neither in Coq nor in Agda. Agda recently added the possibility of adding rewrite rules but this feature is highly experimental and comes with no guaranty. In particular, Agda termination checker does not handle rewriting rules.

Coq cannot handle inductive-recursive definitions [START_REF] Dybjer | A general formulation of simultaneous inductive-recursive definitions in type theory[END_REF] nor function definitions with permuted arguments in function calls while it is no problem for Agda and us.

Conclusion and future work

We proved a general modularity result extending Arts and Giesl's theorem that a rewriting relation terminates if there are no infinite sequences of dependency pairs [2] from first-order rewriting to dependently-typed higher-order rewriting. Then, following [38], we showed how to use Lee, Jones and Ben-Amram's size-change termination criterion to prove the absence of such infinite sequences [START_REF] Lee | The size-change principle for program termination[END_REF]. This extends Wahlstedt's work [38] from weak to strong normalization, and from orthogonal to locally confluent rewriting systems. This extends the first author's work [START_REF] Blanqui | Definitions by rewriting in the calculus of constructions[END_REF] from orthogonal to locally confluent systems, and from systems having a decreasing argument in each recursive call to systems with non-increasing arguments in recursive calls. Finally, this also extends previous works on static dependency pairs [START_REF] Kusakari | Enhancing dependency pair method using strong computability in simply-typed term rewriting systems[END_REF] from simply-typed λ-calculus to dependent types modulo rewriting.

To get this result, we assumed local confluence. However, one often uses termination to check (local) confluence. Fortunately, there are confluence criteria not based on termination. The most famous one is (weak) orthogonality, that is, when the system is left-linear and has no critical pairs (or only trivial ones) [36], as it is the case in functional programming languages. A more general one is when critical pairs are "development-closed" [37].

This work can be extended in various directions. First, our tool is currently limited to PFP rules, that is, to rules where higher-order variables are direct subterms of the left-hand side. To have higher-order variables in deeper subterms like in Example 14, we need to define a more complex interpretation of types, following [START_REF] Blanqui | Definitions by rewriting in the calculus of constructions[END_REF].

Second, to handle recursive calls in such systems, we also need to use an ordering more complex than the subterm ordering when computing the matrices labeling the SCT call graph. The ordering needed for handling Example 14 is the "structural ordering" of Coq and Agda [START_REF] Coquand | Pattern matching with dependent types[END_REF][START_REF] Blanqui | Termination of rewrite relations on λ-terms based on Girard's notion of reducibility[END_REF]. Relations other than subterm have already been considered in SCT but in a first-order setting only [START_REF] Thiemann | The size-change principle and dependency pairs for termination of term rewriting[END_REF].

But we may want to go further because the structural ordering is not enough to handle the following system which is not accepted by Agda: A solution to handle this system is to use arguments filterings (remove the second argument of -) or simple projections [START_REF] Hirokawa | Tyrolean Termination Tool: techniques and features[END_REF]. Another one is to extend the type system with size annotations as in Agda and compute the SCT matrices by comparing the size of terms instead of their structure [1,[START_REF] Blanqui | Size-based termination of higher-order rewriting[END_REF]. In our example, the size of m -n is smaller than or equal to the size of m. One can deduce this by using user annotations like in Agda, or by using heuristics [START_REF] Chin | Calculating sized types[END_REF].

Another interesting extension would be to handle function calls with locally size-increasing arguments like in the following example: rule f x → g ( s x ) rule g ( s ( s x )) → f x

where the number of s's strictly decreases between two calls to f although the first rule makes the number of s's increase. Hyvernat enriched SCT to handle such systems [START_REF] Hyvernat | The size-change termination principle for constructor based languages[END_REF].

( len_fil a f p l ) + ( len_fil a f q m ) H:len_fil a f _ ( app _ p l q m ) > len_fil a f p l I:len_fil a f _ ( app _ p l q m ) > len_fil a f q m J: len_fil_aux true a f p l > len_fil a f p l K: len_fil_aux false a f p l > len_fil a f p l L: fil a f _ ( cons _ x p l ) > fil_aux ( f x ) a f x p l M: fil a f _ ( app _ p l q m ) > app a ( len_fil a f p l ) ( fil a f p l ) ( len_fil a f q m ) ( fil a f q m ) N: fil a f _ ( app _ p l q m ) > len_fil a f p l O: fil a f _ ( app _ p l q m ) > fil a f p l P: fil a f _ ( app _ p l q m ) > len_fil a f q m Q: fil a f _ ( app _ p l q m ) > fil a f q m R: fil_aux true a f x p l > len_fil a f p l S: fil_aux true a f x p l > fil a f p l T: fil_aux false a f x p l > fil a f p l

The whole callgraph is depicted below. The letter associated to each matrix corresponds to the dependency pair presented above and in example 7, except for TC 's which comes from the computation of the transitive closure and labels dotted edges. The argument a is omitted everywhere on the matrices presented below:

The precedence infered for this example is the smallest containing: comparisons linked to the typing of symbols:

Figure 1

 1 Figure 1 Typing rules of λΠ/R

symbol

  Set: TYPE symbol arrow: Set ⇒ Set ⇒ Set symbol El: Set ⇒ TYPE rule El ( arrow a b ) → El a ⇒ El b symbol Bool: TYPE symbol true: Bool symbol false: Bool symbol Nat: TYPE symbol zero: Nat symbol s: Nat ⇒ Nat

  (ax) It is immediate that TYPE ∈ KIND σ = D. (var) By assumption on σ. (weak) If σ |= Γ, x : A, then σ |= Γ. So, the result follows by induction hypothesis. (prod) Is (∀x : A, B)σ in s σ = D? Wlog we can assume x / ∈ dom(σ) ∪ FV(σ). So, (∀x : A, B)σ = ∀x : Aσ, Bσ. By induction hypothesis, Aσ ∈ TYPE σ = D. Let now a ∈ I(Aσ) and σ = [x → a, σ]. Note that I(Aσ) = A σ . So, σ |= Γ, x : A and, by induction hypothesis, Bσ ∈ s σ = D. Since x / ∈ dom(σ) ∪ FV(σ), we have Bσ = (Bσ)[x → a]. Therefore, (∀x : A, B)σ ∈ s σ . (abs) Is (λx : A, b)σ in ∀x : A, B σ ? Wlog we can assume that x / ∈ dom(σ) ∪ FV(σ). So, (λx : A, b)σ = λx : Aσ, bσ. By Lemma 4d, ∀x : A, B σ = Πa ∈ A σ . B [x →a,σ] . By Lemma 4c, B [x →a,σ] is an A σ -indexed family of computability predicates such that B [x →a ,σ] = B [x →a,σ] whenever a → a . Hence, by Lemma 4f, λx : Aσ, bσ ∈ ∀x : A, B σ if Aσ ∈ SN and, for all a ∈ A σ , (bσ)[x → a] ∈ B σ where σ = [x → a, σ]. By induction hypothesis, (∀x : A, B)σ ∈ s σ = D. Since x / ∈ dom(σ) ∪ FV(σ), (∀x : A, B)σ = ∀x : Aσ, Bσ and (bσ)[x → a] = bσ . Since D ⊆ SN, we have Aσ ∈ SN. Moreover, since σ |= Γ, x : A, we have bσ ∈ B σ by induction hypothesis. (app') Is (ta)σ = (tσ)(aσ) in B[x → a] σ ? By induction hypothesis, tσ ∈ ∀x : A, B σ , aσ ∈ A σ and (∀x : A, B)σ ∈ s = D. By Lemma 4d, ∀x : A, B σ = Πα ∈ A σ . B [x →α,σ] . Hence, (tσ)(aσ) ∈ B σ where σ = [x → aσ, σ]. Wlog we can assume x / ∈ dom(σ) ∪ FV(σ). So, σ = [x → a]σ. Hence, by Lemma 4e, B σ = B[x → a] σ . (conv') By induction hypothesis, aσ ∈ A σ , Aσ ∈ s σ = D and Bσ ∈ s σ = D. By Lemma 4b, A σ = B σ . So, aσ ∈ B σ . (fun) By induction hypothesis, Θ f ∈ s f σ = D. Therefore, f ∈ Θ f σ = Θ f since Θ is adequate.

8 DependencyExample 7 .

 87 app x y → x y f x y → app ( f x ) y XX:Pairs Termination in Dependent Type Theory Modulo Rewritingwhose dependency pairs are f x y > app (f x) y and f x y > f x, does not terminate, but there is no way to construct an infinite sequence of dependency pairs without adding an argument to the right-hand side of the second dependency pair. The rules of Example 1 have the following dependency pairs (the pairs whose left-hand side is headed by fil or fil_aux can be found in Appendix B):

Figure 2

 2 Figure 2 Restricted type systems f l and ≺f

Definition 9 (

 9 Accessible system). A well-structured system R is accessible if, for all substitutions σ and rules f l → r with Θ f = ∀ x : T , U and | x| = | l|, we have σ |= ∆ f l→r whenever Θ f : s f , Θ f ∈ s f and [ x → l]σ |= x : T . This property is not always satisfied because the subterm relation does not preserve computability in general. Indeed, if C is an undefined type constant, then C = SN. However, C ⇒ C = SN since ω = λx : C, xx ∈ SN and ωω / ∈ SN. Hence, if c is an undefined function symbol of type Θ c = (C ⇒ C) ⇒ C, then c ω ∈ C but ω / ∈ C ⇒ C . We can now state the main lemma: Lemma 10. Θ is adequate if > terminates and R is well-structured and accessible.

symbol

  Ord: TYPE symbol zero: Ord symbol suc: Ord⇒Ord symbol lim: ( Nat⇒Ord )⇒Ord symbol ordrec: A⇒( Ord⇒A⇒A )⇒(( Nat⇒Ord )⇒( Nat⇒A )⇒A )⇒Ord⇒A rule ordrec u v w zero → u rule ordrec u v w ( suc x ) → v x ( ordrec u v w x ) rule ordrec u v w ( lim f ) → w f (λn , ordrec u v w ( f n ))

  symbol Sort : TYPE symbol arrow : Sort ⇒ Sort ⇒ Sort symbol T : Sort ⇒ TYPE symbol lam : ∀ a b , ( T a ⇒ T b ) ⇒ T ( arrow a b ) symbol app : ∀ a b , T ( arrow a b ) ⇒ T a ⇒ T b rule app a b ( lam _ _ f ) x → f x 6

Figure 3

 3 Figure 3 Matrix of dependency pair C and call graph of the dependency pairs of Example 7

Example 19 (

 19 Division). m/n computes m n . symbol minus: Nat⇒Nat⇒Nat set infix 1 " -" := minus rule 0 -n → 0 rule m -0 → m rule ( s m ) -( s n ) → m -n symbol div: Nat⇒Nat⇒Nat set infix 1 " / " := div rule 0 / ( s n ) → 0 rule ( s m ) / ( s n ) → s (( m -n ) / ( s n ))

  Then, we can conclude by the first induction hypothesis. There are f l 1 . . . l k → r ∈ R and σ such that u = (rσ)t k+1 . . . t n and, for all i ∈ {1, . . . , k}, t i = l i σ. Since f t ∈ C, we have πσ |= Γ f . Since R is accessible, we get that σ |= ∆ f l→r . By condition (d), we have ∆ f l→r f l r : V π where V = ∀x k+1 : T k+1 , . . . ∀x

n : T n , U . Now, we prove that, for all Γ, t and T , if Γ f l t : T (Γ ≺f t : T resp.) and σ |= Γ, then tσ ∈ T σ , by a third induction on the structure of the derivation of Γ f l t : T Example 14 (Recursor on Brouwer ordinals).

  This precedence can be sum up in the following diagram, where symbols in the same box are equivalent:

	Set	arrow			Set,L,0	nil
	Set	El		Set,El,N,L,s	cons
	B	true		Set,N,L,+	app
	B	false		Set,El,B,N,L	len_fil
	N	0		B,Set,El,N,L	len_fil_aux
	N	s	Set,El,B,N,L,len_fil	fil
	N	+	B,Set,El,N,L,len_fil_aux	fil_aux
	Set,N	L
	and comparisons related to calls:
	s	+			s,len_fil	len_fil_aux
	cons,+	app	nil,fil_aux,app,len_fil	fil
	0,len_fil_aux,+	len_fil	fil,cons,len_fil	fil_aux
				fil,fil_aux
		app		len_fil,len_fil_aux
	cons	nil		+
	arrow El	L		0	s	true	false
	Set			N		B

Sorts refer here to the notion of sort in Pure Type Systems, not the one used in some first-order settings.

We renamed the function symbols for the sake of readability.

A. Abel. MiniAgda: integrating sized and dependent types. PAR'10.

T. Arts, J. Giesl. Termination of term rewriting using dependency pairs. TCS 236:133-178, 2000.

H. Barendregt. Lambda calculi with types. In S. Abramsky, D. M. Gabbay, T. S. E. Maibaum, editors, Handbook of logic in computer science. Volume 2. Background: computational structures, p. 117-309. Oxford University Press, 1992.

V. van Oostrom. Confluence for abstract and higher-order rewriting. PhD thesis, Vrije Universiteit Amsterdam, 1994.

V. van Oostrom. Developing developments. TCS 175(1):159-181, 1997.

D. Wahlstedt. Dependent type theory with first-order parameterized data types and wellfounded recursion. PhD thesis, Chalmers University of Technology, 2007.

Acknowledgments. The authors thank the anonymous referees for their comments, which have improved the quality of this article.

(Γ ≺f t : T resp.), as in the proof of Lemma 5 except for (fun) replaced by (fun ≺f ) in one case, and (const) and (dp) in the other case. (fun ≺f ) We have g ∈ Θ g by the first induction hypothesis on g. (const) Since g is undefined, it is neutral and normal. Therefore, it belongs to every computability predicate and in particular to Θ g σ . (dp) By the third induction hypothesis, y i γσ ∈ U i γ σ . By Lemma 4e, U i γ σ = U i γσ .

So, γσ |= Σ and g yγσ ∈ C. Now, by condition (c), g yγσ <f lσ since g yγ < f l. Therefore, by the second induction hypothesis, g yγσ ∈ V γ σ . So, rσ ∈ V π σ and, by Lemma 4d, u ∈ U [xn →tn,..,x k+1 →t k+1 ,πσ] = U θ .

Note that the proof still works if one replaces the relation of Definition 8 by any well-founded quasi-order such that f g whenever f l > g m. The quasi-order of Definition 8, defined syntactically, relieves the user of the burden of providing one and is sufficient in every practical case met by the authors. However it is possible to construct ad-hoc systems which require a quasi-order richer than the one presented here.

By combining the previous lemma and the Adequacy lemma (the identity substitution is computable), we get the main result of the paper: Theorem 11. The relation → = → β ∪ → R terminates on terms typable in λΠ/R if → is locally confluent and preserves typing, R is well-structured and accessible, and > terminates.

For the sake of completeness, we are now going to give sufficient conditions for accessibility and termination of > to hold, but one could imagine many other criteria.

Checking accessibility

In this section, we give a simple condition to ensure accessibility and some hints on how to modify the interpretation when this condition is not satisfied.

As seen with the definition of accessibility, the main problem is to deal with subterms of higher-order type. A simple condition is to require higher-order variables to be direct subterms of the left-hand side, a condition called plain function-passing (PFP) in [START_REF] Kusakari | Enhancing dependency pair method using strong computability in simply-typed term rewriting systems[END_REF], and satisfied by Example 1.

Definition 12 (PFP systems)

∈ K ∪ {KIND} and, for all y : T ∈ ∆ f l→r , there is i such that y = l i and T = T i [ x → l], or else y ∈ FV(l i ) and T = D t with D undefined and | t| = ar(D).

Lemma 13. PFP systems are accessible.

Following Definition 9, assume that Θ f : s f , Θ f ∈ D and πσ |= Γ. We have to prove that, for all (y :

Suppose y ∈ FV(l i ) and T is of the form C t with | t| = ar(C). Then, T σ = SN and yσ ∈ SN since l i σ ∈ T i σ ⊆ SN.

But many accessible systems are not PFP. They can be proved accessible by changing the interpretation of type constants (a complete development is left for future work).

A Proofs of lemmas on the interpretation

A.1 Definition of the interpretation

Lemma 20. F is monotone wrt inclusion.

Proof. We first prove that D is monotone. Let I ⊆ J and T ∈ D(I). We have to show that T ∈ D(J). To this end, we have to prove (1) T ∈ SN and (2) if T → * (x : A)B then A ∈ dom(J) and, for all a ∈ J(A), B[x → a] ∈ dom(J):

1. Since T ∈ D(I), we have T ∈ SN. We now prove that F is monotone. Let I ⊆ J and T ∈ D(I). We have to show that

Since

A.2 Computability predicates

Therefore, tx ∈ SN, and t ∈ SN. 2. Let t ∈ R and t such that t → t . We have to prove that t ∈ R. Let a ∈ P . We have to prove that t a ∈ Q(a). By definition, ta ∈ Q(a) and ta → t a. Since Q(a) ∈ P, t a ∈ Q(a). 3. Let t be a neutral term such that →(t) ⊆ R. We have to prove that t ∈ R. Hence, we take a ∈ P and prove that ta ∈ Q(a). Since P ∈ P, we have a ∈ SN and → * (a) ⊆ P . We now prove that, for all b ∈ → * (a), tb ∈ Q(a), by induction on →. Since t is neutral, tb is neutral too and it suffices to prove that →(tb

A.3 Invariance by reduction

We now prove that the interpretation is invariant by reduction. Since (x : A)B is typable, A is of type TYPE and A / ∈ K ∪ {KIND}. Hence, A σ = I(Aσ) and, by Lemma 24, I(Aσ) = I(Aσ↓).

Since (x : A)B is typable and not a kind, B is of type TYPE and B / ∈ K ∪ {KIND}. Hence,

Therefore, (x :

Note that, by iterating this lemma, we get that v ∈ ∀ x : T , U iff, for all t such that [

B Termination proof of Example 1

Here is the comprehensive list of dependency pairs in the example: ( s p ) + q > p + q D: app a _ ( cons _ x p l ) q m > p + q E: app a _ ( cons _ x p l ) q m > app a p l q m F:len_fil a f _ ( cons _ x p l ) > len_fil_aux ( f x ) a f p l G:len_fil a f _ ( app _ p l q m ) > A,B=(

Which leads to the matrices labeling a loop in the transitive closure:

It would be useless to compute matrices labeling edges which are not in a strongly connected component of the call-graph (like S×R), but it is necessary to compute all the products which could label a loop, especially to verify that all loop-labeling matrices are idempotent, which is indeed the case here. We now check that this system is well-structured. For each rule f l → r, we take the environment ∆ f l→r made of all the variables of r with the following types: a:Set, b:Set, p:N, q:N, x:El a, l:L a p, m:L a q, f:El a⇒ B.


Matthieu Hog

Neus Sabater

Christine Guillemot

LONG SHORT TERM MEMORY NETWORKS FOR LIGHT FIELD VIEW SYNTHESIS

Keywords: Light Field, View Synthesis, Deep Learning

Because light field devices have a limited angular resolution, artificially reconstructing intermediate views is an interesting task. In this work, we propose a novel way to solve this problem using deep learning. In particular, the use of Long Short Term Memory Networks on a plane sweep volume is proposed. The approach has the advantage of having very few parameters and can be run on sequences with arbitrary length. We show that our approach yields results that are competitive with the state-of-the-art for dense light fields. Experimental results also show promising results with light fields with wider baselines.

INTRODUCTION

Real light fields capturing devices exhibit different spatial and angular trade-offs. Plenoptic cameras trade spatial resolution against angular resolution, whereas camera arrays can only capture a limited set of views. Both depth image-based rendering (DIBR) and deep learning approaches have been proposed to increase angular resolution via view synthesis.

In classical DIBR approaches, scene depth is first estimated and used to warp and combine the input views. This has been done using user-defined image labeling [START_REF] Chaurasia | Silhouette-aware warping for image-based rendering[END_REF] or superpixels [START_REF] Chaurasia | Depth synthesis and local warps for plausible image-based navigation[END_REF]. However, methods relying on a hard depth prior to render an image [START_REF] Mcmillan | Plenoptic modeling: An image-based rendering system[END_REF][START_REF] Steven J Gortler | The lumigraph[END_REF][START_REF] Buehler | Unstructured lumigraph rendering[END_REF] have the problem that faulty depth estimation yields very unpleasant artifacts in the rendered image. Other methods focus on formulating view synthesis as a maximum a posteriori estimation [START_REF] Wanner | Variational light field analysis for disparity estimation and superresolution[END_REF][START_REF] Sergi Pujades | Bayesian view synthesis and image-based rendering principles[END_REF]. A more recent approach [START_REF] Penner | Soft 3d reconstruction for view synthesis[END_REF] proposes to propagate depth uncertainties from depth estimation to image rendering. The results are numerically and visually superior to prior methods but it has some serious computational and memory issues.

In the last few years, deep learning approaches have been proposed for view synthesis. The authors in [START_REF] Flynn | Deepstereo: Learning to predict new views from the world's imagery[END_REF] propose a deep learning approach for light fields view synthesis. A Plane Sweep Volume (PSV), i.e. a set of views warped with disparities in a given range, is used as input of two twin networks towers with shared weights. The first network learns masks on each slice of the PSV, selecting zones that correspond to actual points in the scene. The second network learns the most probable color at a given point. The final image is rendered, as the linear combination of the two networks. Although the results are visually stunning and work perfectly for sparsely sampled views, the major problem of this approach is its complexity and the number of parameters. Because of this, the authors in [START_REF] Khademi Kalantari | Learning-Based View Synthesis for Light Field Cameras[END_REF] propose an approach tailored for narrow baseline light fields captured with plenoptic cameras. In this approach, the mean and variance of each slice of the PSV are fed to a first CNN, that learns a disparity on the synthetic view coordinate system. The corner images are then warped using the disparity and concatenated with the depth plus the new view index and passed into a second CNN that learns to refine and combine the warped corner images. The approach gives very good results on Lytro images, however the PSV is rather dense (100 slices), yielding a lot of operations on the first layers of the network. Besides, the network is trained for a fixed amount of slices and, as in [START_REF] Flynn | Deepstereo: Learning to predict new views from the world's imagery[END_REF], it requires to load the entire network at once for the forward pass. This idea of light field angular super-resolution has recently been improved (eg. using microlens images [START_REF] Shahzeb | Spatial and angular resolution enhancement of light fields using convolutional neural networks[END_REF]), but with similar limitations.

In addition to the very high number of parameters which is an issue for computationally and memory limited devices, all current architectures are, by design, bound to only one disparity range. The features trained for a given device cannot be re-used for devices with different baselines. To solve these problems, in this paper we propose to use Recurrent Neural Networks (RNNs), and in particular Long Short Term Memory (LSTM) RNNs, to directly learn view synthesis from a PSV in a modular fashion with low complexity.

RNNs are neural networks in which instead of statically chaining layers, recurrent connections are made between the so-called cells with the particularity that all cells share its parameters. Each cell takes as input the output of the previous cell and a different element of a sequence and outputs a value and provides some information to the next cell. Such network structure has several advantages. First and foremost the number of parameters is very small compared with CNNs, since the cells have the same weights. Second, by changing the number of cells, the RNN can be used with different sequence lengths. Also, the recurrent loop can be run sequentially during the forward pass, making the GPU memory requirement a lot smaller than a conventional CNN.

We show that our approach can produce images of comparable quality with state-of-the-art methods with significantly lower number of weights. As an interesting byproduct, we also show that RNNs somehow learn differently than CNNs for view synthesis. Indeed, while a single CNN usually gives blurred results when used for view synthesis, the proposed approach does not suffer significantly from this defect. While the approach is assessed with dense light fields, we show that the approach can be extended to wider baselines.

LSTMS FOR VIEW SYNTHESIS

LSTMs [START_REF] Hochreiter | Long shortterm memory[END_REF] networks are a variation of RNNs where each cell has a memory, a state, that is updated across the RNN loop. This is to help the propagation of information across RNN iterations. It also solves the problem of vanishing gradients [START_REF] Hochreiter | Gradient flow in recurrent nets: the difficulty of learning long-term dependencies[END_REF]. Classical LSTMs are made of 3 parts, composed of neural layers activated by a sigmoid function, called gates.

In particular, we denote C the cell memory, h the cell output. Because LSTMs are typically used to process temporal sequences (e.g. text, sound), a RNN cell is run on temporal steps noted t. The cell state is updated from C t-1 to C t by removing information (with a point-wise multiplication), then by adding new information (with an addition step). This is done with an input gate σ i , that filters relevant information in the previous cell output and the current input, an update layer T anh u and gate σ u , that computes and selects the update to be done to the cell state, and finally an output gate σ o to select relevant feature to pass in the RNN loop. Specifically, because we are dealing with images, we use convolutional LSTMs [START_REF] Shi Xingjian | Convolutional lstm network: A machine learning approach for precipitation nowcasting[END_REF], a variant of LSTMs that replaces the matrix multiplication done at each layer with convolutions, making the LSTMs cell effectively capturing both spatial and sequence information.

The main idea behind our proposal is that, instead of establishing links in the z-dimension of the PSV via a single, or multiple layers, we learn how to do it with a RNN. Fig. 1 offers a comprehensive overview of our approach. In particular, we try to learn directly the image to synthesize Îd from the PSV, without any depth or selection map estimation. Each LSTM cell takes as input the 4 corner views warped with a depth plane d and concatenated along the color dimension (the depth of the input is then 12). In other words, we treat the depth dimension of the PSV as a temporal dimension for LSTMs traditional approaches. As in other learning methods [START_REF] Khademi Kalantari | Learning-Based View Synthesis for Light Field Cameras[END_REF][START_REF] Flynn | Deepstereo: Learning to predict new views from the world's imagery[END_REF] a groundtruth view is used to evaluate the model prediction and update the learned filter.

In our approach, the cell memory is used to encode the most probable color for each pixel of the new view. One could expect the LSTM to behave as follows. The input and update gates σ i and σ u will select the most relevant color features from the previous cell output and from the current PSV slice. The update gate σ u will deduce, from the previous RNN iterations and the current PSV slice color values what color features are unlikely to compose the true new view colors. The update gate and layer σ u and T anh u will then compute the

σ i σ u T anh u σ o × + × × Tanh C d-δ d Prev. State h d-δ d Prev. Output I d Warped view C d New State h d New Output ReLU ReLU ReLU ReLU ReLU σ d Îd

Synthetic view

Fig. 1: The LSTM cell used in our approach. Each cell takes as input the 4 corner views warped at a specific depth plane d.

It embeds a small CNN to learn features on each slice of the PSV that are later concatenated with the input. At the very last RNN iteration, we pass the cell state into a single layer (in gray) to generate the final image Îd .

new color features to save, presumably because they are more likely. After the new cell memory state is updated, the output gate σ o will filter out the color features that are important to pass on to the next cell. We use a fixed kernel size of 3 × 3 for all the gates and a feature size of 32. Using fewer filters has a negative impact on the approach performance and interestingly, adding more as well. On the very last RNN iteration, we pass the state of the cell through a simple convolutional layer σ d with a kernel size of 1 × 1 and depth of 3 in order to decode the learned features into the final image. Interestingly, we have noticed that using a deeper decoding step provides drastically worse results. Since the gates of the LSTM are composed of only one layer, the learnt filters and update function are rather limited. In order to learn more complex representations of each slice of the PSV, we use a small CNN. In contrast to what has been done in the past [START_REF] Luo | Efficient deep learning for stereo matching[END_REF], we learn the features on the set of 4 views and not on each view independently. Equally, we do not replace the cell input with the learned features but concatenate them. This is to introduce more context in-between views rather than simple image features, but without replacing the input signal, and in practice, we find out that it improves significantly the results justifying the added parameters. The used network is a simple CNN composed of 5 layers of 32features with a kernel size of 3×3. We perform the RNN loop warping the views from foreground to background (as in the rendering step of [START_REF] Penner | Soft 3d reconstruction for view synthesis[END_REF]). Note that reversing the order provides a significantly worse result. Using a bi-directional scheme, as in [START_REF] Schuster | Bidirectional recurrent neural networks[END_REF], does not improve the results but also gives slightly worse results. We hypothesize this is due to the way the network deals with occlusions, performing an operation akin to z-clipping in the LSTM loop.

Because it has been shown to provide sharper image re-

EXPERIMENTS

We follow the training protocol proposed in [START_REF] Khademi Kalantari | Learning-Based View Synthesis for Light Field Cameras[END_REF]. That is to say, we use Lytro Illum subaperture images as training input and groundtruth. The central 7 × 7 views are extracted from the microlens images, as they do not suffer from vignetting and chromatic aberrations. The PSV is rendered for each integer disparity in the range [-12, 12] for the central view. The groundtruth central view is used as a reference to compute the loss and the test metrics. In order to avoid color and optical aberrations that are specific to each camera, we augment the dataset of [START_REF] Khademi Kalantari | Learning-Based View Synthesis for Light Field Cameras[END_REF] with 3 other Lytro Illum datasets [START_REF] Shah | Stanford lytro light field archive[END_REF][START_REF] Rerabek | New light field image dataset[END_REF][START_REF] Guillemot | Inria lytro illum light field dataset[END_REF]. The network is trained using ADAM [START_REF] Diederik | Adam: A method for stochastic optimization[END_REF], with a learning rate of 0.0003, and for 200K iterations. We use a batch size of 10 and as in [START_REF] Khademi Kalantari | Learning-Based View Synthesis for Light Field Cameras[END_REF], we train our network on patches of size 128 × 128. We do not use batch norm and do not crop the final images borders, neither during training nor during testing. Tensorflow implementation of dynamic RNNs is used for training with our custom cell. The overall training time is slightly less than 2 days, although the results do not change much after 100K iterations. Note that we refer to our supplementary material1 for extra details that could not fit in the paper. Model Validation: In order to verify that the network learns as expected we employ the following strategy. We manually unroll the RNN loop and apply the decoding layer σ d of the last iteration to the cell memory state at each iteration. Although it is not strictly what the LSTM memory saves, this technique gives us a visualization of what is happening from an iteration to another. On Fig. 2, we clearly see that zones that have been in focus in the previous iterations adopt their final color, overwriting the previous features, at a current time step. This is done independently at each scene depth plane, In (c&d) we observe that our approach suffer less at objects boundaries. However, as shown in (e&f), our approach is subjects to color bleeding artifacts is some areas.

showing that our LSTM strategies do indeed learn features about the best color its has seen so far. This result is consistent across the entire test set. Also, we observe a correlation between the artifacts in the selection done at each step and artifacts in the final image. These artifacts mostly occur at the edge of objects (as in the third slice of Fig. 2) and usually yield blurred borders in the final image. Quantitative Comparisons: The implementation of [START_REF] Khademi Kalantari | Learning-Based View Synthesis for Light Field Cameras[END_REF] (done by its authors) is used as a baseline to evaluate our method. We also use their test set composed of 30 Lytro Illum images. Note that, as in their experiments, the interpolation and metrics are computed on the input under-exposed images, but gamma-corrected images are shown. For the sake of comparison, we also re-implemented and re-trained the frame interpolation method in [START_REF] Joost Van Amersfoort | Frame interpolation with multi-scale deep loss functions and generative adversarial networks[END_REF] adapting slightly for the view synthesis case. This method uses a deep, hierarchical network, estimating an optical flow residual at 3 different scales. Details about the modifications can be found in the supplementary. We compare the three approaches for all the images of the test set of [START_REF] Khademi Kalantari | Learning-Based View Synthesis for Light Field Cameras[END_REF]. We note that our approach is at least on par with [START_REF] Khademi Kalantari | Learning-Based View Synthesis for Light Field Cameras[END_REF], with an average PSNR of 38 vs 37.2 for [START_REF] Khademi Kalantari | Learning-Based View Synthesis for Light Field Cameras[END_REF] and 34.5 for [START_REF] Joost Van Amersfoort | Frame interpolation with multi-scale deep loss functions and generative adversarial networks[END_REF]. Our approach performs worse than [START_REF] Khademi Kalantari | Learning-Based View Synthesis for Light Field Cameras[END_REF], but better than [START_REF] Joost Van Amersfoort | Frame interpolation with multi-scale deep loss functions and generative adversarial networks[END_REF] in terms of MSE and SSIM. Tab. 1 shows the results for the examples in [START_REF] Khademi Kalantari | Learning-Based View Synthesis for Light Field Cameras[END_REF] and the average for the entire dataset. The full table of results is included in the supplementary. The main reason why the two full-resolution images are numerically and visually better than the hierarchical is that they rely on full-resolution images for the entire pipeline. Small details are not well captured in the depth estimation, and are not recovered during the upper scale depth estimation either, since the depth estimation is hierarchical. We show an example of this in the supplementary material. Visually, it is hard to distinguish the results from the two approaches. We show a visual comparison in Fig. 3, note that in [START_REF] Khademi Kalantari | Learning-Based View Synthesis for Light Field Cameras[END_REF], an important portion of the image is cropped. For both approaches, most of the error is contained in the objects boundaries. Our approach suffers slightly less from these artifacts (e.g. with the foreground leaf) but can sometimes introduce slight color bleeding, in some objects (e.g. the purple flower petal on the white wall). This could be explained by the fact that our network has to reconstruct colors, while [START_REF] Khademi Kalantari | Learning-Based View Synthesis for Light Field Cameras[END_REF] warps the input textures. In terms of parameters, [START_REF] Khademi Kalantari | Learning-Based View Synthesis for Light Field Cameras[END_REF] has 1 644 204 while ours only has 114 400.

Towards variable baseline view synthesis: as stated in the introduction, one of the interest of LSTMs is that they can be used on sequences with variable length. As a last experiment, we test how generalizable is the network trained on small disparities to a wide disparity setup. We use the Beergarten sequence in [START_REF] Dabala | Efficient Multi-image Correspondences for On-line Light Field Video Processing[END_REF], as it is close to a Lytro sequence (i.e. a rectified light field with the same vertical and horizon-tal baseline). The PSV is composed of 43 slices against 25 for the Lytro case. On Fig. 4 we notice that the results are not as good as for the densely sampled dataset, but the network exhibits the same behavior at each iteration, even if it has not trained for this kind of data.

CONCLUSION

Our experiments suggest that RNNs with the proposed architecture are suitable for view synthesis. Not only they provide synthetic views with competitive quality with the state-of-theart, but also with a reduced number of parameters. However, our experiments focused on generating the central view. Since the input of the method is a PSV, we do not expect the results of a training on arbitrary views, done for instance by inputting the PSV warped in the new view coordinate system and concatenated with normalized view index, to be drastically significant. We also show that the approach can be used with light fields with wider baselines despite not being trained explicitly with this particular data. We believe that a LSTM network trained with a dataset composed of both sparse and dense corner views would be able to perform well on arbitrary baselines.

They are numerous improvements that can be brought to this method. First, the use of deeper gates (i.e. gates with more than one layer) would allow the LSTM cells to learn more complex representation about the best synthetic view color. This might be necessary to extend the approach to wider baselines and multi-view rendering. Another improvement could be to follow classical approaches and decompose the problem of view synthesis by learning depth. We could imagine for instance passing the normalized disparity plane as an extra channel in the cell input and instead of learning features about the most probable color, let the network infer the most probable depth of each pixel of the view to synthesize. The output would then be a disparity map and possibly interpolation weights as in [START_REF] Joost Van Amersfoort | Frame interpolation with multi-scale deep loss functions and generative adversarial networks[END_REF], used to generate the final image. This would allow keeping a level of disparity range genericity in contrast to the refinement network in [START_REF] Khademi Kalantari | Learning-Based View Synthesis for Light Field Cameras[END_REF].

Fig. 2 :

 2 Fig. 2: Visualization of the LSTM state at different RNN iterations (to be read from left to right). On top we show the decoded memory state of the LSTM, on the bottom, we display the refocused 4 input views to see what depth plane is currently valid.

Fig. 3 :

 3 Fig. 3: Comparison with [10]. (a&b) show the entire image.In (c&d) we observe that our approach suffer less at objects boundaries. However, as shown in (e&f), our approach is subjects to color bleeding artifacts is some areas.

Fig. 4 :

 4 Fig. 4: Visualization of the LSTM memory state for a wide baseline dataset.

Table 1 :

 1 Image quality metrics for the compared approaches Flower1 31.36 0.97 34.21 0.97 33.43 0.97 Flower2 31.43 0.97 33.26 0.97 32.11 0.96 Rock 31.54 0.96 33.88 0.98 35.63 0.97 Seahorse 31.75 0.96 32.80 0.95 31.62 0.97 Average 34.51 0.96 38.03 0.96 37.18 0.97

	Dataset	[22]	LSTM	[10]
		PSNR SSIM PSNR SSIM PSNR SSIM
	Cars	32.87 0.96 30.24 0.97 31.93 0.97

http://www.irisa.fr/temics/demos/ LSTMViewSynthesis/index.html (a) Synthetic view [10] (b) Synthetic view LSTM (c) Leaf [10] (d) Leaf LSTM (e) Petal [10] (f) Petal LSTM


Jean Bégaint

Franck Galpin

Philippe Guillotel

Christine Guillemot

Technicolor

Deep frame interpolation for video compression

Deep neural networks have been recently proposed to solve video interpolation tasks. Given a past and future frame, such networks can be trained to successfully predict the intermediate frame(s). In the context of video compression, these architectures could be useful as an additional inter-prediction mode. Current inter-prediction methods rely on block-matching techniques to estimate the motion between consecutive frames. This approach has severe limitations for handling complex non-translational motions, and is still limited to block-based motion vectors. This paper presents a deep frame interpolation network for video compression aiming at solving the previous limitations, i.e. able to cope with all types of geometrical deformations by providing a dense motion compensation. Experiments with the classical bi-directional hierarchical video coding structure demonstrate the efficiency of the proposed approach over the traditional tools of the HEVC codec.

Introduction

Inter-prediction is crucial to efficiently compress video content. By capturing temporal redundancies between consecutive frames, inter-prediction methods are able to generate accurate predictions of the frames to encode. The motion between frames is traditionally estimated and compensated via block-based translational motion vectors. To correct local inaccuracies, a residue may then be added to the prediction. Inter-prediction methods can use past and future frames to predict current frames, which is known as bi-directional prediction. This bi-directional prediction is generally used in a hierarchical manner to encode a group of pictures (GOP).

Video frame interpolation is used to generate intermediate frames between two consecutive input frames. Recently, several works have demonstrated improvements in solving frame interpolation tasks by using deep neural networks [START_REF] Liu | Video frame synthesis using deep voxel flow[END_REF][START_REF] Niklaus | Video frame interpolation via adaptive separable convolution[END_REF][START_REF] Niklaus | Context-aware synthesis for video frame interpolation[END_REF][START_REF] Jiang | Super slomo: High quality estimation of multiple intermediate frames for video interpolation[END_REF]. These approaches usually estimate an optical flow, i.e. a per pixel translational displacement, then warp and blend the original input frames to generate the interpolated frame. Video frame interpolation thus shares some characteristics with inter-prediction methods. In the context of video compression, such deep architectures could be useful as an additional inter-prediction technique. Indeed these deep learning approaches are able to estimate the motion between frames in a spatially coherent manner, at the pixel level, which leads to good interpolation results. Moreover, these methods benefit from the fact that no motion information need to be transmitted to the decoder.

This paper introduces a novel inter-prediction method for video compression based on deep frame interpolation networks. For each frame that can be coded with bidirectional inter-prediction from past and future frames, an additional reference frame is provided by interpolating the original reference frames. The method was integrated within the HEVC video codec [START_REF] Sullivan | Overview of the high efficiency video coding (HEVC) standard[END_REF]. BD-rates improvements are measured using the Common Test Condition (CTC) sequences [START_REF] Bossen | Common test conditions and software reference configurations[END_REF].

Related Work

Video frame interpolation algorithms have benefited from recent advances with deep neural networks. Several deep architectures have been proposed in the last few years [START_REF] Mathieu | Deep multi-scale video prediction beyond mean square error[END_REF][START_REF] Van Amersfoort | Transformation-based models of video sequences[END_REF][START_REF] Liu | Video frame synthesis using deep voxel flow[END_REF][START_REF] Niklaus | Video frame interpolation via adaptive separable convolution[END_REF][START_REF] Niklaus | Context-aware synthesis for video frame interpolation[END_REF][START_REF] Jiang | Super slomo: High quality estimation of multiple intermediate frames for video interpolation[END_REF], constantly improving the quality of the interpolation results. These networks usually operate in two stages. First a kind of motion estimation is performed, such as optical flow, then the frame is interpolated from the reference input frames and the estimated motion.

Liu et al. [START_REF] Liu | Video frame synthesis using deep voxel flow[END_REF] were the first to introduce an architecture with an unsupervised learning of the optical flow. Similarly to the classical fully convolutional approaches, their Deep Voxel Flow (DVF) network is trained end-to-end to interpolate an intermediate frame from two consecutive input frames. However, the last layer of the network is a non-trainable interpolation function interpolating the previous layers output and the input frames. The loss function is computed directly as the l1-norm between the interpolated frame and the ground truth. The network thus learns by itself to estimate a kind of optical flow and a temporal mask for the trilinear interpolation layer. The network outputs a voxel flow which represents the per pixel displacement (dx, dy) and a temporal mask dt weighting the trilinear blending.

Niklaus et al. proposed in [START_REF] Niklaus | Video frame interpolation via adaptive convolution[END_REF] an adaptive convolution approach to video frame interpolation (AdaConv ). Instead of relying on a two-steps approach, i.e. first a motion estimation then a pixel synthesis, the authors proposed to implement the pixel synthesis as a convolution over the two input frames. They trained a deep neural network to predict a per pixel spatially adaptive convolution kernel. Thus for each pixel, parameters for a 2D convolutional kernel are predicted, then the input frames are convolved at the current pixel location to predict its interpolated value. Their method is able to handle occlusions, blur and brightness change. However the large kernel to be estimated for each pixel is computationally expensive, as they need a 51 × 51 pixel kernel to handle large motions. This drawback is addressed in their following work [START_REF] Niklaus | Video frame interpolation via adaptive separable convolution[END_REF] in which they introduced separable convolutions (SepConv ) using 1D kernels for faster processing.

In the image compression domain, several deep learning approaches have also been recently proposed [START_REF] Toderici | Full resolution image compression with recurrent neural networks[END_REF][START_REF] Rippel | Real-time adaptive image compression[END_REF][START_REF] Ballé | Variational image compression with a scale hyperprior[END_REF][START_REF] Agustsson | Generative adversarial networks for extreme learned image compression[END_REF]. Current performances already exceed classical image codecs like JPEG [START_REF] Wallace | The JPEG still picture compression standard[END_REF] and JPEG2000 [START_REF] Skodras | The jpeg2000 still image compression standard[END_REF], and can reach state-of-the-art codecs such as HEVC [START_REF] Sullivan | Overview of the high efficiency video coding (HEVC) standard[END_REF] (PSNR). Fewer works have been published on video compression. Han et al. [START_REF] Han | Deep probabilistic video compression[END_REF] proposed an end-to-end trainable video codec based on a variational auto-encoder which incorporates both global and per frame latent variables to capture temporal redundancies. Wu et al. introduced in [START_REF] Chao-Yuan | Video compression through image interpolation[END_REF] an end-to-end architecture based on an image interpolation network to exploit temporal redundancies. A compressed residual information is also learned jointly to correct interpolation inaccuracies.

Similarly, this paper builds upon existing deep frame interpolation methods to target video compression applications. However, the frame interpolation method is introduced here within the classical hybrid video codec architecture, which allows to take advantage of the efficient residual coding and entropy signaling of HEVC.

Coding scheme

To test deep frame interpolation networks in a video compression context, the HEVC HM reference software [START_REF] Bossen | Common test conditions and software reference configurations[END_REF] was modified. For each frame hierarchically coded in the GOP, an extra reference frame, interpolated by the network, is appended to the default reference frames list and can be selected as reference by the rate-distortion optimization process. This new GOP structure is represented in Figure 1. For example, the B1 frame can be predicted with the interpolated reference from the I and B0 frames, in addition to the default HEVC reference frames. Using extra reference frames has two advantages over fully implementing a new inter-prediction mode in HEVC. First, the design change on the legacy decoder is relatively straightforward, but mostly it allows the encoder to use additional interprediction modes from the interpolated reference. Although the best configuration would be to only have blocks with SKIP mode as prediction mode (only motion vector predictions, no residual), MERGE or even INTER from the interpolated frames can still be beneficial compared to a prediction from the default reference frames. To support the use of extra reference frames, several flags need to be inserted into the bitstream. The decoder will then re-interpolate the selected frames when needed, and thus needs to know if an extra reference frame was used as prediction or not for each coded block.

At the frame level, a flag is first set to signal the use or not of the extra reference frames. At the Prediction Unit (PU) level, an integer is added to the motion vector information to store the use of the selected extra reference frame. The sentinel value 0 is set as a signaling method to inform the decoder that no extra reference frames are used for the current PU. The interpolated frame flag is entropy coded with CABAC [START_REF] Marpe | Context-based adaptive binary arithmetic coding in the h. 264/avc video compression standard[END_REF] in order to reduce the syntax size. A CABAC context is also determined from the top and left PU blocks, if they are available for the current block. It should be noted that no specific study was performed on the CABAC context or its initialization, study that would be beneficial once more statistics about the proposed method are obtained.

Experimental results

The coding experiments are performed on the common test sequences [START_REF] Bossen | Common test conditions and software reference configurations[END_REF]. The HEVC HM software version 16.16 was used for all the experiments. The rate-distortion performance are computed with the Bjontegaard metric [START_REF] Bjontegaard | Calculation of average psnr differences between rd-curves[END_REF] using the common 22, 27, 32, 37 Quantization Parameter (QP). Unless specified otherwise, the PSNR is reported for the Y channel only. The default HM random access configuration mode [START_REF] Bossen | Common test conditions and software reference configurations[END_REF] is used as a baseline for the following tests. The default fixed GOP size of 16 is used. Experiments are run with sequences of the classes B, C and D of the CTC [START_REF] Bossen | Common test conditions and software reference configurations[END_REF], affine sequences class [START_REF] Chen | Affine SKIP and MERGE modes for video coding[END_REF] and the legacy Foreman sequence. HEVC is used as the baseline reference. Experiments were conducted with the SepConv approach [START_REF] Niklaus | Video frame interpolation via adaptive separable convolution[END_REF], respectively trained with a l1-norm (SepConv-l1 ) and a perceptual loss (SepConv-lf ), the Deep Voxel Flow (DVF) approach [START_REF] Liu | Video frame synthesis using deep voxel flow[END_REF]. A non deep learning approach, Celiu Flow [START_REF] Liu | Beyond pixels: exploring new representations and applications for motion analysis[END_REF] is used as an additional baseline to measure the effect on using a dense optical flow at the encoder and decoder, compared to the traditional block-based motion compensation.

BD-rate results

The BD-rate results are reported in ??. First, one can note that all the experiments bring improvements over the HEVC codec. The best performances are obtained for the SepConv-l1 method with a mean BD-rate reduction of -2.46%, compared to -2.38% for the SepConv-lf network, -0.09% for DVF and -0.89% for the CeliuFow method.

The SepConv-l1 method outperforms the other methods. This network was specifically trained with the l1-norm, which minimizes the interpolation error energy, explaining the greater average performance of -0.08% over the SepConv-lf network. The l1-norm is often preferred over the l2-norm, as it has been repeatedly shown that it leads to less blurry results [START_REF] Mathieu | Deep multi-scale video prediction beyond mean square error[END_REF]. Surprisingly, the SepConv-lf performs better on three of the sequences, and although it was trained with a perceptual norm the performance loss compared to the one trained with the l1-norm is relatively small. Both SepConv approaches outperform the classical optical flow approach by -1.45%. However the Deep Voxel Flow network has the worst bit-rate distortion performances, with a mean gain of -0.09%. Some values could also not be reported due to memory limitations in the published implementation. It is also important to note that the deep architectures were trained on RGB images, whereas HEVC encodes YCbCr frames with a spatial 4:2:0 sampling. The input frames need to be up-sampled (chroma wise) and converted to RGB before being processed by the network, the inverse operation is performed before the HEVC encoding. There is some loss of information during these conversions. Training the networks to process YCbCr 4:2:0 frames should lead to better results. Affine sequences benefit less from the interpolation methods as they mostly display large global scene motions (due to camera zooms or shakes for example). Such motions are more difficult to estimate for these methods, as they were designed and trained for small local motions estimation. An average bit-rate reduction of -0.84% is obtained while homography models based on local descriptors have already been demonstrated to have superior gains, up to -3.31% [START_REF] Parker | Global and locally adaptive warped motion compensation in video compression[END_REF][START_REF] Begaint | Regionbased models for motion compensation in video compression[END_REF]. It would be interesting to investigate recently proposed deep architectures designed for homography estimation [START_REF] Daniel Detone | Deep image homography estimation[END_REF][START_REF] Erlik Nowruzi | Homography estimation from image pairs with hierarchical convolutional networks[END_REF].

Cost of signaling

To signal the use of the extra interpolated reference frame, a flag is set at the frame level and the PU level. In order to evaluate the cost of the signaling, we performed the same experiments but disabled the flag coding at the PU level and the global flag at the frame level. Results are reported in Table 2 on the CTC sequences. Without signaling, increased performance gains are obtained, with respective improvements of -0.22%, -0.29%, -0.38 % and -0.18% for classes B, C, D and affine. This demonstrates that our current CABAC coding of the flags does not add up to a significant part of the gains, although the flag signaling could still be optimized for greater bit-rate reductions.

The highest bit-rate reduction, -7.36%, is obtained on the "Cactus" sequence with the SepConv-l1 network, which can be explained by the large number of small object motions in this sequence. Estimating and compensating efficiently these small local motions require indeed a lot of syntax signaling (quad-tree splitting, motion vectors information, residual). This costly prediction is avoided by interpolating directly the intermediate blocks with the proposed approach. Figure 2 shows, for some frames of the "Cactus" sequence, the blocks for which the reference interpolated by the deep Table 3: Comparison of the mean interpolation times for each method, on the three classes of the CTC sequences [START_REF] Bossen | Common test conditions and software reference configurations[END_REF]. When the frame distance between the reference frames is smaller, the network prediction is more accurate and more blocks are encoded with the proposed method. As such the traditional hierarchical coding structure might not benefit best the proposed interpolation method, as a frame distance of 8 or 4 frames is challenging for the currently implemented networks.

Qualitative results

Qualitative results are presented in Table 4. Interpolated frames are computed for different distances in a group of pictures. This section provides visual results for interpolations obtained for possible GOP distances between reference frames: 2 and 8. Results are shown for four sequences of the test set: "BQSquare", "Cactus", "BasketBallPass", and "LakeWalking".

One may note that small local motions are well interpolated, for example the people walking in "BQSquare", the objects rotating in "Cactus" and the players and their ball in "BasketBallPass". The interpolation methods perform better for small GOP distances [START_REF] Liu | Video frame synthesis using deep voxel flow[END_REF][START_REF] Niklaus | Video frame interpolation via adaptive separable convolution[END_REF], indeed when the GOP distance between reference frames is too large, blurry outputs are generated. This might be explained by the fact that distant reference frames do not have a motion field that is still locally linear, as assumed by the networks, for example the curved trajectory of the basket ball in the "BasketBallPass" sequence. Moreover both methods struggle with the "LakeWalking" sequence which displays strong scene motion due to the camera movements (the lack of padding for the CeliuFow method is also clearly visible), and also illumination changes.

Complexity

When using deep convolutional networks in conjunction with classical coding architectures, it is difficult to provide a meaningful complexity study as some algorithms are designed to run efficiently on GPU and not on CPU. Instead the interpolation times for each methods are compared for 3 classes from the CTC test sequences (see Table 3). The experiments were run with a single core on an Intel Xeon X5650 CPU, and a Nvidia GeForce GTX 1070 GPU. The SepConv approach is at least 25 times faster than the CeliuFow method, and about 1.3 times faster that DVF. It benefits from running on a GPU, and an efficient CUDA implementation. However the network SepConv network requires 21 million parameters, which takes an approximate size of 82 mega-bytes on the disk, and a single forward pass of a 256x256 "BQSquare", "Cactus", "BasketBallPass", and "LakeWalking".

pixels patch requires around 216 mega-bytes of memory during the execution. This constitute a major drawback for practical hardware implementations of these deep neural networks. However, considering that coming integrated circuit architectures are integrating deep learning capabilities, this may be less of a problem in the coming years.

Conclusion and perspectives

This paper presented a novel inter prediction method based on a deep neural network. The efficiency of different deep architectures was demonstrated against classical methods and the latest HEVC video codec. The prediction accuracy is improved compared to traditional approaches as deep-learning architectures are able to learn a good generalization of motion estimation tasks, with both better modeling and higher spatial resolution. We see this work as a first step in leveraging deep neural networks for frame inter-prediction. The next step is to research, design and train deep interpolation networks specifically in a video compression context, i.e. within a rate distortion optimization (RDO) constraint scheme.

A lot of research remains to be performed to improve the design of deep neural networks for video compression. Networks are usually trained, and operate, on 32bit floating point values. However video codec standards rely on integer operations for the sake of reproducibility. Works have already been proposed for implementing network coefficients quantization [START_REF] Wu | Training and inference with integers in deep neural networks[END_REF], such schemes will need to be studied and adapted for video compression. The interpolation filters used by the network could also be tailored for video inter-prediction. A closer integration in the codec would bring improvements thanks to the RDO loop. Finally, the estimated motion range for these deep architectures is limited to small local motions for now, which limits the efficiency on affine sequences. Learning both a global motion and a local motion field constitutes an important perspective.

Figure 1 :

 1 Figure 1: Coding scheme: illustration for a GOP of 8 frames with the default random access configuration. The SepConv [2] network is used here as the interpolation network. The dashed lines represent the default references, the continuous line represent the extra reference from the deep interpolation. Example is shown for the B1 frame.

Figure 2 :

 2 Figure 2: Examples of references selection on the Cactus sequence at QP=22. Blocks in green are encoded from the interpolated reference by the SepConv-l1 network.

Table 1 :

 1 BD-rate performances comparison for different frame interpolation methods compared to HEVC.

	Class Sequence	SepConv-l1 SepConv-lf	DVF CeLiu Flow
		BQTerrace	-6.38%	-5.94%	-	-2.77%
		BasketballDrive	-1.43%	-1.05%	-	-0.35%
	B	Cactus	-7.36%	-7.07%	-	-4.56%
		Kimono1	-2.05%	-1.71%	-	-0.23%
		ParkScene	-2.36%	-2.14%	-	-0.41%
		BQMall	-3.44%	-2.89% -0.10%	-0.34%
	C	BasketballDrill PartyScene	-3.87% -2.53%	-3.77% -0.71% -3.08% -0.14%	-1.17% -0.37%
		RaceHorses	-1.30%	-1.01% -0.03%	-0.47%
		BQSquare	-3.31%	-5.48%	0.10%	0.06%
	D	BasketballPass BlowingBubbles	-2.93% -2.08%	-2.51% -0.13% -2.29% -0.13%	-0.34% -0.24%
		RaceHorses	-2.21%	-1.84% -0.06%	-0.29%
		CStoreGoods	-0.45%	-0.29%	-	-0.25%
		DrivingRecorder1	-1.37%	-0.93%	0.04%	-0.07%
	Affine	DrivingRecorder2 LakeWalking	-1.24% -0.08%	-1.03% 0.00%	0.01% 0.03%	-0.24% -0.05%
		ParkSunny	-1.34%	-1.34%	-	-0.82%
		ParkWalking	-0.54%	-0.32%	-	-0.03%
	Other foreman	-2.92%	-2.82%	0.08%	-0.32%
	Mean		-2.46%	-2.38% -0.09%	-0.89%

Table 2 :

 2 BD-rate results comparison with and without signaling of the extra reference use at the prediction unit level. BD-rates were measured for the SepConv-l1 network.

Table 4 :

 4 Qualitative

evaluation of the interpolation methods. Sequences (top to bottom):