Bruno Barras

Bruno Bernardo

The Implicit Calculus of Constructions as a Programming Language with Dependent Types

In this paper, we show how Miquel's Implicit Calculus of Constructions (ICC) can be used as a programming language featuring dependent types. Since this system has an undecidable type-checking, we introduce a more verbose variant, called ICC * which fixes this issue. Datatypes and program specifications are enriched with logical assertions (such as preconditions, postconditions, invariants) and programs are decorated with proofs of those assertions. The point of using ICC * rather than the Calculus of Constructions (the core formalism of the Coq proof assistant) is that all of the static information (types and proof objects) is transparent, in the sense that it does not affect the computational behavior. This is concretized by a built-in extraction procedure that removes this static information. We also illustrate the main features of ICC * on classical examples of dependently typed programs.

Introduction

Software verification is an ubiquitous problem. Typing discipline has shown to be a decisive step towards safer programs. The success of strongly typed functional languages of the ML family is an evidence of that claim. Still, in those systems, typing is not expressive enough to address problems such as array bound checks (avoiding access out of array bounds which would lead to runtime errors).

Such an issue can be delt with by using dependent types. Dependent ML [START_REF] Xi | Dependent types in practical programming[END_REF] is an extension of SML implementing a restricted form of dependent types. The idea is to annotate datatype specifications and program types with expressions in a given constraint domain. Type-checking generate constraints whose satisfiability is checked automatically. But it is limited to decidable constraint domains since the programmer is not allowed to help the type-checker by providing the proof of the satifiability of constraints. The main point of having restricted dependent types is that it applies to programming languages with non-pure features (side-effects, input/output, etc.).

Much further in the direction of unrestricted dependent types, we find type systems based on the famous Curry-Howard correspondance that expresses the tight relation between programming and proving. In Martin Löf's Type Theory, types can depend not only on a restricted domain, but on arbitrary objects of the theory. Many actively developped proof systems are based on Type Theory, generally extended with primitive inductive datatypes, and other features sometimes borrowed from programming languages. We list only a small number of these: Epigram, Alf, NuPRL and Coq [START_REF]The coq proof assistant reference manual v8.0[END_REF]. Ideas in this article apply directly to the latter, but we expect possible fallouts for other systems.

Paulin and Werner [START_REF] Paulin-Mohring | Synthesis of ML programs in the system Coq[END_REF] show how Coq can be seen as a software verification tool. One typical example in programming with dependent types is that of vectors. In order to statically check that programs never access a vector out of its bounds, its type is decorated with an integer representing its length. This can lead to more efficient programs since no runtime check is necessary. It is also safer since it is known statically that such program never raises an exception nor returns dummy values.

In the Calculus of Constructions (CC, the core formalism of Coq), one defines a type vect parameterized by a natural number and two constructors nil and cons. vect n is the type of vectors of length n (A is the type of the elements).

vect : nat → Set nil : vect 0 cons : Π(n : nat). A → vect n → vect (S n)

For instance the list [x 1 ; x 2 ; x 3 ] is represented as (cons 2 x 1 (cons 1 x 2 (cons 0 x 3 nil))). In fact, the first argument of cons is not intended to be part of the data structure: it is used only for type-checking purposes. The safe access function can be specified as

get : Π(n : nat) (i : nat). vect n → (i < n) → A,
That is, get is a function taking as argument a vector size n, the accessed index i, a vector of the specified size and a proof that i is within the bounds of the vector. Here again, we have two arguments (n and the proof) that do not participate in computing the result, but merely help type-checking.

We can see that programming in the Calculus of Constructions is quite verbose: programs have arguments that are indeed only static information (type decorations, proof objects, dependencies). There exists a procedure called extraction (described in [START_REF] Letouzey | Programmation fonctionnelle certifiée -L'extraction de programmes dans l'assistant Coq[END_REF]) that produces source code for a number of functional languages from intuitionistic proofs. It tries to remove this static information. The decision of keeping or removing an argument is made by the user when he defines a new type. For this purpose, Coq considers two sorts (the types of types) Prop and Set that are almost similar regarding typing, but types of Prop are intended to be logical propositions (like i < n), while types of Set are the actual datatypes (like nat and vect). In the example, the proof argument of get would be erased, but the length n would not.

The extraction approach of Coq has two main drawbacks. Firstly, since it is based on the Prop/Set dichotomy, it is not able to remove dependency arguments that belong to the Set sort (arguments n of cons and get). This could be improved by doing a dead-code analysis, but it would not allow the user to specify a priori arguments that shall not be used in the algorithmic part of the proof. Secondly, extraction is a tool external to the system. This means that within the logic, the programmer deals with the fully decorated term. In situations where datatypes carry proofs to guarantee invariants (see section 4.4 for a typical example), two datastructures may be equal, but containing different proofs. They could not be proven equal.

The Implicit Calculus of Constructions (ICC, see [START_REF] Miquel | The implicit calculus of constructions. extending pure type systems with an intersection type binder and subtyping[END_REF] and [START_REF] Miquel | Le Calcul des Constructions implicite: syntaxe et sémantique[END_REF]) offers a more satifying alternative to the distinction between Prop and Set. It is 1 a Curry-style presentation of the Calculus of Constructions. It features an implicit product that correspond to an intersection type. It allows the quantification over a domain without introducing extra arguments. The main drawback of this system is the undecidability of type-checking. This is mainly because terms do not carry the arbitrarily complex proofs. This means that programs do not carry enough information to recheck them, which is a problem from an implementation point of view. Proving a skeptical third party that a program is correctly typed requires communicating the full derivation.

The main idea of this paper is to introduce a more verbose variant of ICC such that typing is decidable. This is 1 avant : can be seen as made by decorating terms with the implicit information. The challenge is to ensure that this information does not get in the way, despite the fact that it must be maintained consistent when evaluating a term.

The paper is organized as follows: we define a new calculus (ICC * ), and show its main metatheoretical properties. Consistency is established thanks to a sound and complete translation towards a subset of ICC called ICC -. We also introduce a reduction on decorated terms that enjoys subject-reduction, meaning that it maintains decorations consistent. Then we revisit some classical examples and show that a significative part of the expressiveness of ICC is captured. We also discuss several extensions that would make the system more akin to be a pratical programming language.

2 A Decidable Implicit Calculus of Constructions

Syntax

Its syntax is the same that in the standard Calculus of Constructions in Church style, except that we duplicate each operation (product, abstraction and application) into an explicit one and an implicit one. As often in Type Theory, terms and types belong to the same syntactic class, and special constants called sorts represent the types of types.

Definition 1 (Sorts) The set of sorts is S ::= Prop | Type i (i ∈ N) Sorts (Type i ) i∈N denote the usual predicative universe hierarchy of the Extended Calculus of Constructions [START_REF] Luo | An Extended Calculus of Constructions[END_REF]. There is only one impredicative sort, Prop, because the distinction between propositional types and data types will be made when we define a term as being explicit (data types) or implicit (propositional types).

Definition 2 (Terms) The syntax of terms is:

