Christophe Raffalli
email: raffalli@univ-savoie.fr

Realizability for programming languages

published or not. The documents may come

Realizability for programming languages.

Introduction 1.Realizability

Realizability has been introduced by Kleene in 1945 [START_REF] Kleene | On the interpretation of intuitionistic number theory[END_REF] as a semantics of intuitionistic logic. The key idea is to interpret every proposition as a set of programs (or functions) whose elements, called realizers, compute witnesses for the corresponding proposition. Typically, a realizer of the proposition ∀n: N (A(n) ⇒ ∃m: N B(n, m)) is a program that computes, from a natural number n and a realizer of A(n), an ordered pair formed by an integer m (the 'witness') and a realizer of the formula B(n, m) (the 'justification').

Although Kleene expressed realizers as natural numbers (that is: as codes of recursive functions), the very definition of realizability naturally calls for a functional programming language to express realizers. This is probably why Kreisel [START_REF] Kreisel | Interpretation of analysis by means of constructive functionals of finite types[END_REF] replaced (codes of) recursive functions by closed λ-terms when he introduced the notion of modified realizability. The λ-calculus was introduced by Church [START_REF] Church | A formulation of the simple theory of types[END_REF] in the 30's as a universal programming language based on the sole notion of a function. Besides its applications to logic and realizability, the λ-calculus was the major source of inspiration of functional programming languages, from LISP to ML dialects (SML, Caml, Haskell).

The method of realizability has also been successfully used to prove the strong normalization of many typed λ-calculi. Girard's proof of strong normalization of system F constitutes a particular case of realizability, where types are interpreted as particular sets of programs called reducibility candidates. More recent proofs of strong normalization are based on the method of orthogonality, in which the allowed sets of realizers (i.e. the candidates) are defined from the Typing with constraints More recently, the use of constraints solving for typing [START_REF] Odersky | Type inference with constrained types[END_REF][START_REF] Pottier | A versatile constraint-based type inference system[END_REF] was introduced. A very popular formalism for constraints solving applied to typing is HM(X), which is very well explained by Pottier and Rémy in [START_REF] Pottier | The essence of ML type inference[END_REF]. The key idea of their work is to extract typing constraints from the program in such a way that these constraints and the basic properties of types lie in a decidable fragment of first-order predicate logic, namely: the existential fragment of first-order predicate logic.

In this setting, the fact that a program is typed can be written as a formula of the form A ⇒ ∃t 1 , . . . , t n C

where A is a conjunction of universal axioms like the injectivity of the arrow type ∀t, u, t ′ , u ′ (t

→ u = t ′ → u ′ ⇒ t = t ′ ∧ u = u ′ )
and where C is the conjunction of all constraints extracted from the program. (For instance, if t i , t j and t k are the type variables that are respectively attached to sub-expressions M , N and (M N ) within the program, then C will contain the constraint t i = t j → t k .) This more abstract view is much more helpful to design new type systems. This simplistic description of HM(X) is not really faithful, due to the fact that witnesses cannot be extracted in general in the existential fragment of the predicate calculus (if classical logic is present for instance). In fact, the HM(X) algorithm also relies on the introduction of extra rules to solve the constraints, which rules are usually based on unification.

It is important to understand that in the HM(X) framework, constraints are solved in the syntactic models of types (using unification algorithms). This is still the case in other works based on subtyping (see for instance [START_REF] Aiken | Type inclusion constraints and type inference[END_REF][START_REF] Pottier | Simplifying subtyping constraints: a theory[END_REF]) that are closer to what will be presented here.

Constraints and realizability With realizability in mind, it is no more necessary to express the solutions of the constraints in the algebra of syntactic types. Indeed, we only need to ensure that the constraints have a solution in a suitable realizability model. Since this problem is in general undecidable, we will introduce some sufficient (and non necessary) conditions together with an algorithm to check whether these conditions are satisfied. These conditions will be checked in two phases: we will first saturate the constraints; then, we will require the constraints to be inductive (or well-founded ), thus disallowing arbitrary recursive types. The latter condition is just designed to ensure the existence of a solution in the realizability model. The work presented here resembles those of Aiken, Wimmers and Pottier (among others) [START_REF] Aiken | Type inclusion constraints and type inference[END_REF][START_REF] Pottier | Simplifying subtyping constraints: a theory[END_REF] except for the definition of well-founded constraints and the simplifications of constraints which we omit (in fact they are already implemented in PML). These simplifications are necessary in practice when polymorphism is introduced, because we then copy the constraints at each generalization, and they should be simplified before copying.

Other trends in realizability

Nowadays, there is a great interest in realizability for non-constructive logic. Griffin [START_REF] Griffin | A formulae as-as-types notion of control[END_REF] discovered that Felleisen's [START_REF] Felleisen | Control operators, the SECD machine and the λ-calculus[END_REF] callcc operator was related to Pierce's law. Krivine [START_REF] Krivine | Classical logic, storage operators and second-order lambda-calculus[END_REF] and Parigot [START_REF] Parigot | λµ-calculus an algorithmic interpretation of classical natural deduction[END_REF] applied realizability to classical analysis (i.e. classical second order arithmetic) using extensions of the λ-calculus (by adding a C operator in Krivine's work, or a µ-construction in Parigot's λµ-calculus). Later, this work was extended to ZF set theory [START_REF] Krivine | The curry-howard correspondence in set theory[END_REF], including the dependent axiom of choice [START_REF] Krivine | Dependent choice, 'quote' and the clock[END_REF][START_REF] Raffalli | Realizability of the axiom of choice in hol. (an analysis of krivine's work)[END_REF].

In non-constructive logic, the program extracted from a proof of an existential statement does not compute a correct witness in general. There are two view-points here:

• Realizability can be a semantical tool to analyze proof systems by studying the property shared be all programs realizing a given theorem. This was done for instance by Krivine for the completeness theorem [START_REF] Krivine | Une preuve formelle et intuitionniste du théorème de complétude de la logique classique[END_REF].

This is also interesting because it gives a formal meaning to sentences like "this theorem implies that theorem" of "this theorem is easier than that theorem", because this make sense on programs ("implies" could mean an easy reduction and "easier" could refer to computational complexity). For instance, the completeness theorem for minimal logic is trivial compared to the one for classical propositional logic (see [START_REF] Raffalli | Getting results from programs extracted from classical proofs[END_REF]).

• We can also try to see when proofs using non-constructive principles can lead to programs that really computes the wanted witness. Most works in this area are typically based on Gödel or Friedman syntactic translations from classical to intuitionistic logic. But one may argue that realizability leads to a better comprehension of the phenomena. A key tool here is the use of Krivine's storage [START_REF] Krivine | Classical logic, storage operators and second-order lambda-calculus[END_REF] operator to deal with data types in non constructive proofs. (For the connection between Krivine's approach and negative translations, see [START_REF] Miquel | Relating classical realizability and negative translation for existential witness extraction[END_REF].) This is specially true with the dependant axiom of choice. One interesting hope there, is the discovery of new algorithms by extracting programs from proofs [START_REF] Raffalli | Getting results from programs extracted from classical proofs[END_REF]...

Current works try to extend realizability to the general axiom of choice or other strong axioms. There are also deep connections between Cohen's forcing and realizability that are currently being investigated.

What is done here

We present a toy programming language supporting higher-order functions, extensible records and polymorphic variants, as well as a sufficient condition (that can be tested in polynomial time) to ensure the existence of a realizability model that will guaranty that the evaluation is safe (you do not reach impossible case in the evaluation) and that looping programs have to unfold fixpoints infinitely often.

This property of looping programs is useful because it implies strong normalisation of programs without fixpoint and it also means that if you want to use some termination checker to prove the termination of your programs (which PML does), you just have to focus on fixpoints.

This toy programming language is actually the core of the current implementation of PML1 which enjoys more complex features (like polymorphism, better typing of default case, ...) as well as a proof system that is based on the typing algorithm. These features will be briefly presented in the conclusion.

What is new here is: the simplicity of the algorithm compared to what it can do (this is arguable), the use of realizability, in a subtyping context, to prove that programs are safe in the above sense and the condition for the constraints to be inductive which naturally arises from realizability.

The benefit over HM(X) is (we think) simplicity: for instance, we can get for free extensible records, while they require polymorphism in HM(X). However, we lose type inference because we do not solve the constraints. Nevertheless, a rich language for types can be easily recovered using partial identity functions. This is described in the conclusion.

We also emphasize on the lattice of possible relations between type variables contrary to the lattice of types which is more usual with subtyping. Indeed, as we do not solve constraints, we have no types but only constraints between type variables. However, we found that a lot of interesting generalizations could be done by enlarging the lattice of relations between types. Usually there is only ⊂, ⊃, = and the absence of relation written ⊥. In this simple case, direct constraints between type names can be represented by a directed graph. All the algorithms presented with matrices with coefficients in the lattice of relations could be rephrased as some kind of computation of the transitive closure of a graph. But, we shall see that the presentation using the lattice with four elements {⊥, ⊂, ⊃, =} is elegant, and in the conclusion, we will show a few possible generalizations with larger lattices.

Notes about this document

This document contains a full implementation of the algorithm described here in a literate programming style. The code is extracted from the L A T E X source and compiled. I also wrote some pretty printers for code and typing constraints.

All the examples are generated by running the extracted code on examples with various options controlling what is printed.

Feel free to download this work to study and extend it. It is available using darcs via: darcs get http://lama.univ-savoie.fr/~raffalli/repos/EJCIM

The toyML language

The language is defined from three denumerable sets of identifiers:

• the set of variables V λ = {x, y, . . .},
• the set of constructor names V Σ = {C, Z, S, Cons, Nil, . . .}; and

• the set of label names V Π = {l, car, cdr, . . .}.

The set P of all programs is then defined using the following BNF:

P := x | fun x → P | P P | fix x → P | C[P ] | case P of C[id] → P | • • • | C[id] → P | P.l | {l = P ; . . . ; l = P }
The first three constructs correspond to variables, functions, applications and fix-point. The second line corresponds to variants and case analysis on variants. Finally, the last line corresponds to projections and records.

There is one more restriction that is not shown in the BNF: in records and case analyzes, the variant names in the same case analysis and the labels in the same record must be pairwise distinct. In particular, the programs

case M of C[x] → N 1 | C[x] → N 2 and {l = N 1 ; l = N 2 } are not allowed.
First, we precise some conventions and abbreviations:

• Priorities (to avoid parentheses) follow the usual ML rule: application is left-associative and has a higher priority than functions, fixpoints and cases. Cases are right associative when nested:

-M N P reads (M N ) P .

fun x → M N reads fun x → (M N ).

case

x of C[x] → case y of D[y] → M | E[y] → N reads case x of C[x] → (case y of D[y] → M | E[y] → N ) • fun x 1 . . . x n → M is a shortcut for fun x 1 → . . . fun x n → M • fix f x 1 . . . x n → M denotes fix f → fun x 1 → . . . fun x n → M • C[r] is a shortcut for C[{r}]
when r is a record without curly braces. Moreover, C[] reads C[x] in a case pattern where the variable x does not occur in the right-hand side of the pattern.

• M [x ← N ] represents the (capture avoiding) substitution of N for the variable x in M .

Example: if M is fun x y → x z and if N is fun y → x, then the notation M [z ← N ] refers to the program fun x ′ y → x ′ (fun y → x). • M [(x i ← N i ) i∈I ]
denotes the simultaneous substitution of the variables x i by the terms N i in M , for all i ∈ I.

• case M of (C i [x] → N i ) i∈I denotes the program case M of C i 1 [x] → N i 1 | . . . | C in [x] → N in (where I = {i 1 , . . . , i n }). • {(l i = N i ) i∈I } denotes the program {l i 1 = N i 1 ; . . . ; l in = N in } (where I = {i 1 , . . . , i n }).
To understand how programs compute, we now give the operational semantics for our toy programming language. We will use the notation M ≻ r N to express that the program M evaluates to N using one reduction rule named r. We will also use M ≻ N for the transitive closure of all possible reductions.

