Gilles Dowek
email: gilles.dowek@inria.fr

A Complete Proof Synthesis Method for the Cube of Type Systems

We present a complete proof synthesis method for the eight type systems of Barendregt's cube extended with η-conversion. Because these systems verify the proofs-as-objects paradigm, the proof synthesis method is a one level process merging unification and resolution. Then we present a variant of this method, which is incomplete but much more efficient. At last we show how to turn this algorithm into a unification algorithm.

Introduction

The Calculus of Constructions is an extension of Church higher order logic in which the terms belong to a λ-calculus with dependent types, polymorphism and type constructors. Because of the richness of the terms structure, proofs can be represented as terms through Heyting semantics and Curry-Howard isomorphism. So a proof of a proposition P is merely a term of type P .

A proof synthesis method for Church higher order logic is given in [START_REF] Huet | Constrained Resolution A Complete Method for Higher Order Logic[END_REF]. In this paper we generalize this method to find terms of a given type in the systems of Barendregt's cube (in particular in the Calculus of Constructions) extended with η-conversion. In some sense, because these type systems are more powerful than Church higher order logic, the proof synthesis problem is more complicated. But we claim that because the proofs-as-objects paradigm simplifies the formalisms, it also simplifies the proof synthesis algorithms. In particular resolution and unification can be merged in a uniform algorithm.

We first present a complete method, then we discuss some efficiency improvements, we present a variant of this method which is incomplete but much more efficient and we show how to turn this algorithm into a unification algorithm.

1 Outline of the Method

Resolution and Unification

In first order logic or higher order logic, we have two syntactical categories, terms and proofs. Terms are trees (in first order logic) or simply typed λ-terms (in higher order logic) and proof are build, for instance, with natural deduction rules. These rules combine some proofs and terms to form new proofs. For instance the rule →-elim In first order logic and higher order logic, the resolution algorithm searches for proof-trees. When during the search of a proof-tree, a term-tree is needed, the unification algorithm is called. In type systems, term-trees and proof-trees belong to a single syntactical category, so our algorithm is a one level process merging resolution and unification.

We shortly present now the unification and resolution algorithms for higher order logic [START_REF] Huet | Constrained Resolution A Complete Method for Higher Order Logic[END_REF] [21] [START_REF] Huet | Résolution d' Équations dans les Langages d[END_REF], our goal is to show that a single idea on term enumeration underlies both algorithms.

Higher Order Unification

Higher order unification is based on an algorithm that enumerates all the normal η-long terms of a given type in the simply typed λ-calculus.

Let P 1 → ... → P n → P (P atomic) be a type. All normal η-long terms of this type begin by n abstractions t = [x 1 : P 1 ]...[x n : P n ]t ′

The term t ′ must have type P so it is an atomic term. A variable w : Q 1 → ... → Q p → Q of the context or which is an x i can be the head of this term, only if Q = P . Then this variable must be applied p times in order to get a term of the good type. So then we use recursively our algorithm to instantiate the h i : P 1 → ... → P n → Q i .

In unification, flexible-rigid equations are solved by instantiating the head of the flexible term using this method, the choice of the variable w is very restricted by the rigid term. Rigid-rigid equations are simplified. And flexible-flexible equations are solved in a trivial way.

So the method to enumerate terms underlying higher order unification can be summaried

• try all the possible head variables of the normal η-long form of the term,

• generate new variables for the rest of the term,

• generate a typing constraint to enforce well-typedness of the term,

• use recursively this method to fill these variables.

Higher Order Resolution

Let us present now the resolution method. We just present an incomplete restriction of this method to Horn clauses i.e. propositions on the form

Q 1 → ... → Q n → Q, where Q 1 , ..., Q n , Q are atomic
propositions (free variables are considered as universally quantified in the head of the clause).

When the goal P is atomic we unify it with Q the head of an hypothesis Q 1 → ... → Q n → Q, we generate subgoals σQ 1 , ..., σQ n (where σ is a unifer of P and Q) and we recursively search proofs of these propositions.

When the goal is also a Horn clause P 1 → ... → P n → P , then the clause form of the negation of this goal introduces P 1 , ..., P n as hypothesis and the atomic goal P .

This restriction is called the introduction-resolution algorithm. It can be presented with two rules: the resolution rule between an atomic goal and the head of an hypothesis is just called the resolution rule and the introduction of the hypothesis P 1 when we want to prove P 1 → P is called the introduction rule. It is incomplete. In [START_REF] Huet | Constrained Resolution A Complete Method for Higher Order Logic[END_REF] another rule (the splitting rule) is added to make it complete.

Remark that this method can also be used for hereditary Horn clauses i.e. propositions on the form

Q 1 → ... → Q n → Q, where Q is atomic and Q 1 , ..., Q n are hereditary Horn clauses.

Introduction-Resolution in Type Systems

In type systems, all the propositions can be considered as hereditary Horn clauses where the arrow is generalized to a dependent product, so we can apply the same method.

Furthermore, in type systems, a proof-synthesis method must not only assert that the proposition is provable but also exhibit a proof-term of this proposition.

The introduction-resolution algorithm can be presented that way:

• Introduction: To find a proof of a proposition (x : P 1 )P in a context Γ, find a proof of P in the context Γ[x : P 1 ]. When we have a proof t of P , the term [x : P 1 ]t is a proof of (x : P 1 )P in the context Γ.

• Resolution: To find a proof of P in a context Γ where there is a proposition

f : (x 1 : Q 1 )...(x n : Q n )Q
unify P and Q (consider x 1 , ..., x n as variables in Q) and then if x i has not been instantiated during the unification process, find a proof of σQ i (where σ is a unifier of P and Q). For each i, we get (by unification or as a proof of a subgoal) a term c i of type

Q i [x 1 ← c 1 , ..., x i-1 ← c i-1 ]. The term (f c 1 ... c n ) is a proof of P .
This method is fully described in [START_REF] Helmink | Resolution and Type Theory[END_REF]. Let us give an example. We have an hypothesis

f : (x : T )(y : T )(z : T )(u : (R x y))(v : (R y z))(R x z)
and we want to prove (R a c). We unify (R x z) and (R a c) this gives the substitution x ← a, z ← c.

Then we have to find terms b : T , t : (R a b) and u : (R b c). The term (f a b c t u) is a proof of (R a c). This method is in general incomplete. Another drawback is that no general unification algorithm is known for type systems. Algorithms are known only for the simply typed λ-calculus [START_REF] Huet | A Unification Algorithm for Typed λ-calculus[END_REF] [START_REF] Huet | Résolution d' Équations dans les Langages d[END_REF] and the λΠ-calculus [START_REF] Elliott | Higher-order Unification with Dependent Function Types[END_REF] [11] [START_REF] Pym | Proof, Search and Computation in General Logic[END_REF].

An alternative presentation of this method is the following

• Introduction: we give the proof [x : P 1 ]h for the proposition and the variable h is a subgoal to be proved.

• Resolution: we give the proof (f h 1 ... h p ) for the proposition together with an equation

Q[x 1 ← h 1 , ..., x p ← h p ] = P (in our example (R h 1 h 3 ) = (R a b))
to force the term (f h 1 ... h p ) to have type P . We solve this unification problem which fills some of the variables h i (here h 1 and h 3 ) and then the other variables (here h 2 , h 4 and h 5 ) are subgoals to be proved.

When, to prove a proposition, we first apply the introduction rule n times then the resolution rule, we give the proof [x 1 :

P 1 ]...[x n : P n ](f h 1 ... h p ) i.e.
we give f for the head variable of proof.

Remark that the dependence of the h i on the x j is implicit. So the method to enumerate terms underlying the introduction-resolution method is

• try all the possible head variables of the normal η-long form of the term,

• generate new variables for the rest of the term,

• generate a typing constraint to enforce well-typedness of the term,

• use recursively this method to fill these variables.

So this method is the same as the method underlying higher order unification.

A Method to Enumerate the Terms of a Given Type

Now we use this idea to construct a complete proof synthesis method for type systems. To enumerate the terms t that we can substitute to a variable x of type T we imagine the normal η-long form of t

t = [x 1 : P 1 ]...[x n : P n ](w c 1 ... c p ) or t = [x 1 : P 1 ]...[x n : P n ](y : A)B
and we perform all the elementary substitutions

x ← [x 1 : P 1 ]...[x n : P n ](w (h 1 x 1 ... x n ) ... (h p x 1 ... x n )) x ← [x 1 : P 1 ]...[x n : P n ](y : (h 1 x 1 ... x n ))(h 2 x 1 ... x n y)
Then we enumerate all the terms that can be substituted to the variables h 1 , ..., h p . Because we consider terms in η-long form, the number of abstractions n is the number of products in the type T and the types P 1 , ..., P n are the types of the variables bound in these products. So for completeness we have to consider • all the possible w,

• all the possible p and types for h 1 , ..., h p .

When we perform such a substitution, we have to make sure to get a term of type T . This welltypedness constraint is an equation.

In the introduction-resolution algorithm, the solution of this constraint is called the unification step of resolution. In unification in simply typed λ-calculus, types are always ground, so the constraint relates ground terms an we only have to check that they are identical, this is the selection of the head variables step. In unification in the λΠ-calculus [START_REF] Elliott | Higher-order Unification with Dependent Function Types[END_REF] [11] [START_REF] Pym | Proof, Search and Computation in General Logic[END_REF] this constraint is added to the set of equations, it is the accounting equation.

Here we keep this equation in the context. Equations are constraints that the forthcoming substitutions must verify. Since we do not have a special algorithm to solve these equations but use the standard method to fill the variables and use the equations as constraints on the substitutions, this method is a one level process merging resolution and unification.

Number of Applications

In the introduction-resolution algorithm when we want to prove an atomic proposition P and we resolve it with a variable w : (y 1 : Q 1 )...(y q : Q q )Q (Q atomic) we only consider proofs of the form (w h 1 ... h q ) and the constraint is that the type of this term must be equal to P i.e. Q[y 1 ← h 1 , ..., y q ← h q ] = P .

But in polymorphic type systems the term (w c 1 ... c q ) can still have a type which is a product and we can go on applying variables. This is why the introduction-resolution method is incomplete and why a splitting rule is needed in [START_REF] Huet | Constrained Resolution A Complete Method for Higher Order Logic[END_REF].

Here we consider an infinite number of possibilities for the number of applications and an infinitely branching search tree, we use interleaving to enumerate its nodes. In an incomplete but more efficient method we consider a restriction which is more or less similar to the introductionresolution method.