M ::= x | s (s ∈ S) | Π(x : M 1 ). M 2 | λ(x : M 1 ). M 2 | M 1 M 2 | Π{x : M 1 }. M 2 | λ{x : M 1 }. M 2 | M 1 {M 2 }
The second line gathers explicit constructions while the third one gathers implicit constructions. As usual we consider terms up to α-conversion. The set of free variables of term t is written FV(t). Arrow types are explicit nondependent products (T → U stands for Π(x : T ). U when x / ∈ FV(U )). Substitution of the free occurrences of variable

x by N in term M is noted M [x/N ].
Definition 3 (Contexts) Contexts are mappings from variables to types:

Γ ::= [] | Γ; x : M
We write DV(Γ) the set of variables x that are declared in Γ, i.e. such that (x : T ) ∈ Γ for some term T .

Extraction

We define inductively an extraction function M → M * that associates a term of ICC to every term of our calculus. This function removes the static information: domains of abstractions, implicit arguments and implicit abstractions.

Let us first recall the syntax of terms of ICC (see [START_REF] Miquel | Le Calcul des Constructions implicite: syntaxe et sémantique[END_REF] or [START_REF] Miquel | The implicit calculus of constructions. extending pure type systems with an intersection type binder and subtyping[END_REF]) Definition 4 (ICC terms)

M ::= x | s (s ∈ S) | Π(x : M 1 ). M 2 | ∀(x : M 1 ).M 2 | λx.M | M 1 M 2
We write β for the one step β-reduction on ICC terms. As a general rule, we write → h R the head reduction of R (for any relation R, e.g. β), so that reduction occurs in the left subterm of applications (implicit or explicit applications in the case of decorated terms). → R denotes the contextual closure, → * R the reflexive transitive closure of → R , → + R the transitive closure of → R ,and ∼ =R its reflexive, symmetric, transitive closure.

Definition 5 (Extraction)

s * = s x * = x (Π(x : T ). U ) * = Π(x : T * ). U * (Π{x : T }. U ) * = ∀(x : T * ).U * (λ(x : T ). U ) * = λx.U * (λ{x : T }. U ) * = U * (M N ) * = M * N * (M {N}) * = M *
Beware that extraction does not preserve α-conversion for any term. So, many properties of extraction will hold only for well-typed terms2 .

Typing rules

As in the traditional presentation of Pure Type Systems [START_REF] Barendregt | Lambda Calculi with Types[END_REF], we define two sets Axiom ⊂ S 2 and Rule ⊂ S3 by

Axiom = {(Prop, Type 0 ); (Type i , Type i+1 ) | i ∈ N} Rule = {(Prop, s, s); (s, Prop, Prop) | s ∈ S} ∪{(Type i , Type j , Type max(i,j) ) | i, j, ∈ N}
We will also consider these two judgements:

• the judgement Γ that means "the context Γ is wellformed"

• the judgement Γ M : T that means "under the context Γ, the term M has type T ". By convention, we will implicitly α-convert M in order that DV(Γ) and the set of bound variables of M are disjoint.

Definition 6 (Typing judgements) They are defined in figure 1.

They are very similar to the rules of a standard Calculus of Constructions where product, abstraction and application are duplicated into explicit and implicit ones. There are though two important differences:

• in the (I-LAM) rule, we add the condition x / ∈ FV(M * ) (variables introduced by an implicit abstraction cannot appear in the extraction of the body), so x is not used during the computation. This excludes terms like λ{x : T }. x.

• In the (CONV) rule we replace the usual conversion (it would be ∼ =β ie ) by the conversion of extracted terms.

This last modification completely changes the semantics of the formalism. Despite of being apparently very close to the Calculus of Constructions, it is in fact semantically much closer to ICC (usual models of CC do not validate the (CONV) rule). Before developping the metatheory of our system, we shall make some precisions on the subset of ICC we are targetting.

Definition 7 (Typing rules of ICC -) See figure 2.

In comparison to ICC as presented in [START_REF] Miquel | The implicit calculus of constructions. extending pure type systems with an intersection type binder and subtyping[END_REF], we made the following restrictions:

• we removed η-reduction and the rules related to subtyping (rules CUM and EXT), to make things simpler, but we consider extending our system with these rules (or equivalent ones);

• we also removed rule (STR) for quite different reasons.

In our formalism, non-dependent implicit products are intended to encode preconditions of a program: a proof of Π{_ : P }. Q yields a program with specification Q provided you can produce a proof of P ; but the strengthening rule makes this type equivalent to Q. So this rule would not require a proof of P prior to using a program with specification Q.

Proposition 1 (Soundness of extraction) Obviously, the completeness results regarding typing does not hold for the full ICC system, since the removed rules (subtyping and strengthening) are clearly not derivable. But we can show the completeness w.r.t. ICC -.

(i) Γ ⇒ Γ * ICC - (ii) Γ M : T ⇒ Γ * ICC -M * : T * Proof.

Proposition 2 (Completeness of extraction)

For any derivable judgement Γ ICC -M : T , there exists ∆, N and U such that

∆ N : U ∧ ∆ * = Γ ∧ N * = M ∧ U * = T
Proof. This property relies mostly on the context conversion result. The proof is a bit tedious but is not difficult.

Consistency

Consistency of ICC * is an easy consequence of consistency of ICC -[10] and of Lemma 3 (Soundness of extraction).

Proposition 3 (Consistency)

There is no proof of the absurd proposition. There exists no term M such that the fol-

Γ ICC -M : U [x/N ] (INST) Γ ICC -M : T Γ ICC -T : s T ∼ =β T Γ ICC -M : T (CONV)

Reduction rules for decorated terms

We consider two kinds of β-reduction, whether related to explicit or implicit terms.

It is important to note that these reduction rules are not necessary to the definition of our calculus. However, they play an important role for the decidability of type-checking since they provide a way to find a decorated and well-typed term in weak head normal form.

Definition 8 (β-reduction) The explicit β-reduction or β ereduction, and the implicit β-reduction or β i -reduction, are defined by

(λ(x : T ). M ) N βe M [x/N ] (λ{x : T }. M ) {N} βi M [x/N ]
We define then the β-reduction by βie = βe ∪ βi .

We have the following result: The proof is quite long although not difficult. It follows the same pattern as in the standard Calculus of Constructions.

Decidability of type inference

As usual, decidability of type-checking requires the decidability of type inference. In our case, we can consider two kinds of type inference: inferring a decorated term or a term of ICC -. The second one is enough for decidability of type-checking, but from implementation purposes, it is desirable to have the former. This raises the problem of inferring the type of an application. For this, we compute the weak head normal form (w.r.t. β ie ) of type of the function to check if it reduces to a product. If so, using subject reduction and soundness of β ie we prove that the function is typed by the computed product. If not, we need a completeness result saying that if a type is equivalent to a product, then it β ie reduces to a product.

We need some preliminaries in order to introduce a type inference algorithm.

Lemma 4 (Normalization of → h

βi ) Let M be a well-typed term of ICC * . There exists a term N in β i weak head normal form (WHNF) such that M → * βi N .

Proof. Intuitively, this is because β i substitutes variables introduced by an implicit abstraction, and such variables are not allowed to appear in the head of the term.

Lemma 5 (Completeness of β ie -reduction) Let M be a well-typed term of ICC * and N be a term of ICC such that M * → β N . There exists a term N of ICC * such that N * = N and M → + βie N .

Proof. We proceed as in Lemma 3.4 of [START_REF] Miquel | Arguments implicites dans le calcul des constructions: étude d'un formalisme à la curry[END_REF] except that we only need the fact that → h βi terminates.

