Christophe Raffalli
email: christophe.raffalli@univ-savoie.fr

Frédéric Ruyer
email: frederic.ruyer@univ-savoie.fr

Realizability of the axiom of choice in HOL. (An analysis of Krivine's work)

published or not. The documents may come

Realizability of the axiom of choice in HOL. (An analysis of Krivine's work)

Introduction

This work gives a way of realizing the axiom of choice (AC) in higher order logic (HOL). It follows from an idea of J-L Krivine developed in [START_REF] Krivine | Dependent choice, 'quote' and the clock[END_REF], consisting in introducing a new constant in the λC-calculus which could be interpreted with a "clock".

However, the theorem AC clock which is realized by this clock is not the usual axiom of choice. Nevertheless, it implies the dependant axiom of choice AC D (and in fact the non extensional axiom of choice AC N E ) and we will give and study the behaviour of the program extracted from the proof of AC N E using the AC clock axiom realized by a clock instruction.

To get more readable terms, we also use a part of the formalism of system ST developed in [START_REF] Raffalli | System ST, Toward A Type System for Extraction AND Proof of Programs[END_REF][START_REF] Raffalli | System ST, β-reduction and completeness[END_REF][START_REF] Ruyer | Types, sous-types et preuves[END_REF] inspired by the work of Michel Parigot [START_REF] Parigot | Recursive programming with proofs[END_REF], Christine Paulin [START_REF] Paulin-Mohring | Synthesis of ML programs in the system Coq[END_REF], Catherine Parent [START_REF] Parent | Synthesizing proofs from programs in the Calculus of Inductive Constructions[END_REF], Stephano Berardi [START_REF] Berardi | Pruning simply typed λ-terms[END_REF] and Philippe Curmin [START_REF] Curmin | Marquage des preuves et extraction de programmes[END_REF] which allows to remove computationally useless parts of a proof. Our first goal was to "prune" the proof given in the original paper [START_REF] Krivine | Dependent choice, 'quote' and the clock[END_REF], for example by removing parts concerning comparison of integers, or equality tests. But in the paper to appear [START_REF] Krivine | Realizability in classical logic. Phd Course[END_REF] the author gives almost the same result as us. What is different in our approach is that we address more strictly the gap between synctactic typability (⊢ t : A) and semantic realizability (t A), using propositions without algorithmic contents in the type syntax thanks to the special arrow ⇀.

For example, it allows us to avoid the uncomfortable notations like ∩ m<n ({m} → . . . which are replaced by ∀m(m < n ⇀ N m → . . . We also can give a type to the term Comp (see fact 3), whereas in [START_REF] Krivine | Realizability in classical logic. Phd Course[END_REF] it is used only on the semantic side.

Remark: All the terms given in this article have been produced by the PhoX proof assistant developed by C.Raffalli [START_REF] Raffalli | the phox proof assistant version 0.8[END_REF].

λC-calculus

We use the same formalism as in [START_REF] Krivine | Dependent choice, 'quote' and the clock[END_REF], stacks allowing to handle easily lists of arguments, although it adds some steps of reduction.

Terms and stacks

We suppose given a denumerable set V of variables, and one constant : C. The sets Λ c and Π are defined by mutual induction as follows:

• Λ c = V {C} {λx.t; t ∈ Λ c } {(tu); t, u ∈ Λ c } {k π ; π ∈ Π} • Π = {ǫ} {t.π; t ∈ Λ c , π ∈ Π}

Execution of processes and weak head reduction

The set of processes is defined as P = Λ c × Π; we write t ⋆ π for (t, π). There are four rules of reduction:

1. (push) (tu) ⋆ π ≻ t ⋆ u.π

v)v 1 • • • v n ≻ w.h.r u[x := v]v 1 • • • v n , and it is here simu- lated by (λx.u v)v 1 • • • v n ⋆ π ≻ n+2 u[x := v] ⋆ v 1 • • • v n .
π. But we will see soon that it gives an elegant way of defining the value of a formula.

Evaluable processes

We say that a set of process P ⊂ P is saturated if it is closed by anti-reduction: ∀p ∈ P, q ≻ p implies q ∈ P Suppose we have defined a set ⊥ ⊥ of evaluable processes, which is saturated. If S ⊂ Π, we note S ⊥ = {t ∈ Λ c ; ∀π ∈ S, t ⋆ π ∈ ⊥ ⊥}. Every L ⊂ Λ c such that there is an S ⊂ Π such that L = S ⊥ is called a truth value. This means we call truth value the orthogonal of a set of stacks. Sets of stacks themselves could be considered as counter proofs or falsity values.

It is clear that . ⊥ is decreasing, that is:

S ⊂ S ′ =⇒ S ′⊥ ⊂ S ⊥
Therefore, Π ⊥ is the least truth value, and ∅ ⊥ = Λ c the largest one.

The semantics we will define for HOL will always be (implicitly) parametrised by the choice of a saturated set ⊥ ⊥ of evaluable processes. Moreover, some specific results may depend upon specific properties of this set.

We now end this section by one last definition (which is used for the interpretation of implication): if Φ is a set of λ-terms and S is a set of stacks then: Φ.S = {t.π; t ∈ Φ and π ∈ S}

HOL with propositions and types

Here we define HOL [START_REF] Church | A formulation of the simple theory of types[END_REF], with two sorts of formulas:

• Propositions: which are formulas without algorithmic content. Their interpretation will be either true or false.

• Types: which are formulas with algorithmic content. They will be interpreted by set of programs of the form S ⊥ in order to be able to realize Peirce's law.

In fact this will be two copies of the same logic (except that we will extract programs only for one of them) which interact only through one special implication written ⇀ with a proposition on the left and a type on the right.

The interpretation of P ⇀ A will be the interpretation of A when P is true and the largest possible interpretation Λ c = ∅ ⊥ when P is false. This connective is similar to parigots A ↾ P in [START_REF] Parigot | Recursive programming with proofs[END_REF] which is a conjunction instead of an implication.

Sorts, terms and formulas

The set of sorts S is defined by the grammar:

S = V|C|S → S
V is a denumerable set of variables of sorts, and C is a set of sorts constants.

In the rest of the paper, we will suppose that {τ ; o; ω} ⊂ C, τ denoting the sort of types, o denoting the sort of propositions and ω denoting the sort of natural numbers.

We associate to each sort s a denumerable set of variables V s , whose elements are noted x s and define the set of terms T as the set of simply-typed λ-terms using the set of sorts S as simple types and using at least the following constants with their given sorts:

       0 : ω; s : ω → ω; → : τ → τ → τ ; → : o → o → o; ∀ s : (s → τ ) → τ ; ∀ s : (s → o) → o ⇀: o → τ → τ       
There are two arrows that we write in the same way but which have distinct sorts. There are also two polymorphic universal quantifiers. The context and the following convention will avoid confusion:

We will use the capital letters A, B, C for types (that is expressions of sort τ ) and the letter P , Q, R for propositions that is expressions of sort o. Therefore, if we write A → B we know that the arrow here is of sort τ → τ → τ .

We note as usual ∀x A instead of ∀(λx.A), A → B for (→ A B) and ∀x:A B for ∀x(A(x) → B). We use these notations both for types and propositions.

Deduction rules

A context Γ is a finite set of propositions of sort o and pairs (x, A), x being a λ-variable and A a type of sort τ . We note x : A instead of (x, A). We write a context:

Γ = P 1 , • • • P n , x 1 : A 1 , • • • x m : A m
In proofs, we will manipulate two kinds of sequents: Γ ⊢ t : A when we prove a type A (here t is a λ-term) and Γ ⊢ P when P is a proposition.

The rules for HOL with propositions and types are given in figure 1.

Lemma 1 If σ is a substitution on variables, we note A[σ] (resp. Γ[σ]) the result of the substitution on the formula A(resp. the context Γ).

If Γ ⊢ A then Γ[σ] ⊢ A[σ]
Proof: Immediate induction on the size of the derivation. Remark: The semantics of the new connective ⇀ is reflected by its rules, because there is nothing to prove when P is false in the introduction rule. However, one could consider a rule saying Γ ⊢ ¬P implies Γ ⊢ t : P ⇀ A for any term t. This rule is not derivable because in a derivation the free variables of a term are always declared in the context.

Γ ⊢ C : (((A → B) → A) → A) Γ ⊢ (((P → Q) → P ) → P )
Figure 1: HOL rules with propositions and types

-for every s ∈ V ∪ C , s ∈ M.
s → s ′ = s → s ′ . Remark: we should allow for non full model to allow completeness result even for realizability (see [START_REF] Farkh | Complete types in an extension of the system AF2[END_REF][START_REF] Farkh | Complete types in an extension of the system AF2[END_REF]), but this is not needed important here.

We will assume that ω is the set of natural numbers N, τ = P(Π) and o = {0; 1}.

• ⊥ ⊥ is a saturated set of processes.

Once a model M is defined, we can build the set of terms with parameters in M : we just need to consider that s∈S {a; a ∈ s} is a subset of C (the set of constants), and that each of these constants has the intended sort (or sorts, because the same element may appear in the interpretation of more that one sort) : a ∈ s, then a : s. Now, we define the notion of interpretation (or value) of a closed term with parameters in the model. We write it . M and it is defined by induction as follows:

• for every a in |M|, a = a

• 0 ω = 0 and s ω→ω = x → x + 1. • → τ →τ →τ = A → B → (A ⊥ .B). • → o→o→o = P → Q → if P = 1 then Q else 0. • ⇀ = P → A → if P = 1 then A else ∅. • ∀ (s→τ )→τ = A → x∈s A(x).
• ∀ (s→o)→o = P → if (for all x in s, P (x) = 1) then 1 else 0.

• (t)u = t ( u ). • λx.t = a → t[x := a] .
• for every other constant of sort s, c s in C, c s ∈ s should be given with the definition of the model.

We will need a little lemma on substitutions:

Lemma 2 For all terms A and v, if x is a F.V. of A, then A[x := v] = A[x := v ] .
Proof: It is an easy proof on the structure of the term A.

When the context is clear, to lighten the writing, we will often allow us not to underline a parameter and not to write the model as exponent.

The truth value of a type A (of sort τ ), written |A| is A ⊥ .

Remark : |∀X X| is the least truth value.

We now give some comments about the choices in the way the semantics is presented:

• We choose not to interpret the terms with free variables. In fact there are two equivalent alternatives: use terms with parameters in the model and substitute all variables by terms before computing the interpretation, or parametrise the valuation with a function giving the value of the variables.

• For a type, as we said, A is not the truth value but a set of counter proofs. This explains why the definition are the dual of the natural definition for truth value. The truth value of a predicate is |A| = A ⊥ . This is because we choose τ = P(Π).

It would have been equivalent to take for τ the set of sets of terms which are the dual of a set of stacks. This would require to change a bit the interpretation of the connectives (for instance ∀ becomes an intersection). This alternative gives a definition which is the same as the one used for intuitionist system F or AF2 [START_REF] Krivine | Programming with Proofs[END_REF], but requires a few easy lemmas in the classical case to prove that the interpretation of the connectives preserves the property of being a dual of a set of stacks.

These, notions are also related to game semantics, as explained in the work of Coquand [START_REF] Coquand | A semantics of evidence for classical arithmetic[END_REF]: intuitively, a stack might be seen as the environment, and a term as a program that will give an answer to the environment, i.e. "sending" the environment in ⊥ ⊥. For the reader, things might become clearer after reading the interpretation of the term that computes the minimum of a predicate (see theorem 2 below), the semantic interpretation of its type (together with the behaviour of the program) allowing to describe the play between ∃loïse and ∀belard (see also the work of Hayashi [START_REF] Hayashi | Can Poofs be Animated by Games?[END_REF] for a more detailed presentation of the subject).

Adequation lemma

We say that a term t realizes a type A in a model M if t ∈ |A| M , and we write M t A (or t A if the context is clear enough).

We say that a formula without algorithmic content P is satisfied in M, and we write M P if P = 1.

We say that a substitution σ = [

x 1 := t 1 , . . . , x m = t m ] realizes a context Γ = P 1 • • • P n , x 1 : A 1 • • • x m : A m in a model M if

and only if:

• for all 1 ≤ i ≤ m and M t i A i

• and for all 1 ≤ i ≤ n, M P i

We write this M σ Γ (or σ Γ if the context is clear enough).

Our aim is to show the following theorem:

Theorem 1 (adequation lemma) Let us fix a model M. For all context Γ, if σ Γ and Γ ⊢ t : A then tσ A.

We first show a lemma about propositions:

Lemma 3 For all contexts Γ, if σ Γ and Γ ⊢ P then M P .

Proof: We make the proof by induction on the length of the deduction.

Axiom'

Γ = P 1 • • • P n , x 1 : A 1 • • • x m : A m ⊢ P i trivial because M P j for all 1 ≤ j ≤ n. → ′ -Intro Γ, P ⊢ Q Γ ⊢ P → Q
We suppose that M P i for all 1 ≤ i ≤ n. We have P → Q = 1 if and only if P = 0 of Q = 1. Therefore, we assume P = 1, and by induction hypothesis, we have

M Q which means Q = 1. → ′ -Elim Γ ⊢ P → Q Γ ⊢ P Γ ⊢ B ′
We suppose that M P i for all P i in Γ. By I.H., P = 1 and P → Q = 1. Thus, Q = 1.

∀ ′ -Intro Γ ⊢ P Γ ⊢ ∀x s P with x not free in Γ. We need lemma 1. It is here easy to conclude with I.H. and the interpretation of ∀.

∀ ′ -Elim Γ ⊢ ∀x s P Γ ⊢ P [x := u]
For every u of sort s. Immediate with the interpretation of ∀.

Proof:

We can now prove the adequation lemma by induction on the length of the deduction.

Axiom Γ = P 1 • • • P n , x 1 : A 1 • • • x m : A m ⊢ x i : A i trivial because tσ = t i . → -Intro Γ, x : A ⊢ t : B Γ ⊢ λx.t : A → B We have to show that (λx.t)σ ∈ |A → B|. We have (λx.t)σ = λx.(tσ)
because we can rename the bound variable x to avoid capture. Take π in A → B , by the interpretation of →, there is t A in |A| an π B in B such that π = t A .π B . We have:

(λx.t)σ ⋆ π ≻ tσ[x := t A ] ⋆ π B By I.H. , tσ[x := t A ] belongs to |B| (because σ[x := t A ] Γ, x : A). Therefore, tσ[x := t A ] ⋆ π B ∈ ⊥ ⊥, so (λx.t)σ ⋆ π too by saturation. → -Elim Γ ⊢ t : A → B Γ ⊢ u : A Γ ⊢ (tu) : B
We have (tu)σ = (tσ uσ). Take π in B .

Ct ⋆ π ≻ t ⋆ k π .π
We just have to check that k π ∈ |A → B|. Take π ′ ∈ A → B ; by the interpretation of →, there is

t A in |A| an π B in B such that π ′ = t A .π B . k π ⋆ π ′ = k π ⋆ t A .π B ≻ t A ⋆ π
The conclusion is immediate.

∀ -Intro

Γ ⊢ t : A Γ ⊢ t : ∀xA with x not free in Γ. Take π ∈ ∀xA = ∀λx s .A . There is an a in s such that π ∈ λx s .A (a) = A[x := a] . By lemma 1, and the I.H. , we have

tσ ∈ A[x := a] . ∀ -Elim Γ ⊢ t : ∀x s A Γ ⊢ t : A[x := v] Take v of sort s. We have to check that tσ ∈ A[x := v]. It is easy be- cause A[x := v] = A[x := v ] = λx.A ( v ), which is a subset of ∀x s A . Therefore, |∀x s A| is a subset of |A[x := v]|,
and the conclusion is immediate from the I.H.

Conjunction and existential

In this section, to ease reading, we really start to use notation introduced at the end of section 3.1. Fact 1 We extract the following constructor and destructors for pairs:

We define the type (A

× B) = ∀K ((A → B → K) → K)
• If Γ ⊢ a : A and Γ ⊢ b : B then Γ ⊢ pair[a, b] : A × B. • If Γ ⊢ c : A × B then Γ ⊢ pi1[c] : A and Γ ⊢ pi2[c] : B We define the type ∃x A(x) = ∀K (∀x:A K → K) and the λ-term box[a] = λx (x a).
Fact 2 We extract the following constructor and destructor for existential:

• If Γ ⊢ a : A(x) then Γ ⊢ box[a] : ∃x A(x). • If Γ ⊢ b : ∃x A(x) and Γ ⊢ f : ∀x:A B then Γ ⊢ b f : B.
We now have a conjunction × and an existential quantifier ... however, very often, to simplify the extracted program and to deal with conjunction mixing types and propositions, we will use specific coding. For instance, if we want to write an existential on two type Ax, Bx and a proposition P x, we will use the formula:

∀K (∀x:A (B(x) → P(x) ⇀ K) → K).

Leibniz equality and extensionality

The equality can be defined both as a type or a proposition, using Leibniz definition. One remarkable point, is that the interpretation of the equality type can only be two values (as for propositions). This fact will be essential to realize axioms involving equality like ∀x(0 = sx).

The type and proposition a = b are defined by ∀X(Xa → Xb) (this is two distinct definitions, but we only write one, since we use the same notation for both implication and quantification). Proof: Recall that Xa = X ( a ) and choose for X the characteristic function of { a } when a = b .

Corollary 1

The following rules preserve the adequation lemma (and will simplify extracted λ-terms):

Equality Equality' Γ ⊢ t : A[x := a] Γ ⊢ a = b Γ ⊢ t : A[x := b] Γ ⊢ P [x := a] Γ ⊢ a = b Γ ⊢ P [x := b] Extensionality Γ ⊢ P ↔ Q Γ ⊢ P = Q
where the formula P ↔ Q := (P → Q) ∧ (Q → P ).

Proof: Immediate from the previous lemma. One just have to notice that P [x := a] = P [x := a ] and M P ↔ Q implies P = Q .

Corollary 2 For any model and any terms t 1 , . . . , t p (possibly with x free in t i or p = 0), we have λx (x t 1 . . . t p ) ∀n(0 = sn) and λx x ∀n, m(sn = sm → n = m) (here x = y := x = y → ∀X X). This means that the axioms ∀n(0 = sn) ∀n, m(sn = sm → n = m) may be used both at the level of propositions and type while preserving the adequation lemma.

Proof: Let us choose a model M. We use that fact that in M the sort ω is interpreted by natural numbers in the standard way. Therefore, we have 0 = sa and sa = sb implies a = b.

For the first result, we take n ∈ ω and u ∈ |(0 = sn)| and π ∈ ∀X X = Π and we have to show that λx ( The second result is immediate because the previous lemma and the choice of models implies sa = sb = a = b . Important remark: the previous rules allow to deduce Γ ⊢ λx x : a = b from Γ ⊢ a = b. This means that the equality as a proposition implies the equality as a type. The converse is not true, because sometimes, an equality proof may contain a k π constant that will arrive in head position. This means an equality proof may raise an exception and in this case we can not derive the corresponding propositional equality.

Remark: all the previous results are even simpler (like in recent Krivine's work [START_REF] Krivine | Realizability in classical logic. Phd Course[END_REF]) if one consider a new type predicate x = y with the interpretation a = b = Π when a = b and a = b = ∅ when a = b. Then, t ∀n(0 = sn) for any term and we can realize the equivalence between Leibniz equality and the negation of our new type predicate a = b.

Some results on integers

In this section, we give some more or less well-known results on integers. We note, for n ∈ N, n C the Church integer λx.λf.f n x.

Recursion principle and induction principle

We define the formulas N(x) = ∀X (X(0) → ∀y:X X(S(y)) → X(x)), we add a new propositional predicate a < b with the sort ω → ω → o interpreted by the usual ordering on natural numbers (we could also define a < b = ∀X (X(Succ[a]) → ∀n:X X(Succ[n]) → X(b)), but it makes no difference to use a new constant with axioms or a definition, at the level of propositions, for extracted programs).

We also define the following λ-terms which are the two constructors on natural numbers, the recursor and a term comp that compares two integers and distinguish three cases (equal, less or greater):

• Zero = λx λf x, • Succ[n] = λx λf (f (n x f)), • NRec[t 0 , t S , n] = pi2[n pair[Zero, t 0 ] λp pair[Succ[pi1[p]], t S pi1[p] pi2[p]]] • comp = λn NRec[comp1, comp2, n], with

Fact 3 The previous programs were extracted from the following proofs:

• For all n ∈ N, ⊢ n C : N (n), and especially ⊢ Zero : N (0).

• ⊢ λn Succ[n] : ∀n(N n → N sn).

• If ⊢ t 0 : X(0), u : N(y), v : X(y) ⊢ tS(u,v) : X(S(y)) and ⊢ n : N(p) then ⊢ NRec[t 0 , t S , n] : X(p).

• ⊢ comp : ∀X ∀n,p:N

(n = p ⇀ X) → ((n < p) ⇀ X) → ((p < n) ⇀ X) → X Proof:
The first three items are very usual.

For the last one let us explain the behaviour of the term: if we suppose that n N n ′ and p N p ′ then comp n p a b c reduces to

a if n = p, b if n < p and c if p < n.
If we did not use the special arrow ⇀ in the type of comp, then a, b and c would receive as argument the proof of the relation between n and p. We here see the purpose of mixing propositions and types. Now, for the proof itself, it is a double recursion on n and p, using the extensionnality in the last case to be able to replace Sn = Sp by n = p.

Let Y be a fixpoint operator i.e. such that for all π and f : Y ⋆ f.π ≻ f ⋆ (Y f ).π. We will see that the fact that < is well founded is associated directly to a fixpoint combinator. We have the following fact:

Fact 4 Y ∀X (∀a (∀b:N ((b < a) ⇀ X(b)) → N(a) → X(a)) → ∀a:N X(a)).
This means we can use this as axiom and keep the adequation lemma.

Proof: Take X, and f ∀a

(∀b:N ((b < a) ⇀ X(b)) → N(a) → X(a)
). We want to prove that for all n ∈ N, if t N n and π ∈ Xn , then Y ⋆ f.t.π ∈ ⊥ ⊥. We have:

Y ⋆ f.t.π ≻ f ⋆ (Y f ).t.π
We can assume as induction hypothesis that for all m < n, s N m and

π ′ ∈ Xm we have (Y f ) ⋆ s.π ′ ≻ Y ⋆ f.s.π ′ ∈ ⊥ ⊥. So, (Y f ) (N m → m < n → Xm), that is (Y f ) ∀b(N b → b < n → Xb). So, with our hypothesis on f , we have f ⋆ (Y f ).t.π ∈ ⊥ ⊥.

Minimum principle

The formula No lt expressing that no natural number less than n satisfies the predicate Q) is defined as:

No lt(n, Q) = ∀p:N (Q(p) → (p < n) ⇀ ∀XX)
We define three terms to prove the minimum principle:

• Min unique = λn λn ′ λq λq ′ λm λm ′ λe comp n n ′ e m ′ n q m n ′ q ′ • Min fix [k] = (Y λr λa λq λf (f a q λb λq ′ (k (r b q ′ )))) • Min exists = λn λq (C λk (Min fix [k] n q))
Fact 5 (Unicity of the minimum)

⊢ Min unique : ∀Q ∀n,p N(n) → N(p) → Q(n) → Q(p) → No lt(n, Q) → No lt(p, Q) → ∀X ((n = p ⇀ X) → X)
Proof: We apply the hypothesis No lt(n, Q) and No lt(p, Q) with respectively N(n), Q(n) and N(p), Q(p) to get then the premises of comp in Fact 3 !

The behaviour of Min unique is easy to understand with the help of comp.

Fact 6 (existence of the minimum) Let us define the type that expresses that the minimum of the predicate Q exists:

∃ Min Q = ∀K (∀n:N (Q(n) → No lt(n, Q) → K) → K)
We have ⊢ Min exists : ∀Q ∀n:

N (Q(n) → ∃ Min Q)
Proof: Choose an integer n with n ′ : N(n), q : Q(n). We use the Peirce law with k : (∃ Min Q) → ∀X X, and we have to deduce that Min fix [k] m q : ∃ Min Q.

Using fact 4, what we have to prove is that

λr λa λq 0 λf f a q 0 λb λq ′ k r b q ′ : ∀a ∀b:N (b < a) ⇀ Q(b) → ∃ Min Q → N(a) → Q(a) → ∃ Min Q Now, we have the hypothesis r : ∀b:N ((b < a) ⇀ Q(b) → ∃ Min Q), A : N(a)
and q ′ : Q(a), and we have to show:

λf (f A q ′ λb λq ′ 0 (k (r b q ′ 0 ))) : ∃ Min Q We assume f : ∀n 0 :N (Q(n 0 ) → No lt(n 0 , Q) → K)
and we use it with a. We have to prove λb λq ′ 0 (k (r b q ′ 0 )) : No lt(a, Q) and that leads to deduce k (r B q ′′ ) : ∀XX from B : N(b) and q ′′ : Q(b), and it is immediate using k : (∃ Min Q) → ∀XX and r :

∀b 0 :N ((b 0 < a) ⇀ Q(b 0 ) → ∃ Min Q).
To understand how Min exists works, we run the program:

Min exists ⋆ a.q.f.π ≻ Min fix [k f.π ] ⋆ a.q.f.π ≻ f ⋆ a.q.M.π with M = λb λq ′ (Min fix [k f.π ] b q ′ )
If the above was typed, we have

a ∈ |N(n)|, q ∈ |Q(n)|, M ∈ |No lt(n, Q)| , f ∈ |∀n:N (Q(n) → No lt(n, Q) → K)| and π ∈ K .
Having f in head position with the stack a.q.M.π means that the program pretends that n is the minimum. To get a more precise understanding of how the program behaves, we introduce a new constant κ wich will play the role of the opponent (you may read [START_REF] Krivine | Realizability in classical logic. Phd Course[END_REF] for the relation between games theory and realizability). We suppose given a term s for the successor (e.g λnSucc[n]), and 0 = Zero. Assume Q is a decidable predicate (which makes κ possibly recursive), and the constant has the following behaviour: κ ⋆ s n 0.q.ξ.π ≻ ξ ⋆ s p 0.q ′ .π ′ for a p < n and a term q ′ Q(p) if there exists one. Else, κ ⋆ s n 0.q.ξ.π ≻ s n 0 ⋆ ǫ If we take a storage operator T as defined in [START_REF] Krivine | Realizability in classical logic. Phd Course[END_REF], we have the following: Theorem 2 For every integer n and any program ⊢ q : Q(n), using a constant κ associated to Q as above, every reduction of ((Min exists )s n 0)q ⋆ T κ.π ends on the Church integer p ⋆ ǫ with p the least integer such that Q(p) is inhabited.

In fact, the proof does not depend on the specific behaviour of Min exists , but only on its specification.

Proof: We take ⊥ ⊥ = {p such that every reduction of p ends on k n ⋆ǫ}. We have to show that ((Min exists )s n 0)q ⋆ T κ.π ∈ ⊥ ⊥. By the adequation lemma, we have:

((Min exists )s n 0)q ∀x(N x → No lt(x, Q) → ⊥) → ⊥
By definition of , we have to show that T κ ∀x(N (x) → Q(x) → No lt(x, Q) → ⊥). Take n ∈ N; we must have:

T κ N (n) → Q(n) → No lt(n, Q) → ⊥
By theorem 11 of [START_REF] Krivine | Realizability in classical logic. Phd Course[END_REF] concerning the behaviour of T , it is sufficient to show that for every π, for every q Q(n), and ξ No lt(n, Q), κ ⋆ s n 0.q.ξ.π ∈ ⊥ ⊥. Here, two things can happen:

• either n is the least integer satisfying Q, in this case the execution stops at the good state.

• either there is a p < n and a q ′ Q(p). In this case, we have: κ⋆s n 0.q.ξ.π ≻ ξ⋆s p 0.q ′ .π ′ Now he have to show that ξ⋆s p 0.q ′ .π ′ ∈ ⊥ ⊥. By the specification of ξ, we just have to check that π ′ ∈ (p < n) ⇀ ∀XX which is immediate by the semantics.

We shall notice that the previous remark concerning the behaviour of Min exists shows us that the term keeps T κ in the head of its stored continuation, which is coherent with the intuitive meaning of the program given thanks to the gamesemantics style interpretation we gave of its type.

Application : realizing AC

The idea is to realize the following shape of the axiom of choice; it is divided into three parts describing the properties we attend of the choice constructor C:

• The first part of the specification expresses that if F (x, X) is inhabited, so is C(F, x, X).

• The second part expresses that C is functional, that is it gives only one candidate X for each choice of x (the formal definition of F unc will be given later).

• The third part expresses that if X is chosen by C(F, x), then we have F (x, X).

Thus, our formulation of N AC (the name is explain below) is the following:

∀F ∃C ∀x∀X(F (x, X) → ∃XC(F, x, X)) × F unc(C(F ))× ∀x∀X(C(F, x, X) → F (x, X))
Remark: the above formalisation is polymorphic. The variables x and X could have any sort s and s ′ and therefore, F could have any sort of the shape s → s ′ → o. However, this axiom is not the standard axiom of choice. It is the non extensional axiom of choice (hence it's name NAC). Nevertheless, when the sort of x is ω this is really the countable axiom of choice, because C will really be a choice function with argument in ω.

The reason it is not the usual axiom of choice for sorts more complex that ω is the following: if the sort of x is ω → o, then one would also expect the following to hold for C:

∀F, x, x ′ , X, X ′ (∀y, y ′ (x(y) ↔ x ′ (y ′ )) ∧ C(F, x, X) ∧ C(F, x ′ , X ′ ) → X = X ′ )
This formula means that C is extensional (in general, this formula is defined by induction on the sort of C), and we did not state this in our formulation, but only that C was functional which is much weaker.

A new constant

To realize the axiom of choice, we need to add a new constant to the λ-calculus and show that it realizes a specific axiom.

Let F (x, X) be a formula with parameter F, x, X in a model M, and φ a λ-term.

Using the axiom of choice, there is a function Ψ such that φ F (x, Ψ(F, x, φ)) if and only if ∃X ∈ M φ F (x, X).

• T 1 = χ T ′ 1 Lemma 5 Using our new constant χ, we can prove:

T 1 : ∀F ∀x ∀X ′ (F(x,X ′ ) → ∃X Z(F,x,X))
Proof: Using the axiom for the constant χ, it is enough to prove ,Φ(F,x,n)) and g : ∀X (Z(F,x,X) → K). We must show Min exists m f λa λq λm 0 (g λx 0 (x 0 a q m 0 )) : K, using fact 6, what is left to prove is: λa λq λm 0 (g λx 0 (x 0 a q m 0 )) :

⊢ T ′ 1 : ∀F ∀x ∀n:N (F(x,Φ(F,x,n)) → ∃X Z(F,x,X)) Assume m : N(n), f : F(x
∀n 0 :N (F(x,Φ(F,x,n 0 )) → No lt(n 0 , λn 0 F(x,Φ(F,x,n 0 ))) → K)
It means we want (g λx 0 (x 0 A q m)) : K with A : N(a), q : F(x,Φ(F,x,a)) and m : No lt(a, λn 0 F(x,Φ(F,x,n 0 ))). This is immediate using the definition of Z.

Then next lemma will show that Z defines a function. To define when a predicate is a function, we use the following definition:

Func(Q) = ∀x ∀X,X ′ (Q(x,X) → Q(x,X ′ ) → (X = X ′ )).
Remark: we can not use propositional equality here. Indeed, the algorithmic content of the next lemma, may trigger some backtracking as we will explain later with more details. Therefore, in the next lemma, Func and = are used as type.

Lemma 6 We define the term T 2 = λz λz ′ (z (z ′ λn λf λm λn ′ λf ′ λm ′ (Min unique n n ′ f f ′ m m ′ λx x)))

and we have ⊢ T 2 : ∀F Func(Z(F));

Proof: This is an immediate application of the fact 5.

The last lemma shows that Z always chooses a well suited X:

Lemma 7 We define the term

T 3 = λz (z λa λb λc b)
and we have ⊢ T 3 : ∀F ∀x ∀X:Z(F,x) F(x,X).

Proof: Immediate from the definition of Z.

Finally, if we put together the previous three lemmas, and if we quantify over Z (with an existential), we realize the following theorem:

∀F ∃C ∀x ∀X (F(x,X) → ∃X C(F,x,X)) × Func(C(F)) × ∀x ∀X (C(F,x,X) → F(x,X))

Now, we will encode the conjunction and existential as usual to simplify the term, and we get the following theorem: We can briefly and intuitively deduce from the behaviour of the program for the minimum principle the behaviour of T N AC : To be able to choose an X such that F (x, X), you have to give a witness. As in the minimum principle, T N AC will always choose this witness! However, when you use the fact that the choice is functional, you will have access to the two natural numbers build by the χ constant for two previous choices. Then the term will backtrack to the choice with the smallest natural number to make the two choices identical.

In fact we could change the behaviour of the term χ with χ ⋆ t.φ.π ≻ t ⋆ clock.φ.π where clock is the current time. In this case, when T N AC detects that two choices should have been identical, then, it will backtrack to the latest choice, which seems the most efficient behaviour. You may read [START_REF] Krivine | Realizability in classical logic. Phd Course[END_REF] for a proof that χ realizes the same formula using the clock in specific models called generic models.

Remark: the previous theorem shows that the axiom of choice is realized. We proved it using a new constant χ in the λ-calculus, a new constant Z in the logic and a new axiom relating both. This shows that the derivation used in the previous theorem preserve the adequation lemma in all models.

However, as previously mentioned, we only realize the non extensional axiom of choice. Nevertheless, this non extensional axiom of choice is sufficient to prove the countable axiom of choice or the dependant axiom of choice, which suffices for analysis in general.

The next challenge for realisability is therefore the extensional axiom of choice, or at least the extensional choice on real numbers. . .

2 .

 2 (pop) λx.t ⋆ u.π ≻ t[x := u] ⋆ π 3. (store) C ⋆ t.π ≻ t ⋆ k π .π 4. (restore) k π ⋆ t.π ′ ≻ t ⋆ πThis formalism has one drawback: it increases the number of steps. Effectively, we have usually (λx.u

(

  tu)σ ⋆ π ≻ tσ ⋆ uσ.π By I.H., we have uσ ∈ |A| and tσ ∈ |A → B|, then it is clear that tσ ⋆ uσ.π ∈ ⊥ ⊥ by definition of the interpretation of →, and (tσ uσ) ⋆ π too by saturation. ⇀-Intro Γ, A ⊢ t : B Γ ⊢ t : A ⇀ B Suppose that M A. By the interpretation of ⇀, we have A ⇀ B = B and by I.H. , we have tσ ∈ |B|. It is OK. Else, we have A ⇀ B = ∅ and |A ⇀ B| = Λ c and we don't need any I.H. to conclude. ⇀-Elim Γ ⊢ t : A ⇀ B Γ ⊢ A Γ ⊢ t : B By the previous lemma 3, we have M A, and thus A ⇀ B = B . By I.H., tσ ∈ |A ⇀ B|, and so tσ ∈ |B|. Peirce law Γ ⊢ C : ∀A∀B(((A → B) → A) → A) Take A and B in the model, π ∈ A and t ∈ |((A → B) → A)|. We have

  and the three terms pair[a, b] = λx (x a b), pi1[c] = (c λa λb a), and pi2[c] = (c λa λb b).

Lemma 4

 4 When a = b is a proposition, a = b = 1 if and only if a = b .

-

  comp1 = λp (p λa λb λc a λx λa λb λc b) and -comp2 = λn λr λp NRec[λa λb λc c, λp ′ λr ′ (r p ′ ), p].

Theorem 3 (

 3 a realizer of NAC) We define the term T N AC = λx (x T 1 T 2 T 3 ) and we get⊢ T N AC : ∀F ∀K   ∀C   ∀x ∀X (F(x,X) → ∃X C(F,x,X)) → Func(C(F)) → ∀x ∀X (C(F,x,X) → F(x,X)) Immediate from the three previous lemmas.

Γ, x : A ⊢ x : A Γ, P ⊢ P → -Intro :→ ′ -Intro : Γ, x : A ⊢ t : B Γ ⊢ λx.t : A → B Γ, P ⊢ Q Γ ⊢ P → Q → -Elim : → ′ -Elim : Γ ⊢ t : A → B Γ ⊢ u : A Γ ⊢ (tu) : B Γ ⊢ P → Q Γ ⊢ P Γ ⊢ Q ∀ -Intro : ∀ ′ -Intro : Γ ⊢ t : A Γ ⊢ t : ∀xA If x not free in Γ. Γ ⊢ P Γ ⊢ ∀xP If x not free in Γ. ∀ -Elim ∀ ′ -Elim : Γ ⊢ t : ∀x s A Γ ⊢ t : A[x := v]For every v of sort s.Γ ⊢ ∀x s P Γ ⊢ P [x := v]For every v of sort s.⇀-Intro : ⇀-Elim : Γ, P ⊢ t : A Γ ⊢ t : P ⇀ A Γ ⊢ t : P ⇀ A Γ ⊢ P Γ ⊢ t : A

Ψ just needs to choose such an X. The problem is that Ψ is not in the model, since its third argument is a λ-term.

To solve this problem, we consider a surjection n → t n from N to Λ and one inverse of this surjection t → n t . This means we choose a (non unique) index n t for each λ-term t. We will use n t as a natural number, but also as a Church numeral when using it in a λ-term. This means we can write n t N (n t ).

Using this surjection, we define a function Φ(F, x, n) = Ψ(F, x, t n ). Now, Φ is in the model and

We define a new constant added to Λ, χ, with the following reduction rule.

The following axiom preserves the adequation lemma.

Proof: Take K, F , x and x in the model and u : ∀n:N (F(x,Φ(F,x,n)) → K) and φ : F (x, X). We just have to show n φ .φ.Π ∈ ∀n:N (F(x,Φ(F,x,n)) → K) which is immediate using the definition of Φ.

Realization of NAC

We will proceed with three lemmas:

We want to be able to choose X such that F (x, X) if there exists one. To do so, we can take Φ(F,x,n) where n is the smallest integer satisfying this property.

We define the following predicate:

However, Z 1 describes an integer n, and we want to choose the second argument of F (i.e. Φ(F, x, n)). For this, we define:

where n is the smallest integer such that F(x,Φ(F,x,n)) if there is one. This definition is a coding of existential and conjunction specific to our need (with a propositional equality) to make the extracted term as simple as possible. Now, our first lemma will show that Z does choose an X such that F (x, X) when there exists one. To do so, we need the following terms:

• T ′ 1 = λn λf λg (Min exists n f λa λq λm (g λx (x a q m)))


Pierre Hyvernat
email: hyvernat@iml.univ-mrs.fr

Predicate transformers and Linear Logic yet another Denotational Model

In the refinement calculus, monotonic predicate transformers are used to model specifications for (imperative) programs. Together with a natural notion of simulation, they form a category enjoying many algebraic properties. We build on this structure to make predicate transformers into a denotational model of full linear logic: all the logical constructions have a natural interpretation in terms of predicate transformers (i.e. in terms of specifications). We then interpret proofs of a formula by a safety property for the corresponding specification.

Introduction

The first denotational model for linear logic was the category of coherent spaces ( [START_REF] Girard | Linear logic[END_REF]). In this model, formulas are interpreted by graphs; and proofs by cliques (complete subgraphs). This forms a special case of domain à la Scott.

From a conceptual point of view, the construction of interfaces is a little different: first, the model looks a little more dynamic; then, seeds -the notion corresponding to cliques-are not closed under substructures; and finally, they are closed under arbitrary unions (usually, only directed unions are allowed).

What was a little unexpected is that the interpretation of linear proofs used in the relational model can be lifted directly to this structure to yield a denotational model of full linear logic in the spirit of /hyper/multi-coherence or finiteness spaces.

A promising direction for further research is to explore the links between the model presented below and non-determinism as it appears both in the differential lambda-calculus ( [START_REF] Ehrhard | The differential lambda calculus[END_REF][START_REF] Ehrhard | Differential interaction nets[END_REF]) and different kind of process calculi. We expect such a link because of the following remarks: this model comes from the semantics of imperative languages; it can be extended to a model of the differential lambda calculus (which can be seen as a variant of "lambda calculus with resource") and there is a completely isomorphic category in which predicate transformers are replaced by (two-sided) transition systems. In particular, all of the logical operations presented below have natural interpretations in terms of processes...

Relations and Predicate Transformers

Definition 1. A relation r between two sets is a subset of their cartesian product. We write r ∼ for the converse relation: r ∼ = (b, a) | (a, b) ∈ r . The composition of two relations r ⊆ A × B and r ′ ⊆ B × C is defined by

r ′ • r = (a, c) | (∃b ∈ B) (a, b) ∈ r ∧ (b, c) ∈ r ′ .
If X is a set, Id X denotes the identity on X, i.e. Id X = {(a, a) | a ∈ X}.

There seems to be three main notions of morphisms between sets. These give rise to three important categories in computer science:

-Set, where morphisms are functions; -Rel, where morphisms are (binary) relations; -Pow, where morphisms are monotonic predicate transformers.

One can go from Set to Rel and from Rel to Pow using the same categorical construction ( [START_REF] Gardiner | An algebraic construction of predicate transformers[END_REF]) which cannot be applied further.

Definition 2. A predicate transformer from

A to B is a function from P(A) to P(B). A predicate transformer P is monotonic if x ⊆ x ′ implies P (x) ⊆ P (x ′ ).
From now on, we will consider only monotonic predicate transformers. The adjective "monotonic" is thus implicit everywhere.

The term "predicate" might not be the most adequate but the terminology was introduced by E. Dijkstra some decades ago, and has been used extensively by computer scientists since then. Formally, a predicate on a set A can be identified with a subset of A by the separation axiom of ZF set theory; the confusion is thus harmless. Definition 3. If r is a relation between A and B, we write r : P(A) → P(B) for the following predicate transformer:

(called the direct image of r) r (x) = b ∈ B | (∃a ∈ A) (a, b) ∈ r ∧ a ∈ x .
Note that in the traditional version of the refinement calculus ( [START_REF] Back | Refinement Calculus: a systematic introduction[END_REF]), our r is written {r ∼ }, but this notation clashes with set theoretic notation and would make our formulas very verbose with ∼ everywhere.

Interfaces

Several denotational models of linear logic can be seen as "refinements" of the relational model. This very crude model interprets formulas by sets; and proofs by subsets. It is degenerate in the sense that any formula is identified with its linear negation! Coherent spaces ( [START_REF] Girard | Linear logic[END_REF]), hypercoherent spaces ( [START_REF] Ehrhard | Hypercoherences: a strongly stable model of linear logic[END_REF]), finiteness spaces ( [START_REF] Ehrhard | Finiteness spaces[END_REF]) remove (part of) this degeneracy by adding structure on top of the relational model. We follow the same approach: Definition 4. An interface X is given by a set |X| (called the state space) and a predicate transformer P X on |X| (called the specification).

The term "specification" comes from computer science, where a specification usually takes the form:

if the program is started in a state satisfying φ, it will terminate; and the final state will satisfy ψ. Such a specification can be identified with the (monotonic) predicate transformer ψ → "biggest such φ". This point of view is that of the wp calculus, introduced by Dijkstra ("wp" stands for "weakest precondition"). Note that the specification "goes backward in time": it associates to a set of final states (which we want to reach) a set of initial states (which guarantee that we will reach our goal). 3For a complete introduction to the field of predicate transformers in relation to specifications, we refer to [START_REF] Back | Refinement Calculus: a systematic introduction[END_REF].

In the coherence semantics, a "point" is a complete subgraph,4 called a clique. Since the intuitions behind our objects are quite different, we change the terminology.

Definition 5. Let X be an interface, a subset x ⊆ |X| is called a seed of X if x ⊆ P X (x). We write S(X) for the collection of seeds of X.

More traditional names for seeds are safety properties, or P -invariant properties: if some initial state is in x, no matter what, after each execution of a program satisfying specification P , the final state will still be in x. In other words, P maintains an invariant, namely "staying in x". In particular, there can be no program deadlock when starting from x.

The collection of cliques in the (hyper)coherent semantics forms a c.p.o.: the sup of any directed family exists. The collection of seeds in an interface satisfies the stronger property: Lemma 1. For any interface X, S(X), ⊆ is a complete sup-lattice.

Proof. ∅ is trivially a seed; and by monotonicity of P , a union of seeds is a seed.

⊓ ⊔

The fact that seeds are closed under union may seem counter-intuitive at first; but one possible interpretation is that we allow for non-deterministic data. For example, all denotational models of linear logic have an object for the booleans: its state space is {t, f }, and the cliques are always ∅, {t} and {f }. The union of {t} and {f } is usually not itself a clique because "one cannot get both true and false". However, if one interprets union as a non-deterministic sum, then {t, f } is a perfectly sensible set of data.

However, nothing guarantees that a seed is the unions of all its finite subseeds; a given seed needs not even contain any finite seed!. (The canonical example being P X (x) = X, with X infinite.)

Constructions on Interfaces

A denotational model interprets formulas as objects in a category (and proofs as morphisms). We thus need to define all the constructions of linear logic at the level of interfaces. The most interesting cases are the linear negation and the tensor product (and the exponentials, but they will be treated in section 6).

Note that there will always be an "ambient" set A for predicates. We write x for the A-complement of x.

Let X = (|X|, P X ) and Y = (|Y |, P Y ) be two interfaces; Definition 6. The dual of X is defined as (|X|, P ⊥ X ) where P ⊥ X (x) = P X (x). We write it X ⊥ . An antiseed of X is a seed in X ⊥ .
In terms of specifications, a ∈ P ⊥ (x) means "if the program is started in a, and if execution terminates, the final state will be in x". If P is concerned with wp calculus, then P ⊥ is concerned with wlp calculus. (Weakest liberal precondition, also introduced by Dijkstra.) This operation of "negation" is the reason we do not ask for any properties on the predicate transformer. It respects neither continuity nor commutation properties! In many respects, this operation is not very well-behaved.

Definition 7. The tensor of X and Y is the interface (|X| × |Y |, P X ⊗ P Y ) where P X ⊗ P Y (r) is the predicate transformer r → x×y⊆r P X (x) × P Y (y) .
We write it X ⊗ Y . P X ⊗ P Y is the most natural transformer to construct on |X| × |Y |. It was used in [START_REF] Back | Product in the refinement calculus[END_REF] to model parallel execution of independent pieces of programs. The intuition is the following: a program satisfies P X ⊗ P Y if, when you start it in the pair (a i , b i ) ∈ P X ⊗ P Y (r) of initial states, the two final states will be related through r. In particular, this means that execution is synchronous: both executions need to terminate. Definition 8. The with of X and Y is the interface

(|X| + |Y |, P X & P Y ) where P X & P Y (x, y) = P X (x), P Y (y) . 5 We write it X & Y .
This operation is not very interesting from the specification point of view: it is a kind of disjoint union. Definition 9. The other connectives are defined as usual:

-0 = (∅, Id); ⊤ = 0 ⊥ ; 1 = ({ * }, Id); ⊥ = 1 ⊥ ; -X ⊕ Y ( plus) is the interface X ⊥ & Y ⊥ ⊥ ; -X & Y ( par) is the interface X ⊥ ⊗ Y ⊥ ⊥ ; -X -• Y is the interface X ⊥ & Y .
We have:

Lemma 2. ⊥ = 1; ⊤ = 0 and X ⊕ Y = X & Y .
The proof is immediate. The first two equalities are satisfied in several of the denotational models of LL; the second one is a little less common. (For example, it is satisfied in finiteness spaces, but in no ...-coherence spaces.)

As an application of the definitions, let's massage the definition of

A -• B into something readable: (a, b) ∈ A -• B(r) ⇔ { definition } (a, b) ∈ A ⊥ & B (r) ⇔ { definition, involutivity of ⊥ } (a, b) ∈ A ⊗ B ⊥ ⊥ (r) ⇔ { definition of ⊥ } (a, b) / ∈ A ⊗ B ⊥ (r) ⇔ { definition of ⊗ } ¬ (∃x × y ⊆ r) a ∈ A(x) ∧ b ∈ B ⊥ (y) ⇔ { logic } (∀x × y ⊆ r) a / ∈ A(x) ∨ b / ∈ B ⊥ (y) ⇔ { logic } (∀x × y ⊆ r) a ∈ A(x) ⇒ b ∈ B(y) ⇔ { lemma: x × y ⊆ r iff r x ⊆ y } (∀ r x ⊆ y) a ∈ A(x) ⇒ b ∈ B(y) ⇔ { change of variable: y → y } (∀ r x ⊆ y) a ∈ A(x) ⇒ b ∈ B(y).
From this, we derive:

Lemma 3. (a, b) ∈ A -• B(r) iff a ∈ A(x) ⇒ b ∈ B( r x) for all x ⊆ |X|. For any interface X, Id |X| ∈ S(X -• X).

The shapes of images along X

& Y are usually difficult to visualize, but we have the following on "rectangles": Lemma 4. Let X and Y be interfaces; then for all x ⊆ |X| and y ⊆ |Y | we have:

P X ⊗ P Y (x × y) = P X (x) × P Y (y) ⊆ P X & P Y (x × y). Proof. That P X ⊗ P Y (x × y) = P X (x) × P Y (y) is straightforward. Suppose now a ∈ P X (x) and b ∈ P Y (y), let's show that (a, b) ∈ P X & P Y (x × y): suppose x ′ × y ′ ⊆ x × y ⇒ { claim (see below) } x ⊆ x ′ ∨ y ⊆ y ′ ⇒ { monotonicity } a ∈ P X (x ′ ) ∨ b ∈ P Y (y ′ ). Claim: x ′ × y ′ ⊆ x × y ⇒ x ⊆ x ′ ∨ y ⊆ y ′ Proof of claim: suppose ¬(x ⊆ x ′ ) ∧ ¬(y ⊆ y ′ ) ⇒ x ∩ x ′ = ∅ ∧ y ∩ y ′ = ∅ ⇒ x × y ∩ x ′ × y ′ = ∅ ⇒ ¬(x ′ × y ′ ⊆ x × y).
⊓ ⊔ Furthermore, seeds in A and B are related to seeds in A ⊗ B and A & B in the following way: Lemma 5. Let A and B be interfaces. We have:

(i) if x ∈ S(A) and y ∈ S(B) then x × y ∈ S(A ⊗ B); (ii) if x ∈ S(A) and y ∈ S(B) then x × y ∈ S(A & B).
Proof. The first point is obvious; the second point is a direct consequence of Lemma 4. ⊓ ⊔

Linear Proofs and Seeds

The previous section gave a way to interpret any linear formula F by a interface F * . (When no confusion arises, F * is written F .) We now interpret linear proofs of F as subsets of the state space of F * . 6 We refer to [START_REF] Girard | Linear logic[END_REF] or the abundant literature on the subject for the motivations governing those inference rules.

(

) If π is ⊢ 1 then π * = { * }; (2) if π is ⊢ Γ, ⊤ then π * = ∅; (3) if π is π 1 ⊢ Γ ⊢ Γ, ⊥ then π * = (γ, * ) | γ ∈ π * 1 ; (4) if π is π 1 ⊢ Γ, A, B ⊢ Γ, A & B then π * = γ, (a, b) | (γ, a, b) ∈ π * 1 ; (5) if π is π 1 ⊢ Γ, A π 2 ⊢ ∆, B ⊢ Γ, ∆, A ⊗ B then π * = π * 1 ⊗ π * 2 = γ, δ, (a, b) | (γ, a) ∈ π * 1 ∧ (δ, b) ∈ π * 2 ; (6) if π is π 1 ⊢ Γ, A ⊢ Γ, A ⊕ B then π * = γ, (1, a) | (γ, a) ∈ π * 1 ; 1
6 recall that a sequent A1, . . . An is interpreted by A1 & . . . An and the notation π ⊢ Γ means "π is a proof of sequent Γ "

(7) if π is π 1 ⊢ Γ, B ⊢ Γ, A ⊕ B then π * = γ, (2, b) | (γ, b) ∈ π * 1 ; (8) if π is π 1 ⊢ Γ, A π 2 ⊢ Γ, B ⊢ Γ, A & B then π * is γ, (1, a) |(γ, a) ∈ π * 1 ∪ (γ, (2, b))| γ, b ∈ π * 2 ; (9) if π is π 1 ⊢ Γ, A π 2 ⊢ ∆, A ⊥ ⊢ Γ, ∆ then π * = (γ, δ) | (∃ a) (γ, a) ∈ π * 1 ∧ (δ, a) ∈ π * 2 .
This interpretation is correct in the following sense:

Proposition 1. If π a proof of F , then π * is a seed in F * .
Proof. By induction on the structure of π: we will check that seeds propagate through the above constructions. It is mostly trivial computation, except for two interesting cases:

(

): suppose that π 1 is a seed in Γ & A and that π 2 is a seed in ∆ & B. We need to show that π 1 ⊗ π 2 = γ, δ, (a, b) | (γ, a) ∈ π 1 ∧ (δ, b) ∈ π 2 is a seed in the sequent Γ & ∆ & (A ⊗ B). Let γ, δ, (a, b) ∈ π 1 ⊗ π 2 ⇔ (γ, a) ∈ π 1 and (δ, b) ∈ π 2 ⇒ { π1 and π2 are seeds in Γ, A and ∆, B } (γ, a) ∈ Γ, A(π 1 ) and (δ, π 2 ) ∈ ∆, B(π 2 ). By contradiction, let γ, δ, (a, b) / ∈ Γ, ∆, A ⊗ B(π 1 ⊗ π 2 ) ⇒ γ, δ, (a, b) ∈ Γ ⊥ ⊗ ∆ ⊥ ⊗ (A ⊗ B) ⊥ (π 1 ⊗ π 2 ) ⇒ { for some u × v × r ⊆ π1 ⊗ π2: } γ ∈ Γ ⊥ (u) ∧ δ ∈ ∆ ⊥ (v) ∧ (a, b) ∈ (A ⊗ B) ⊥ (r) ⇒ . . . ∧ (∀x × y ⊆ r) a ∈ A ⊥ (x) ∨ b ∈ B ⊥ (y) . 5
In particular, define x = π 1 u and y = π 2 v; it is easy to show that x × y ⊆ r, so that we have a ∈ A ⊥ (x) or b ∈ B ⊥ (y). Suppose a ∈ A ⊥ (x): we have γ ∈ Γ ⊥ (u) and u × x ⊆ π 1 (easy lemma); so by definition, (γ, a) ∈ Γ ⊥ ⊗ A ⊥ (π 1 ), i.e. (γ, a) / ∈ Γ, A(π 1 )! This is a contradiction. Similarly, one can derive a contradiction from b ∈ B ⊥ (y). This finishes the proof that

π 1 ⊗ π 2 is a seed of Γ, ∆, A ⊗ B. (9): let π 1 be a seed in Γ, A = Γ ⊥ -• A and π 2 a seed in ∆, A ⊥ , i.e. π ∼ 2 is a seed in A -• ∆. Let's show that π = (γ, δ) | (∃a) (γ, a) ∈ π 1 ∧ (δ, a) ∈ π 2 = π ∼ 2 • π 1 is a seed in Γ, ∆. Suppose (γ, δ) ∈ π ∼ 2 • π 1 , i.e. that (γ, a) ∈ π 1 and (a, δ) ∈ π ∼ 2 for some a. We will prove that (γ, δ) is in Γ, ∆(π) = Γ ⊥ -• ∆(π). According to Lemma 3, we need to show that if γ ∈ Γ ⊥ (u) then δ ∈ ∆( π u). Let γ ∈ Γ ⊥ (u) ⇒ { (γ, a) ∈ π1 ⊆ Γ ⊥ -• A(π1) } a ∈ A π 1 u ⇒ { (a, δ) ∈ π ∼ 2 ⊆ A -• ∆(π ∼ 2 ) } δ ∈ ∆ π ∼ 2 π 1 u ⇔ δ ∈ ∆ π u . ⊓ ⊔

Morphisms, Categorical Structure

To complete the formal definition of a category of interfaces, we need to define morphisms between interfaces. This is done in the usual way:

Definition 10. A linear arrow from X to Y is a seed in X -• Y .
Here is a nicer characterization of linear arrows from X to Y :

Lemma 6. r ∈ S(X -• Y ) iff r P X (x) ⊆ P Y r (x) for all x ⊆ |X|. Proof. Suppose r is a seed in X -• Y , let b ∈ r P X (x) ⇒ there is some a s.t. (a, b) ∈ r and a ∈ P X (x) ⇒ { r is a seed in X -• Y } (a, b) ∈ P X -• P Y (r) ⇒ { definition of -• } b ∈ P Y ( r x).
Conversely, suppose r P X (x) ⊆ P Y r (x); let (a, b) ∈ r, and a ∈ P X (x). We have b ∈ r P X (x), and by hypothesis, b ∈ P Y ( r x).

⊓ ⊔

Lemma 7. If r ∈ S(X -• Y ) and r ′ ∈ S(Y -• Z) then r ′ • r ∈ S(X -• Z).
Proof. This is the essence of point (9) from Proposition 1; or a simple corollary to Lemma 6.

⊓ ⊔

Taken together with Lemma 3, this makes interfaces into a category: Definition 11. We write Int for the category with interfaces as objects and linear arrows as morphisms.

This category is an enrichment of the usual category Rel. The construction can be summarized in the following way: Lemma 8. Int is obtained by lifting Rel through the following specification structure ( [START_REF] Abramsky | A specification structure for deadlockfreedom of synchronous processes[END_REF]):

-if X is a set, Pr X ≡ P(X) → P(X); -if r ⊆ X × Y , P ∈ Pr X and Q ∈ Pr Y , then P {r}Q iff r • P ⊆ Q • r .
Let's now turn our attention to the structure of this category: Lemma 9. In Int, ⊤ is terminal and & is the cartesian product.

Proof. This is immediate.

⊓ ⊔ Lemma 10. ⊥ is an involutive contravariant functor.

Proof. Involutivity is trivial; contravariance is only slightly trickier:

r is a seed in A -• B ⇔ { Lemma 6 } ∀x r A(x) ⊆ B r x ⇔ ∀x B r x ⊆ r A(x) ⇔ { lemma: y ⊆ r x iff r ∼ y ⊆ x } ∀x r ∼ B r x ⊆ A(x) ⇒ { in particular, for x of the form r ∼ x; we have x ⊆ r r ∼ x (lemma) } ∀x r ∼ B ⊥ (x) ⊆ A ⊥ r ∼ x i.e. r ∼ is a seed in B ⊥ -• A ⊥ . The action of ⊥ on morphisms is just ∼ . ⊓ ⊔ Corollary 1.
Int is autodual through ⊥ ; 0 is initial; and ⊕ is the coproduct.

It is now easy to see that linear arrows transform seeds into seeds, and, in the other direction, antiseeds into antiseeds:

Proposition 2. Suppose r is a linear arrow from X to Y :

(i) r is a sup-lattice morphism from S(X) to S(Y ); (ii) r ∼ is a sup-lattice morphism from S(Y ⊥ ) to S(X ⊥ ).
Proof. Let r ∈ S(X -• Y ) and x ⊆ X(x); we want to show that r x ⊆ Y ( r x).

Let b ∈ r x ⇔ (∃a) (a, b) ∈ r ∧ a ∈ x ⇒ { r is a seed in X -• Y } (∃a) (a, b) ∈ X -• Y (r) ∧ a ∈ x ⇒ { definition of X -• Y with the fact that r x ⊆ r x } b ∈ Y ( r x).
Showing that r commutes with sups is immediate: it commutes with arbitrary unions, even when the argument is not a seed. The second point follows because

r ∼ ∈ S(Y ⊥ -• X ⊥ ). ⊓ ⊔ Lemma 11. ⊗ [ & ] is a categorical tensor product with neutral element 1 [⊥].
Proof. We need to show the bifunctoriality of ⊗. This was actually proved in the previous section (Proposition 1, point [START_REF] Back | Refinement Calculus: a systematic introduction[END_REF]). The bifunctoriality of & follows by duality; and the rest is immediate.

⊓ ⊔

As a summary of this whole section, we have:

Proposition 3.
Int is a * -autonomous category. (In particular, Int is symmetric monoidal closed.)

Proof. This amounts to checking trivial equalities, in particular, that the following diagram commutes:

(where d is the natural isomorphism X ≃ X ⊥⊥ ) X -• Y ⊥ / / d -1 X • •d Y ) ) S S S S S S S S S S S S S S S Y ⊥ -• X ⊥ ⊥ X ⊥⊥ -• Y ⊥⊥ It is immediate because d = Id and ⊥ = ∼ . ⊓ ⊔

Exponentials

The category Int is thus a denotational model for multiplicative additive linear logic. Let's now add the exponentials !X and ?X. Unsurprisingly, we will use finite multisets; here are the necessary definitions and notations: Definition 12. Let S be a set; -if (s i ) i∈I and (t j ) j∈J are finite families on S, say (s i ) ≃ (t j ) iff there is a bijection σ from I to J such that s i = t σ(i) for all i in I. -A finite multiset over S is an equivalence class of ≃. We write [s i ] for the equivalence class containing (s i ). -M f (S) is the collection of finite multisets over S.

-Concatenation of finite families 7 can be lifted to multisets; it is written +.

-If x and y are two subsets of S, we write x * y for the set

{[a, b] | a ∈ x∧b ∈ y}.
Its indexed version is written i∈I x i ; it is a kind of commutative product.

-If U and V are two subsets of M f (A), the set {u + v | u ∈ U ∧ v ∈ V } is written U * V (same symbol,

but no confusion arises).

Definition 13. For X = (|X|, P ), define !X = (M f (|X|), !P ) where

[a 1 , . . . a n ] ∈ !P (U ) ⇔ ∃(x i ) 1≤i≤n i x i ⊆ U ∧ (∀i = 1, . . . n) a i ∈ P (x i ) Let ?X = !(X ⊥ ) ⊥ .
Recall that a multiset [a i ] is in x i iff there is a bijection σ s.t. ∀i, a i ∈ x σ(i) .

A useful intuition is that [a 1 , . . .] ∈ !P (U ) iff [a 1 , . . .] is in a "weak infinite tensor" n X ⊗n (U ). In terms of specifications and programs, it suggests multithreading: for an initial state [a 1 , . . . a n ], start n occurrences of the program in the states a 1 ,. . . a n ; the final state is nothing but the multiset of all the n final states. 8 The "weak" part means that we forget the link between a particular final state and a particular initial state.

Note that this is a "non-uniform" model in the sense that the web of !X contains all finite multisets, not just those whose underlying set is a seed. It is thus closer to non-uniform (hyper)coherence semantics (see [START_REF] Bucciarelli | On phase semantics and denotational semantics: the exponentials[END_REF] or [START_REF] Boudes | Non-uniform hypercoherences[END_REF]) than to the traditional (hyper)coherence semantics.

7 defined on the disjoint sum of the different index sets 8 The interpretation of !, like that of ⊗ is a synchronous operation.

Let's prove a simple lemma about the exponentials:

Lemma 12. Suppose U ⊆ M f (|A|): (i) [a] ∈ !A(U ) iff there is some x "included" in U (i.e. ∀a ∈ x [a] ∈ U ) s.t. a ∈ A(x); (ii) l + l ′ ∈ !A(U ) iff there are V * V ′ ⊆ U s.t. l ∈ !A(V ) and l ′ ∈ !A(V ′ ); (iii) [a] ∈ ?A(U ) iff for all x "included" in U, a ∈ A(x); (iv) l + l ′ ∈ ?A(U ) iff for all V * V ′ ⊆ U , l ∈ ?A(V ) or l ′ ∈ ?A(V ′ ).
Proof. The first point is immediate and the second is left as an exercise. The third and last point are consequences of the definition of ? in terms of !.

⊓ ⊔

Define now the interpretation of proofs with exponentials:

(10) if π is π 1 ⊢ Γ, A ⊢ Γ, ?A then π * = γ, [a] | (γ, a) ∈ π * 1 ; (11) if π is π 1 ⊢ Γ ⊢ Γ, ?A then π * = γ, [ ] | γ ∈ π * 1 ; (12) if π is π 1 ⊢ Γ, ?A, ?A ⊢ Γ, ?A then π * = (γ, l + l ′ ) | (γ, l, l ′ ) ∈ π * 1 ; (13) if π is π 1 ⊢ ?Γ, A ⊢ ?Γ, !A
then we define γ 1 , . . . γ l , [a 1 . . . a n ] ∈ π * if for each j = 1, . . . l, there is a partition γ j = 1≤i≤n γ i j and the following holds: for each i = 1, . . . n, (γ i 1 , . . . γ i l , a i ) ∈ π * 1 .

Proposition 4. If π a proof of ⊢ Γ , then π * is a seed of Γ .

Proof. Points [START_REF] Bucciarelli | On phase semantics and denotational semantics: the exponentials[END_REF] and [START_REF] Boudes | Non-uniform hypercoherences[END_REF] are immediate. [START_REF] Hyvernat | Predicate transformers and linear logic: second order[END_REF]: suppose π 1 is a seed Γ, ?A, ?A and let (γ, l + l ′ ) be an element of π. By contradiction, suppose that (γ, l + l ′ ) / ∈ Γ, ?A(π)

⇔ (γ, l + l ′ ) ∈ Γ ⊥ ⊗ !A ⊥ (π) ⇔ { for some u × U ⊆ π } γ ∈ Γ ⊥ (u) ∧ l + l ′ ∈ !A ⊥ (U ) ⇔ { Lemma 12 } γ ∈ Γ ⊥ (u) ∧ (∃V * V ′ ⊆ U ) l ∈ !A ⊥ (V ) ∧ l ′ ∈ !A ⊥ (V ′ ) ⇒ { lemma: u × V × V ′ ⊆ π1 } γ ∈ Γ ⊥ (u) ∧ l ∈ !A ⊥ (V ) ∧ l ′ ∈ !A ⊥ (V ′ ) ⇒ (γ, l, l ′ ) ∈ Γ ⊥ ⊗ !A ⊥ ⊗ !A ⊥ (π 1 ) ⇔ (γ, l, l ′ ) /
∈ Γ, ?A, ?A(π 1 ), which contradicts the fact that π 1 is a seed in Γ, ?A, ?A.

This allows us to transform any sequent ?Γ = ?B 1 & . . . ?B n into ?(B 1 ⊕ . . . B n ), and thus, formally ends the proof of Proposition 4 point (13).

Linear Interfaces and Linear Seeds

What is the structure of those interfaces that come from a linear formula? The answer is unfortunately trivial:

Proposition 5. If F is a linear formula, then P F = Id P|F | .
Proof. Immediate induction. Let's treat the case of the exponentials: suppose

F (x) = x; suppose moreover that [a 1 , . . . a n ] ∈ U ⇒ a i ∈ F ({a i }) for all i and {a i } = {[a 1 , . . . a n ]} ⊆ U ⇒ [a 1 , . . . a n ] ∈ !F (U ) Similarly, suppose [a 1 , . . . a n ] ∈ !F (U ) ⇒ each a i ∈ F (x i ) = x i for some (x i ) s.t. x i ⊆ U ⇒ { [a1, . . . an] ∈ xi } [a 1 , . . . a n ] ∈ U . ⊓ ⊔
In particular, every subset of |F | is a clique and an anticlique: the situation is thus quite similar to the purely relational model. In the presence of atoms however, interfaces become much more interesting.

Adding atoms is sound because the proof of Proposition 1 doesn't rely on the particular properties of interfaces. Note that we need to introduce a general axiom rule and its interpretation:

(14) if π is ⊢ X, X ⊥ then π * = Id |X| = {(a, a) | a ∈ |X|}.
This is correct in the sense that π * is always a clique in X & X ⊥ . With such atoms, the structure of linear interfaces gets non trivial. 9 For example, let's consider the following atom X = {-, +}, P defined by: -P (∅) = ∅ and P (|X|) = |X|; -P ({+}) = {-} and P ({-}) = {+}. This is the simplest example of an interesting interface, and corresponds to a "switch" specification. (Interpret -as "off" and + as "on".) Lemma 14. if P is the above specification:

(i) P ⊥ = P ; (ii) P • P = Id; (iii) S(X) = ∅, {+, -} ; (iv) (+, -), (-, +) ∈ S(X ⊗ X).
Proof. This is just trivial computation...

⊓ ⊔

Point (iv) shows in particular that a seed in X ⊗ Y needs not contain a product of seeds in X and Y . (Compare with Lemma 5.)

The hierarchy generated from this single interface is however still relatively simple: call a specification deterministic if it commutes with non-empty unions and intersections.

Lemma 15. Let F be any specification constructed from the above P and the linear connectives. Then F is deterministic. Moreover, F is of the form f where f is an obvious bijection on the state space of F . 10 A less trivial (in the sense that it is not deterministic) specification is the following: if X is a set, magic X (x) = X. In terms of programming, the use of the magic command allows to reach any predicate, even the empty one!

Lemma 16. Id |X| magic X -• magic X (Id |X| ) if X = ∅.
Thus we cannot strengthen the definition of seeds to read "x = P (x)" without imposing further constraints on our specifications. It is still an open question to find a nice class of predicate transformers for which it would be possible. (However, considerations about second order seem to indicate that strengthening the definition of seeds in such a way is not a good idea.)

In the case with atoms, because the structure of seeds (sup-lattice) is quite different from the structure of cliques in the ...-coherent model (domain), it is difficult to relate seeds and cliques. In particular, a seed needs not be a clique (since the union of arbitrary cliques is not necessarily a clique); and a clique needs not be a seed (since a subset of a seed is not necessarily a seed).

Conclusion

One aspect which was not really mentioned here is the fact that linear arrows from A to B are equivalent to the notion of forward data refinement (Lemma 6) from the refinement calculus. In particular, a linear proof of A -• B is a proof that specification B implements specification A. It would interesting to see if any application to the refinement calculus could be derived from this work. In the same direction, trying to make sense of the notions of backward data refinement, or of general data refinement in terms of linear logic could prove interesting. The fact that this model is degenerate in the propositional case is disappointing, but degeneracy disappear when we consider Π 1 logic, and a fortiori when we consider full second-order (see [START_REF] Hyvernat | Predicate transformers and linear logic: second order[END_REF]). The point of extending this propositional model to Π 1 is to remove the dependency on specific valuations for the atoms present in a formula.

One the interesting consequences of this work is that a a proof of a formula F gives a guarantee that the system specified by the formula F can avoid deadlocks seems to point toward other fields like process calculi and similar models for "real" computations. This direction is currently being pursued together with the following link with the differential lambda-calculus ( [START_REF] Ehrhard | The differential lambda calculus[END_REF]): one property of this model which doesn't reflect any logical property is the following; we have a natural transformation A -• !A called co-dereliction, which has a natural interpretation in terms of differential operators on formulas (see [START_REF] Ehrhard | Differential interaction nets[END_REF]). Note that such a natural transformation forbids any kind of completeness theorem, at least as far as "pure" linear logic is concerned.

11

 11

10

  where f (x) = {f (a) | a ∈ x} 11 A data refinement from specification F to specification G is a predicate transformer P s.t. P • F ⊆ G • P ; a forward [resp. backward] data refinement is a data refinement which commutes with arbitrary unions [resp. arbitrary intersections].

In a previous version, interfaces also had to enjoy the property P (∅) = ∅ and P (|X|) = |X|. This condition doesn't interact well with second order interpretation and has thus been dropped.

[START_REF] Gardiner | An algebraic construction of predicate transformers[END_REF] The intuition is that a set of data is coherent iff it is pairwise coherent.

it uses implicitly the fact that P(|X| + |Y |) ≃ P(|X|) × P(|Y |)

We can extend this to a model for Π 1 logic, and even to full second order, see[START_REF] Hyvernat | Predicate transformers and linear logic: second order[END_REF].

(13): suppose that Γ contains only one formula B. The general case will follow from a lemma proved below (Lemma 13). Suppose that π 1 is a seed in ?B, A; let (l, [a 1 , . . . a n ]) be in π, i.e. (l i , a i ) ∈ π 1 for i = 1, . . . n, for some partition (l 1 , . . . l n ) of l. Suppose by contradiction that (l, [a 1 . . .

, which contradicts the fact that π 1 is a seed in ?B, A. ⊓ ⊔ Lemma 13. For all interfaces X and Y , we have

Proof. The state spaces are isomorphic via

We will use this transparently, for example l X + l Y ∈ R iff (l X , l Y ) ∈ R. This is possible because the sets are disjoint: we can always split a multiset in x * y into two multisets in x and y. (In other words: if x ∩ y = ∅ then x * y ≃ x × y.) Notice also that (1, a) ∈ X & Y (x, y) ⇔ a ∈ X(x) so that when considering a particular element of X + Y (x, y), only one part of the argument (x, y) is really important; the other can be dropped (or replaced with ∅). ⊓ ⊔