Variables in the Proposition to be Proved

In some type systems, the variables h i may have occurrences in the type of h j for j > i. We could first instantiate the variable h i and then instantiate the variable h j when it has a ground type, but it is well known that it is more efficient to solve the variable h j first. For instance to enumerate the terms of the type T = ∃x : N at.(P x) we must not enumerate all the terms n of type N at and for each n enumerate the terms of type (P n), but enumerate first the terms of type (P x).

Thus in polymorphic type systems when we have a variable in the proposition to be proved, it is not always possible to know the number and the types of abstractions: if the proposition to be proved is T = (x 1 : P 1 )...(x n : P n )P (P atomic) and the head of P is a variable that can be substituted then a substitution may increase the number of products in T and therefore the number of abstractions in t. So we have to delay the instantiation of x : T until we have instantiated T in a term (x 1 : P 1 )...(x n : P n )P where the head of P cannot be substituted.

η-conversion

In this paper we consider pure type systems extended with η-conversion. The methods developed here should also be applicable for pure type systems without η-conversion but, as in higher order unification [START_REF] Huet | A Unification Algorithm for Typed λ-calculus[END_REF] [22], we would need to consider more elementary substitutions.

2 Pure Type Systems Extended with η-conversion

Definition

A pure type system extended with η-conversion [START_REF] Barendregt | Introduction to Generalized Type Systems[END_REF] is a λ-calculus given by a set S (the elements of S are called sorts), a subset Ax of S × S and a subset R of S × S × S.

Definition 1 Functional Type System

A type system is said to be functional if

< s, s ′ >∈ Ax and < s, s ′′ >∈ Ax implies s ′ = s ′′ < s, s ′ , s ′′ >∈ R and < s, s ′ , s ′′′ >∈ R implies s ′′ = s ′′′
In this paper we consider systems such that S = {P rop, T ype}, Ax = {< P rop, T ype >}, if < s, s ′ , s ′′ >∈ R then s ′ = s ′′ and < P rop, P rop, P rop >∈ R. These systems are the eight systems of Barendregt's cube. All these systems are functional. Examples are the simply typed λ-calculus, the λΠ-calculus [19] [7] [16], the system F, the system Fω [START_REF] Girard | Interprétation fonctionnelle et élimination des coupures dans l'arithmétique d'ordre supérieur[END_REF] and the Calculus of Constructions [2] [5].

Definition 2 Syntax T ::= s | x | (T T ) | [x : T ]T | (x : T )T
In this paper we ignore variable renaming problems. A rigorous presentation would use de Bruijn indices [START_REF] De Bruijn | Lambda Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem[END_REF]. The terms s are sorts, the terms x are called variables, the terms (T T ′ ) applications, the terms [x : T ]T ′ λ-abstractions and the terms (x : T )T ′ products. The notation T → T ′ is used for (x : T )T ′ when x has no free occurrence in T ′ .

Let t and t ′ be terms and x a variable. We write t[x ← t ′ ] for the term obtained by substituting t ′ for x in t. We write t ≡ t ′ when t and t ′ are βη-equivalent.

Definition 3 Context

A context Γ is a list of pairs < x, T > (written x : T ) where x is a variable and T a term. The term T is called the type of x in Γ.

We write [x 1 : T 1 ; ...; x n : T n ] for the context with elements x 1 : T 1 , ..., x n : T n and Γ 1 Γ 2 for the concatenation of the contexts Γ 1 and Γ 2 .

Definition 4 Typing Rules

We define inductively two judgements: Γ is well-formed and t has type T in Γ (Γ ⊢ t : T ) where Γ is a context and t and T are terms. Empty:

[ ] well-formed Declaration: Γ ⊢ T : s s ∈ S Γ[x : T ] well-formed Sort: Γ well-formed < s, s ′ >∈ Ax Γ ⊢ s : s ′ Variable: Γ well-formed x : T ∈ Γ Γ ⊢ x : T Product: Γ ⊢ T : s Γ[x : T ] ⊢ T ′ : s ′ < s, s ′ , s ′′ >∈ R Γ ⊢ (x : T )T ′ : s ′′ Abstraction: Γ ⊢ (x : T )T ′ : s Γ[x : T ] ⊢ t : T ′ s ∈ S Γ ⊢ [x : T ]t : (x : T )T ′ Application: Γ ⊢ t : (x : T )T ′ Γ ⊢ t ′ : T Γ ⊢ (t t ′ ) : T ′ [x ← t ′ ] Conversion: Γ ⊢ T : s Γ ⊢ T ′ : s Γ ⊢ t : T T ≡ T ′ s ∈ S Γ ⊢ t : T ′ Definition 5 Well-typed Term
A term t is said to be well-typed in a context Γ if there exists a term T such that Γ ⊢ t : T .

Definition 6 Type

A term T is said to be a type in the context Γ if it is a sort or if there exists a sort s such that Γ ⊢ T : s.

Proposition 1 If Γ ⊢ t : T then T is a type.
Proof By induction on the length of the derivation of Γ ⊢ t : T .

Proposition 2

The βη-reduction is strongly normalizable and confluent on well-typed terms. Thus a well-typed term has a unique βη-normal form. Two well-typed terms are equivalent if they have the same βη-normal form. Proof Proofs of strong normalization and confluence for β-reduction are given in [START_REF] Th | Une Théorie des Constructions[END_REF] [START_REF] Geuvers | A Modular Proof of Strong Normalization for the Calculus of Constructions[END_REF]. As remarqued in [START_REF] Geuvers | The Church-Rosser Property for βη-reduction in Typed Lambda Calculi[END_REF] the strong normalization proof of [START_REF] Geuvers | A Modular Proof of Strong Normalization for the Calculus of Constructions[END_REF] can be adapted to βη-reduction and does not need confluence. Then confluence proofs for βη-reduction are given in [START_REF] Geuvers | The Church-Rosser Property for βη-reduction in Typed Lambda Calculi[END_REF] [30] [START_REF] Th | An Algorithm for Testing Conversion in Type Theory, Logical Frameworks I[END_REF].

Proposition 3 In a functional type system, in which reduction is confluent, a term t well-typed in a context Γ has a unique type modulo βη-equivalence. Proof By induction over the structure of t.

Definition 7 Atomic Term

A term t is said to be atomic if it has the form (u c 1 ... c n ) where u is a variable or a sort. The symbol u is called the head of the term t.

Proposition 4 A normal well-typed term t is either an abstraction, a product or an atomic term. Proof If the term t is neither an abstraction nor a product then it can be written in a unique way

t = (u c 1 ... c n )
where u is not an application. The term u is not a product (if n ̸ = 0 because a product is of type s for some sort s and therefore cannot be applied and if n = 0 because t is not a product). It is not an abstraction (if n ̸ = 0 because t is in normal form and if n = 0 because t is not an abstraction). It is therefore a variable or a sort.

Proposition 5 Let T be a well-typed normal type, the term T can be written in a unique way T = (x 1 : P 1 )...(x n : P n )P with P atomic. Proof By induction over the structure of T .

Definition 8 η-long form

Let Γ be a context and t be a βη-normal term well-typed in Γ and T the βη-normal form of its type. The η-long form of the term t is defined as

• If t = [x : U ]u then the η-long form of t is [x : U ′ ]u ′ where U ′ is the η-long form of U in Γ and u ′ the η-long form of u in Γ[x : U ]. • If t = (x : U )V then the η-long form of t is (x : U ′ )V ′ where U ′ is the η-long form of U in Γ and V ′ the η-long form of V in Γ[x : U ]. • If t = (w c 1 ... c p ) then we let T = (x 1 : P 1 )...(x n : P n )P (P atomic). The η-long form of t is [x 1 : P ′ 1 ]...[x n : P ′ n ](w c ′ 1 ... c ′ p x ′ 1 ... x ′ n )
where c ′ i is the η-long form of c i in Γ, P ′ i the η-long form of P i in Γ[x 1 : P 1 ; ...; x i-1 : P i-1 ] and x ′ i the η-long form of x i in Γ[x 1 : P 1 ; ...; x i :

P i ].
The well-foundedness of this definition is proved in [8] [9].

Definition 9 normal η-long form Let t be a term well-typed in a context Γ, the normal η-long form of t is the η-long form of its βη-normal form.

Definition 10 Subterm

We consider well-typed normal η-long terms labeled with the contexts in which they are welltyped: t Γ . Let t Γ such a term, we define by induction over the structure of

t Γ the set Sub(t Γ ) of strict subterms of t Γ • if t Γ is a sort or a variable then Sub(t Γ ) = {}, • if t Γ is an application, t = (u v), then Sub(t Γ ) = {u Γ , v Γ } ∪ Sub(u Γ ) ∪ Sub(v Γ ), • if t Γ is an abstraction, t = [x : P ]u, then Sub(t Γ ) = {P Γ , u Γ[x:P ] } ∪ Sub(P Γ ) ∪ Sub(u Γ[x:P ] ), • if t Γ is a product, t = (x : P )u, then Sub(t Γ ) = {P Γ , u Γ[x:P ] } ∪ Sub(P Γ ) ∪ Sub(u Γ[x:P ] ).

The M eta Type System

Let T be a type system of the cube. In order to express the proof synthesis method, we have to be allowed to declare a variable that stands for any well-typed term of T . For instance a variable that stands for P rop i.e. a variable of type T ype and this is not possible in T because the term T ype is not well-typed.

We want also to be allowed to express a term t : T ′ which is well-typed in Γ[x : T ] as t = (f x) with f well-formed in Γ. We want actually to be allowed to define f = [x : T ]t whatever the terms T and t may be. In general this cannot be done in T , because the type (x : T )T ′ may be not well-typed. So we are going to embed our type system T in another type system: the M eta type system.

Definition 11 M eta M eta =< S ′ , Ax ′ , R ′ > S ′ = {P rop, T ype, Extern}
Ax ′ = {< P rop, T ype >, < T ype, Extern >} R ′ = {< P rop, P rop, P rop >, < P rop, T ype, T ype >, < T ype, P rop, P rop >, < T ype, T ype, T ype >, < P rop, Extern, Extern >, < T ype, Extern, Extern >}