Proposition 5 (Existence of a β ie -WHNF) For every well-typed term M of ICC * there exists a term N in β ie -WHNF such that M → * βie N .

Proof. Let N be the normal form of M * . (ICC is strongly normalizing cf [START_REF] Miquel | Le Calcul des Constructions implicite: syntaxe et sémantique[END_REF]). By lemma 5, we have a term M 0 such that M → * βie M 0 with M * 0 = N . Then, by lemma 4, there is a term N in β i -WHNF such that M 0 → * βi N and N * = N (lemma 3). N is also in β e -WHNF otherwise its extracted term would not be in normal form. So N is a reduct of M in WHNF.

Proposition 6 (Decidability of type inference)

There exists a sound, complete and terminating type inference algorithm.

This algorithm receives as an input a well-founded context Γ and a term M , and returns either false or a decorated term T such that Γ M : T .

Proof. The cases of variable and sort are trivial. Cases of abstractions and products are not very tough either because we can decide in ICC whether we have or not T * ∼ =β s. We already explained how to deal with the application cases.

Examples

Our long term goal is to design a formalism dedicated to software verification. In this section, we develop several examples that illustrate the features of our formalism such as programming with dependent types, datatype invariants, pre/post-conditions. Short of having datatypes as in the Calculus of Inductive Constructions, we use impredicative encodings.

In the following examples, when the type of variables is obvious, we shall not write them (as in λx {y}. Πz. M ).

vect := λm. Π{P : nat → Prop}. P 0 → (Π{n}. A → P n → P (S n)) → P m nil := λ{P} f g. f cons {n} x v := λ{P} f g. g {n} x (v {P} f g)

append : Π{n 1 } {n 2 }. vect n 1 → vect n 2 → vect (n 1 + n 2 ) := λ{n 1 } {n 2 } v 1 v 2 . v 1 {λn . vect (n + n 2 )} v 2 (λ{n } x v . cons {n + n 2 } x v )

Vectors

Miquel showed how lists and vectors can be encoded in ICC [START_REF] Miquel | The implicit calculus of constructions. extending pure type systems with an intersection type binder and subtyping[END_REF]. We adapt his example to ICC * (see figure 3). It consists in merging definitions of vectors in ICC and CC: the definitions of CC have to be decorated with implicit/explicit flags as in ICC. Note that vect and P are explicit functions since we want to distinguish vectors of different lengths. But P itself is implicit since it is only used to type the other two arguments, which correspond to constructors.

The reader can check that by extraction towards ICC, these definitions becomes strictly those for the untyped λcalculus:

nil * = λf g. f cons * = λx v f g. g x (v f g)
Here, cons * has arity 2 (if we consider it returns vectors), and there is no extra argument P .

Concatenation of two vectors can be expressed easily if we assume that addition satisfies 0 + n ∼ =β n and (S n) + m ∼ =β S (n + m), which is the case for the usual impredicative encoding of natural numbers.

In the Calculus of Constructions, computing the length of a vector is useless since a vector always comes along with its length (either as an extra argument or because it is fixed). In ICC * , when we decide to make the length argument implicit, it cannot be used in the explicit part of the program. For instance, it is illegal to define the length of a vector as λ{n} (v : vect n). n. It has to be defined as recursive function that examines the full vector.

We hope we made clear that in many situations, the Implicit Calculus of Constructions allows to have the safety of a dependently typed λ-calculus, but all the typing information (here P and the vector size) does not get in the way, since objects are compared modulo extraction.

Equality

As already shown by Miquel, Leibniz equality can be defined by impredicative encodings (see figure 4) in ICC, and adapting it to ICC * is straightforward. Let us remark that x is not needed to produce a proof of x = x. The elimination rule eq_ind allows to derive the usual theory of equality such as symmetry and transitivity, etc.

In the example of append above, we avoided many troubles because addition was defined a particular way. If it had been defined for instance by induction on the second argument, then types vect n 2 and vect (0 + n 2 ) would not be convertible. However, it is possible to prove them equal, we should be able to use such a proof to "change" one type for the other. Definition eq_ind allows that, but it raises the issue that the equality proof has to be explicit. We would like to avoid this situation because it makes the computational behavior of the extracted term depend on logical proofs.

In order to fix this, we can think of having a stronger elimination principle eq_ind2 where the equality proof is also implicit. In ICC, such axiom is problematic since it is equivalent to ∀x y, x = y, which is not inconsistent per se, but it is incompatible with most useful extensions, e.g. assuming 0 = 1. Anyway, in the restricted calculus (ICC -), this axiom is validated by the model of ICC -in Miquel's thesis. Furthermore, since the denotation of the type of eq_ind2 contains the identity λx. x, it is also valid to add axiom eq_ind2_elim. 3 There is, to our knowledge, no easy way to turn this equality into a reduction rule, since x, y and p are all implicit arguments, without losing the Church-Rosser property.

Predicate subtyping a la PVS

One key feature of PVS [START_REF] Owre | The formal semantics of PVS[END_REF] is its allows predicate subtyping, which corresponds to the comprehension axiom in set theory. For instance, one can define the type of even number as a subtype of the natural numbers satisfying the appropriate predicate. When a number is claimed to have this type, it had to be proven it is actually even, and a typechecking condition (TCC) is generated.

In the Calculus of Constructions, this can be encoded as a dependent pair formed by a natural number and a proof object that it is actually even. The coercion from even numbers to numbers is simply the first projection. This encoding is not faithfull since it might happen that there exists two eq := λA x y. Π{P : A → Prop}. P x → P y refl : Π{A} {x}. eq A x x := λ{A} {x} {P} (H : P x). H : eq_ind :

Π{A} {x} {y} (p : eq A x y) {P : A → Prop}. P x → P y := λ(p : eq A x y) p {P} H. p {P} H eq_ind2 :

Π{A} {x} {y} {p : eq A x y} {P : A → Prop}. P x → P y eq_ind2_elim :

Π{A} {x} {p} {P} a. eq (P x) (eq_ind2 {A} {x} {x} {p} {P} a) a 4 (let us call them π 1 and π 2 ) of the fact that, say, 4 is even. Then (4, π 1 ) and (4, π 2 ) and distinct inhabitants of the type of even numbers while they represent the same number. In ICC * , this issue can be avoided by making the second component of the pair implicit. 5 Let us define Even as:

Π{P : Prop}. (Π(n : nat) {H : even n}. P ) → P

The coercion can then be defined as the first projection:

λ(x : Even). x {nat} (λn {H}. n) : Even → nat
and the equalities such as (4, π 1 ) = π 2 ) is proven by reflexivity.

Subtyping coercions

In ICC, vectors are subtypes of lists. Here, we have no subtyping but we can easily write a coercion from vectors to lists (defined as Π{P : Prop}. P → (A → P → P ) → P ):

λ(v : vect n) {P} f g. v {λ_. P} f λ{n} x v. gxv has type vect n → list.
Remark that the extraction of this coercion is λv f g.v f (λx v.g x v), which η-reduces to the identity.

Another illustration of the expressiveness of ICC is the example of terms indexed by the set of variables (var denotes the type used to represent variables): term := λ(s : var → Prop). Π{P : Prop}.