Here are the reduction rules: beta reduction

(fun x → M )N ≻ β M [x ← N ].
This rule corresponds to the replacement of the formal argument x in the body of the function by the real argument N the function is applied to.

fixpoint fix x → M ≻ µ M [x ← (fix x → M )].
The fixpoint rule allows for recursive definition (see the examples below).

projection

{(l i = P i ) i∈I }.l j ≻ π P j if j ∈ I
Here we project a record field. The implementation actually uses a more complex rule:

{l 1 = P 1 ; . . . ; l n = P n }.l i ≻ π p i [l 1 ← p 1 , . . . , l i-1 ← p i-1 ] when 1 ≤ i ≤ n.
This extended rule allows fields of a given record to mention previously defined fields (without using a fixpoint).

Exercise 1 Show how to express this feature using a fixpoint.

case selection case C j [N ] of (C i [x] → P i ) i∈I ≻ σ P j [x ← N ] if j ∈ I
Here the case corresponding to the given variant is selected and the argument of the variant is substituted as expected.

congruence M ≻ r M ′ implies E[M ] ≻ r E[M ′ ]
Here we use a context E[], that is a program with one unique hole, to express the fact that the above reduction can be performed anywhere inside a program. Contexts can bind variables, which means that we allow reduction under function abstractions or in the right-hand side of case analysis.

A program may also contain a manifest error , corresponding to a piece of code that cannot be reduced, and that would lead to a runtime error when executed. To indicate such errors, we define the notation M ⇑ as follows:

• (fun x → M ).l ⇑ case fun x → M of . . . ⇑ • C[M ].l ⇑ C[M ] N ⇑ • {. . .}N ⇑ case {. . .} of . . . ⇑ • case D[. . .] of (C i [x] → . . .) i∈I ⇑ when D = C i for all i ∈ I.
• {(l i = . . .) i∈I }.k ⇑ when k = l i for all i ∈ I.

Moreover, we require that every program that contains an erroneous piece of code is also considered as a manifest error:

• If M ⇑, then E[M ] ⇑ (where E[
] is an arbitrary context with one hole).

Definition 2 (safe) We say that a program M is safe when it cannot reduce to an error, that is:

M ≻ M ′ implies M ′ ⇑.
Here are some examples of programs and reductions:

omega The shortest looping λ-term (that reduces to itself):

(fun x → x x) (fun x → x x)
halving A partial function that computes the half of even numbers only (figure 1 gives an example of reduction using this program):