The strong normalization and confluence of βη-reduction for this system are not yet fully proved. But since all the terms typable in the M eta type system are typable in the Calculus of Constructions with Universes [START_REF] Th | An analysis of Girard's paradox[END_REF] [25] (identifying the sorts Extern and T ype 1 ), the β-reduction is strongly normalizable and confluent [START_REF] Th | An analysis of Girard's paradox[END_REF] [START_REF] Luo | An Extended Calculus of Constructions[END_REF]. It is conjectured in [START_REF] Geuvers | The Church-Rosser Property for βη-reduction in Typed Lambda Calculi[END_REF] that in a pure type system in which the β-reduction is strongly normalizable the βη-reduction also is. Then assuming strong normalization, confluence is proved in [START_REF] Geuvers | The Church-Rosser Property for βη-reduction in Typed Lambda Calculi[END_REF] [30] [START_REF] Th | An Algorithm for Testing Conversion in Type Theory, Logical Frameworks I[END_REF].

Proposition 6 Because the M eta type system is functional and βη-reduction is confluent, if a term t is well-typed in a context Γ then it has a unique type modulo βη-equivalence.

3 Constrained Quantified Contexts and Substitution

Constrained Quantified Contexts Definition 12 Constrained Quantified Contexts

A quantified declaration is a triple < Q, x, T > (written Qx : T ) where Q is a quantifier (∀ or ∃), x a variable and T is a term. A constraint is a pair of terms < a, b > (written a = b). A constrained quantified context is a list of quantified declarations and constraints. If Γ contains the declaration ∀x : T then the variable x is said to be universal in Γ. If it contains the declaration ∃x : T then x is said to be existential in Γ. These constrained quantified contexts are generalizations of Miller's mixed prefixes [START_REF] Miller | Unification Under a Mixed Prefix[END_REF] which are lists of quantified declarations.

Usual contexts are identified with constrained quantified contexts with only universal variables.

Definition 13 Equivalence Modulo Constraints

Let Γ be a constrained quantified context, we define the relation between terms ≡ Γ as the smallest equivalence relation compatible with terms structure such that

• if t ≡ t ′ then t ≡ Γ t ′ , • if (a = b) ∈ Γ then a ≡ Γ b.

Definition 14 Typing Rules

First we modify the rules to deal with the new syntax. The declaration rule is modified in

Γ ⊢ T : s s ∈ S Γ[Qx : T ] well-formed the variable rule is modified in Γ well-formed Qx : T ∈ Γ Γ ⊢ x : T the product rule is modified in Γ ⊢ T : s Γ[Qx : T ] ⊢ T ′ : s ′ < s, s ′ , s ′′ >∈ R Γ ⊢ (x : T )T ′ : s ′′ the abstraction rule is modified in Γ ⊢ (x : T )T ′ : s Γ[Qx : T ] ⊢ t : T ′ s ∈ S Γ ⊢ [x : T ]t : (x : T )T ′ and we add a constraint rule Γ ⊢ a : T Γ ⊢ b : T Γ[a = b] well-formed
Then we extend the system by replacing the conversion rule by

Γ ⊢ T : s Γ ⊢ T ′ : s Γ ⊢ t : T T ≡ Γ T ′ s ∈ S Γ ⊢ t : T ′
This defines two new judgements: Γ is well-formed using the constraints and t has type T in Γ using the constraints.

Remark that a term may be well-typed in Γ using the constraints and still be not normalizable.

Definition 15 Well-typed Without Using the Constraints

Let Γ be a context and t and T be two terms. The term t is said to be of type T in Γ without using the constraints if there exists ∆ subcontext of Γ (i.e. obtained by removing some items of Γ) such that ∆ has no constraints, is a well-formed context and ∆ ⊢ t : T . Proposition 7 If a term is well-typed in a context without using the constraints then it is strongly normalizable.

Definition 16 Normal Form of a Context

Let Γ be a well-formed context, the normal form of Γ is obtained by normalizing (in normal η-long form) all the types of variables that are well-typed without using the constraints and all the constraints which terms are well-typed without using the constraints.

Proposition 8 Let Γ be a well-formed context and Γ ′ be its normal form. The context Γ ′ is well-formed and if Γ ⊢ t : T then Γ ′ ⊢ t : T . Proof By induction on the length of the derivation of Γ well-formed and Γ ⊢ t : T .

Definition 17 Ground Term

A term t is said to be ground in a context Γ if it has no occurrence of an existential variable.

Definition 18 Rigid and Flexible Terms A normal η-long term well-typed without the constraints which is an abstraction, a product or an atomic term (w c 1 ... c n ) with w universal variable or sort is said to be rigid. A normal η-long term well-typed without the constraints which is atomic (w c 1 ... c n ) with w existential variable is said to be flexible.

Definition 19 Success and Failure Contexts

A normal well-formed context Γ is said to be a success context if it has only universal variables and constraints relating identical terms. It is said to be a failure context if it contains a constraint relating two normal η-long ground terms which are not identical.

Proposition 9 Let Γ be a normal context which is neither a success context nor a failure context. Then there exists an existential variable x : T whose type T is well-typed without using the constraints and has the form (x 1 : P 1 )...(x n : P n )P with the term P atomic and rigid in the context Γ[∀x 1 : P 1 ; ...; ∀x n : P n ]. Proof Let us consider the leftmost item which is neither a universal variable nor a normal η-long constraint relating identical terms (such an item exists since the context is not a success context).

If this item is a constraint (a = b), we let Γ = ∆[a = b]∆ ′ , the terms a and b are well-typed in ∆ so, since there are neither existential variables nor (non trivial) constraints in ∆, they are ground, well-typed without the constraints and normal. These terms are different and the context Γ is a failure context. So if Γ is not a failure context then this item is an existential variable ∃x : T and T is well-typed without the constraints and ground.

Substitution

Definition 20 Existential Context

A context (well-formed or not) is said to be existential if it contains only declarations of existential variables and constraints but no declarations of universal variables.

Definition 21 Substitution

A finite set σ of triples < x, γ, t > where x is a variable, γ an existential context and t a term is said to be a substitution if for each variable x there is at most one triple of the form < x, γ, t > in σ. When σ contains only one triple < x, γ, t > we write it σ = x ← γ, t.

Definition 22 Variable Bound by a Substitution

Let x be a variable and σ be a substitution. If the substitution σ contains a triple < x, γ, t > then x is said to be bound by σ. The context γ is said to be the context associated to x in σ.

Definition 23 Substitution Applied to a Term

Let x be a variable and σ a substitution. If there is a triple < x, γ, t > in σ then we let σx = t else we let σx = x. This definition extends straightforwardly to terms by

• σs = s, • σ(t u) = (σt σu), • σ[x : T ]u = [x : σT ]σu,
• σ(x : T )u = (x : σT )σu.

Definition 24 Substitution Applied to a Context

Let Γ be a context and σ a substitution, the context σΓ is defined inductively by The substitution σ is said to be well-typed in a context Γ if and only if the context σΓ is wellformed, no universal variable of Γ is bound by σ and for each existential variable x of type T in Γ and bound by σ, we have (σ∆)γ ⊢ t : σT where ∆ is the unique context such that Γ = ∆[∃x : T ]∆ ′ and < x, γ, t > the unique triple of σ binding the variable x.