(Π(x : var). {s x} → P ) → (P → P → P ) → P It corresponds to a type with two constructors: one of type Π{s : var → Prop} (x : var). {s x} → term s to build variables, and the second of type Π{s : var → Prop}. term s → term s → term s to build applicative terms.

If set s is included in set s (i.e. there is a proof h of Πx. s x → s x), then any term of term s can be seen as a term of term s . This can be done by the following function that recursively goes through the term to update the proofs:

lift : term s → term s := λt {P} f g. t {P} (λx {H}. f x {h x H}) (λt 1 t 2 . g t 1 t 2 )
We can notice that, as previously, the extraction of this term η-reduces to the identity. This is no coincidence since in ICC, vectors are a subtype of lists and term s is a subtype of term s , and Miquel proved that if M has type T in ICC, there is a derivation that there exists a term M that (1) has type M without using rule (EXT) (thus there exists a term of ICC * that extracts to M ) and ( 2) M η-reduces to M .

We conclude that adding η-reduction to our system would be of great interest. It would be very natural to introduce a notion of coercion: terms which extraction reduces to the identity. In cases where we manipulate extracted terms (for instance in the conversion test), then coercions can be dropped. On the other hand, for reduction of decorated terms, coercions can be used to update the implicit subterms of its argument.

Euclidean division

This example illustrates how to encode programs with preconditions and postconditions. Euclidean division can be expressed as a primitive recursive function, following this informal algorithm: div a b := if a = 0 then (0, 0) else let (q, r) := div (a -1) bin if r = b -1 then (q + 1, 0) else (q, r + 1)

One would like to specifiy that if b is not 0 (precondition), then div a b returns a pair (q, r) such that a = bq + r ∧ r < b (α) (postcondition). To express the result, we define a type diveucl, parameterized by a and b that encodes pairs (q, r) that satisfy (α). More precisely, it is a triple made of 2 explicit components of type nat and an implicit proof of (α) (this is instance of the predicate subtyping scheme, section 4.3). See figure 5 The program can then be written without difficulty (figure 5) by adapting the proof made in the Calculus of Constructions, assuming nat_elim to define programs by recursion on a natural number and eq_nat_elim to decide if two numbers are equal. The point of using ICC * is that div actually behaves as the informal algorithm. Within CC, div is a function of arity 3 returning a triple. So if we have two distinct proofs P 1 and P 2 of b = 0, (div a b P 1 ) and (div a b P 2 ) reduce to triples (q, r, f (P 1 )) and (q, r, f (P 2)) respectively, for some f . The two proofs f (P 1 ) and f (P 2 ) of the postcondition (α) have no particular reason to be equal.

div_elim {k} {b} div k {diveucl (S k) b} (λq r {H 0 }. eq_nat_elim r (b -1) {diveucl (S k) b} (λ{H 1 }. div_intro {S k} {b} (S q) 0 {π 2 H 0 H 1 }) (λ{H 1 }. div_intro {S k} {b} q (S r) {π 3 H 0 H 1 }))) where: π 1 : b = 0 → 0 = b.0 + 0 ∧ 0 < b π 2 : k = bq + r ∧ r < b → r = b -1 → Sk = b(q + 1) + 0 ∧ 0 < b π 3 : k = bq + r ∧ r < b → r = b -1 → Sk = bq + (Sr) ∧ Sr < b
Not only this is solved by ICC * , but furthermore, (div 17 5 {P 3 }) is convertible to (div 11 3 {P 4 }) since the quotient and remainder of both divisions are equal. This is not the case in CC (even assuming proof-irrelevance) since div_intro also depends on the inputs a and b.

Ongoing and Future work

We have shown that the Implicit Calculus of Constructions provides a simple yet powerful way to write dependently typed programs and proof-carrying programs where specifications and proofs do not interfere with the computational content. However there are still aspects that are not completely satisfactory.

Heterogeneous equality

As often in type theory, equality is among the most difficult features to design. Leibniz equality allows to compare only objects of the same type, which is a bit restrictive since in our system, comparing objects of different types is not a concern: only the behavior of their extracted form matters. It would be nice to see how an heterogeneous equality can be integrated to ICC * , for instance to have elimination like eq_ind2_elim, but not restricted to reflexivity proofs.

McBride [START_REF] Mcbride | Dependently Typed Functional Programs and their Proofs[END_REF] has extensively studied an heterogeneous equality (he used to call John Major Equality), and he implemented it in Epigram [START_REF] Mcbride | The view from the left[END_REF].

Inductive Types

Most of the ideas extend straightforwardly to inductive types, by analogy with their impredicative encoding. Of course, inductive types are more expressive: injectivity and discrimination of constructors, dependent elimination schemes cannot be derived with the impredicative encodings. However, we believe that these principles do not conflict with the implicit arguments.

Implementation

We are implementing this system as an alternative version of Coq. Despite the fact that the formalism is quite different from the one implemented by Coq (the models are completely different), the cost of its implementation seems amazingly low: the type of terms has to be slightly changed (to duplicate product, abstraction and application into implicit/explicit pairs). But then the code is adapted straightforwardly since the type-checking algorithm is almost the same.

Related works Epigram

McBride and Alternkirch have designed the Observational Type Theory [START_REF] Altenkirch | Towards observational type theory[END_REF], and this theory is implemented in Epigram 2. Some efforts have been made to make the theory less verbose. In [START_REF] Brady | Inductive families need not store their indices[END_REF], it is shown how vector length can be removed from constructors. However, only information that is uniquely recoverable can be erased. For instance, in the example of terms with their set of variables, the proof that variables belong to the set cannot be made implicit.

Proof-irrelevant Calculus of Constructions

Werner [START_REF] Werner | On the strength of proof-irrelevant type theories[END_REF] introduces a variant of the Calculus of Constructions where objects of the Prop kind can be erased. His idea is very similar to ours since he modifies conversion so that proofs of a given proposition are always convertible. On the one hand, this does not require a complicated model since proof-irrelevance is a valid property in the classical model of the Calculus of Constructions [START_REF] Miquel | The not so simple proofirrelevent model of CC[END_REF]. On the other hand, this approach does not address the problem of other extra arguments (types, domains of abstractions, dependencies belonging to Set).

Subset Types

In [START_REF] Sozeau | Subset coercions in Coq[END_REF], Sozeau introduces a feature similar to the predicate subtyping of PVS. Like in this article, it is encoded thanks to a dependent pair made of an object and a proof that this object satisfies the predicate. In his method, he shows that proofs do not get in the way by forbiding writing programs that depend on the second part of the pair. The latter can be used only to build a proof appearing as a second part of another pair. However, it is not clear that his method would help hiding the proofs in the example of terms carrying their set of variables.

Anyway, he added to Coq a feature that allows a phase distinction between programming and proving properties, like PVS' TCC. Our approach could take advantage of it.

Conclusion

We have shown how a restriction of the Implicit Calculus of Constructions can be turned into a implementable system, and we developped several typical examples. We shall stress on the fact that some problems seem less difficult to deal with than in most type systems implemented so far. Now, it remains to see if we can capture a bit more of the expressiveness of ICC while keeping a decidable typechecking.