fix half n → case n of | Z[] → Z[] | S[n'] → case n' of | S[n"] → S[half n"]
length The length of lists and an example of reduction in figure 2

fix length l → case l of | Nil[] → Z[] | Cons[c] → S[length c.cdr]
The above examples were reduced using a specific strategy (call-by-value) which is implemented in the code given in this course (see appendix A). However, we will prove properties that are independent from the evaluation strategy. This is natural because the language is purely functional (no side-effect allowed) and therefore enjoys the Church-Rosser property : See [START_REF] Barendregt | The Lambda Calculus: Its Syntax and Semantics[END_REF] to see the proof techniques used for Church-Rosser.

Theorem 3 (Church-Rosser property ) If M ≻ M 1 and M ≻ M 2 , then there exists a program M 0 such that M 1 ≻ M 0 and M 2 ≻ M 0 . (fix half n → . . .) S[S[Z[]]] ≻µ (fun n → case n of | Z[] → Z[] | S[n'] → case n' of | S[n"] → S[(fix half n → . . .) n"]) S[S[Z[]]] ≻ β case S[S[Z[]]] of | Z[] → Z[] | S[n'] → case n' of | S[n"] → S[(fix half n → . . .) n"] ≻σ case S[Z[]] of | S[n"] → S[(fix half n → . . .) n"] ≻σ S[(fix half n → . . .) Z[]] ≻µ S[(fun n → case n of | Z[] → Z[] | S[n'] → case n' of | S[n"] → S[(fix half n → . . .) n"]) Z[]] ≻ β S[case Z[] of | Z[] → Z[] | S[n'] → case n' of | S[n"] → S[(fix half n → . . .) n"]] ≻σ S[Z[]]
≻ β case Cons[car = A[]; cdr = Cons[car = B[]; cdr = Nil[]; ]; ] of | Nil[] → Z[] | Cons[c] → S[(fix length l → . . .) c.cdr] ≻σ S[(fix length l → . . .) { car = A[]; cdr = Cons[car = B[]; cdr = Nil[]; ]; }.cdr] ≻π S[(fix length l → . . .) Cons[car = B[]; cdr = Nil[]; ]] ≻µ S[(fun l → case l of | Nil[] → Z[] | Cons[c] → S[(fix length l → . . .) c.cdr]) Cons[car = B[]; cdr = Nil[]; ]] ≻ β S[case Cons[car = B[]; cdr = Nil[]; ] of | Nil[] → Z[] | Cons[c] → S[(fix length l → . . .) c.cdr]] ≻σ S[S[(fix length l → . . .) { car = B[]; cdr = Nil[]; }.cdr]] ≻π S[S[(fix length l → . . .) Nil[]]] ≻µ S[S[(fun l → case l of | Nil[] → Z[] | Cons[c] → S[(fix length l → . . .) c.cdr]) Nil[]]] ≻ β S[S[case Nil[] of | Nil[] → Z[] | Cons[c] → S[(fix length l → . . .) c.cdr]]] ≻σ S[S[Z[]]]
Corollary 4 (Uniqueness of normal form) If a term M reduces to a normal term (that is: a term where no further reduction can be performed), then this normal term M ′ is unique. If moreover the term M is safe, then its unique normal form M ′ contains no manifest error (i.e. M ′ ⇑).

The listing 1 is the type definition in Caml for the abstract syntax of programs. The type of programs is parameterized by 'a to be able to decorate programs with type names. Each constructor of the language, except variables, needs one parameter for its type, and each binding occurrence of a variable (fun and case) also needs a parameter for the type of the bound variable.

type i d = s t r i n g type c i d = s t r i n g type l i d = s t r i n g type ' a program = | Var of i d | App of ' a program * ' a program * ' a | Fun of i d * ' a * ' a program * ' a | Fix of i d * ' a * ' a program * ' a | Cst of c i d * ' a program * ' a | Cas of ' a program * ( c i d * i d * ' a program * ' a ) l i s t * ' a | Rec of ( l i d * ' a program ) l i s t * ' a | Pi of ' a program * l i d * ' a
Listing 1: type for programs in program.ml

Realizability candidates

We shall now define and manipulate particular sets of programs: realizability candidates. To define them, we will use the method of orthogonality, which is a systematic way to define such candidates from the particular correctness invariant we want to convey throughout the proofs.

This correctness invariant is embodied as a particular set of programs written ⊥ ⊥ (read: double bottom), that we define here as follows, first defining the notion of bad reduction: Definition 5 A reduction of a term M is bad if it yields an erroneous term or if it is infinite while using only finitely many times the fixpoint rules.

The set ⊥ ⊥ is defined as the set of all programs that do not have bad reduction. This means that ⊥ ⊥ is the set of all safe programs whose infinite reductions use infinitely many times the fixpoint reduction rule.

This definition means that we are not only interested in the safety of programs, but also in the way programs may loop. The condition about infinite reduction sequences has been added here to ensure that every term M ∈ ⊥ ⊥ that does not contain the fix construct is strongly normalizable. In particular, the looping term (fun x → x x) (fun x → x x) does not belong to ⊥ ⊥. (But the looping fixpoint fix x → x does.)

Note that by definition, the set ⊥ ⊥ is closed under arbitrary reductions.

Exercise 6 (too difficult) Show that ⊥ ⊥ is not a recursive set of programs. It is probably not even recursively enumerable! Since the idea of orthogonality is based on the interaction between programs (seen as players) and their possible opponents, we first need to define what is an opponent of a program. Very often, opponents are taken as the evaluation contexts corresponding to the given reduction strategy. To preserve the independence from a particular reduction strategy, and due to our general form of case construct, we need to take arbitrary contexts as opponents:

Definition 7 (context) A context E is an arbitrary program in ⊥ ⊥, whose 'holes' are represented by the occurrences of a variable χ that has been fixed once and for all. (This variable may occur 0, 1 or more times in E). When M is a term and E is a context, we write

M ⋆ E for E[χ ← M ].
Note that with this definition, contexts cannot capture variables. (This will be an important property in what follows.) Indeed, if E is fun x → χ and if M is fun y → x, then M ⋆ E denotes the program fun x ′ → fun y → x, and not the program fun x → fun y → x where the variable x has been captured.

The same definition (with the same notation) will be also used to compose contexts. It is thus important to remark that Lemma 8 The operation E ⋆ F is associative.

Proof: Let E, F, G be three contexts, then (E ⋆ F ) ⋆ G = G[χ ← F [χ ← E]] and E ⋆ (F ⋆ G) = (G[χ ← F ])[χ ← E].
Both are equal without any hypothesis (which is rare for properties of substitution) because we substitute twice the same variable. This can be formally checked by induction on G.

Our notion of realizability candidates will only work if the set ⊥ ⊥ is ⊥ ⊥saturated according to the definition below. This definition may seem complicated ... In fact, you can rediscover the definition by first trying to prove the adequacy lemma 26, and you will see that all the properties written here are just what is needed-and nothing more.

Definition 9 (⊥ ⊥-saturated sets) We say that a set A of programs is ⊥ ⊥saturated if the following conditions holds (for all contexts E):

1. If M [x ← P ] ⋆ E ∈ A and P ∈ ⊥ ⊥, then (fun x → M ) P ⋆ E ∈ A. 2. If P j [x ← M ] ⋆ E ∈ A, M ∈ ⊥ ⊥ and P i ∈ ⊥ ⊥ for all i ∈ I, then (case C j [M ] of (C i [x] → P i ) i∈I ) ⋆ E ∈ A. 3. If P j ⋆ E ∈ A and P i ∈ ⊥ ⊥ for all i ∈ I, then {(l i = P i ) i∈I }.l j ⋆ E ∈ A.
4. If for all n ∈ N and for a fresh variable x, we have

M n (x) ⋆ E ∈ A and M ∈ ⊥ ⊥, then (fix x → M ) ⋆ E ∈ A. (Writing M 0 (x) = x and M n+1 (x) = M [x ← M n (x)].) Lemma 10 The set ⊥ ⊥ is ⊥ ⊥-saturated.
Proof: We treat each case separately, following a common pattern: we do a proof by coinduction: we prove that if there is a bad reduction from the term given in the conclusion, then we can construct a bad reduction in the initial term.

We first need to recall what is a proof by coinduction: It is a way to construct a sequence (finite of infinite) with a given property and at each step of the proof we need to check that we really extend the sequence (we say that each step is productive). In fact, this is too restrictive, we should allow some steps where the sequence stagnates, but we must prove that these steps cannot occur consecutively infinitely often.

1. We prove the following lemma: let E be a term where the variable χ i occurs exactly once for all i ∈ I.

Assume that E[(χ i ← (fun x → M i ) P i ) i∈I ] ∈ ⊥ ⊥, and for all i ∈ I, P i ∈ ⊥ ⊥, then E[(χ i ← M i [x ← P i ]) i∈I ] ∈ ⊥ ⊥.
Proving this allows us to deduce the property we want by renaming each occurrence of χ in the initial context with a different name (χ i ) i∈I and taking M i = M and P i = P for all i ∈ I.

Proving this lemma means that we can assume that we have a bad reduction (unsafe or infinite using finitely many time the fix-point rule

) of E[(χ i ← (fun x → M i )P i ) i∈I ] and construct by coinduction a bad reduction of E[(χ i ← M i [x ← P i ]) i∈I ].
There are only four possible cases for the first reduction (basically because there is no critical pair for the reduction of our language):

• If it occurs in E: E ≻ r E ′ , then the variables χ i may be erased or duplicated. We can replace duplicated variables in E ′ by distinct variables and ignore erased variables. This means that there is a context E ′′ , a family of variables {χ ′ j } j ∈ J and a function ψ from

J to I such that E ′ = E ′′ [(χ ′ j ← χ ψ(j)
) j∈J ] and all χ j occur exactly once in E ′′ . The function ψ j is not surjective when some variables χ i are erased in E ′ and it is not injective when they are duplicated. Then, we have,

E[(χ i ← M i [x ← P i ]) i∈I ] ≻ r E ′′ [(χ ′ j ← M ψ(j) [x ← P ψ(j) ]
) j∈J ] and we conclude by coinduction.

• If the first reduction occurs in M j ; M j ≻ r M ′ j for some j, then we write

M ′ i = M i if i = j and we have E[(χ i ← M i [x ← P i ]) i∈I ] ≻ r E[(χ i ← M ′ i [x ← P i ]
) i∈I ] which allows to conclude by coinduction. • If the first reduction occurs in P j ; P j ≻ r P ′ j for some j, then we write

P ′ i = P i if i = j and we have E[(χ i ← M i [x ← P i ]) i∈I ] ≻ * r E[(χ i ← M i [x ← P ′ i ]) i∈I ].
The symbol ≻ * r represents 0, 1 or more reduction step using the same rule r. If there is no reduction (which means that x does not occur free in M j ), then we need to remark that this case can not happens consecutively infinitely often, because that would mean that there is a bad reduction in one the terms P i ∈ ⊥ ⊥ which is impossible. Therefore this steps does not entail productivity.

• If the first reduction is the reduction of the redex substituted to χ j for some j ∈ I:

(fun x → M j )P j ≻ β M j [x ← P j ]. Then, we can take E ′ = E[χ j ← M j [x ← P j ]]
, and we do have

E[(χ i ← M i [x ← P i ]) i∈I ] = E ′ [χ i ← M i [x ← P i ]) i∈I\{j} ]
. This step is not directly productive, but it can not happens infinitely often because the size of the index set I decreases while in the previous step, which in not productive either, I remains unchanged.

2. This case is similar to the previous case, but more cumbersome to write.

3. This case is still similar and even a bit simpler than the first case.

4. For the fixpoint case, assuming a bad reduction of

E[(χ i ← fix x → M i ) i∈I ],
we can take n to be the total number of reductions of the fixpoint rule and produce a bad reduction of E[(χ i ← M n i (x)) i∈I ] using the same technique. The productivity will come from the fact the the number of reductions of the fixpoint rule will decrease when we apply one.

We can now define orthogonality and realizability candidates: Definition 11 (Orthogonality) Let M be a set of programs and E a set of contexts. We define their orthogonal as follows:

M ⊥ = {E contexts in ⊥ ⊥ s.t. for all M ∈ M, M ⋆ E ∈ ⊥ ⊥} E ⊥ = {M programs in ⊥ ⊥ s.t. for all E ∈ E, M ⋆ E ∈ ⊥ ⊥}
Lemma 12 Orthogonality enjoys the following very general properties:

1. It is contravariant : if M ⊂ M ′ then M ′ ⊥ ⊂ M ⊥ (the same holds for context).
2. Double orthogonal is covariant.

3. M ⊂ E ⊥ if and only if E ⊂ M ⊥ .
4. E ⊂ E ⊥⊥ and E ⊥⊥⊥ = E ⊥ (the same holds for programs).

5. If E i is a family of set of contexts indexed by i ∈ I, then

i∈I E i ⊥ = i∈I E ⊥ i and i∈I E ⊥ i ⊂ i∈I E i ⊥ 6. If E is a set of contexts, then E ⊥ ⊂ ∅ ⊥ = ⊥ ⊥.
Proof:

1. Assume that E ⊂ E ′ for two sets of contexts. Let M ∈ E ′ ⊥ , for all E ∈ E, we have E ∈ E ′ and therefore M ⋆ E ∈ ⊥ ⊥. This means that M ∈ E ⊥ . The same works for set of programs.

2. Immediate from 12.1.

3. We prove the left to right implication, the converse having an identical proof. Let E be a set of contexts and M be a set of programs, assume that M ⊂ E ⊥ and let E be a context in E. We want to show that E ∈ M ⊥ so we take M ∈ M ⊂ E ⊥ and we have immediately

M ⋆ E ∈ ⊥ ⊥. 4. By 12.3 E ⊂ E ⊥⊥ comes from E ⊥ ⊂ E ⊥ and E ⊥⊥⊥ ⊂ E ⊥ comes from E ⊂ E ⊥⊥ ⊂ E ⊥⊥⊥⊥ . 5. Let E ∈ i∈I E ⊥ i , then E ∈ E ⊥ j for some j ∈ I. Then, let M be in i∈I E i , we have M ∈ E j which means that M ⋆ E ∈ ⊥ ⊥. This establishes i∈I E ⊥ i ⊂ i∈I E i ⊥
For the orthogonal of union, we have

M ∈ i∈I E ⊥ i if and only if ∀i ∈ I, ∀E ∈ E i , M ⋆ E ∈ ⊥ ⊥ which is equivalent to ∀E ∈ i∈I E i , M ⋆ E ∈ ⊥ ⊥.
This exactly means M ∈ i∈I E i ⊥ .

6. Let E be a set of contexts with no occurrence of χ, Then M ⋆ E = E ∈ ⊥ ⊥ for any program M. Therefore, E ⊥ = P. Definition 13 (realizability candidates) Because of the above property, we will be only interested by set of programs that are the orthogonal of some set of contexts. We call this kind of sets realizability candidates and we write C the set of all realizability candidates.

Lemma 14 (property of realizability candidates) :

1. If M ∈ C then M ⊥⊥ = M.
2. Realizability candidates are closed by arbitrary intersections.

3. ⊥ ⊥ is the largest realizability candidate.

4.

The smallest realizability candidate is ⊥ ⊥ ⊥ and contains all variables. We will write it ⊥ ⊥ 0

Any realizability candidate

A is ⊥ ⊥-saturated and verifies ⊥ ⊥ 0 ⊂ A ⊂ ⊥ ⊥.

Proof: The first property 14.1 is exactly 12.4 because candidates are themselves some orthogonal, 14.2 is 12.5, 14.3 is 12.6, 14.4 is immediate from 12.1.

⊥ ⊥ 0 contains all variables because x ⋆ E ∈ ⊥ ⊥ if and only if E ∈ ⊥ ⊥.
The last property, is immediate from 14.3 and 14.4 and because ⊥ ⊥ being saturated, all its subsets are saturated.

Finally, we end this section by defining constructions on candidates and sets of contexts that we will need to interpret types: Definition 15

• If M is a realizability candidate and E a set of contexts, then

M.E = {E[χ ← χ M ] s.t. M ∈ M and E ∈ E} • If M and N are realizability candidates then M → N = (M.N ⊥ ) ⊥ • If E i are contexts for all i ∈ I, then Σ n i=1 C i [E i ] = {(case χ of (C i [χ] → E i ) i∈I ) ⋆ E s.t. ∀i ∈ I, E i ⋆ E ∈ E i } • If A i are realizability candidates for all i ∈ I, then Σ n i=1 C i [A i ] = (Σ n i=1 C i [A ⊥ i ]) ⊥
• If E i are contexts for all i ∈ I, then

Π n i=1 l i : E i = i∈I {χ.l i ⋆ E i s.t. E i ∈ E i }
• If A i are realizability candidates for all i ∈ I, then

Π n i=1 l i : A i = (Π n i=1 l i : A ⊥ i ) ⊥

Lattices and matrices

The main tool for the typing-checking algorithm are matrices with coefficients given in two lattices. The first lattice expresses the relation between types: it as four elements. But what is a type ... In fact, types will be just names (so we should say type names) that we will interpret using realizability candidates in the next section. Realizability candidates being sets, the possible relation between type names are:

• No relation is known : denoted 0

• α ⊂ β is known to hold : denoted i.

• α ⊃ β is known to hold : denoted i * .

• α = β is known to hold : denoted 1. This means we have a set B = {0, i, i * , 1} which can be given a lattice structure with 0 ≤ i ≤ 1 and 0 ≤ i * ≤ 1 (see figure 3). This lattice is isomorphic to (Z/2Z) 2 and we can define on it supremum (denoted x∨y), infimum (denoted x ∧ y or x.y), subtraction (denoted xy and defined as the smallest element such that (xy) ∨ y = x ∨ y).

0 i ⋆ (meaning ⊃) 1 (meaning =) i (meaning ⊂)
We will also need the adjoin operation denoted x * exchanging i and i * and keeping 0 and 1 unchanged.

We use a second inf-lattice B ′ = {0, i, i * , j, j * , 1} ⊃ B whose lattice structure is given by figure 4. We see on this figure that not all supremum are defined in B ′ . This lattice will be used to construct an ordering between type names that we will use to define the interpretation of types by induction on this order. Here are the intended meaning for the element of B ′ :

• i represents α β : α must be defined before or at the same time as β.

• i * represents α β : α must be defined after or at the same time as β.

• j represents α ≺ β : α must be defined before β.

• j * represents α ≻ β : α must be defined after β.

• 1 represents α ≍ β : α and β must be defined simultaneously.

• 0 represents the absence of constraints between the definitions of α and β.

With the lattice B ′ , the product x.y do not coincide with the infimum. The main property of the product is that it expresses transitivity. If x denotes a relation known to hold between α and β and y denotes a relation known to hold between β and γ, then, the relation denoted by x.y is known to hold between α and γ.

Using this intuition, we define the product on B ′ as follows j.1

= j = i = j ∧ 1, j * .1 = j * = i * = j * ∧ 1, j.i = j = i = j ∧ i and j * .i * = j * = i * = j * ∧ i * .
In all other cases, we have j.i = j ∧ i.

Remark: The structure of (B, ., ∨) is very similar to the structure of tropical semiring which was introduced by Simon (a computer scientist from Brasil, hence the name) and which is now used in algebraic geometry. The only difference is that in tropical semiring, (B, .) is a group and here we just have a monoid.

The structure of B and B ′ is characterized by the following definitions:

Definition 16 (relation lattice) (B, ≤, 0, 1, ., x → x * ) is a relational (resp. partial relational) lattice if • (B, ≤
) is a lattice (resp. an inf-lattice) with 0 as its bottom element.

• . is a binary increasing operation which is commutative, associative with 1 as neutral element and distributing over sup when they are defined.

• x → x * is an idempotent and increasing unary operator. Moreover, (x.y) * = x * .y * and x.x = x.

• x-y, the least element such that x∨y = (x-y)∨y satisfies (x-y)∧y = 0.

Lemma 17

The lattices B and (resp. inf-lattice B ′ ) are relational (resp. partial relational) lattice.

Proof: Just a boring check on the table defining the lattices operations.

Here is the code for the basic operation on both lattice B and B ′ (we do not give separate implementation for both lattices):

Listing 2: definition of the lattices in lattice.ml We will need to manipulate vectors and matrices with coefficients in the above lattices. We will mainly use sparse matrices and represent vector as list of pairs with the index and the coefficient, ordered by index. A representation as a map table with O(ln n) insertion and deletion would be better .. Now, we also need some operations on matrices and vectors like ordering (which is point-wise ordering), supremum (which is point-wise supremum) and multiplication defined as usual with product and supremum taking the place of addition. Here are some formal definitions (for these definitions, we just consider that vectors are column or line matrices and just give the definitions for matrices):

Definition 18 Let A = (A i,j ) i∈I,j∈J , A ′ = (A ′ i,j
) i∈I,j∈J and B = (B j,k ) j∈J,k∈K be three matrices with index in the finite sets I, J, K and coefficients in a relational lattice (partial or total). Then

• A ≤ A ′ is true if for all i ∈ I, j ∈ J we have A i,j ≤ A ′ i,j .
• A ∨ A ′ is the matrix (A i,j ∨ A ′ i,j ) i∈I,j∈J .

• A -A ′ is the matrix (A i,j -A ′ i,j ) i∈I,j∈J .

• A.B = (C i,k ) i∈I,k∈K with C i,k = j∈J A i,j .B j,k .

• A * = (a * j,i ) j∈J,i∈I .

• We will say that a square matrix A is an hermitian matrix if A = A * . Remark: an hermitian matrix can only have the coefficients 0 and 1 on the diagonal.

To define all operations on vectors and matrices we first define a fold operation on two vectors. It take four other arguments: three functions (called respectively when an index is bound in the first, second of both vectors) and the initial accumulator Exercise 19 Understand the code below. Listing 5: matrix and vector operations in matrix.ml

l e t f o l d 2 v e c t o r : ( ' a → ' i → ' b → ' c → ' a ) → ( ' a → ' i → ' b → ' a ) → ( ' a → ' i → ' c → ' a ) → ' a → ( ' i , ' b ) v e c t o r → ( ' i , ' c ) v e c t o
We introduce some notations for hermitian matrices with coefficients in the lattice B or B ′ . Let A = (a α,β ) α,β∈I Definition 22 (multi-vector ) A multi-vector is a vector where the same indices can be bound several times (to different values). Another way to say this is that a multi-vector with coefficients in a set X is a vector with coefficients in P(X). This is why when C is a multi-vector, we will write c ∈ C i and not

• A |= α ⊂ β iff a α,β ≥ i (when A has coefficients in B) • A |= α ⊃ β iff a α,β ≥ i * (when A has coefficients in B) • A |= α = β iff a α,β ≥ 1 (when A has coefficients in B) • A |= α β iff a α,β ≥ i (when A has coefficients in B ′ ) • A |= α β iff a α,β ≥ i * (when A has coefficients in B ′ ) • A |= α ≍ β iff a α,β ≥ 1 (when A has coefficients in B ′ ) • A |= α ≺ β iff a α,β ≥ j (when A has coefficients in B ′ ) • A |= α ≻ β iff a α,β ≥ j * (
C i = c
For the implementation, we define multi-vectors as vectors of lists:

1 type ( ' index , ' c o e f ) m u l t i v e c t o r = ( ' index , ' c o e f l i s t ) v e c t o r Listing 6: matrix and vector operations in matrix.ml

Typing constraints

The first (trivial) step of the typing algorithm is to decorate programs with type names.

We consider that T is a countable set of such names and each subprograms is decorated with a different name in T except for variables: all occurrences of the same variable are decorated with the same name.

For the implementation, we use as names the positions given by the parser, keeping only the position of the binding occurrence for variables.

Here is the decorated version of the term omega :

((fun x α 0 → (x x) ρ 0 ) ϕ 0 (fun x α 1 → (x x) ρ 1 ) ϕ 1 ) ρ 2
and the decorated version of the halving an even number, applied to unary representation of three (this program will fails):

((fix half α 1 → (fun n α 0 → (case n of | Z[ β 0 ] → Z[ γ 0 ] σ 0 | S[n' β 2 ] → (case n' of | S[n" β 1 ] → S[(half n") ρ 0 ] σ 1 ) χ 0 ) χ 1 ) ϕ 0 ) ϕ 1 S[S[S[Z[ γ 1 ] σ 2 ] σ 3 ] σ 4 ] σ 5 ) ρ 1
Definition 23 The typing constraints extracted from a program consist in a triplet (C, R, D) where:

• C, the constructor constraints, is a vector and D, the destructor constraints, a multi-vector with index in T and coefficients in the disjoin sum of the following sets, using specific notations for an intuitive reading:

-T 2 writing those pairs α → β -Finite maps from V Σ to T , writing the map associating

α i to C i for i ∈ I as Σ i∈I C i [α i ] or C 1 [α 1 ] + C 2 [α 2 ] + . . .
-Finite maps from V Π to T , writing the map associating the α i to l i for i ∈ I as Π i∈I l i :

α i or l 1 : α 1 × l 2 : α 2 × . . .
• R, the relational constraints, is an hermitian matrix with only 1 on the diagonal (recall that in general there could be 0 or 1 on the diagonal of such a matrix).

Here C represents the constraints coming from data constructors in the code, D from data destructors and R the other constraints (coming only from the fixpoints and the right-hand side of case analysis). D is a multi-vector, because the same variable can be destroyed (applied to an argument for instance) more than once. This will be clear in definition 24 We introduce the following notations for constraints (similar to those introduced for matrices in the previous section):

• (C, R, D) |= α ⊂ β iff R |= α ⊂ β • (C, R, D) |= α ⊃ β iff R |= α ⊃ β • (C, R, D) |= α = β iff R |= α = β • (C, R, D) |= α → β ⊂ γ iff C γ = α → β • (C, R, D) |= γ ⊂ α → β iff α → β ∈ D γ • (C, R, D) |= Σ i∈I c i [α i ] ⊂ γ iff C γ = Σ i∈I C i [α i ] • (C, R, D) |= γ ⊂ Σ i∈I C i [α i ] iff Σ i∈I C i [α i ] ∈ D γ • (C, R, D) |= Π i∈I c i : α i ⊂ γ iff C γ = Π i∈I l i : α i • (C, R, D) |= γ ⊂ Π i∈I l i : α i : iff Π i∈I l i : α i ∈ D γ
Here is the code to define data types for constraints (the triplet (C, R, D)). It does not exactly obey the above definition because we use the fact that the index set I above will always be a singleton for Σ in C and Π in D. Definition 24 (extracted constraints) The initial typing constraints K 0 = (C, R 0 , D), extracted from an annotated program, are the smallest constraints (ordered point-wise for the matrix R 0 and by set inclusion for the vector C and multi-vector D, regarded as set of pairs) verifying:

open P a r s e r U t i l open L a t t i c e open Matrix open Program

type c o n s t r u c t o r = | CSum of c i d * p o s i t i o n | CPro of ( l i d * p o s i t i o n ) l i s t | CFun of p o s i t i o n * p o s i t i o n type d e s t r u c t o r = | DSum of ( c i d * p o s i t i o n ) l i s t | DPro of l i d * p o s i t i
• If (M ϕ N α ) ρ is a sub-term of the program then K 0 |= ϕ ⊂ α → ρ • If (fun x α → M ρ ) ϕ is a sub-term of the program then K 0 |= α → ρ ⊂ ϕ. • If (fix x α → M ϕ ) ρ is a sub-term of the program then K 0 |= ϕ ⊂ α and K 0 |= ϕ ⊂ ρ • If C[M β ] σ is a sub-term of the program then K 0 |= C[β] ⊂ ρ • If (case M σ of (C i [x β i ] → N ρ i i ) i∈I ) ρ is a sub-term or the program, then for all i ∈ I, K 0 |= ρ i ⊂ ρ and K 0 |= σ ⊂ Σ i∈I C i [β i ] • If {(l i = M ρ i ) i∈I } γ is a sub-term of the program then K 0 |= Π i∈I l i : ρ i ⊂ γ • If (M γ .l) ρ is a sub-term or the program then K 0 |= γ ⊂ l : ρ
Here are the initial constraints for the term omega, using the annotation given above:

C = {α 0 → ρ 0 ⊂ ϕ 0 , α 1 → ρ 1 ⊂ ϕ 1 } R 0 = {} D = {α 0 ⊂ α 0 → ρ 0 , ϕ 0 ⊂ ϕ 1 → ρ 2 , α 1 ⊂ α 1 → ρ 1 }
and those for halving applied to the unary representation of the natural number three:

C = {α 0 → χ 1 ⊂ ϕ 0 , Z[γ 0 ] ⊂ σ 0 , ⊂ γ 0 , S[ρ 0 ] ⊂ σ 1 , S[σ 4 ] ⊂ σ 5 , S[σ 3 ] ⊂ σ 4 , S[σ 2 ] ⊂ σ 3 , Z[γ 1 ] ⊂ σ 2 , ⊂ γ 1 } R 0 = {ϕ 0 ⊂ ϕ 1 , ϕ 0 ⊂ α 1 , σ 0 ⊂ χ 1 , χ 0 ⊂ χ 1 , σ 1 ⊂ χ 0 } D = {ϕ 1 ⊂ σ 5 → ρ 1 , α 1 ⊂ β 1 → ρ 0 , α 0 ⊂ Z[β 0 ] + S[β 2 ], β 2 ⊂ S[β 1 ]}
Definition 25 (interpretation) An interpretation satisfying the typing constraints K 0 = (C, R 0 , D) is a function α → ||α||, associating realizability candidates to type names appearing in K 0 satisfying the conditions given below. Moreover, we will write |α| for ||α|| ⊥ . Here are the conditions:

• If K 0 |= ϕ ⊂ α then ||ϕ|| ⊂ ||ρ|| • If K 0 |= ϕ ⊂ α → ρ then ||ϕ|| ⊂ ||α|| → ||ρ|| • If K 0 |= α → ρ ⊂ ϕ then ||α|| → ||ρ|| ⊂ ||ϕ|| • If K 0 |= Σ i∈I C i [β i ] ⊂ ρ then Σ i∈I C i [||β i ||] ⊂ ||ρ|| • If K 0 |= ρ ⊂ Σ i∈I C i [β i ] then ||ρ|| ⊂ Σ i∈I C i [||β i ||] • If K 0 |= Π 1≤i≤n l i : ρ i ⊂ γ then Π 1≤i≤n l i : ||ρ i || ⊂ ||γ|| • If K 0 |= γ ⊂ Π 1≤i≤n l i : ρ i then ||γ|| ⊂ Π 1≤i≤n l i : ||ρ i ||
Theorem 26 (adequation lemma) If there is an interpretation for an annotated program M satisfying the typing constraints K 0 extracted from M , then M ∈ ⊥ ⊥ which implies that M is safe and that all infinite reductions use the fixpoint rule infinitely often.

Proof: Let M be an annotated program, (C, R 0 , D) be the constraints extracted from M and assume that we have an interpretation satisfying these constraints. If N is a subterm of M we write Γ(N ) = x α 1 1 , . . . , x αn n the set of free variables that are bound above N with their type annotation (all the free variables of N are mentioned in Γ(N )). We say that a substitution σ = [(

x i ← u i ) i∈{1,...,n} ] satisfies Γ(N ) if for all 1 ≤ i ≤ n we have u i ∈ ||α i ||.
Next, we show by induction on the structure of M , that for all subterm N β , if σ is a substitution satifying Γ(N ), then N σ ∈ ||β||.

• If N β = x β the result is immediate from the definition of substitution satisfying Γ(x β ).

• If N β = N γ 1 N φ 2 ,
we know that ||γ|| ⊂ ||φ|| → ||β|| and by induction hypothesis, we have • If N β = (fun y φ → N γ 1 ) β , we have ||φ|| → ||γ|| ⊂ ||β|| and by induction hypothesis, for σ ′ satisfying Γ(N 1 ), we have

N 1 σ ∈ ||γ|| and N 2 σ ∈ ||φ||. Let us choose E ∈ |β|, we must prove N ⋆ E ∈ ⊥ ⊥. We have N σ ⋆ E = N 1 σ ⋆ E[χ ← χ N 2 σ], E[χ ← χ N 2 σ] ∈ ||φ||.
N 1 σ ′ ∈ ||γ||. Therefore, it is enough to choose E ∈ ||φ||.|γ| and show that N σ ⋆ E ∈ ⊥ ⊥ (this gives N σ ∈ (||φ||.|γ|) ⊥ = ||φ|| → ||γ|| ⊂ ||β||). From E ∈ ||φ||.|γ| we deduce that E = E ′ [χ ← χ P ] with P ∈ ||φ|| and E ′ ∈ |γ|. We have N σ ⋆ E = E ′ [χ ← (fun y → N 1 )σ P ].
Up to a renaming of y, we assume that y is not free in the domain and images of σ and we have

E ′ [χ ← (fun y → N 1 )σ P ] = E ′ [χ ← (fun y → N 1 σ) P ] ≻ β N 1 σ[y ← P ] ⋆ E ′ .
Then, by the definition of saturated sets and because P ∈ ||φ|| ⊂ ⊥ ⊥, we just need to prove that

N 1 σ[y ← P ] ∈ ||γ||, which is immediate because P ∈ ||φ|| implies that σ • [y ← P ] is a substitution satisfying Γ(N 1 ) = y φ , Γ(N ). • If N β = (fix x φ → N γ 1
) β , we have ||γ|| ⊂ ||φ|| and ||γ|| ⊂ ||β||. As in the previous case, we assume x not to be free in the domain nor the images of σ. We prove by induction that for all n ∈ N we have (N

1 σ) n (x) ∈ ||γ||. If n = 0, this is immediate because σ ′ = σ • [x ← x] satisfies Γ(N 1 ) because x ∈ ⊥ ⊥ 0 ⊂ ||φ||. For the induction case, we assume (N 1 σ) n (x) ∈ ||γ|| and prove (N 1 σ) n+1 (x) ∈ ||γ||. The hypothesis ||γ|| ⊂ ||φ|| implies that σ • [x ← (N 1 σ) n (x)] is a substitution satisfying Γ(N 1 ). Then, let E ∈ |γ|, we have (N 1 σ) n+1 (x)⋆E = N 1 σ[x ← (N 1 σ) n (x)]⋆E ∈ ⊥ ⊥ by the induction hypothesis on N 1 .
Finally, by definition of saturated set, we know that (N

1 σ) n (x) ⋆ E ∈ ⊥ ⊥ for all n ∈ N implies (fix x → N 1 σ) = N σ ⋆ E ∈ ⊥ ⊥ which is what we wanted (we do have N 1 σ ∈ ||γ|| ⊂ ⊥ ⊥). • If N β = C[N φ 1 ] β , we have C[||φ||] = (C[|φ|]) ⊥ ⊂ ||β||. Let E ∈ C[|φ|] be, which means that E can be written (case χ of C[χ] → E 1 ) ⋆ E ′ where E 1 ⋆ E ′ ∈ ||φ|| ⊥ . By induction hypothesis we deduce N 1 σ ⋆ (E 1 ⋆ E ′ ) ∈ ⊥ ⊥ which implies by saturation that N ⋆ E ∈ ⊥ ⊥. • If N β = case P γ of (C i [x φ i i ] → N β i i ) i∈I , we have for all i ∈ I, ||β i || ⊂ ||β|| and ||γ|| ⊂ Σ i∈I C i [||φ i ||]. Let E be a context in |β|. The induction hypothesis and ||β i || ⊂ ||β|| implies that for any term Q i ∈ ||φ i ||, we have N i σ[x i ← Q i ] ⋆ E = Q i ⋆ (N i σ[x i ← χ] ⋆ E) ∈ ⊥ ⊥ for all i ∈ I. This means that N i σ[x i ← χ] ⋆ E ∈ ||φ i || ⊥ = |φ i |. Thus by definition of Σ, this means that (case χ of (C i [x i ] → N i σ) i∈I ) ⋆ E ∈ Σ i∈I C i [|φ i |] ⊂ ||γ|| ⊥ which gives, together with P σ ∈ ||γ||, N σ ⋆ E = P σ ⋆ (case χ of (C i [x i ] → N i σ) i∈I ) ⋆ E ∈ ⊥ ⊥. • If N β = {(l i = N γ i i ) i∈I } β , we have Π i∈I l i : ||γ i || ⊂ ||β|| and by induction hypothesis, N i σ ∈ ||γ i ||. Let E ∈ Π i∈I l i : |γ i |, E can be written χ.l j ⋆ E j for some j such that E j ∈ |γ j |. Therefore, N j σ ⋆ E j ∈ ⊥ ⊥ which implies by saturation that (N σ).l j ⋆ E j = N σ ⋆ E ∈ ⊥ ⊥. • If N β = (N φ
1 .l) β , we have ||φ|| ⊂ l : ||β|| and, by induction hypothesis,

N i σ ∈ ||φ||. Let E ∈ |β|, by definition of Π, we have E[χ ← χ.l] ∈ Π l : |β| ⊂ |φ|. Therefore, N σ ⋆ E = N i σ ⋆ E[χ ← χ.l] ∈ ⊥ ⊥.
Here is the code extracting the constraints from an annotated program. It starts with a few functions adding constraints in the triplet (C, R 0 , D), not forgetting to ensure that R 0 has only 1 on its diagonal: The first step when checking the constraints is saturation. To define it, we need to define a new product C.R.D where C are constructor constraints, R is a matrix with coefficient in B and D are destructor constraints. This product is partial and the fact that it is undefined will be a type error . Here is the definition:

Definition 27 (ternary product) R ′ = C.R.D is the smallest hermitian matrix for lattice ordering such that:

• If (C, R, D) |= α → β ⊂ γ, (C, R, D) |= γ ⊂ γ ′ and (C, R, D) |= γ ′ ⊂ α ′ → β ′ then R ′ |= α ′ ⊂ α and R ′ |= β ⊂ β ′ • If (C, R, D) |= Σ i∈I C i [α i ] ⊂ γ, (C, R, D) |= γ ⊂ γ ′ and (C, R, D) |= γ ′ ⊂ Σ j∈J C j [α ′ j ] then, if I ⊂ J, for all i ∈ I R ′ |= α i ⊂ α ′ i .
If I ⊂ J, then the product is undefined (here we assume that C i = C j implies i = j).

• If (C, R, D) |= Π j∈J l j : α j ⊂ γ, (C, R, D) |= γ ⊂ γ ′ and (C, R, D) |= γ ′ ⊂ Π i∈I l i : α ′ i then, if I ⊂ J, for all i ∈ I R ′ |= α i ⊂ α ′ i .
If I ⊂ J, then the product is undefined (here we assume that l i = l j implies i = j).

• If (C, R, D) |= L ⊂ γ , (C, R, D) |= γ ⊂ γ ′ and (C, R, D) |= γ ′ ⊂ R and
(L, R) matches one of the following pairs: (Σ , → ), (Π , → ), ( → , Σ), ( → , Π), (Σ , Π ), or (Π , Σ ) then R ′ = C.R.D is undefined

Remark: this definition really resembles two matrix products where the summation indexes are γ and γ ′ which do not appear as index in the result matrix.

Here is the code defining this ternary product: We need to compute the smallest saturated constraints (C, R, D) such that R ≥ R 0 . A first way is to define R n+1 = R n .R n ∨ C.R n .D. Recall that R 0 has only 1 on the diagonal. This property is preseved for all the matrices R n because 1 is the top element of the lattice B and this implies R n .R n ≥ R n . The fact that the sequence is increasing implies that it converges toward the wanted matrix because the lattice B is of finite height 2. This means that the limit is reached before n = 2N 2 where N is the number of lines of the matrix R, that is the number of type names mentioned in the initial constraints. When the above sequence reaches its limit R, we have

R = R.R ∨ C.R.D.
However, the abobe definition would lead to a bad complexity. A better sequence is:

• S 0 = R ′ 0 = R 0 • T n = R ′ n .S n ∨ S n .R ′ n ∨ C.S n .D • R ′ n+1 = T n ∨ R ′ n • S n+1 = T n -R ′ n
With this definition, we clearly have for all n, S n ≤ T n ≤ R ′ n and by induction we get R ′ n ≤ R n . The sequence R ′ n is still increasing, and by definition of the subtraction, we have R ′ n = 0≤i≤n S n . Then, we deduce R ′ n+1 ≥ S i .S j for 0 ≤ i, j ≤ n and R ′ n+1 ≥ C.S i .D for 0 ≤ i ≤ n, which implies by summing the inequalities

R ′ n+1 ≥ R ′ n .R ′ n ∨ C.R ′ n .
D and therefore we have R ′ n = R n by induction.

Remark: when R ′ n reaches its limit, we have S n = 0 (because T n ≤ R ′ n , otherwise the limit would not be reached) which is an easy stopping condition.

To compute the complexity, let us define |S n | the number of non zero coefficients of S n and N the number of types names in the annotated program M which produced the initial constraints (C, R 0 , D). The definition of subtraction implies that S n+1 ∧ R n = 0 (the matrix with only 0). This means that the total number of non zero coefficients in all the matrices S n (Σ 1≤i≤n |S n |) is less then 2. Remark: the analysis here assumes a constant time access to vectors and matrix coefficients. A more reasonnable complexity would be O(N 3 ln 2 (N )).

Exercise 30 Find the best representation of each matrix to get a complexity O(N 3 ln 2 (N )) (or better, but in this case, let me know ... especially if you drop the 3 exponent.).

This means that we proved the following theorem:

Theorem 31 Let (C, R 0 , D) be the constraints extracted from an annotated program M , the smallest saturated constraints (C, R, D) such that R ≥ R 0 can be computed (if it exists) in polynomial time (O(N 3 ln 2 (N ))).

It is also trivial, from the fact that R ≥ R 0 , that is we can find an interpretation satisfying the constraint (C, R, D), it also satisfies (C, R 0 , D).

Here is the code computing the saturated constraints: Unfortunately, even if (C, R, D) can be computed from (C, R 0 , D), it does not imply that the constraints are satisfiable. We need another criteria: the well-foundedness of the constraints. This is here that we will use the lattice B ′ :

28 in 29 f n 0 W0 W0
Listing 13: well-foundedness check in typing.ml Now, we can state our last theorem:

Theorem 34 If the saturated constraints K = (C, R, D) are well founded then, they are satisfiable which means that there is an interpretation using definition 25 satisfying the constraints.

Proof: Let W be the hermitian matrix witnessing the well-foundedness of the saturated constraints (C, R, D). We can directly define the interpretation as follows:

||α|| = {||β|| s.t. K |= β ⊂ α} ∨ {||β|| → ||γ|| s.t. K |= β → γ ⊂ α} ∨ {Σ i∈I C i [||β i ||] s.t. K |= Σ i∈I C i [β i ] ⊂ α} ∨ {Π i∈I l i : ||β i ||] s.t. K |= Π i∈I l i : β i ⊂ α}
The use of the well foundedness constraints is to show that this definition makes sense. For this, we need to remark that by definition of W , if β is used in the definition of α, then we have W |= β α and moreover, if β is used in the definition of α at the right of an implication, then W |= β ≺ α.

This means that if W |= β α but W |= β ≍ α then, we can define ||β|| strictly before ||α||. Next, we remark that W |= β ≍ α is an equivalence relation and for {β 1 , . . . , β n } an equivalence class of this relation, we know that ||β i || is only used in a covariant position in the definitions of ||β j || for 1 ≤ i, j ≤ n. This means that ||β 1 ||, . . . , ||β n || can be defined simultaneously as a smallest fixpoint using the above definition.

Next, we prove that this interpretation satisfies the constraints (C, R, D). For C and R this is immediate because they are directly included in the definition. To treat the destructors contraints D, we first remark that the above definition is equivalent to:

||α|| = {||β|| → ||γ|| s.t. ∃α ′ , K |= β → γ ⊂ α ′ and K |= α ′ ⊂ α} ∨ {Σ i∈I C i [||β i ||] s.t. ∃α ′ , K |= Σ i∈I C i [β i ] ⊂ α ′ and K |= α ′ ⊂ α} ∨ {Π i∈I l i : ||β i ||] s.t. ∃α ′ , K |= Π i∈I l i : β i ⊂ α ′ and K |= α ′ ⊂ α}
This is true, just by replacing the ||β||'s in {||β|| s.t. K |= β ⊂ α} by their definition.

Then, we may verify that constraints in D are satisfied:

• If K |= α ⊂ β → γ, we have ||α|| = {||β|| → ||γ|| s.t. ∃α ′ , K |= β ′ → γ ′ ⊂ α ′ and K |= α ′ ⊂ α}.
• If K |= α ⊂ Σ i∈I C i [β i ] or K |= α ⊂ Π i∈I l i : β i , the proof is similar.

Further work

We describe here, extensions of the algorithm that are already implemented in PML but for which there is no theoretical result published (this should change in the near future).

Types

Consider the following program:

fix id nat n → case n of | Z[] → Z[] | S[n'] → S[id nat n']
It is clear what it does: it is a function copying a unary natural number! In other terms, this is the partial identity function whose domain is exactly the unary natural numbers. But what does the type-checking algorithm when we use that function ? It creates constraints that ensures that the argument of the function id nat is a unary natural number and constraints enforcing that the result can only be used as a natural number. This means that we can use partial identity functions as types. We just need to decide a syntax for types, for instance:

Type := Type → Type | [C 1 [Type]| . . . |C n [Type]]
| {l 1 : Type; . . . ; l n : Type} | fix t → T Which will be translated as partial identity functions as follows (if T is a type, then T is a partial identity function):

T 1 → T 2 = fun f → fun x → T 2 (f (T 1 x)) [C 1 [T 1 ]| . . . |C n [T n ]] = fun s → case s of (C i [x] → C i [T i x]) 1≤i≤n {l 1 : T 1 ; . . . ; l n : T n } = fun r → {(l i = T i r.l i ) 1≤i≤n } fix t → T = fix t → T
What remains to do is to show that the above translation from types to programs do correspond in some sense to identity functions. This is easy by induction for all cases but function types. For function types, we need the notion of η-equivalence. We also would like to have parametric types, which can be done by having a new kind of arrow in type constraints which is interpreted exactly as the set of identity functions and this will ensure that parametric types are used with the correct number of parameters. This approach even allows for higher-order parametric types which are not available in usual ML implementations.

Simplification of the constraints and Polymorphism

The current implementation of PML extends the algorithm presented here with an algorithm simplifying the typing constraints by removing type names which can not be accessed anymore (as in [START_REF] Pottier | Simplifying subtyping constraints: a theory[END_REF]). A type name is said to be accessible in a program if, by using this program, we can create new constraints on this name. This is very important to have a reasonable complexity in practice.

Moreover, it allows for a nice implementation of polymorphism that defines the least set of type names that must be generalized. Not taking the least set would result in a non terminating algorithm. This least set is a smallest set satisfying some closure property and containing all type names α that are accessible from the left and the right which means that the newly created constraints are respectively of the form ⊂ α and α ⊂ .

Larger lattices

Many applications require using an enlarged lattice for type constraints that will still be a relational lattice. Here are a few (the ones used in PML):

• The type constraints contain a lot of information useful for a compiler.

Unfortunately, if we use types, we do not want to compile the corresponding identity function and we can loose some information. A solution is to replace our lattice B with B × B using one component for type constraints ignoring types and the other for types constraints with types. This basically allows for maximum sharing compared with an approach when one would type-check the program twice: with types and without types.

• The language presented here do not have a default case in case analysis nor extensible records. Both features require the typing constraints to know that some variant constructors or labels can be ignored. This can be done by replacing the lattice B with functions in V Σ ∪ V Π → fin B (here → fin means function which are constant except on a finite set). This allows to say that a constraint ignores or concerns only specific variants or labels. This is exactly what we need for default cases and extensible records.

• Operator overloading is a very nice feature of programming languages. When an operator is overloaded, we need to know what implementation to choose, one way is to replace the lattice B by the set of binary decision diagram having elements of B at their leafs and testing boolean variables at their nodes. These variables express specific choices for overloaded operators. For instance if the constant 0 α (written with its type annotation) can be interpreted by two programs zero int β and zero float β ′ , the type constraints will be something like β ⊂ α=zero int α and β ′ ⊂ α=zero float α where α = zero int and α = zero float are boolean variables which indicates which version of 0 is chosen. These variables clearly need to satisfy the axioms ¬(α = zero int ∧ α = zero float) and α = zero int ∨ α = zero float.

This was surprisingly easy to implement in PML ... However, this is clearly NP-complete. But other parts of traditional ML compilation have bad worst-case complexity (polymorphism is exponential, test for exhaustive pattern-matching is NP-complete, ...).

Figure 1 :

 1 Figure 1: Reduction of halving

Figure 2 :

 2 Figure 2: Reduction of length

7 .

 7 First, it is clear that {χ} ⊥ = ⊥ ⊥: by definition, M ∈ {χ} ⊥ if and only if M ⋆χ = M ∈ ⊥ ⊥. Let E be a set of contexts with at least one occurrence of χ in one element E ∈ E. Then, M ⋆ E ∈ ⊥ ⊥ implies that E[χ ← M ] ∈ ⊥ ⊥ which implies that M ∈ ⊥ ⊥, because if M has a bad reduction, then E[χ ← M ] has also one, because χ really occurs in E.

Figure 3 :Figure 4 :

 34 Figure 3: The lattice B

  . Then, matrices are just vectors of vectors: open L a t t i c e type ( ' index , ' c o e f ) v e c t o r = ( ' i n d e x * ' c o e f ) l i s t ( * o r d e r e d by i n d e x * ) type ( ' index1 , ' index2 , ' c o e f ) m a tri x = ( ' index1 , ( ' index2 , ' c o e f ) v e c t o r ) v e c t o r Listing 3: vectors in matrix.ml

2 Listing 4 :

 24 r → ' a = fun bn l n rn a v e c t o r 1 v e c t o r 2 → l e t rec f n a c c v1 v2 = match v1 , v2 with | v1 , [ ] → L i s t . f o l d l e f t ( fun a c c ( i , c ) → l n a c c i c ) a c c v1 | [ ] , v2 → L i s t . f o l d l e f t ( fun a c c ( i , c ) → rn a c c i c ) a c c v2 | ( i , c ) : : v1 , ( i ' , c ' ) : : v2 when i = i ' → f n ( bn a c c i c c ' ) v1 v2 | ( i , c ) : : v1 , ( i ' , c ' ) : : when i < i ' → f n ( l n a c c i c ) v1 v2 | ( i , c ) : : , ( i ' , c ' ) : : v2 ( * when i > i ' * ) → f n ( rn a c c i ' c ' ) v1 v2 in f n a v e c t o r 1 v e c t o r fold on vectors in matrix.ml Using this folding function, we implement all the needed operations on vectors and matrices: l e t s u m v e c t o r v1 v2 = L i s t . r e v ( f o l d 2 v e c t o r ( fun a c c i c c ' → ( i , sup c c ' ) : : a c c ) ( fun a c c i c → ( i , c ) : : a c c ) ( fun a c c i c → ( i , c ) : : a c c ) [ ] v1 v2 ) l e t s u b v e c t o r v1 v2 = L i s t . r e v ( f o l d 2 v e c t o r ( fun a c c i c c ' → l e t c ' ' = sub c c ' in i f c ' ' = Nothing then a c c e l s e ( i , c ' ' ) : : a c c ) ( fun a c c i c → ( i , c ) : : a c c ) ( fun a c c i c → a c c ) [ ] v1 v2 ) l e t sum matrix m1 m2 = L i s t . r e v ( f o l d 2 v e c t o r ( fun a c c i v1 v2 → ( i , s u m v e c t o r v1 v2 ) : : a c c ) ( fun a c c i v → ( i , v ) : : a c c ) ( fun a c c i v → ( i , v ) : : a c c ) [ ] m1 m2) l e t s u b m a t r i x m1 m2 = L i s t . r e v ( f o l d 2 v e c t o r ( fun a c c i v1 v2 → l e t v = s u b v e c t o r v1 v2 in i f v = [ ] then a c c e l s e ( i , v ) : : a c c ) ( fun a c c i v → ( i , v ) : : a c c ) ( fun a c c i v → a c c ) [ ] m1 m2) l e t d o t p r o d u c t v1 v2 = f o l d 2 v e c t o r ( fun a c c i c c ' → sup a c c ( p r o d u c t c ( a d j o i n c ' ) ) ) ( fun a c c i c → a c c ) ( fun a c c i c → a c c ) Nothing v1 v2 l e t m a t r i x p r o d u c t m1 m2 = L i s t . f i l t e r ( fun ( , r ) → r <> [ ] ) ( L i s t . map ( fun ( i , v1 ) → i , L i s t . f i l t e r ( fun ( , r ) → r <> Nothing ) ( L i s t . map ( fun ( j , v2 ) → j , d o t p r o d u c t v1 v2 ) m2) ) m1)

  when A has coefficients in B ′ ) Lemma 20 Using the definition of multiplication and the above notation, we can give an equivalent to the definition of Hermitian matrix multiplication: if A, B are Hermitian matrices with coefficienst in B. Then, A.B in the smallest matrix such that A |= α ⊂ β and B |= β ⊂ γ implies A.B |= α ⊂ γ Proof: Immediate. Exercise 21 If A and B are hermitian matrices with coefficients in B ′ write a similar lemma with four cases, because you have to use and ≺.

  |β| and N 1 σ ∈ ||φ|| → ||β|| = (||φ||.|β|) ⊥ which gives the wanted result.

  l e t a d d c o n s t r u c t o r i n f o i c = { i n f o with c o n s t r u c t o r s = L i s t . r e v ( f o l d 2 v e c t o r ( fun a c c i c c ' → a s s e r t f a l s e ) ( fun a c c i c → ( i , c ) : : a c c ) ( fun a c c i c → ( i , c ) : : a c c ) [ ] i n f o . c o n s t r u c t o r s [ i , c ] ) ; r e l a t i o n s = sum matrix i n f o . r e l a t i o n s [ i , [ i , Equal ] ] ; } l e t a d d d e s t r u c t o r i n f o i d = { i n f o with d e s t r u c t o r s = L i s t . r e v ( f o l d 2 v e c t o r ( fun a c c i c c ' → ( i , c @ c ' ) : : a c c ) ( fun a c c i c → ( i , c ) : : a c c ) ( fun a c c i c → ( i , c ) : : a c c ) [ ] i n f o . d e s t r u c t o r s [ i , [ d ] ] ) ; r e l a t i o n s = sum matrix i n f o . r e l a t i o n s [ i , [ i , Equal ] ] ; } l e t a d d c o e f m i 1 i 2 = sum matrix m ( sum matrix ( sum matrix [ i 1 , [ i 1 , Equal ] ] [ i 2 , [ i 2 , Equal ] ] ) a d d d e s t r u c t o r i n f o s a l l ( DPro ( l i d , r e s ) ) in f n i n f o s env p | Rec ( r e c o r d , a l l ) → l e t , i n f o s , l l = L i s t . f o l d l e f t ( fun ( env , i n f o s , l l ) ( l i d , p ) → l e t a r g = g e t i n d e x env p in l e t l l = ( l i d , a r g ) : : l l in l e t i n f o s = f n i n f o s env p in l e t env = ( l i d , a r g ) : : env in env , i n f o s , l l ) ( env , i n f o s , [ ] ) r e c o r d in a d d c o n s t r u c t o r i n f o s a l l ( CPro l l ) in f n { c o n s t r u c t o r s = [ ] ; d e s t r u c t o r s = [ ] ; r e l a t i o n s = [ ] } [ ] p Listing 10: constraints extraction in typing.ml 6 Checking the constraints

exception

  Type Error of p o s i t i o n * c o n s t r u c t o r * p o s i t i o n * d e s t r u c t o r l e t t e r n a r y p r o d u c t c o n s t r u c t o r s r e l a t i o n s d e s t r u c t o r s = f o l d 2 v e c t o r ( fun a c c i c v → f o l d 2 v e c t o r ( fun a c c j ( ds : d e s t r u c t o r l i s t ) r → i f l e q Leq r then L i s t . f o l d l e f t ( fun a c c ( d : d e s t r u c t o r ) → try match c , d with | CFun( arg , r e s ) , DFun( arg ' , r e s ' ) → a d d c o e f ( a d d c o e f a c c r e s r e s ' ) arg ' a r g | CSum( c i d , a r g ) , DSum( l ) → a d d c o e f a c c a r g ( L i s t . a s s o c c i d l ) | CPro ( l ) , DPro ( l i d , a r g ) → a d d c o e f a c c ( L i s t . a s s o c l i d l ) a r g | → r a i s e Not found with Not found → r a i s e ( Type Error ( i , c , j , d ) ) ) a c c ds e l s e a c c ) ( fun a c c j → a c c ) ( fun a c c j → a c c ) a c c d e s t r u c t o r s v ) ( fun a c c i → a c c ) ( fun a c c i → a c c ) [ ] c o n s t r u c t o r s r e l a t i o n s Listing 11: ternary product in typing.ml after extraction Definition 28 (saturated constraints) We say that the typing constraints (C, R, D) are saturated if and only if R ≥ R.R ∨ C.R.D. Exercise 29 Write a more intellegible (but longer) definition of saturated constraints using the notation (C, R, D) |= . . ., lemma 20 and the definition 27 of ternary product.

N 2 .

 2 The product R ′ n .S n , S n .R ′ n and C.S n .D needs a computing time which is less than O(N |S n |) (the N for the product C.S n .D is there because D is a multi-vector). We have also the same upper bound for the number of nonzero coefficients O(N |S n |) in the resulting matrices. This means that the two supremums and the subtraction can be done in time O(N |S n |) too. Therefore, globally, we have a complexity of Σ 1≤i≤2N 2 O(N |S n |) ≃ O(N 3 ).

  l e t s a t u r a t e v e r b o s e i n f o = l e t rec f n n Rn Sn = l e t Tn = sum matrix ( sum matrix ( m a t r i x p r o d u c t Rn Sn ) ( m a t r i x p r o d u c t Sn Rn ) ) ( t e r n a r y p r o d u c t i n f o . c o n s t r u c t o r s Sn i n f o . d e s t r u c t o r s ) in l e t S n p l u s o n e = s u b m a t r i x Tn Rn in i f S n p l u s o n e = [ ] then Rn e l s e l e t R n p l u s o n e = sum matrix Tn Rn in f n ( n+1) R n p l u s o n e S n p l u s o n e in l e t R = f n 0 i n f o . r e l a t i o n s i n f o . r e l a t i o n s in { i n f o with r e l a t i o n s = R } Listing 12: constraint saturation in typing.ml

  end | VFun( id , p , env ) , SApp ( c , s t a c k ) → e v a l ( Some " \\ b e t a " ) ( ( id , c ) : : env ) p s t a c k | VRec ( r e c o r d ) , SPi ( l i d , s t a c k ) → u n f o l d ( Some " \\ p i " ) ( L i s t . a s s o c l i d r e c o r d ) s t a c k | VCst ( c i d , v ) , SCas ( c a s e s , s t a c k ) → l e t id , p , env = L i s t . a s s o c c i d c a s e s in e v a l ( Some " \\ sigma " ) ( ( id , v ) : : env ) p s t a c k | VFix ( p , env ) , s t a c k → e v a l ( Some " \\mu" ) env p s t a c k | → a s s e r t f a l s e with Not found → a s s e r t f a l s e in e v a l None [ ] p SEmpty

Listing

  |= β ⊂ β ′ and K |= γ ′ ⊂ γ. This implies ||β|| ⊂ ||β ′ || and ||γ ′ || ⊂ ||γ|| which implies ||β ′ || → ||γ ′ || ⊂ ||β|| → ||γ|| and therefore ||α|| ⊂ ||β|| → ||γ||

The other sets in the supremum are empty otherwise the ternary product C.R.D would be undefined and this contradicts the hypothesis that (C, R, D) are saturated. Because of saturation, for all α ′ , β ′ , γ ′ such that K |= β ′ → γ ′ ⊂ α ′ and K |= α ′ ⊂ α, we also have K

  16: Call by calue in program.ml

	Index
	⊥ ⊥-saturated, 10	relation lattice, 16
	abstract syntax of programs, 9	relational constraints, 21
	adequation lemma, 23	safe, 7
	adjoin operation, 15	satisfiable, 30
	bad reduction, 9	saturated constraints, 27
	beta reduction, 6	ternary product, 26
	call-by-value, 7, 33 case selection, 6 Church-Rosser property, 7 closure, 34	type error, 26 type names, 15 types, 15 typing constraints, 21
	coinduction, 11	variables, 5
	constructions, 14
	constructor constraints, 21
	constructor names, 5
	context, 6, 10
	contravariant, 12
	covariant, 12
	destructor constraints, 21
	double bottom, 9
	extracted constraints, 22
	fixpoint, 6
	fold, 18
	hermitian matrix, 18
	interpretation, 23
	label names, 5
	lattices, 15
	manifest error, 7
	multi-vector, 20
	operational semantics, 6
	opponent, 10
	orthogonal, 12
	productive, 11
	projection, 6
	property of realizability candidates, 13
	realizability candidates, 9, 13

http://lama.univ-savoie.fr/tracpml

with Not found → P r i n t f . f p r i n t f s t d e r r "Unbound i d e n t i f i e r %s \n" name ; e x i t 1

Listing 9: extracting the root annotation in typing.ml Now, we have the extraction of constraints itself. It uses an environment env to store the decoration of free variables: Definition 32 We say that the saturated constraints (C, R, D) are well-founded if there exists an hermitian matrix W with coefficients in B ′ and 1 on the diagonals such that:

Theorem 33 We can compute the matrix W (when it exists) and test if the constraints (C, R, D) are well-founded in polynomial time complexity.

Proof: We can easily (in time O(N 2 ln 2 N )) produce an initial matrix W 0 ≥ R (we use B ⊂ B ′ to write this) satisfying all conditions but the last one and then, we can define a sequence computing the smallest matrix W such that W ≥ W 0 and W ≥ W.W using an algorithm similar to the previous one.

Example: for the term omega, even the initial matrix W 0 is undefined because it should satisfy

Here is the code checking for well-foundedness, with a first function adding the initial constraints α ≺ β coming from the constraints like K |= α → α ′ ⊂ β: l e t a d d c o e f s t r i c t m i 1 i 2 = sum matrix m ( sum matrix

) ) l e t o r d e r s a t u r a t e v e r b o s e i n f o s = l e t rec f n n Wn Sn = i f v e r b o s e then begin p r i n t m a t r i x a s j u d g m e n t p r i n t r e l a t i o n i n B p a s t e x ( " S " ˆs t r i n g o f i n t n ) Sn ; p r i n t a s 0 " \\ c r " ; p r i n t n e w l i n e (

A Call by value semantics

We can also give some code for a call-by-value semantics. First, let us define values as a BNF :

Here is the type definition for values, with a few differences:

• It is parameterized, because 'a program is parameterized.

• In the fun case, we give an environment holding the value for all variables.

This avoid us to perform substitution. We are making a closure. To program call by value we will use an abstract machine with a stack, and an environment. The stack will hold not only arguments for functions, but all pending destructors. This is reflected by the following type definition with stack constructors corresponding to application (SApp to hold an argument and RApp to remember the function while computing the argument), projection (SPi) and case analysis (SCas). The constructor RCst and RRec remembers the constructor and the rest of a record while computing one of the field.

Listing 15: Stacks in program.ml

Here is now the code for a call-by-value interpretor. You may notice that it basically consists in two mutually recursive functions: eval and unfold. The first is evaluating programs more or less as expected. The second function is applying the stack elements to a value.

We could have simplified the code but removing RApp, RCst and RRec if we used OCaml's stack. But we preferred to give a tail-rec evaluator nearer to the behavior of some compiled code.

Exercise 35 (not easy and out of the scope of this course) prove that this code implements call by value evaluation.

Exercise 36 There is a small trick is the code below to implement some sort of recursive definition which is not in the definition of the operational semantics of the language .


In India, the decade of 1990s will be marked by its integration into a globalised economy as a result of its policy of liberalisation. By favouring the development of export industries and of delocalisation, liberalisation has enabled the growth of women's employment in most of the countries of the South, particularly in India and in our case in small cities of an industrial cluster in Tamil Nadu In traditionnal areas where some husbands do not fulfil their responsibilities as head of family, women look upon their employers as their benefactors as they provide the women the possibility of earning even though their salaries might be ridiculously low. Our study show that the factory has enabled many women to step out of their domestic space increased their mobility and their new use of urban space, either to go to work or to visit relatives, helped them to be less dependant on the in-laws by an involvement in the decisions taken about the way in which income are to be used and thus earning respect in society. These new activities provide the women an opportunity to express their desire to create a forum for speech collective action, and new identity and thus to establish their autonomy and scope for negotiation and empowerment.

Context of the study

In India, the development of export industries during the 1990s has enabled the growth of women's employment in most of the countries of the South, particularly in India and in our case in Vellore district (fig. 1). The example of a leather industrial cluster in rural Tamil Nadu fully brings out this phenomenon. This industrial cluster is the main producer of leather products in India. Shoe factories and tanneries have created job opportunities for women who constitute the unskilled labour in this sector, even though these women are much better educated than agricultural workers. The number of working Indian women is growing, the majority of such women, that is to say the poorest, work from compulsion and because they never had any choice, and for salaries which are distinctly lower than those of men (except in public service).

Main questions

As a human geographer, it seems important in my opinion to use the new theoretical approaches on gender issues and apply them to analyse mobilities. Until now, Social and spatial Mobilities are male biased. The invisibility of the women in the studies concerning mobilities is obvious. Male mobility versus settled female. Talking about mobilities implies many forms of movement : mobility is spatial and social or vertical and horizontal. Mobility must be analysed as a process. In India except the female migration of marriage, the female work mobilities are not studied. So my study is focussed on the different forms of female work mobilities : spatial, intersectorial, professional and social. To understand fully the implications of industrialisation for women, we would also need to examine the impact of women's earnings on intrahousehold income and decision making. In other words, we would need to analyse wether a wage empowers women within the household and increases their autonomy. In the view of Amartya [START_REF] Sen | Un nouveau modèle économique, développement, justice et liberté[END_REF], salaried employment of women increases their power to negotiate their position and power both at home and in the economy and helps towards their social emancipation.

Methodology

For our study, The leather industrial cluster in Vellore district in Tamil Nadu has been chosen because we can find different types of jobs for women in agriculture and industry.

Almost 80 shoe factories are located along the Palar river around Ambur and Ranipet employing almost 6000 permanent workers according to the Inspector of factories. But according to our survey, a lot of casual workers are employed, so it's difficult to know the exact number of women employed. But, today, according to the managers, we can say that more than 16000 young women (<45 years) of different communities (hindu, christian and muslim) are employed in these shoe factories. So to conduct a survey concerning the different occupations of women in Palar Valley and the impact of the work on gender relations, we have decided to make some interviews, almost two hundred between Vanyambadi and Ranipet. During these interviews, we get on topics concerning socio-economic characteristics, religion, cast, level of education, migratory steps, professionnal biography and most of all, the mobilities of the women (activities oustside the house during one day, one week…) and the relationship with husband and family and problems (poverty, ill-treatment, beating, alcoholism…). We stayed almost one or two hours with each person. During our second survey, we have decided to focus my research around Ranipet, which is an important industrial zone in Palar valley. This city of almost 70 000 inhabitant belongs to an industrial zone who covers also Walajapet and Arcot. To understand the circular mobilities and the activities of the women and their condition, we interviewed some managers about the social advantages (maternal holidays, holidays canteen…), the wages for male and female, overtime…We are not very confident about theirs answers, and it is difficult to have any confirmation because the unions are forbidden. But we have to know that a minimum salary doesn't exist and because of these conditions, there is a big turnover amongst the workers. To have an idea about the residence of these women, we met the manager of the ESI (Insurance of the workers) who gets all the details about the residence of these women workers, because the managers of the factories have to declare their workers to the Insurance. But the ESI only knows the residence of the permanent workers and we must bare in mind that there is a casualisation of the labour in this formal sector. Anyway, it helps us to identify the villages and the areas of the cities representative of the industrialised labour.

Flexibility of labour market and emergence of salaried class of women industrial workers

Globalisation, which has helped in the growth of export oriented manufacturing industries, has given the impetus to the emergence of salaried class of women industrial workers not only in urban areas but in rural areas as well. In the context of globalisation and international competitiveness, employers prefer locating their factories in small cities in order to optimise the cost of production and to benefit from economies of scale. At this time of global capital market, it is imperative for all employers to have cheap and flexible labour of internationally comparable quality in order to maintain and increase the competitive advantage at the international scale.

For example, in Palar valley, many shoe factories have closed not only, because of the campaign against the killing of the cows, but also because the competition is very hard, considering the fact that the women labour is cheaper in China, Bangladesh and Pakistan as we have been said by the 15 managers we met recently. And it is well known that hundreds tanneries have closed since 1998 because of the pollution. But now, the chairman of the KH group of companies in Ranipet (Hashim) said that the leather industry has invested Rs 150 crores in the last 8 years on the installation of common effluent treatment plants of which only 20 crores were given as subsidy by government. Concerning the problem of cow slaughter, the industrialist is very upset because 90% of the leather came from goats, sheep and buffaloes1 . Anyway, it remains a big political issue.

The processes of rendering industrial production more flexible and of globalisation have not had the same effect on women as on men. Though this flexibility is the reason for feminisation of jobs long dominated by men, several studies have also shown that women are paid less than men, under take new types of employment (part time, temporary, domiciliary, unit rate ...) and cannot claim promotion in jobs which make their jobs insecure. Women, whose labour costs less, are much sort after by employers, even more in rural than in urban areas as we can see in Palar valley. It has been observed that female labour is cheap not only because of difference between the wages of men and women but also because of the lack of security and lack of protection which characterise women's labour and are both linked to the flexibility of the labour market. On the other hand women also prefer some flexibility in their work which allows them to take care of their families. Their docility is also the reason for employers preferring women labourers.. The processes of rendering industrial production more flexible and of globalisation have not had the same effect on women as on men. Though this flexibility is the reason for feminisation of jobs long dominated by men, several studies have also shown that women are paid less than men, under take new types of employment (part time, temporary, domiciliary, unit rate...) and can not claim promotion in jobs which make their jobs insecure. Women, whose labour costs less, are much sort after by employers, even more in rural than in urban areas as we can see in Palar valley. It has been observed that female labour is cheap not only because of difference between the wages of men and women but also because of the lack of security and lack of protection which characterise women's labour and are both linked to the flexibility of the labour market. On the other hand women also prefer some flexibility in their work which allows them to take care of their families. Their docility is also the reason for employers preferring women labourers. Anyway, the number of working Indian women is growing, the majority of such women, that is to say the poorest, work from compulsion and because they never had any choice, and for salaries which are distinctly lower than those of men (except in public service).

However, the perception of the women work has changed with the industrialisation. Usually, in this traditional area, working outside the house is usually dishonour. During our first survey in 1999 concerning all types of women work in this valley, many women told us that women couldn't work outside the house because they can't assume their traditional roles of wives, mothers or daughter in law. However the limit between domestic work and household industry (beedie roller, agabarties. weavers...) is very difficult to define. Many of the women cannot make the difference. We have to notice that Vellore district is the first district in TN where the non-agricultural work conducted mainly by women is predominant. If at the beginning of the industrialisation, the shoe factory work was not well perceived because of the risk of "love affairs", now except in the remote areas, the shoe factory is appreciated by the women workers an their families, because it represents a social mobility. For example many agricultural and non agricultural women workers are very proud to say that their daughters have never worked in the mud of the paddy field under the sun and they have only worked in shoe factories. However, it's more an intergenerational social mobility. Shoe factory is represented as a modern and prestigious place, because the conditions of work seem better (women are well dressed) out of the sun in a nice place with regular hours of work.

After this survey, we can define a profile of the women workers in Palar Valley: Most of them belonged to the age -group 15-45 years to cutting and sitching. Some of them have entered the industry as adolescent workers (Muslims) mostly as helpers. Most of the women in age group 18-25 are not married. Our survey has shown that a majority (60-70%) of women belongs to backward casts and now scheduled casts. But unlike the agricultural sector, we can find some women of medium and high casts. The majority of the workers are Hindus (60-70%), and the remaining 30% are Muslims and/or Christians. If the manager is Muslim, it's possible to have 30% Muslim workers, because of the community preference. Generally, the Muslim women are secluded because of the purdah (seclusion), but because of the extreme poverty of certain people of this community, the family send the girls (10 years for the youngest) to the shoe factories. To be politically correct the Muslim managers employ 90% of women (in one factory, I met a female human resources manager Hindu, and she had a MA history ). But in other factories managed by Hindus, you can have mixed assembly line.

If at the beginning of the industrialisation (1980), no special qualification was required, now because of the increasing demand of work, managers ask for higher level of education (8-10 th standard), except for the Muslims (community preference). The Christians are generally more educated than Hindu and Muslims and they are also present in the public service. The average income of the majority of these workers is less than 1500 Rs (30 euros).

They are used to working from 8 am to 6 p.m. with one hour overtime compulsory. Managers can give some different incentives if the workers work 24 days continuously or if they produce more … If they miss one day, they have a penalty of 100Rs (10% of the salary) ; it s a way to limit the big turnover : for one euro difference, workers can go to another factory.

But for a better understanding of the employment situation, it's possible to distinguish between permanent workers (> 3 years) and casual (flexible) workers who represent a majority of workers which can be divided in 3 categories : temporary (<2 years), seasonal (3-6 months) and daily workers. Only the permanent workers can get some welfare benefits as insurance and provided fund, maternity leaves, bonus… What is common in this area and elsewhere (N. Neetha,2002), is the growing casualisation of female labour in particular and the clear indication that the growing use of female labour has been associated with the greater insecurity of labour contracts and the generally inferior conditions and pay involved in employing women rather than men (T.S. [START_REF] Papola | Gender and employment in India[END_REF]. The number of employment opportunities created by casualisation certainly are more, but they are also in worse conditions. This largest employment change is in the industrial subcontracting sector. Many big companies as we have seen in this valley subcontract for their production. Some of the producers give sometimes out work to home based workers through contractors. Even many medium scale industries in the organised sector subcontract work to home-based women workers. Subcontracting of work given out to home based workers seems to have expanded phenomenally over the past decade, most of all during peak seasons. In a lot of colonies surveyed in Ranipet area, a majority of households, at least one woman was reported to be doing some kind of home-based work. However this type of jobs created in this way are irregular and low paid, far below the poverty line income (500 Rs = 10 euros) and most of all on a piece rate basis.

Circular mobilities and new life spaces

During our survey, we ask women about all their spatial mobilities (frequency and nature).

The main mobility concerning the commuters who can go to work eventually with the company buses. The main shoe factories send the vans to the village to pick up the workers.

Those who can't get these special buses go by walk or by the public buses. So, they can spend one hour in the transport to go to work. With their triple role (work, childcare et cooking), women can begin the day at 4pm and finish at 10pm. Some of them prefer going far away to earn more, that means 1euro more. But for this shuttle, they used to go by groups of neighbours, friends, without male chaperons. It's a first time for most of these young women to go outside without father brother, husband, … It is a way also for them to create a female collective identity. They can discuss many topics concerning the life in the family, the love affairs… And this commuting has impulsed some other types of movings around to market, friends.

When they are coming back home, they can stop to buy some food, to make shopping, to meet some friends… Theirs life space is not restricted to the domestic space but has been broaden (fig. 2).

Réalisation : Aimée Laffite (UMR ADES)

Factories are perceived as a dangerous environment for fidelity and chastity of married and unmarried women. Emergence of love affairs which could affect the endogamy rules is feared. The promiscuity in factories (except in factories whose manager is Muslim) can favour some love affairs between different casts and even different communities. Families fear this "danger" for their daughters, but the attraction of a financial enhancement overcomes the advantages these inconveniences. So, the factory is a space of new sociabilities and gender interaction where men and women of different communities and cast are mixed.

The other interesting case concerning Muslims women who are used to going to factories with the burquah in private buses and by walk, the burquah is a way for them to negociate the public male space, with the burquah, they can deal the unwelcome attentions of the men when they are in the streets. However in the factories, they have to remove the burquah, but the place appears safe to them, because most of the workers are women.

Paradoxically, this burquah can give them the right to penetrate the public male space .

Gender identity and impact of life cycles

In such rural areas, where the patriarchal ideology is very deep rooted, growth of female salaried class, even with the increased exploitation of women which it implies, maybe a factor leading to emancipation as stated by some of the women who were interrogated about their condition.

In spite of bad work conditions (low salaries, casualisation, overtime compulsory), but better than any other activity (except public services) most of the unmarried women may prefer going to the factory than doing nothing at home where they get bored and they can escape the control exercised by their family and neighbour. Women of factories used to getting married later than the other women get, because sometimes they are the only one in the family who can bring money and also it's the only way for them to prepare their dowry.

But after marriage some of the women have to give up their jobs in the factories to look after children. Some of them however manage to get work which can to be done at home, till the children grow up, but for pathetically low salaries (at unit rate) and do not get the welfare benefits (bonus or allowance, maternity leave, retirement benefit ...). This system which is highly prized by the mothers who have been interviewed, minimises in many ways the contradictions between the necessity to stay at home and look after the children and the necessity to leave the children in order to work outside. The system of employment on unit rate payment increases the exploitation of these isolated women who have no legal right to demand better working conditions and higher salaries. The social-cultural factors, marriage, child bearing, and related household responsibilities were the often-cited factors for high labour turnover. But because of poverty and to support family, many married Hindu and Christian women have to work and most of all the widows and the abandoned women.

Never the less, none of the women interviewed would, in no condition, like to give up their jobs in factories or fight for better wages, as according to them the "exploitation" in factories is insignificant compared to that which they experience at home. In rural areas where some men do not fulfil their responsibilities as heads of family, women look upon their employers as their benefactors as they provide the women the possibility of earning even though their salaries might be ridiculously low. This regular income has however enable the women to negotiate the sharing of power within the family or even to participate in decision making (empowerment). The general deterioration of living conditions and patriarchal attitudes have forced them to look after their families and at the same time to take up an income generating occupation. On the other hand women are often the first victims of closure of industries. India has had only a mild experience of the Asian crisis, but considering the global crisis in certain manufacturing industries, is no exception to the loss of thousands of jobs among working women.

But the majority of the women met give the earnings to the father and in some cases to their husbands. So our first impressions confirm the fact that few women workers are empowered. Paradoxically in these industrialised rural areas, some of these women have sometimes been the only ones to have a regular employment in the formal sector. In these rural areas, were employment is seasonal, men are out of work or are forced to migrate temporarily to neighbouring towns for employment in construction and service sectors. So, it is less the entry in factory employment than the migration of men that contributes to the autonomy of women. Even if the men are at home without any job, none of them want to take care of the children or participate to any chores.

In this traditional society, changes in the relationship between men and women by the assumption of responsibility and power by women -idea of empowerment of women -can not be easily realised by new opportunities of employment, because of the patriarchal nature of rural society and a biased view about the respective responsibilities of the husband and the wife. It is taken for granted that men work because they are the primary breadwinners. Bibliography BADGETT M.V.L., FOLBRE N., (1999), Responsabilités familiales et sociales : les normes du comportement masculin et féminin et leurs incidences économiques , Revue internationale du travail, n° spécial : femmes, genre et travail,vol.138, n°3, pp.343-363. BANERGEE N (ed.) Indian women in a changing industrial scenario, 1991, Sage. BAUD, I.S.A. et G.A. de BRUIJNE (1993), Gender, Small-Scale Industry and Development Policy, IT Publications, Londres.

Hindu,

august 2003