• σ[ ] = [ ] • σ(∆[Qx : T ]) = (σ∆
Proposition 10 Let Γ be a context, σ a substitution and T and T ′ terms such that T ≡ Γ T ′ . Then σT ≡ σΓ σT ′ . Proof By induction on the length of the derivation of T ≡ Γ T ′ .

Proposition 11 Let σ be a substitution, t and u two terms and x a variable which is not bound by σ and which is not free in any σy for y ̸ = x. Then σ(t

[x ← u]) = (σt)[x ← σu].
Proof By induction over the structure of t.

Proposition 12 Let Γ be a context, σ a substitution well-typed in Γ and x a variable declared of type T in Γ. Then σΓ ⊢ σx : σT . Proof Since the substitution σ is well-typed in Γ, the context σΓ is well-formed. If x not bound by Γ then σx = x and Qx : σT ∈ σΓ so σΓ ⊢ σx : σT . If x is bound by σ then there exists a unique triple < x, γ, t > in σ. Let us write Γ = ∆[∃x : T ]∆ ′ . We have σx = t. Since σ is well-typed in Γ we have (σ∆)γ ⊢ t : σT and (σ∆)γ is a prefix of σΓ. So σΓ ⊢ σx : σT .

Proposition 13 Let Γ be a context, σ a substitution well-typed in Γ, t and T two terms such that Γ ⊢ t : T . We have σΓ ⊢ σt : σT . Proof By induction on the length of the derivation of Γ ⊢ t : T .

• If the last rule is the sort rule then we use the fact that σΓ is well-formed.

• If the last rule is the variable rule then we use the fact that σΓ is well-formed and σΓ ⊢ σx : σT .

• If the last rule is the product rule then by induction hypothesis we have σΓ ⊢ σT : s and (σΓ)[∀x : σT ] ⊢ σT ′ : s ′ , so σΓ ⊢ σ(x : T )T ′ : s ′′ .

• If the last rule is the abstraction rule then by induction hypothesis we have σΓ ⊢ σ(x : T )T ′ : s and (σΓ)[∀x : σT ] ⊢ σt : σT ′ , so σΓ ⊢ σ[x : T ]t : σ(x : T )T ′ .

• If the last rule is the application rule then by induction hypothesis we have σΓ ⊢ σt : σ(x : T )T ′ and σΓ ⊢ σt ′ : σT , so we get σΓ ⊢ σ(t t ′ ) : (σT ′ )[x ← σt ′ ] and since x is not bound by σ and is not free in any σy for y ̸ = x, we have σΓ ⊢ σ(t t ′ ) : σ(T ′ [x ← t ′ ]).

• If the last rule is the conversion rule then by induction hypothesis we have σΓ ⊢ σT : s, σΓ ⊢ σT ′ : s and since T ≡ Γ T ′ we have σT ≡ σΓ σT ′ , so σΓ ⊢ σt : σT ′ .

Definition 26 Composition of Substitutions

Let σ and τ two substitutions. The substitution τ • σ is defined as

(τ • σ) = {< x, τ γ, τ t > | < x, γ, t >∈ σ} ∪ {< x, γ, t > | < x,

A Complete Method Informal Introduction

When we search a proof of a proposition T in a context Γ we search a substitution σ well-typed in Γ[∃x : T ] such that σ(Γ[∃x : T ]) is a success context. When we have a context which contains several existential variables we choose such a variable x of type T = (x 1 : P 1 )...(x n : P n )P with P atomic rigid in Γ[∀x 1 : P 1 ; ...; ∀x n : P n ] and we perform an elementary substitution instantiating this variable. In the general case the elementary substitutions have the form

x ← [x 1 : P 1 ]...[x n : P n ](w (h 1 x 1 ... x n ) ... (h p x 1 ... x n ))
Let us write (y 1 : Q 1 )(y 2 : (Q 2 y 1 ))...(y q : (Q q y 1 ... y q-1 ))(Q y 1 ... y q ) the type of w. For the substitutions such that p = q we only need to declare the new variables h 1 , ..., h q used in the substitution and the constraint expressing the well-typedness of the substitution

(⃗ x : ⃗ P )(Q (h 1 x 1 ... x n ) ... (h q x 1 ... x n )) = (⃗ x : ⃗ P )P
(where (⃗ x : ⃗ P )t is an abbreviation for (x 1 : P 1 )...(x n : P n )t). For the substitutions such that p = q + r, r ≥ 1, we first declare the variables h 1 , ..., h q , then we need the type of the term (w (h 1 x 1 ... x n ) ... (h q x 1 ... x n )) to be a product, we introduce therefore two existential variables H 1 and K 1 and a constraint

(⃗ x : ⃗ P )(Q (h 1 x 1 ... x n ) ... (h q x 1 ... x n )) = (⃗ x : ⃗ P )(z : (H 1 x 1 ... x n ))(K 1 x 1 ... x n z)
Then we can introduce the variable h q+1 with the type (⃗ x : ⃗ P )(H 1 x 1 ... x n ). If r = 1 we just need a last constraint expressing the well-typedness of the substitution

(⃗ x : ⃗ P )(K 1 x 1 ... x n (h q+1 x 1 ... x n )) = (⃗ x : ⃗ P )P
and in the general case we introduce in the same way 4r items and then a well-typedness constraint.

We also have to include other elementary substitutions in which the variable x is substituted by a term of the form [x 1 : P 1 ]...[x n : P n ]u where u is a sort or a product.

Definition 27 Elementary Substitutions

Let Γ be a normal context well-formed in the M eta type system such that the type of the type of universal variables is P rop or T ype but not Extern and which is neither a success nor a failure context. We choose in Γ an existential variable x whose type is normal η-long and has the form T = (x 1 : P 1 )...(x n : P n )P with P atomic rigid in Γ[∀x 1 : P 1 ; ...; ∀x n : P n ] (such a variable exists because the context in neither a success nor a failure context) and we construct the set of substitutions Σ(Γ) in the following way.

Notation If t is a term, (⃗ x : ⃗ P )t is an abbreviation for (x 1 : P 1 )...(x n : P n )t.

• For every w which is a universal variable declared in the left of x or which is an x i Γ[∀x 1 : P 1 ; ...; ∀x n :

P n ] ⊢ w : (y 1 : Q ′ 1 )...(y q : Q ′ q )Q ′ (Q ′ atomic)
We let

Q 1 = Q ′ 1 Q 2 = [y 1 : Q ′ 1 ]Q ′ 2 ... Q q = [y 1 : Q ′ 1 ]...[y q-1 : Q ′ q-1 ]Q ′ q Q = [y 1 : Q ′ 1 ]...[y q : Q ′ q ]Q ′ We have w : (y 1 : Q 1 )(y 2 : (Q 2 y 1 ))...(y q : (Q q y 1 ... y q-1 ))(Q y 1 ... y q )
For every r ≥ 0 we consider the following substitutions with r-splitting. Let s be the sort type of Q ′ and s ′ the sort type of P in Γ[∀x 1 : P 1 ; ...; ∀x n :

P n ]. For every sequence s 1 , s ′ 1 , ..., s i , s ′ i , ..., s r , s ′ r such that < s 1 , s ′ 1 , s >∈ R, ..., < s i , s ′ i , s ′ i-1 >∈ R and s ′ r = s ′ , we consider the substitution x ← γ, t where t = [x 1 : P 1 ]...[x n : P n ](w (h 1 x 1 ... x n ) ... (h q+r x 1 ... x n )) γ = φχ 1 ...χ r ψ with φ = [∃h 1 : (⃗ x : ⃗ P )Q 1 ; ∃h 2 : (⃗ x : ⃗ P )(Q 2 (h 1 x 1 ... x n ));
...;

∃h q : (⃗ x : ⃗ P )(Q q (h 1 x 1 ... x n ) ... (h q-1 x 1 ... x n ))] χ 1 = [∃H 1 : (⃗ x : ⃗ P )s 1 ; ∃K 1 : (⃗ x : ⃗ P )(z : (H 1 x 1 ... x n ))s ′ 1 ; (⃗ x : ⃗ P )(Q (h 1 x 1 ... x n ) ... (h q x 1 ... x n )) = (⃗ x : ⃗ P )(z : (H 1 x 1 ... x n ))(K 1 x 1 ... x n z); ∃h q+1 : (⃗ x : ⃗ P )(H 1 x 1 ... x n )] for all i, 1 < i ≤ r χ i = [∃H i : (⃗ x : ⃗ P )s i ; ∃K i : (⃗ x : ⃗ P )(z : (H i x 1 ... x n ))s ′ i ; (⃗ x : ⃗ P )(K i-1 x 1 ... x n (h q+i-1 x 1 ... x n )) = (⃗ x : ⃗ P )(z : (H i x 1 ... x n ))(K i x 1 ... x n z); ∃h q+i : (⃗ x : ⃗ P )(H i x 1 ... x n )] and if r = 0 ψ = [(⃗ x : ⃗ P )(Q (h 1 x 1 ... x n ) ... (h q x 1 ... x n )) = (⃗ x : ⃗ P )P ] otherwise ψ = [(⃗ x : ⃗ P )(K r x 1 ... x n (h q+r x 1 ... x n )) = (⃗ x : ⃗ P )P ]
• If P is a sort then for every sort s, such that < s, P >∈ Ax, we consider also the substitution

x ← [ ], [x 1 : P 1 ]...[x n : P n ]s
and for every pair of sorts < s, s ′ > such that < s, s ′ , P >∈ R we also consider the substitution

x ← γ, t

where t = [x 1 : P 1 ]...[x n : P n ](y : (h x 1 ... x n ))(k x 1 ... x n y) γ = [∃h : (⃗ x : ⃗ P )s ; ∃k : (⃗ x : ⃗ P )(y : (h x 1 ... x n ))s ′ ]
The set Σ(Γ) is the set which contains all the substitutions considered above.

Definition 28 Derivation A derivation of a context Γ is a list of substitutions [σ 1 ; ...; σ m ] such that σ i ∈ Σ(σ i-1 σ i-2 ...σ 1 Γ) and σ m σ m-1 ...σ 1 Γ is a success context.

Definition 29 Search tree

Let Γ be a context, we build a tree, called the search tree of Γ. Nodes are labeled by contexts and edges by elementary substitutions. The root is labeled by Γ. Nodes labeled by success and failure contexts are leaves. From a node labeled by a context ∆ which is neither a success context nor failure context, for each σ of Σ(∆) we grow an edge labeled σ to a new node labeled by σ∆.

Success nodes are in bijection with the derivations of Γ. A semi-algorithm of proof synthesis is to enumerate the nodes of the tree in order to find a success node. Since the number of sons of a node may be infinite we have, in order to get an finitely branching tree, to delay the exploration of node with r-splitting for r generations. For x, we perform the substitution with head Antisym and 0-splitting

x ← (Antisym h 1 h 2 h 3 h 4 ) We get the context ∆[∃h 1 : T ; ∃h 2 : T ; ∃h 3 : (R h 1 h 2 ); ∃h 4 : (R h 2 h 1 ); (Eq h 1 h 2 ) = (Eq a b)].
For h 1 , we perform the substitution with head a and 0-splitting

h 1 ← a
For h 2 , we perform the substitution with head b and 0-splitting

h 2 ← b
We get the context ∆[∃h 3 : (R a b); ∃h 4 : (R b a)] (we do not write the trivial constraints). For h 3 , we perform the substitution with head u and 0-splitting

h 3 ← u We get the context ∆[∃h 4 : (R b a)].
For h 4 , we perform the substitution with head v and 0-splitting

h 4 ← v
And we get the success context ∆. Let θ be the composition of these substitutions, θx = (Antisym a b u v).

As we will see in the following, in this example, at each step, all the substitutions but the one considered leed to obviously hopeless contexts.

An Example with Splitting

Let ∆ = [∀A : P rop; ∀B : P rop; ∀I : P rop → P rop; ∀u : (P : P rop)((I P ) → P ); ∀v : (I (A → B)); ∀w : A] and Γ = ∆[∃p : B]. For p, we perform the substitution with head u and 1-splitting

p ← (u h 1 h 2 h 3 )
with the new variables: h 1 : P rop, h 2 : (I h 1 ), H : P rop, K : H → P rop and h 3 : H. We get the context ∆[∃h 1 : P rop; ∃h 2 : (I h 1 ); ∃H : P rop; ∃K : H → P rop; ∃h 3 :

H; h 1 = (x : H)(K x); (K h 3 ) = B].
For h 1 , we perform a product substitution

h 1 ← (x : h ′ )(k ′ x)
We get the context ∆[∃h ′ : P rop; ∃k ′ : h ′ → P rop; ∃h 2 : (I ((x : h ′ )(k ′ x))); ∃H : P rop; ∃K : H → P rop; ∃h 3 : H;

(x : H)(K x) = (x : h ′ )(k ′ x); (K h 3 ) = B].
For h 2 we perform the substitution with head v and 0-splitting

h 2 ← v
We get the context ∆[∃h ′ : P rop; ∃k ′ : h ′ → P rop; (I ((x : h ′ )(k ′ x))) = (I (A → B)); ∃H : P rop; ∃K : H → P rop;

∃h 3 : H; (x : H)(K x) = (x : h ′ )(k ′ x); (K h 3 ) = B].
For h ′ we perform the substitution with head A and 0-splitting

h ′ ← A ∆[∃k ′ : A → P rop; (I ((x : A)(k ′ x))) = (I (A → B)); ∃H : P rop; ∃K : H → P rop; ∃h 3 : H; (x : H)(K x) = (x : A)(k ′ x); (K h 3 ) = B].
For k ′ we perform the substitution with head B and 0-splitting

k ′ ← [x : A]B
We get the context ∆[∃H : P rop; ∃K : H → P rop; ∃h 3 : H;

(x : H)(K x) = (A → B); (K h 3 ) = B].
For H we perform the substitution with head A and 0-splitting

H ← A
We get the context ∆[∃K : A → P rop; ∃h 3 : A; (x : A)(K x) = (A → B);

(K h 3 ) = B].
For K we perform the substitution with head B and 0-splitting

K ← [x : A]B
We get the context ∆[∃h 3 : A]. For h 3 we perform the substitution with head w and 0-splitting

h 3 ← w
And we get the success context ∆. Let θ be the composition of all these substitutions, θp = (u (A → B) v w).

Properties

Well-typedness

In this section Γ is a normal context well-formed in the M eta type system such that the type the type of universal variables is P rop or T ype but not Extern and which is neither a success nor a failure context and σ = x ← γ, t is a substitution of Σ(Γ). We write Γ = ∆[∃x : T ]∆ ′ . We prove that the substitution σ is well-typed in the context Γ. so in the context ∆γ

[x 1 : P 1 ]...[x n : P n ](w (h 1 x 1 ... x n ) ... (h q+1 x 1 ... x n )) : (⃗ x : ⃗ P )(K 1 x 1 ... x n (h q+1 x 1 ... x n ))
Then if we assume this for i we deduce

[
(w (h 1 x 1 ... x n ) ... (h q+i+1 x 1 ... x n )) : (K i+1 x 1 ... x n (h q+i+1 x 1 ... x n )) so in the context ∆γ [x 1 : P 1 ]...[x n : P n ](w (h 1 x 1 ... x n ) ... (h q+i+1 x 1 ... x n )) : (⃗ x : ⃗ P )(K i+1 x 1 ... x n (h q+i+1 x 1 ... x n ))
So we deduce Let Γ be a well-formed context, the substitution θ is said to be a solution to Γ if

Soundness

• the substitution θ is well-typed in Γ,

• the context θΓ is a success context.

Definition 31 Normal Solution to a Context

Let Γ be a well-formed context, the substitution θ, solution to Γ, is said to be a normal solution to Γ if

• the substitution θ binds exactly the existential variables of Γ,

• for each existential variable x of Γ, the context associated to x by θ is empty and σx is normal η-long in the context θ∆ where ∆ is the unique context such that Γ = ∆[∃x : T ]∆ ′ .

Definition 32 Normal Form of a Solution Let Γ be a well-formed context and θ a solution to Γ. We define θ ′ the normal form of θ in Γ by induction over the length of Γ.

• If Γ = [ ] then we let θ ′ = {}. • If Γ = ∆[∀x : T ] or Γ = ∆[a = b]
then θ is a solution to ∆, we let θ ′ be the normal form of θ in ∆.

• If Γ = ∆[∃x : T ] then θ is a solution to ∆. We let θ 1 be the normal form of θ in ∆. We have θΓ ⊢ θx : θT , let t be the normal η-long form of θx in θΓ. We let

θ ′ = θ 1 ∪ {< x, [ ], t >}.
Proposition 20 Let Γ be a context and Γ ′ be a context obtained by removing some constraints relating identical terms. If Γ is well-formed then Γ ′ is well-formed. If Γ ⊢ t : T then Γ ′ ⊢ t : T .

Proof By induction on the length of the derivation of Γ well-formed or Γ ⊢ t : T .

Proposition 21 Let ∆ and γ be two contexts such that ∆γ is a success context and γ is an existential context. Then γ is a list of constraints relating terms well-typed without using the constraints and whose normal forms are identical.

Proof By induction on the length of γ.

splitting algorithm this is found in both cases, but the price to pay is inefficiency, with the weak splitting this is found when the type of the existential variable is A → B but not when it is B. Roughly speaking, this means that when we must use a proposition with a quantifier on a proposition or a predicate (for instance an induction axiom) the weak splitting algorithm finds the proposition to be used only when it can be seen in the type of the existential variable, and not when the proof requires an induction loading [START_REF] Helmink | Resolution and Type Theory[END_REF] (as here from B to A → B). This weak splitting algorithm is quite similar to the introduction-resolution method [START_REF] Helmink | Resolution and Type Theory[END_REF] for some unification algorithm. Actually some proofs that cannot be synthesized by introductionresolution can be synthesized with weak splitting. For instance in a context that contains the universal variables u : (P : P rop)(P → A) and v : (B → C) the proof (u (B → C) [x : B](v x)) : A is synthesized by the weak-splitting algorithm and not by the introduction-resolution method. To get exactly the introduction-resolution method we would have to forbid completely product substitutions.

This method with weak splitting is incomplete but its transitive closure is complete [START_REF] Dowek | Démonstration Automatique dans le Calcul des Constructions[END_REF]. This means that even if it cannot be synthesized, each proof can be broken up in smaller proofs that can be synthesized.

Unification 10.1 Ground Unification

The unification problem is to decide if given a context Γ (with universal and existential variables but no constraints) and two terms a and b well-typed in Γ with the same type, there exists a substitution θ well-typed in Γ, such that for every variable x bound by θ, the context associated to x by θ contains no constraints and such that θa = θb. In first order unification and higher order unification we do not require θ to fill all the existential variables of Γ, moreover the substitution θ may introduce new existential variables. This tolerance is due to the fact that in first order and higher order logic, types are all supposed to be inhabited, so from any unifier we can deduce a ground unifier by filling the unfilled variables with arbitrary terms. So unifiability is equivalent to ground unifiability. This is not the case any more in type systems where we have empty types. In unification in simply typed λ-calculus under a quantified context [START_REF] Miller | Unification Under a Mixed Prefix[END_REF] types may also be empty and unifiability is not equivalent to ground unifiability. The notion of unifiability considered in [START_REF] Miller | Unification Under a Mixed Prefix[END_REF] is the one of ground unifiability.

A semi-algorithm for deciding ground unifiability is to apply the method developed in this paper to the context Γ[a = b]. Moreover this algorithm enumerates all the ground unifiers.

In contrast with what happens in simply typed λ-calculus, we have to solve flexible-flexible equations. Indeed these equations may have no solution since the head variables of the terms may have empty types. Moreover it is proved in [START_REF] Miller | Unification Under a Mixed Prefix[END_REF] that the problem of deciding the existence of solutions for flexible-flexible unification problems under a quantified context is undecidable in simply typed λ-calculus. This proof generalizes easily to type systems.

Toward Open Unification

The utility of an open unification algorithm is not obvious, since in a proof-search algorithm (or more generally in an algorithm that uses unification) existential variables are introduced to be filled-in and not to remain forever.

If we still need such an algorithm we may remark that flexible-flexible equations have to be solved since, in contrast with what happens in simply typed λ-calculus, they may have no solution. The equation a = b is flexible-flexible, but there is no solution to this problem. Indeed, let us suppose there is one and consider t = θx. We have t : (P : P rop)P so t = [P : P rop]t ′ with t ′ : P . So t ′ is neither an abstraction nor a product. It is an atomic term (f c 1 ... c n ). If f were the variable P we would have n = 0 and thus t ′ = P which is impossible for type reasons, so f ̸ = P . Since So (f c 1 [P ← (A → B)]) = f which is impossible since a variable cannot be equal to an application. Searching for solutions of flexible-flexible equations seems to be rather difficult, since the head variable of an elementary substitution may now be any variable of Γ and also any new variable. We would have to design a proof search algorithm similar to the one described in this paper but that enumerates all the proofs of a proposition, under all the possible sets of axioms.

It may be possible to recognize flexible-flexible equations that have solutions and those that do not have any and keep the former unsolved until the end of the process as we do in unification in simply typed λ-calculus. In this case the normalization of terms well-typed using such constraints is not obvious, we may have to perform one normalization step as an elementary operation of the algorithm. Also some product substitutions have to be performed when the types of the variables to be instantiated in flexible-rigid and flexible-flexible equations has an existential head variable.

In contrast with ground unifiability, open unifiability seems a quite difficult problem with small interest.

Conclusion

In this paper we have described an semi-decision procedure for type systems. In fact, since proof checking is decidable in these systems, the existence of such a procedure is obvious: we just need to enumerate all the lists of characters until we get a proof of the proposition to be proved. Of course this method (which is sometime used to prove the semi-decidability of predicate calculus) is of no practical interest. We can let it be more realist in enumerating not all the lists of characters but only the normal λ-terms (or proof-trees), this method is comparable to the methods of the early sixties based on the search of a counter Herbrand model.

Resolution excludes more hopeless tentatives by remarking that in a premise ∀x.(P x), we need to instantiate x by t only if (P t) is an instance of the proposition to be proved or an hypothesis of another premise. This method formulated by Robinson [START_REF] Robinson | A Machine-Oriented Logic Based on the Resolution Principle[END_REF] for first order logic and by Huet [START_REF] Huet | Constrained Resolution A Complete Method for Higher Order Logic[END_REF] for higher order logic is generalized here to type systems. The notions of proof-term that appear in these systems simplify the method and makes more explicit the idea of blind enumeration of proof-terms regulated by a failure anticipation mechanism exploiting type constraints.

A

  → B A B combines two proofs (one of A → B and one of A) to get a proof of B. The rule ∀-elim ∀x : A.B t : A B[x ← t] combines a proof (of ∀x : A.B) and a term (of type A) to get a proof of B[x ← t]. So proofs are heterogeneous trees. For instance, in the proof∀f : T → T.((P f ) → (Q f )) [x : T ] [x : T ]x : T → T (P [x : T ]x) → (Q [x : T ]x) (P [x : T ]x) (Q [x : T ]x)the subtree [x : T ] [x : T ]x : T → T is a term derivation.

t = [x 1 :

 1 P 1 ]...[x n : P n ](w c 1 ... c p )To mark the dependency of the c i on the x j we writet = [x 1 : P 1 ]...[x n : P n ](w (d 1 x 1 ... x n ) ... (d p x 1 ... x n ))To find the d i we use recursively the same algorithm. So we first taket = [x 1 : P 1 ]...[x n : P n ](w (h 1 x 1 ... x n ) ... (h p x 1 ... x n ))

  )γ where γ is the context associated to x by σ if the variable x is bound by σ and γ = [Qx : σT ] otherwise. • σ(∆[a = b]) = (σ∆)[σa = σb] Definition 25 Substitution Well-typed in a Context

  γ, t >∈ τ and x not bound by σ} Proposition 14 Let σ and τ two substitutions and t be a term, we have (τ • σ)t = τ σt. Proof By induction over the structure of t.Proposition 15 Let σ and τ two substitutions and Γ be a context, we have (τ • σ)Γ = τ σΓ. Proof By induction over the length of Γ.Proposition 16 Let Γ be a context and σ and τ two substitutions, such that σ is well-typed in Γ and τ is well-typed in σΓ then τ • σ is well-typed in Γ.Proof We have (τ • σ)Γ = τ σΓ, so the context (τ • σ)Γ is well-formed. No universal variable of Γ is bound by τ • σ. If Γ = ∆[∃x : T ]∆ ′ then σ(∆[∃x : T ]) ⊢ σx : σT sousing the previous proposition τ σ(∆[∃x : T ]) ⊢ τ σx : τ σT , i.e. (τ • σ)(∆[∃x : T ]) ⊢ (τ • σ)x : (τ • σ)T .

1 A

 1 First Order Example Let ∆ = [∀T : P rop; ∀R : T → T → P rop; ∀Eq : T → T → P rop; ∀Antisym : (x : T )(y : T )((R x y) → (R y x) → (Eq x y)); ∀a : T ; ∀b : T ; ∀u : (R a b); ∀v : (R b a)] and Γ = ∆[∃x : (Eq a b)].

[x 1 :

 1 P 1 ]...[x n : P n ](w (h 1 x 1 ... x n ) ... (h q+r x 1 ... x n )) : (⃗ x : ⃗ P )(K r x 1 ... x n (h q+r x 1 ... x n )) then using the last constraint (ψ) [x 1 : P 1 ]...[x n : P n ](w (h 1 x 1 ... x n ) ... (h q+r x 1 ... x n )) : (⃗ x : ⃗ P )P In the same way, if σ = x ← γ, t with t = [x 1 : P 1 ]...[x n : P n ]u where u is a sort or a product then the term t also is well-typed and has also type T in the context ∆γ in the M eta type system. Proposition 19 The substitution σ is well-typed in the context Γ in the M eta type system. Proof Let us write ∆ ′ = [e 1 ; ...; e n ]. We prove by induction on i that the substitution σ is well-typed in ∆[∃x : T ][e 1 ; ...; e i ] in the M eta type system. We have σ(∆[∃x : T ]) = ∆γ and σT = T , so the context σ(∆[∃x : T ]) is well-formed in the M eta type system and we have σ(∆[∃x : T ]) ⊢ t : σT . Obviously σ binds no universal variables of ∆[∃x : T ]. So σ is well-typed in ∆[∃x : T ]. Let us assume now that the substitution σ is well-typed in ∆[∃x : T ][e 1 ; ...; e i ]. The item e i+1 is either the declaration of a variable Qy : P or a constraint a = b. In the first case we have ∆[∃x : T ][e 1 ; ...; e i ] ⊢ P : s for some sort s, and in the second ∆[∃x : T ][e 1 ; ...; e i ] ⊢ a : U and ∆[∃x : T ][e 1 ; ...; e i ] ⊢ b : U for some U . So since the substitution σ is well-typed in ∆[∃x : T ][e 1 ; ...; e i ] we have in the first case σ(∆[∃x : T ][e 1 ; ...; e i ]) ⊢ σP : s and in the second σ(∆[∃x : T ][e 1 ; ...; e i ]) ⊢ σa : σU and σ(∆[∃x : T ][e 1 ; ...; e i ]) ⊢ σb : σU So the context σ(∆[∃x : T ][e 1 ; ...; e i+1 ]) = σ(∆[∃x : T ][e 1 ; ...; e i ])[σe i+1 ] is well-formed. Then since we have ∆γ ⊢ t : T and σ obviously binds no universal variables of ∆[∃x : T ][e 1 ; ...; e i+1 ], the substitution σ is well-typed in ∆[∃x : T ][e 1 ; ...; e i+1 ] in the M eta type system.

Definition 30 :

 30 Solution to a Context

  Consider [∀A : P rop; ∀B : P rop; ∀u : A; ∃x : (P : P rop)P ] a = (x (A → B) u) b = (x B)

  (t ′ [P ← (A → B)] u) = t ′ [P ← B] we have (f c 1 [P ← (A → B)] ... c n [P ← (A → B)] u) = (f c 1 [P ← B] ... c n [P ← B])

  x 1 : P 1 ]...[x n : P n ](w (h 1 x 1 ... x n ) ... (h q+i x 1 ... x n )) : (⃗ x : ⃗ P )(K i x 1 ... x n (h q+i x 1 ... x n )) using the constraint of χ i [x 1 : P 1 ]...[x n : P n ](w (h 1 x 1 ... x n ) ... (h q+i x 1 ... x n )) : (⃗ x : ⃗ P )(z : (H i+1 x 1 ... x n ))(K i+1 x 1 ... x n z)in the context ∆γ[∀x 1 : P 1 ; ...; ∀x n : P n ] we have (w (h 1 x 1 ... x n ) ... (h q+i x 1 ... x n )) : (z : (H i+1 x 1 ... x n ))(K i+1 x 1 ... x n z)

	and since
	h q+i+1 : (⃗ x : ⃗ P )(H i+1 x 1 ... x n )