1

  inria-00429543, version 1 -3 Nov 2009Author manuscript, published in "FoSSaCS, Budapest : Hungary (2008)"

  By mutual structural induction on the derivations of Γ and Γ M : T . To each rule of ICC * correspond an equivalent rule of ICC -. For rules (E-APP) and (I-APP), we use the substitutivity of extraction ((M [x/N ]) * = M * [x/M * ]) which holds for well-typed terms.

Figure 2 .

 2 Figure 2. Typing rules of ICC -

Lemma 3 (Proposition 4 (

 34 Soundness of the β ie -reduction) We have for well-typed terms:M → βie N ⇒ M * → * β N * Note that β i -reductions are not translated: if M → βi N , then M * = N * . Subject reduction) If Γ M : T and M → *βie M then we have Γ M : T .

Figure 3 .

 3 Figure 3. Vectors

Figure 4 .

 4 Figure 4. Equality

  for the types of nat_elim : Π(n : nat) {P : nat → Prop}. P 0 → (Πk. P k → P (S k)) → P n eq_nat_elim : Πm n {P : Prop}. (Π{H : m = n}. P ) → (Π{H : m = n}. P ) → P diveucl : nat → nat → Prop div_intro : Π{a} {b} q r {H : a = bq + r ∧ r < b}. diveucl a b div_elim : Π{a} {b} {P : Prop}. diveucl a b → (Πq r {H : a = bq + r ∧ r < b}. P ) → P div := λ(a b : nat) {H : b <> 0}. nat_elim a {λa. diveucl a b} (div_intro {0} {b} 0 0 {π 1 H}) (λk (div k : diveucl k b).

Figure 5 .

 5 Figure 5. Euclidean division

For instance, (λ{x : T }. x) * depends on the name of the binder.

MetatheoryUnlike ICC, the basic metatheory can be proven just like for PTSs (see for instance[START_REF] Barendregt | Lambda Calculi with Types[END_REF]). This is due to the fact that it relies heavily on the form of the typing rules, but very little3 inria-00429543, version 1 -3 Nov 2009 [] (WF-E) Γ T : s x / ∈ DV(Γ) Γ; x : T (WF-S) Γ (s 1 , s 2 ) ∈ Axiom Γ s 1 : s 2 (SORT) Γ (x : T ) ∈ Γ Γ x : T (VAR) Γ T : s 1 Γ; x : T U : s 2 (s 1 , s 2 , s 3 ) ∈ Rule Γ Π(x : T ). U : s 3 (E-PROD) Γ; x : T M : U Γ Π(x : T ). U : s Γ λ(x : T ). M : Π(x : T ). U (E-LAM) Γ M : Π(x : T ). U Γ N : T Γ M N : U [x/N ] (E-APP) Γ T : s 1 Γ; x : T U : s 2 (s 1 , s 2 , s 3 ) ∈ Rule Γ Π{x : T }. U : s 3 (I-PROD) Γ; x : T M : U Γ Π{x : T }. U : s x / ∈ FV(M * ) Γ λ{x : T }. M : Π{x : T }. U (I-LAM) Γ M : Π{x : T }. U Γ N : T Γ M {N} : U [x/N ] (I-APP) Γ M : T Γ T : s T * ∼ =β T * Γ M : T (CONV)Figure 1. Typing rules of ICC * on the nature of conversion. We first prove inversion lemmas. They allow us to characterize the type R of judgment Γ M : R according to the nature of the term M . Other important properties are substitutivity and context conversion.Lemma 1 (Substitutivity) The following rule is derivable:Γ 1 M 0 : T 0 Γ 1 ; x 0 : T 0 ; Γ 2 M : T Γ 1 ; (Γ 2 [x 0 /M 0 ]) M [x 0 /M 0 ] : T [x 0 /M 0 ]Lemma 2 (Context conversion) Typing is preserved by well-typed conversion in the context:Γ M : T ∧ Γ * ∼ =β ∆ * ∧ ∆ ⇒ ∆ M : T3.1 Preservation of the theoryIn this section, we prove that ICC * is equivalent to ICC -. That is, any derivation in ICC * has a counterpart in ICC - and vice versa. First, it is easy to show that any derivation of ICC * can be mapped into a derivation in ICC -:

inria-00429543, version 1 -3 Nov 2009[] ICC - (WF-E) Γ ICC -T : s x / ∈ DV(Γ) Γ; x : T ICC - (WF-S) Γ ICC -(s 1 , s 2 ) ∈ Axiom Γ ICC -s 1 : s 2 (SORT) Γ ICC -(x : T ) ∈ Γ Γ ICC -x : T (VAR) Γ ICC -T : s 1 Γ; x : T ICC -U : s 2 (s 1 , s 2 , s 3 ) ∈ Rule Γ ICC -Π(x : T ). U : s 3 (EXPPROD) Γ ICC -T : s 1 Γ; x : T ICC -U : s 2 (s 1 , s 2 , s 3 ) ∈ Rule Γ ICC -∀(x : T ).U : s 3 (IMPPROD) Γ; x : T ICC -M : U Γ ICC -Π(x : T ). U : s Γ ICC -λx.M : Π(x : T ). U (LAM) Γ ICC -M : Π(x : T ). U Γ ICC -N : T Γ ICC -M N : U [x/N ] (APP) Γ; x : T ICC -M : U Γ ICC -∀(x : T ).U : s x / ∈ FV(M )Γ ICC -M : ∀(x : T ).U (GEN)Γ ICC -M : ∀(x : T ).U Γ ICC -N : T

Thanks to Alexandre Miquel for pointing out these two facts.

Proof-irrelevance is not provable in CC, nor in Coq

Note that this does not work in ICC because of the strengthening rule.


B Dacre

T Sim

Free Space Representation for a Mobile Robot moving on a Rough Terrain

This paper addresses the problem of autonomous navigation for mobile robots on rough terrains 1 . We propose a free space structuring as a promising way to improve the e ciency of path planning for all-terrain mobile robots. This space structuring is based on the characterization of con guration space regions for which the locomotion architecture can guarantee terrain irregularities absorption and stability of the vehicle.

A planner based on this approach has been implemented and experimental results show its interest for practical use.

Introduction

There is an increasing interest in developping mobile robots for applications requiring autonomous navigation on natural terrains (planetary exploration 4] 5] 11], public safety robotics and other hazardous missions 7] 8]). This paper addresses the path planning problem for such all-terrain mobile robots.

Research in motion planing has been very active over the past decade. Most of the work has addressed the problem of nding a collision-free path for manipulators or for mobile robots moving in planar environments (see 6] for an overview). This problem is usually solved by a decomposition of the con guration space into networks of free regions. Graph search techniques and heuristics are then used to search a path from which a safe sequence of motions can be computed.

However, motion planning is almost inexistent in the litterature for mobile robots moving on non-planar terrains. There already exists all-terrain mobile robots which use simple path generation techniques for their autonomous navigation. These approches use the terrain model to characterize the traversability of small terrain patches (roughness of the patch, preferred crossing direction,. . .). In 4] 9], paths are computed from this characterization by gradient propagation techniques. The AMR robot 7] uses a 2D pathplanner similar to the one presented in 2] to plan a path that avoids the patches classi ed as obstacle.

These simple techniques are certainly su cient for the case of benign terrains. However, they will fail to nd a safe path for a robot moving on a rough terrain: in this case, the binary notion of obstacles and non obstacles regions does not hold anymore; the obstacles depend on the ability of the robot to cross over the irregularities of the terrain and their characterization requires to better formalize the constraints acting on the placement of the robot on the terrain.

We are aware of a very few contributions that consider this rather new topic of the path planning problem. A geometric 3D planner is described in 10] for the case of a 3-wheels robot moving on a polygonal terrain. This planner produces paths which not only satisfy collision-free constraints, but also stability and non-holonomic constraints. This planning technique is derived from the approach described in 1] for the planar case; it consists of exploring a discretized representation of the Con guration Space to incrementally search for a safe trajectory. A similar formulation of the problem is reported in 8] for the Intelligent Locomotion of a four tiltable track robot. As mentionned by the authors, this incremental search of a safe trajectory can be very time consuming and we feel that having a preprocessing step aimed at discovering the \good" CS-regions could be used to better guide a more complex path-planning method.

The main contribution of this paper is to produce such a preprocessing. We provide a characterization of the CS-regions for which the locomotion architecture of the robot can guarantee terrain irregularities absorption and stability of the vehicle.

The paper is organized as follows: After a presentation of the robot and terrain models, Section 2 gives a more formal statement of the placement problem and of the constraints acting on the placements of the robot. Section 3 presents an algorithm that characterizes the admissibility of a given CS-region. Finally, Section 4 combines these results to obtain an octree representation of these admissible regions. The algorithm have been implemented and experimental results are presented at the end of the section.

2 Formalization of the placement problem.

2.1 General statement.

We consider an articulated robot consisting of a body and n wheels attached to it by suspensions. These suspensions allow the wheels to keep a better contact to the terrain, but on the other hand, the placement of the robot becomes complex : it results from the interaction with the terrain and the balance of the suspensions, which are modeled by springs.

The terrain is known by a discrete elevation map, that is the elevation values z on a discrete regular grid in (x; y).

In the sequel, we consider that 3 conditions are required for a placement to be valid : (C1) all the wheels remain in contact with the ground. (C2) the springs cannot be stretched beyond some limit length. (C3) the robot does not tip-over, which requires that the projection of its gravity center remains inside the convex hull of the projections of all the contact points (called the support polygon). Our purpose is to determine domains of the con guration space which verify these conditions.

The placement parameters.

Let us de ne a local frame (G; u; v; w) attached to the robot, where G is the gravity center of the robot, and (u; v; w) are respectively its longitudinal, lateral and vertical axis (see Fig. 1).

We assume that, when all the springs are in their steady state, the wheels belong to the same plane P S perpendicular to w axis, at height w 0 in the local frame. Then, the coordinates of wheel i are (u i ; v i ; w 0 + l i ) where u i and v i are some xed values related to the geometry of the robot, and l i is

v w u G M 0 v i u i w o l i s
Figure 1: Model of the vehicle the algebraic extension of the spring (l i = 0 being its natural length). That means that the springs always keep a vertical orientation in the robot's frame. Additionally, we assume that the positions (u i ; v i ) of the wheels are symmetrically distributed around the vehicle. Fig. 1 shows an example of a 6-wheels robot, with the parameters detailed above.

A position of the robot's body is de ned by the 6-dimensional vector p = (x G ; y G ; z G ; ; ; ), where (x G ; y G ; z G ) are the coordinates of point G, and ( ; ; ) are respectively the horizontal orientation of u axis, the roll angle and the pitch angle2 . These parameters de ne the transform matrix from the robot frame to the space frame (O; x; y; z):

M(p) = T(x G ; y G ; z G )R(w; )R(v; )R(u; ):
Therefore, a complete placement of the robot is given by (6 + n) independant parameters : the 6-dimensional vector p = (x G ; y G ; z G ; ; ; ) de ning the position of the robot's body in the space, and the n spring extensions l i , giving the wheel positions.

Nevertheless, the interactions with the terrain constrain these parameters and therefore reduce the dimension of the robot's con guration space. This will be developped in the next section.

De nition of the con guration space.

The placement of the robot results from its weight and the reaction of the ground exerted through the springs.

The static equilibrium state is reached when the total energy of the robot is minimized. In the following, we consider a simple energy function, including only the compression energy of the springs: E((l i ) i=1:::6 ) = 6 X i=1 kl i 2 :

(1

)
where k is the sti ness coe cient of the springs. Moreover, the wheels are supposed to stay over the terrain, which constrains their positions. Let z = f(x; y) be an analytic expression of the terrain, the free space being the set of points such that z > f(x; y). The position of wheel i is de ned by the position p of the robot's body and the length l i of its spring. We call W i (p; l i ) the volume occupied by the wheel. The placement of wheel i is strictly expressed as : 8M(x; y; z) 2 W i (p; l i ); z f(x; y):

In order to keep a simple constraint expression, we approximate the wheel's shape by a point 3 denoted M i (x i ; y i ; z i ). Hence the constraint is only applied to this contact point M i . Moreover, we are only interested in the placements which keep all the wheels in contact with the terrain (condition C1). Therefore, the contact constraints become :

z i = f(x i ; y i ) (2)
where x i ,y i and z i are related to the placement p and to the length l i by: (x i ; y i ; z i ) T = M(p)(u i ; v i ; w 0 + l i ) T For given values of the three parameters (x G ; y G ; ), the remaining parameters (z G ; ; ; (l i ) i=1:::6 ) result from the minimization of energy (1) under equality constraints (2). Thus we consider the three dimensional con guration space induced by the parameters (x G ; y G ; ). Any con guration de nes the placement of the robot as follows :

De nition 1 For any con guration q = (x G ; y G ; ) 2 CS = R 2 S 1 , the associated placement of the robot is the set of parameters (p; (l i ) i=1:::n ) such that :

E((l i ) i=1:::n ) is minimal. 8i 2 1; n]; z i = f(x i ; y i ).

The admissible con gurations.

There remains to link together the requirements C2 and C3 de ned in section 2.1 and the con guration parameters (x G ; y G ; ). [START_REF] Barraquand | Robot Motion Planning: A distributed Representation Approach[END_REF] or by a sphere, with an appropriate change of function f, which corresponds to growing the terrain by the radius of the wheels.

Constraint C2 limits the n spring elongations l i to a given value denoted L max . According to constraint C3, the robot is stable when the vertical projection of its gravity center belongs to the support polygon. The shape of this support polygon is clearly a function of , and the lengths (l i ) i=1:::n . However, we assume that the less stable position is obtained when all the springs are the longest [START_REF] Faverjon | Object Level programming of industrial robots[END_REF] . The stability thus only depends on and , and we can determine a subset S ] 2 ; 2 2 such that for any pair ( ; ) 2 S, the robot position is stable.

We can now de ne precisely the admissible space of the robot.

De nition 2

The admissible subset ACS is the set of con gurations q 2 CS such that : 8i 2 1; n]; jl i j L max .

( ; ) 2 S.

In the remaining, we propose a method to built a hierarchical decomposition of ACS relying on the analysis of the admissibility of a domain x y in CS.

3 Admissiblity of a CS region.

We consider now a region R CS = x 1 ; x 2 ] y 1 ; y 2 ] 1 ; 2 ] CS. Our purpose is to determine if the region R CS is in ACS or not.

Overview.