Acknowledgements

The author thanks Gérard Huet who has supervised this work and Amy Felty, Herman Geuvers, Christine Paulin and the anonymous referees for many helpful comments and criticisms.

This research was partly supported by ESPRIT Basic Research Action "Logical Frameworks".

 Proposition 17The context ∆γ is well-formed in the M eta type system. Proof By induction on the length of γ, we check that the types of the existential variables and the constraints of γ are well-typed in the M eta type system.

Since (x 1 : P 1 )...(x n : P n )P is well-typed in the M eta type system, the terms P i are well-typed in the M eta type system of type P rop or T ype but not Extern. The term (y 1 : Q ′ 1 )...(y q : Q ′ q )Q ′ is either the type of a universal variable or one of the P i , its type is therefore P rop or T ype but not Extern. So the types of the Q ′ i and of Q ′ are P rop or T ype but not Extern. So the terms Q i and Q are well-typed in the M eta type system. The terms (H i x 1 ... x n ) and (h x 1 ... x n ) are well-typed in the M eta type system and have the type s with < s, s ′ , s ′′ >∈ R for some s ′ and s ′′ . So s is equal to P rop or T ype, but not to Extern.

So the terms (⃗ x : ⃗ P )(Q i (h 1 x 1 ... x n ) ... (h i-1 x 1 ... x n )), (⃗ x : ⃗ P )s i , (⃗ x : ⃗ P )(z : (H i x 1 ... x n ))s ′ i , (⃗ x : ⃗ P )(Q (h 1 x 1 ... x n ) ... (h q x 1 ... x n )), (⃗ x : ⃗ P )(K i-1 x 1 ... x n (h q+i-1 x 1 ... x n )), (⃗ x : ⃗ P )(z : (H i x 1 ... x n ))(K i x 1 ... x n z), (⃗ x : ⃗ P )(H i x 1 ... x n ), (⃗ x : ⃗ P )(Q (h 1 x 1 ... x n ) ... (h q x 1 ... x n )), (⃗ x : ⃗ P )(K r x 1 ... x n (h q+r x 1 ... x n )), (⃗ x : ⃗ P )P , (⃗ x : ⃗ P )s and (⃗ x : ⃗ P )(y : (h x 1 ... x n ))s ′ are well-typed in the M eta type system and have the type P rop, T ype or Extern. Proposition 18 In the M eta type system we have ∆γ ⊢ t : T . Proof For the substitution with 0-splitting we have