Similarly to the con guration vector q, we de ne the vector r of the remaining placement parameters : r = (z G ; ; ; (l i ) i=1:::n ).

Let r 0 be a domain which is guaranteed to contain any admissible placement. For example, l i necessarily belongs to l i = L max ; L max ].

For any wheel i, we can determine the area in the 3-dimensional natural space of all its positions for all placements in R CS r 0 . The vertical projection of this area gives an (x; y)-region called contact region R i . The contact of the wheel onto the terrain belongs to the set of points (x; y; z) of the terrain such that (x; y) 2 R i . The elevation map is used to compute a sort of bounding box of this terrain portion, called contact envelope V i (cf Section 3.2).

The de nition of a placement given in Section 2.3 establishes relations between the placement parameters and the elevation of the terrain. These relations allow to deduce a new placement interval r from the contact envelopes (cf Section 3.3). The thicker the envelopes are, the larger are the parameter intervals r.

For this reason, the contact envelopes must be as close as possible to the terrain.

The obtained placement domain R CS r necessarily contains all the possible placements of the robot in region R CS , whatever the terrain's shape inside the contact envelopes. If this interval is in accordance with the constraints C2 and C3, R CS is guaranteed to be in ACS. Otherwise, we consider that the region R CS could contain placements which would not verify the constraints, and we declare R CS to be forbidden.

The contact envelopes.

In this section, we show how to compute, for each wheel, the terrain envelope where the contact should occur. We rst determine an average plane P a from the points of the terrain over all the contact regions. Then we compute for each wheel the limit values of the terrain elevation relatively to plane P a .

3.2.1 The contact regions (R i ) i=1:::n .

We rst consider the in uence of , and (l i ) i=1:::n . Let (G 0 ; u 0 ; v 0 ) be the horizontal frame obtained from the vertical projection of (G; u; v),(see Fig. 2). In this frame, the vertical projection of wheel i is given by the two rst coordinates of R(v; )R(u; )(u i ; v i ; w 0 + l i ). When , and l i vary in , and l i , this projection remains in an area which we approximate by the minimum enclosing rectangle u 0 1 ; u 0 2 ] v 0 1 ; v 0 2 ].

When q varies in R CS , this rectangle sweeps an area in accordance with the values of x, y and (see Fig. 2). This area is approximated by a polygon which de nes the expected contact region R i . Now, we compute a plane approximation over the union of all contact regions. For this purpose, we collect the points of the elevation map over all the contact regions. The approximation plane is computed by a least square method. Let A, B and X be matrices de ned as follows :

∆θ x ∆ y ∆ u'1 u'2 v'1 v'2
A = 0 B @ x 1 y 1 1 . . . . . . . . . x p y p 1 1 C A ; B = 0 B @ z 1 . . . z p 1 C A;X = 0 @ a b c 1 A
where ((x i ; y i ; z i )) i=1:::p are the collected points of the elevation map, and a, b and c are the coe cients of the plane equation : z = ax + by + c. Vector X is given by the matrix equation : AX = B: whose solution is : X = (A T A) 1 A T B: with

A T A = 0 @ P x 2 i P x i y i P x i P x i y i P y 2 i P y i P x i P y i p 1 A A T B = 0 @ P x i z i P y i z i P z i 1 A
Let us just mention that, in order to spare memory, we compute directly the matrices A T A and A T B, by adding for each new point, the associated terms to the matrices. When all the points have been collected, there only remains to inverse a 3 3 symetrical matrix, and to multiply it by a 3-dimensional vector.

The coe cients a, b, c de ne the plane which minimizes the quadratic mean of the vertical distances to the elevation map data. This average plane denoted P a provides a placement called p a : p a = (x a ; y a ; z a ; a ; a ; a )

with:

8 > > > > > > < > > > > > > : x a = x1+x2 2 y a = y1+y2
2 z a = ax a + bx a + c a = 1+ 2 2 a = arctan((b cos a a sin a ) cos a ) a = arctan(a cos a + b sin a ) This placement is not supposed neither to have any optimal property nor to correspond to the mean values on each placement parameters. It is only a good indication on what could be the placement of the robot upon the contact regions. p a will be used as a reference position to determine the bounds of the placement parameters around it.

3.2.3

The contact envelopes (V i ) i=1:::n . For each contact region R i , we compute the extreme elevation di erences between the points of the elevation map and P a . For any point M(x; y; z) in the elevation map, this di erence is z = z (ax+by +c). Let z min i and z max i be the extreme values of z on the contact region R i . The contact envelope is : Vi = M 2 R 3 (x; y) 2 Ri and z (ax + by + c) 2 z min i ; z max i ]

Fig. 3 illustrates this notion of contact envelopes. Notice that all the envelopes have the same orientation, de ned by the common average plane P a , but each has a speci c depth, since it is computed separatly on each contact region. However, one may wonder why a di erent mean plane is not computed on each region, which would provide envelopes even closer to the terrain. The reason is that in order to be valid on the whole region R CS , the computed domain r must be independant of (x; y; ). This will be clari ed in the following section. We now use equation (1) which characterizes a placement, to give some bounds on each parameter, according to the dimensions of the contact envelopes.

According to De nition 1, the placement minimizes the robot's energy E. The partial derivates of E with respect to z G , and need therefore to be null. As these di erentiations of E yield too complex expressions, we introduce three new parameters to de ne the relative placement of the robot with respect to P a (Section 3.3.1). The bounds on these parameters can be easily obtained (Section 3.3.2), and then related to the bounds of r (Section 3.3.3).

Relative placement from the average plane.

We introduce three parameters ( ; ; d 0 ) characterizing the position of the steady state plane P S of the robot (whose equation is w = w 0 in the robot's frame) relatively to the average plane P a . Let be the line P S \ P a and the angle between the two planes. We denote by the orientation of the robot in plane P S relatively to . Finally, we call d 0 the distance of point M 0 (0; 0; w 0 ) in the robot's frame to plane P a .

Actually, we are interested in the limits of parameters d 0 and (which respectively correspond to the vertical position and the attitude of the robot) for any value of .

Fig. 3 illustrates these notations, and will give a support to the following developments. Three contact points M 1 ; M 2 and M 3 are represented, with the associated distances to P a and the spring lengths l i , which are the distances to P S .

Determination of the bounds on the

robot's position. Let (d i ) i=1:::n be the distances of the wheels to P a : d i = cos a cos a z i . The length of each spring can be related to the associated d i by: l i = 1 cos (d i d 0 ) tan (sin u i + cos v i ): (3) The di erentiation of E with respect to d 0 yields :

n X i=1 (d i d 0 ) sin n X i=1 (sin u i + cos v i ) = 0
Let us remind that the wheels are assumed to be symetrically placed around the vehicle. This implies : P u i = P v i = P u i v i = 0, and we nally obtain :

d 0 = 1 n n X i=1 d i :
Hence d 0 is between the mean of minimal values of d i on each contact envelope, and the mean of the maximal values. Since d i can be bounded according to the elevation bounds z min i ; z max i ] computed in Section 3.2.3, the extreme values of d 0 are:

d min 0 = 1 n cos a cos a n X i=1 z min i d max 0 = 1 n cos a cos a n X i=1 z max i
Similarly, the di erentiation by leads to :