then using the constraint ψ

For the substitution with r-splitting (r ≥ 1), we prove by induction on i that in ∆γ, for all i ≥ 1

For i = 1 we have

in the context ∆γ[∀x 1 : P 1 ; ...; ∀x n : P n ] we have

and since

Proposition 22 Let Γ be a well-formed context and θ a solution to Γ. Let θ ′ be the normal form of θ. Then θ ′ is a normal solution to θ.

Proof By induction on the length of Γ.

Lemma 1 Let Γ be a context, if there exists a derivation [σ 1 ; ...; σ m ] of Γ, then there exists a normal solution to Γ.

Proof The substitution σ m • ... • σ 1 , is a solution to Γ. Let θ be its normal form.

The substitution θ called the substitution denoted by the derivation [σ 1 ; ...; σ m ].

Now we prove that the substitution θ which is well-typed in the M eta type system is also well-typed in the original system T .

Proposition 23 Let Γ be a context well-formed in a type system T and T be either a term welltyped in Γ in the system T or the symbol T ype. Let t be a normal η-long term such that Γ ⊢ t : T in the M eta type system such that for every subterm of t which is a product (x : U )U ′ if we let s be the type of U , s ′ be the type of U ′ and s ′′ be the type of (x : U )U ′ , we have < s, s ′ , s ′′ >∈ R (the set of rules of the system T ) and for every subterm of t which is a sort s we have s = P rop (and not T ype), then we have Γ ⊢ t : T in the system T . Proof By induction over the structure of t.

U ] in the type system T and by induction hypothesis Γ[∀x : U ] ⊢ u ′ : U ′ in the system T . So Γ ⊢ t : T in the system T .

• If t = (x : U )U ′ then by induction hypothesis U and U ′ are well-typed in the system T and since the rule < s, s ′ , s ′′ > is a rule of the system T , we have Γ ⊢ t : T in the system T .

• If t = (x c 1 ... c n ) with x variable declared in Γ then x is well-typed in Γ in the system T and we prove by induction on i that the type of c i is well-typed in the system T and c i is well-typed in the system T and we conclude that Γ ⊢ t : T in the system T .

• If t is a sort then by hypothesis t = P rop, it is well-typed in the system T .

Proposition 24 Let Γ be a well-formed context in the system T , [σ 1 ; ...; σ m ] be a derivation of Γ and θ the substitution denoted by this derivation. Let x be an existential variable of Γ and t = θx. For every subterm of t which is a product (x : U )U ′ if we let s be the type of U , s ′ be the type of U ′ and s ′′ be the type of (x : U )U ′ , we have < s, s ′ , s ′′ >∈ R (the set of rules of the system T ) and for every subterm of t which is a sort s we have s = P rop (and not T ype), Proof By induction on m.

Proposition 25 Let Γ be a context well-formed in the system T , [σ 1 ; ...; σ m ] a derivation of Γ and θ the substitution denoted by this derivation. The substitution θ is well-typed in Γ in the system T .

Proof By induction on the length of Γ.

Theorem 1 Soundness