f( ) = tan cos = B C A where 8 < : A = P n i=1 (d i d 0 ) 2 B = sin P n i=1 d i u i + cos P n i=1 d i v i C = sin 2 P n i=1 u 2 i + cos 2 P n i=1 v 2 i
As function f is monotonous on ] 2 ; 2 , we can deduce the maximal angle max between P S and P a from the maximal value of B C A . Let us rst give some bounds to A, B and C, for any value of :

5 max jAj = max( n X i=1 (d max i d min 0 ) 2 ; n X i=1 (d max 0 d min i ) 2 ) max jBj = v u u t max( n X i=1 diui) 2 + max( n X i=1 divi) 2 min jCj = min n X i=1 u 2 i ; n X i=1 v 2 i
All these values may be computed from the bounds on (d i ) i=1:::n [START_REF] Giralt | The French Planetary Rover VAP: Concept and Current Developments[END_REF] .

The rst condition to be sure there exists a bound to is to insure that maxjAj < minjCj (otherwise there could exist some terrain con guration for which = 2 ). Under this condition, the bounds on can be expressed as follows : max = 2 arctan 1 K (1 p K 2 + 1)] with K = maxjBj minjCj maxjAj 3.3.3 The new placement domain r.

The bounds on and can be related to max . It can be easily shown that : cos = cos( a ) cos( a ). Hence maxj a j = maxj a j = max which gives : = a max ; a + max ] = a max ; a + max ] P n i=1 d i u i is obtained by adding d max i u i when u i > 0, d min i u i otherwise. The minimal value is obtained with d min i u i when u i > 0 and d max i u i otherwise. The same reasoning can be ap-

plied to P n i=1 d i v i .
Finally, the bounds on (l i ) i=1:::n are obtained by minimizing and maximizing expression (3) : 8i; l i = l min i ; l max i ] with:

l min i = 1 cos max (d min i d max 0 ) tan max p u 2 i + v 2 i l max i = 1 cos max (d max i d min 0 ) + tan max p u 2 i + v 2 i
The admissibility of R CS is now very simple to establish, according to De nition 2. Region R CS is declared admissible if : 8i; l i L max ; L max ] (4) S (5) Proposition 1 For any cubic region R CS CS, if the computed placement domain r veri es conditions (4) and ( 5), then R CS ACS.

4 Hierarchical decomposition of CS.

The analysis of CS-regions is now used to compute an approximate cell decomposition of ACS. This cell decomposition relies on an octree decomposition of CS.

4.1 The octree structure.

Octree-type representations have already been used for path-planning; see for example 3]. An octree is a recursive decomposition of a cubic space into subcubes. It is a tree of degree eight whose nodes represent in our case cubic regions of CS, also called voxels.

Any voxel can be analyzed according to Proposition 1. If the voxel is in ACS, we declare it FREE. Otherwise, we cannot conclude, and the voxel is declared MIXED [START_REF] Latombe | Robot Motion Planning[END_REF] . It must be subdivided into eight smaller voxels, for which the test will eventually be successful. This recursive decomposition is performed up to a level p max for which the approximation is ne enought.

The approximate decomposition of ACS consists of all the FREE voxels.

The construction methods.

There mainly exist two methods for building an octree :

The bottom-up method : the voxels of level p max are rst analyzed. The octree is then recursively deduced from the nest level : any voxel of level i is declared FREE if its eight sons of level i + 1 are FREE. Otherwise, it is declared MIXED. This method has a major drawback : it requires to test Figure 4: Octree decomposition of ACS associated to the environment of Figure 5. a great amount of voxels at the nest level, even in areas where such a ne decomposition is not needed.

The top-down method : the root node (level 0) is rst analyzed and is recursively decomposed up to level p max . If a voxel of level i is found to be FREE, it is no longer decomposed. Otherwise it is considered as MIXED and must be subdivided into eight voxels of level i+1 which are analyzed in turn. However, in our case, large CS-regions are unlikely to be in ACS and their analysis would require to consider an important amount of elevation map datas. We choose to combine both methods, in order to avoid their respective drawbacks. A reference level, called p 0 , is choosen in the octree. We rst analyze all the voxels of level p 0 , and we recursively re ne it in the top-down fashion. Then the levels i < p 0 are built according to the bottom-up method.

The choice of a good reference level leads to a minimum number of useless test operations. This reference level mostly depends on the complexity of the terrain. Nevertheless the level where voxels have a size of the order of the robot's length gives usually the best results.

However, searching for a free path between 2 con gurations does not require to compute a complete free space representation. We propose in the next section a search method relying on an incremental building of the octree.

Incremental search for an admissible

path.

Let q s and q g be respectively the start and goal con gurations. We rst create in the octree the largest FREE voxels V s and V g containing q s and q g . Path search from V s to V g is performed by a classical A algorithm.

At each step of the search, the FREE neighbours of the current voxel are expanded as follows : Let V be the current voxel, belonging to level i, and let V 0 be one of its neighbours at the same level. If V 0 is FREE, we recursively analyze its father in order to determine the largest FREE voxel adjacent to V . In the other case, we analyze, among its sons, the 4 voxels adjacent to V . The free sons are appended to the list of neighbours. The MIXED ones are recursively analyzed up to level p max . This procedure is applied to the 6 neighbours of V , and returns the complete list of the largest FREE voxels adjacent to V .

Finally, the search returns a sequence of large voxels connecting V s to V g .

Experimental results.

Figures 4 shows the octree computed for the environment of Figure 5 with p max = 6. The terrain is a 64 64 elevation map.

The path search technique described above was used to improve the e ciency of a path planner based on an extension of 10]. Figure 5 shows a trajectory obtained for a 6-wheeled robot. The total time for planning this trajectory is about 1 minute on a Silicon Graphics INDIGO workstation.

Conclusion.

In this paper, we have addressed a rather new topic of the path-planning problem, ie. computing a safe path for a mobile robot moving on a rough terrain. We proposed a method, using con guration space, to characterize the placements for which the locomotion architecture of the robot can guarantee terrain irregularities absorption and stability of the vehicle.

We believe that the free space representation proposed in this work captures the essential constraints acting on the placement of the robot over the terrain. Therefore, the CS-regions resulting from the path search can be used to limit the search space for more sophisticated (but also more computationally expensive) path planners which consider additional constraints such as collision or non-holonomic constraints.

Natural extensions of this work would deal with a better integration of these di erent planning techniques to obtain a more e cient path planner.

Figure 2 :

 2 Figure 2: Computation of the contact regions

Figure 3 :

 3 Figure 3: Placement variations around the average plane 3.3 The placement domain r.

Figure 5 :

 5 Figure 5: (A) The initial consiguration. (B) The goal con guration. (C) The trajectory obtained for a six wheels robot by using the free-space structuring described here.

This work has been done in the framework of the Automatic Planetary Rover project conducted by the French Spatial Agency. It was partially supported by C.N.E.S. and by the ESPRIT Project PROMotion 6546.

j j < 2 ; j j < 2 .

This hypothesis is not restrictive and facilitates the computation.

In order to keep simple expressions, we give them according to the bounds on d i , since d min i = cos a cos a z min i and d max i = cos a cos a z max i .

[START_REF] Giralt | The French Planetary Rover VAP: Concept and Current Developments[END_REF] In the expression of maxjBj, the maximal value of

Note that our octree does not contain FULL voxels.