Let Γ be a (non constrained, non quantified) context and P a well-typed type in Γ. Let Γ ′ = Γ[∃x : P ]. If there exists a derivation of Γ ′ then there exists a proof t of P in Γ in T . Proof Let θ be the substitution denoted by the derivation of Γ ′ . The substitution θ is well-typed in Γ ′ in the system T and is a normal solution to Γ ′ . Let t = θx. Since θ is normal we have θΓ ′ = θΓ. We have θΓ ′ = θΓ, θΓ = Γ, θP = P and θΓ ′ ⊢ θx : θP so Γ ⊢ t : P . The proof t is called the proof denoted by the derivation.

Completeness

Definition 33 The Relation < Let < be the smallest transitive relation defined on normal η-long terms such that

As proved in [START_REF] Dowek | A Second Order Pattern Matching Algorithm in the Cube of Typed λ-Calculi[END_REF] [START_REF] Dowek | Démonstration Automatique dans le Calcul des Constructions[END_REF], this relation is well-founded, which means that a function that recurses both on a strict subterm and on the type of its argument is total.

Definition 34 Size of a Term

Let Γ be a context and t a term well-typed in Γ. Let T be the normal η-long form of the type of t in Γ. We define by induction over <, the size of t Γ (|t Γ |)

Definition 35 Size of a Substitution

The size of a substitution θ = {< x i , γ i , t i >} is the sum of the sizes of the t i .

Proposition 26 If Γ is a failure context, then for every substitution σ, σΓ is also a failure context and therefore is not a success context.

Proof Let a = b be a constraint of Γ relating two ground different terms, then (σa = σb) is (a = b) which is a constraint relating two well-typed ground different terms.

Lemma 2 Let Γ be a well-formed context and θ a normal solution to Γ, then there exists a derivation of Γ which denotes θ.

Proof By induction on the size of θ. The context Γ is not a failure context because there exists a substitution θ such that θΓ is a success context. If it is a success context then [ ] is a derivation of Γ. Otherwise let us chose an existential variable x with a normal η-long type (x 1 : P 1 )...(x n : P n )P such that P is atomic rigid. Let t = θx. Since θ is well-typed in Γ, θΓ ⊢ t : (x 1 : θP 1 )...(x n : θP n )θP . Since the term P is atomic rigid, the term θP is atomic. Then t = [x 1 : θP 1 ]...[x n : θP n ]u with u atomic or a product (η-long form).

• If u = (w u 1 ... u p ) then let q the number of products of the type of w and r = p -q. Since the type of u is atomic we have p ≥ q, i.e. r ≥ 0. We let

with γ defined in the algorithm. Then we build the terms to be substituted to the variables h i (1 ≤ i ≤ p) and H i and K i (1 ≤ i ≤ r). We let

..[x n : P n ]u i And for all 1 ≤ i ≤ r, (w u 1 ... u q+i-1 ) has a type which is a product, let (y : U i )V i be this product. We let

Let us prove that the substitution θ ′ is smaller than θ. We have

with γ defined in the algorithm. Then we build the terms to be substituted to the variables h and k. We let

We have θ = θ ′ • σ. Let us prove that the substitution θ ′ is smaller than θ. We have

In both cases, by induction hypothesis, there exists a derivation D of σΓ that denotes θ ′ and [σ]D is a derivation of Γ that denotes θ.

Theorem 2 Completeness

Let Γ be a (non constrained, non quantified) context and P a type well-typed in Γ such that there exists a term t such that Γ ⊢ t : P then there exists a derivation of Γ ′ = Γ[∃x : P ] which denotes the normal η-long form of the proof t. Proof Let t ′ be the normal η-long form of t, and θ = {< x, [ ], t ′ >}. The substitution θ is a normal solution to Γ ′ , so there exists a derivation of Γ ′ that denotes θ.

Efficiency Improvements

To improve the efficiency of this method we have to recognize nodes that cannot lead to success nodes and prune the search tree.

Incremental Partial Checking of Constraints

First we must perform incremental partial checking of the constraints. So we define a function of simplification, which is very similar to the SIMPL function from [START_REF] Huet | A Unification Algorithm for Typed λ-calculus[END_REF] [START_REF] Huet | Résolution d' Équations dans les Langages d[END_REF]. In order to define this function we have to modify a little the syntax of constraints: a constraint is now a triple < δ, a, b > where δ is a context with universal variables only. If Γ = ∆[< δ, a, b >]∆ ′ then the terms a and b must be well-typed and have the same type in ∆δ.

Definition 36 Simplification

We consider only constraints well-typed without the constraints. While there are rigid-rigid constraints in Γ and the simplification has not failed we iterate the process of replacing Γ by Γ

• if a and b are both atomic with the same head variable and they have the same number of arguments, a = (w u 1 ... u p ), b = (w t 1 ... t p ), we let

• in the other cases the simplification fails.

If the simplification fails then the branch is hopeless, it can be pruned.

Using the Flexible-Rigid Constraints

When we have a well-typed flexible-rigid constraint, and we can solve the head variable of the flexible term (i.e. when the head of its type is rigid) we must solve it first, the only candidates for the head variable in an elementary substitution are the bound variables and the head of the rigid term [21] [22]. The other variables lead to unsolvable rigid-rigid constraints.

Using the Flexible-Flexible Constraints

When we have a well-typed flexible-flexible constraint and we can solve one of the head variables, we must solve it first, the constraint does not help to restrict the number of substitutions, but it may become a flexible-rigid constraint the next step. Moreover solving constraints helps to unfreeze types of existential variables and constraints that are not well-typed without the constraints.

Avoiding Splitting

The term (Q (h 1 x 1 ... x n )...(h q x 1 ... x n )) in the definition of the method is atomic, if it is rigid then all the solutions with r-splitting r ̸ = 0 lead to hopless constraints and therefore they can be avoided. In particular in the λΠ-calculus, we never consider existential variables for types or predicates and so splitting can always be avoided.

Solving some Decidable Unification Problems

When we have a constraint well-typed without the constraints which is either a first order unification problem [START_REF] Robinson | A Machine-Oriented Logic Based on the Resolution Principle[END_REF], an argument-restricted unification problem [START_REF] Miller | Unification Under a Mixed Prefix[END_REF] [27], a second order matching problem [START_REF] Huet | Résolution d' Équations dans les Langages d[END_REF] [24] [8] [START_REF] Dowek | Démonstration Automatique dans le Calcul des Constructions[END_REF], a second-order-argument-restricted matching problem [START_REF] Dowek | A Second Order Pattern Matching Algorithm in the Cube of Typed λ-Calculi[END_REF] [9] then we can solve it using always terminating algorithms and apply the substitutions obtained in this way. In a system with such heuristics, the elimination of a first-order universal quantifier is a one-step operation and the elimination of a higher-order universal quantifier is a more complex operation that needs several steps and can lead to backtracking.

Priority to the Rightmost Variable

When we have two existential variables x and y such that y is declared on the right of x and x has an occurrence in the type of y, if both variables may be instantiated then we have to begin with the rightmost. For instance if we have an axiom u : (P n) and we search an integer x such that (P x). We have two existential variables: x : N at and y : (P x). If we instantiate y by u then x will be automatically instantiated by n. But if we begin by instantiating x, we will instantiate x by 0, 1, 2, etc. and fail to prove (P 0), (P 1), (P 2), etc. before we reach x = n.

Normalizing some ill-typed terms

An important improvement of the method would be to recognize some normalizable ill-typed terms and then be able to use the constraints more efficiently. For instance it is possible to prove that if t is a normal η-long term and σ an elementary substitution x ← [x 1 : P 1 ]...[x n : P n ]u where u is a product or an atomic term with a head variable which is a universal variable or a sort (but not one of the x i ), then σt is normalizable.

Extension to The Calculus of Constructions With Universes

Definition 37 The Calculus of Constructions With Universes and Without Cumulativity The Calculus of Constructions With Universes and Without Cumulativity is a pure type system which has an infinite number of sorts : P rop, T ype 0 (= T ype), T ype 1 , T ype 2 , T ype 3 , ..., the axioms P rop : T ype 0 and T ype i : T ype i+1 and the rules < P rop, P rop, P rop >, < T ype i , P rop, P rop >, < P rop, T ype i , T ype i >, < T ype i , T ype j , T ype max{i,j} >

The strong normalization and confluence of βη-reduction for this system are not yet fully proved. But since all the terms typable in this system are typable in the Calculus of Constructions with Universes [START_REF] Th | An analysis of Girard's paradox[END_REF] [25], the β-reduction is strongly normalizable and confluent [3] [25]. It is conjectured in [START_REF] Geuvers | The Church-Rosser Property for βη-reduction in Typed Lambda Calculi[END_REF] that in a pure type system in which the β-reduction is strongly normalizable the βη-reduction also is. Then assuming strong normalization, confluence is proved in [START_REF] Geuvers | The Church-Rosser Property for βη-reduction in Typed Lambda Calculi[END_REF] [30] [START_REF] Th | An Algorithm for Testing Conversion in Type Theory, Logical Frameworks I[END_REF].

In an extension of the method presented here to the Calculus of Constructions With Universes and Without Cumulativity we do not need a M eta type system any more because all the terms we consider in the algorithm in this system are well-typed in this system. More generaly the forumulation of this method for an arbitrary normalizable pure type system T seems to requires only the definition of a M eta type system for T .

In a system which has a large number of sorts, there may be a large number of substitutions of the form σ = x ← γ, t with t = [x 1 : P 1 ]...[x n : P n ]u where u is a sort or a product. For instance, in the Calculus of Constructions With Universes and Without Cumulativity, we can instantiate a variable x : P rop by an infinite number of terms (y : h)(k y) with h : T ype(i) and k : (y : h)P rop. In order to avoid more inefficiencies it seems possible to use sort variables and constraints on these variables as in the method of floating universes [17] [23].

An Incomplete but more Efficient Method

In the example in section 5.2, in order to get the proof (u (A → B) v w) : B we have considered the elementary substitution with 1-splitting p ← (u h 1 h 2 h 3 ) with three applications although the type of u begins by only two products.

Because we have to consider all these possible degrees of splitting, the method is quite inefficient, we get a much more efficient one if we restrict the rule to elementary substitutions with 0-splitting and a number of abstractions ranging from 0 to the number of products of the type of the existential variable we substitute. Let us call this algorithm algorithm with weak splitting (by opposition the previous one can be called algorithm with strong splitting). The search tree of the weak splitting algorithm is finitely branching.

This algorithm with weak splitting cannot synthesize a proof of B, but it can synthesize a proof of A → B. Indeed with the variable p ′ : A → B we perform the substitution

with the types h 1 : P rop, h 2 : (I h 1 ) (remark that we have no abstraction although the type of p ′ begins by a product). The constraint h 1 = A → B suggests the substitution

then we have an existential variable h 2 : (I (A → B)) we perform the substitution

The synthesized proof is (u (A → B) v) : (A → B). Remark that this term is not in η-long form, this form is [w : A](u (A → B) v w) : (A → B).

In both proofs considered above (of B and A → B) the problem is to remark that the variable u of type (P : P rop)((I P ) → P ) must be applied to the proposition (A → B). With the strong


Jean-Loup Bertaux

A revised UV albedo spectrum of Phobos

We present a revised spectral albedo of PHOBOS, collected in the UV (190-310 nm) with SPICAM during several encounters of Mars Express with Phobos.

Introduction

The SPICAM instrument on board Mars Express was used at almost all encounters of Mars Express with Phobos, in order to retrieve the albedo spectrum and try to determine the composition of its soil. Early results in the UV range (180-310 nm) were reported at DPS in 2004 by Perrier et al. (2004). They showed no sign of variation on Phobos, a low albedo , and three broad absorption spectral features at 210-240 nm, 255 and 300 nm.

Reason for revision

However, this early analysis was based on a calibration of SPICAM using observations of the star Delta Scorpii in 2004, and based on its IUE absolute flux. We realized that this star is not appropriate, since it became highly variable since 2001. Therefore, new calibrations were performed on other stars in 2005 and 2009. They show no variation between these dates, but the absolute calibration level and shape is somewhat different.

Results

As a result, the revised albedo spectrum of Phobos is higher by a factor of about two (at ∼ 3%) in the range 200-300 nm; the spectral features have decreased significantly. There is still a significant absorption at 210-240 nm, similar to the well known interstellar dust absorption peak, which has been assigned by some authors to PAH molecules.

.


The invention of turbo codes Claude Berrou claude.berrou@imt-atlantique.fr

The institution where I spent my entire career was called, at its creation in 1977, École Nationale Supérieure des Télécommunications de Bretagne. Today the name is IMT Atlantique. I was recruited as a lecturer as soon as this institution was founded and for about ten years, I devoted myself entirely to teaching semiconductor physics, digital and analog integrated circuits, and microwaves. It was exciting and research did not seem necessary to me, even if of course constant technology survey was indispensable.

In 1988, a colleague I did not know very well asked me for a meeting. He was Alain Glavieux, a recognized expert in digital communications who was working at that time on the improvement of an underwater acoustic video transmission system. This system had already been used to observe the wreck of the Titanic, but its quality needed to be improved.

Alain explained to me in detail what he was proposing to study. The surface receiver contained an equalizer followed by an error-correcting decoder, both functions based on the Viterbi algorithm. But the equalizer could only provide the decoder with binary decisions. I was therefore asked to imagine an equalization circuit, as simple as possible, able to provide the decoder with weighted decisions. These probabilistic data would increase the correction power of the decoder and a gain of about 2 dB could be expected in the link budget.

At that time, the subject was topical and two publications, one by Gérard Battail [START_REF] Battail | Pondération des symboles décodés par l'algorithme de Viterbi[END_REF] and the other by Joachim Hagenauer and Peter Hoeher [START_REF] Hagenauer | A Viterbi Algorithm with Soft-Decision Outputs and its Applications[END_REF] were precious starting points for me. I knew the Viterbi algorithm because I had supervised students in the design of a gate-array integrated circuit on this subject. However, my expertise was still limited.

So here I was, spending days in convolutional code lattices, in the company of probability logarithms and under the double injunction of good performance and simplicity. This work was certainly the most intense of all that I undertook. A convincing result was finally obtained, with the help of my colleague Patrick Adde, and was presented at ICC' 1993 [START_REF] Berrou | A low complexity soft-output Viterbi decoder architecture[END_REF].

This was also the period when some experts were questioning the validity of the limits established by Claude Shannon or, at least, the reasons why they were inaccessible. The best performing code that had been imagined until then was a concatenated code: a Reed-Solomon encoder followed by a convolutional encoder. About three decibels kept it away from the theoretical limit.

Others [4], before me, had observed that the corresponding decoder was suffering from a strong asymmetry. The outer decoder (according to the Berlekamp-Massey algorithm for example) can benefit not only from the redundancy produced by the Reed-Solomon code but also from the work of the inner decoder, and thus indirectly from the redundancy produced by the convolutional code. The reverse is not true: the inner decoder does not benefit from the outer decoder's power of correction.

It seemed to me that this asymmetry could be easily corrected if the Reed-Solomon code was replaced by a second convolutional code. The weighted output Viterbi decoder was now available to implement a near-optimal feedback. A few days were enough to validate this idea and the rest went very quickly: introduction of extrinsic information (the concept had already been introduced in [START_REF] Gallager | Low-density parity-check codes[END_REF], a publication I did not know), invention of recursive systematic convolutional (RSC) codes, replacement of serial concatenation by parallel concatenation. On this last point, the motivation was linked to my intention to concretize this new coding/decoding scheme by an integrated circuit which would be designed in part by my students. Parallel concatenation simplifies considerably the specifications in that only one clock is needed to drive all the elements of the circuit, as opposed to two decoders that work with distinct rates.

Meanwhile, Alain Glavieux and I had become very friendly. One of his doctoral students, Punya Thitimajshima, a Thai national, started to study recursive systematic convolutional codes and made it his main thesis topic. He was also interested in an algorithm that I did not know: the maximum a posteriori (MAP) algorithm [START_REF] Bahl | Optimal decoding of linear codes for minimizing symbol error rate (Corresp.)[END_REF]. Alain and his PhD student pointed out to me that what separated the performance of my new coding/decoding scheme from Shannon's limits could be reduced by replacing the output-weighted Viterbi algorithm with this MAP algorithm. I therefore got interested in it, without being really convinced by the possibility of making a version that could be implemented on silicon. Thus, the patent filed in 1991 on the parallel concatenation of RSC codes and its iterative decoding mentioned the Viterbi decoding with weighted output while the publication, two years later and under the name of turbo code, was based on the MAP algorithm. I salute the memory of Alain and Punya, who were taken from us too soon.

Then came the time of invited conferences and awards. This gave me the opportunity to meet a lot of colleagues, most of whom I was discovering as I was taking my first steps in this vast international coding and communications community. Scientific research is not practiced in a world without relief, fortunately. The diversity of approaches and actors is to be respected and promoted, whether they are experimenters like Marconi or Tesla, or theorists like Poincaré or Einstein. Let us keep in mind what the latter of these great scientists had observed and of which I became convinced: "We can't solve problems by using the same kind of thinking we used when we created them". In this state of mind, interdisciplinarity is a valuable path, albeit a somewhat perilous one, because it is not always fully appreciated by expert committees.


Les résidus pharmaceutiques dans la nappe alluviale du Gave de Pau : de l'état des lieux à la gouvernance de la contamination pour garantir une alimentation en eau potable de qualité

Enzo Lana

To cite this version:

Enzo Lana. Les résidus pharmaceutiques dans la nappe alluviale du Gave de Pau : de l'état des lieux à la gouvernance de la contamination pour garantir une alimentation en eau potable de qualité.

v

  Une situation problématique aujourd'hui : les micropolluants sont responsables de la disparition d'une espèce aquatique tous les dix ans environ et leurs effets sur la santé humaine sont encore mal appréciés (Synteau; INRAE, 2020). v Une pollution diffuse puisque chaque être vivant consommateur de médicaments rejette des métabolites dans le milieu naturel via les fèces et les urines. Introduction Direction: Sylvie Clarimont, Professeur de Géographie, Université de Pau et des Pays de l'Adour, UMR 6031 TREE Doctorant: Enzo Lana, Université de Pau et des Pays de l'Adour, UMR 6031 TREE

-Mixte : quantitative et qualitative -Exploratoire et itérative : des

  ateliers pédagogiques M1 et M2, deux stagiaires et une thèse doctorat pour organiser des allers -retours entre le terrain et l'université.Les résidus pharmaceutiques dans la nappe alluviale du Gave de Pau : de l'état des lieux à la gouvernance de la contamination pour garantir une alimentation en eau potable de qualité

				Projet REMANAP
	Approches et objectifs
			Approche		Origines	Caractériser la
			Analytique	contamination	pollution
	REMANAP :
	Un programme de recherche interdisciplinaire associant des chimistes, des	Approche territoriale	acteurs Modes de gouvernance Degré de sensibilisation des	Elus Gestionnaires Consommateurs Professionnels de santé	Saisir les représentations de l'eau et du médicament
	géographes, des
	économistes et des juristes	Approche comparative		Le cas suisse Le cas suédois	Donner un contrepoint et identifier des
						leviers d'actions
	Méthodologie hybride			Ribérac, La Roche-	Présentation du terrain
					Chalais
						Ø 50 communes
						Ø Proximité du bassin
						industriel de Lacq
	Stage 3 Mois Construction et passation d'un questionnaire test	Master 1 DAST -Atelier de diagnostic Diffusion d'un questionnaire Sphinx online sur le territoire de la CA Pau Béarn Pyrénées	Stage 3 mois Diagnostic de territoire et enjeux santé	5 syndicats producteurs d'eau potable	Ø Une problématique de pollution de la ressource d'origine agricole
	2 nd Semestre	1 er Semestre			2 nd Semestre
	2020	2021			2021
					Thèse E.Lana
				Revue de presse
				Passation entretiens
				semi directifs
				exploratoires
				Approche comparative

Doctoriales Sciences Sociales de l'eau 2021, Sep 2021, Chateauroux, France. . hal-04121642 ---Le territoire du Plan d'Action Territorial du Gave de Pau : Ø 174 000 habitants Ø 1100 agriculteurs Ø Créé en 2008 Ø Il est constitué de Thèse E.Lana Etat de l'art Construction des grilles d'entretiens d'après les 1 er retours de l'enquête quantitative Premier cadrage théorique

v De faibles contrôles, en France, de présence de résidus médicamenteux dans la ressource en eau qui ne permettent pas d'établir spatialement de durée d'impact ou de danger pour la santé humaine. v Des approches en SHS encore assez rares, surtout dans les villes moyennes. v Un parti-pris de la thèse original : via l'analyse des pratiques et du contexte territorial de mieux saisir les représentations de l'eau et du médicament.


teaching and research institutions in France or abroad, or from public or private research centers.