Ilik Danko

AN INTERPRETATION OF THE SIGMA-2 FRAGMENT OF CLASSICAL ANALYSIS IN SYSTEM T

We show that it is possible to define a realizability interpretation for the Σ 2 -fragment of classical Analysis using Gödel's System T only. This supplements a previous result of Schwichtenberg regarding bar recursion at types 0 and 1 by showing how to avoid using bar recursion altogether. Our result is proved via a conservative extension of System T with an operator for composable continuations from the theory of programming languages due to Danvy and Filinski. The fragment of Analysis is therefore essentially constructive, even in presence of the full Axiom of Choice schema: Weak Church's Rule holds of it in spite of the fact that it is strong enough to refute the formal arithmetical version of Church's Thesis.

Introduction

In the middle of the 20 th century, Kurt Gödel showed how to give a computational interpretation and a relative consistency proof of intuitionistic Arithmetic via his System T of equations between functionals definable by primitive recursion (in higher types) [START_REF] Gödel | Collected works. Unpublished essays and lectures, volume III, chapter In what sense is intuitionistic logic constructive[END_REF][START_REF] Gödel | Collected works[END_REF]. Thanks to the fact that the induction axiom intuitionistically proves its own double negation translation, the interpretation also applies to classical Arithmetic. However, since the Axiom of Choice, (AC) ∀x∃yA(x, y) → ∃f ∀xA(x, f (x)),

does not intuitionistically prove its double negation translation, the interpretation does not apply to classical Analysis. Gödel was of course aware of this fact and suggested [21, §2.43] that an extension of System T is needed which can interpret the logical schema, ¬¬∀x(A(x) ∨ ¬A(x)), known as Kuroda's Conjecture [START_REF] Kuroda | Intuitionistische untersuchungen der formalistischer logik[END_REF], intuitionistically equivalent to the nowadays better known schema of Double Negation Shift, (DNS) ∀x¬¬B(x) → ¬¬∀xB(x).

Gödel must have also been aware of the difficulty involved in giving a computational interpretation to Kuroda's Conjecture, for already his 1941 lecture at Yale [START_REF] Gödel | Collected works. Unpublished essays and lectures, volume III, chapter In what sense is intuitionistic logic constructive[END_REF] considers the special case when the formula A(x) is ∃y T(x, x, y) -where T is Kleene's predicate verifying that the Turing machine with code x, when run on input x, terminates with code y -which directly proves (see [START_REF] Troelstra | Metamathematical Investigations of Intuitionistic Arithmetic and Analysis[END_REF]) the negation of the formal arithmetical version of Church's Thesis, (CT 0 ) ∀x N ∃y N A(x, y) → ∃e N ∀x N ∃u N (T (e, x, u) ∧ A(x, U (u))).

In spite of that, Spector and Kreisel [START_REF] Spector | Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics[END_REF][START_REF] Gödel | Collected works[END_REF] managed to give a computational interpretation of DNS by extending System T with bar recursion, the computational adequacy of which was shown using a formal version of Brouwer's principle of Bar Induction [START_REF] Spector | Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics[END_REF][START_REF] William | Functional interpretation of bar induction by bar recursion[END_REF]. This approach to extracting computational content from proofs in Analysis via an extension of the primitive recursive System T with a general recursive schema, has been much refined over the 50 years since it appeared [START_REF] Kreisel | Review of the paper "The model G of the theory BR" by Ersov[END_REF][START_REF] Bezem | On the computational content of the axiom of choice[END_REF][START_REF] Kohlenbach | Applied Proof Theory: Proof Interpretations and Their Use in Mathematics[END_REF][START_REF] Berger | Refined program extraction from classical proofs[END_REF][START_REF] Berger | A computational interpretation of open induction[END_REF][START_REF] Berger | Modified bar recursion and classical dependent choice[END_REF][START_REF] Berger | Modified bar recursion[END_REF][START_REF] Seisenberger | Program from proofs using classical dependent choice[END_REF] and has been applied to obtain results in Analysis proper, notably in Kohlenbach's Proof Mining programme [START_REF] Kohlenbach | Applied Proof Theory: Proof Interpretations and Their Use in Mathematics[END_REF].

Nevertheless, as Schwichtenberg showed already in 1979 [START_REF] Schwichtenberg | On bar recursion of types 0 and 1[END_REF], higher type primitive recursion is closed over the schema of bar recursion at types 0 and 1, and since a previous analysis of Kreisel [31, §12.2] shows that those low types are sufficient for interpreting the classical Axiom of Choice for formulas of the form ∃α ∈ N → N∀x ∈ NA 0 (α, x), A 0 -quantifier-free, we in fact known that we should need no more than the primitive recursive functionals themselves in order to give a realizability interpretation of the uniformly realizable part of Analysis. Yet, it has remained unclear up to this day how to avoid using general recursive schemata altogether.

One alternative is offered by the use of so called computational side-effects (control operators) from the theory of programming languages. Krivine [START_REF] Krivine | Dependent choice, 'quote' and the clock[END_REF] used a realizability interpretation based on a virtual machine which can execute lambda calculus terms, extended with a control operator and a special machine instruction called "quote". Herbelin [START_REF] Herbelin | A constructive proof of dependent choice, compatible with classical logic[END_REF] gave a more direct approach based on rewrite rules for a type theory extended with a control operator and a coinductive treatment of the existential quantifier. Both approaches rely on a proper extension of System T that can give a computational interpretation to full classical logic. However, given that there are classically true arithmetic statements that do not have a recursive realizer, it is not clear what the meaning of control operators outside the Σ 0 1 -fragment is. In this paper, we show that computational side-effects are not needed in the language of realizers, that is, although they are conceptually essential, control operators can be seen as a meta-mathematical technique. Proofs of the Σ 2 -fragment of Analysis, with the full Axiom of Choice, are essentially constructive and realizable by System T terms only. The soundness of the interpretation relies on a form of Markov's Principle (the Shift rule), rather than full classical logic [START_REF] Bezem | On the computational content of the axiom of choice[END_REF][START_REF] Krivine | Dependent choice, 'quote' and the clock[END_REF][START_REF] Herbelin | A constructive proof of dependent choice, compatible with classical logic[END_REF] or continuity principles [START_REF] Spector | Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics[END_REF][START_REF] William | Functional interpretation of bar induction by bar recursion[END_REF][START_REF] Berger | A computational interpretation of open induction[END_REF][START_REF] Berger | Modified bar recursion and classical dependent choice[END_REF].

Conservative extension of System T with operators for composable continuations

The constructive interpretation of proofs of Section 3 is based on Gödel's System T in its lambda-calculus formulation [START_REF] Troelstra | Metamathematical Investigations of Intuitionistic Arithmetic and Analysis[END_REF][START_REF] Schwichtenberg | Proofs and Computations[END_REF]. Nevertheless, we consider it a conceptual advantage to use an intermediate system, the System T + obtained when System T is extended with a control operator for composable continuations, the so called call-by-name variant of the shift operator of Danvy and Filinski [START_REF] Danvy | Abstracting control[END_REF]. The control operator is a key conceptual ingredient that led us to the interpretation [START_REF] Herbelin | An intuitionistic logic that proves Markov's principle[END_REF][START_REF] Ilik | Constructive Completeness Proofs and Delimited Control[END_REF][START_REF] Ilik | Delimited control operators prove double-negation shift[END_REF][START_REF] Ilik | A direct version of Veldman's proof of open induction on Cantor space via delimited control operators[END_REF].

The goal of this technical section is to prove the following conservativity theorem, as well as prove that suitable equations important for Section 3 hold of System T (+) (Proposition 1).

Normalization Theorem. Every term of System T + maps to a term in normal form of System T.

The types of System T (+) are N, functions N → N, functionals (ex. (N → N) → N), and Cartesian products of these. Types will be denoted by σ, τ :

T ∋ σ, τ ::= N | σ → τ | σ * τ.
Terms of System T + are constants associated with a sequent σ 1 ; . . . ; σ n ⊢ τ (also written γ ⊢ τ for γ a finite ordered list of types) which means that a term is of type τ and the free variables that appear in the term are of types σ 1 , . . . , σ n . The terms, marked in sans-serif face, are defined inductively as follows. This style of presenting lambda calculus terms, known as deBruijn convention, keeps the language of terms first-order, that is, it avoids problems related to handling variables as names that we have to keep track of externally to the system: hyp denotes the variable corresponding to the nearest preceding lambda abstraction lam or a shift, wkn hyp denotes the second most recent introduced variable, wkn wkn hyp the third one, and so on. Seen as natural numbers (hyp is 0, wkn is successor), these are just so called deBruijn indices.

hyp (σ; γ) ⊢ σ wkn γ ⊢ σ (τ ; γ) ⊢ σ lam (σ; γ) ⊢ τ γ ⊢ σ → τ app γ ⊢ σ → τ γ ⊢ σ γ ⊢ τ pair γ ⊢ σ γ ⊢ τ γ ⊢ σ * τ fst γ ⊢ σ * τ γ ⊢ σ snd γ ⊢ σ * τ γ ⊢ τ zero γ ⊢ N succ γ ⊢ N γ ⊢ N rec γ ⊢ N γ ⊢ σ γ ⊢ N → σ → σ γ ⊢ σ shift (N → σ → N; γ) ⊢ N γ ⊢ σ For example,
The terms of System T have a great computational potential, they can compute any higher-type primitive recursive function. There is, however, a subclass of terms which denote computations that have finished, the so called terms in normal form. These will be sufficient for denoting programs and data extracted from proofs in classical Analysis in Section 3. Technically, the normal forms are known as βnormal in reference to the associated β-reduction relation. Here we give a direct inductive characterization of normal terms (⊢ r ),

e γ ⊢ e σ γ ⊢ r σ lam (σ; γ) ⊢ r τ γ ⊢ r σ → τ pair γ ⊢ r σ γ ⊢ r τ γ ⊢ r σ * τ zero γ ⊢ r N succ γ ⊢ r N γ ⊢ r N defined at the same time with the so called neutral terms (⊢ e ), hyp (σ; γ) ⊢ e σ wkn γ ⊢ r σ (τ ; γ) ⊢ e σ app γ ⊢ e σ → τ γ ⊢ r σ γ ⊢ e τ fst γ ⊢ e σ * τ γ ⊢ e σ snd γ ⊢ e σ * τ γ ⊢ e τ rec γ ⊢ e N γ ⊢ r σ γ ⊢ r N → σ → σ γ ⊢ e σ .
Neutral terms correspond to computation that are "blocked": neutral terms are those that contain open/free variables that block a β-reduction step from happening.

A property that will be later used (proof of Corollary 1) follows directly from the shape of normal forms: any closed normal term of type N, i.e. a term of type ∅ ⊢ r N, is actually a numeral, that is, built only from zero and succ-terms. This follows because closed normal terms cannot be neutral: a neutral term necessarily has at least one free variable.

We are now ready to state our first theorem precisely.

Normalization Theorem. There is a normalization procedure ↓such that, for every term p of System T + of type γ ⊢ τ , the term ↓ p is a term in normal form of System T of the same type (γ ⊢ r τ ).

This theorem is not a standard fact from the theory of lambda calculus with control operators. As a matter of fact, we present the first proof that control operators can be completely eliminated from System T.

Specialists will recognize the proof method as a normalization-by-evaluation [START_REF] Berger | An inverse of the evaluation functional for typed lambda-calculus[END_REF] or type-directed partial evaluation [START_REF] Danvy | Type-directed partial evaluation[END_REF] argument. Nevertheless, the addition of control operators requires us to perform the proof in so called continuation-passing style; a similar technique has been used to provide a constructive completeness proof for non-minimal intuitionistic logic when disjunction and the existential quantifier are present [START_REF] Ilik | Constructive Completeness Proofs and Delimited Control[END_REF][START_REF] Ilik | Continuation-passing style models complete for intuitionistic logic[END_REF].

The proof is constructive and can be formalized in a suitable predicative metatheory such as Martin-Löf Type Theory (for a modern formulation see [START_REF]Homotopy Type Theory: Univalent Foundations of Mathematics[END_REF]). At her convenience, the reader may find this full mechanization of the proof in Agda notation in [START_REF] Ilik | Formal proof of normalization of System T+ in Agda[END_REF]; one can also use this machine-checked constructive proof directly in order to compute, for example, that the term for the Ackermann function A(3,2) really evaluates to succ • • • succ We first need a precise way to speak about extensions of type contexts γ (imposed by the fact that we want to normalize potentially open terms). This is formalized by the initial segment, or prefix, preorder ≥ as follows.

≥ refl γ ≥ γ ≥ cons γ 2 ≥ γ 1 (σ; γ 2 ) ≥ γ 1
For example, the proof of τ 1 ; τ 2 ; γ ≥ γ will be denoted by ≥ cons ≥ cons ≥ refl . The transitivity of ≥ is proven as the (right-associative) operation (-) • (-), defined by recursion on the construction of the proofs of

γ 3 ≥ γ 2 and γ 2 ≥ γ 1 . (-) • (-) : γ 3 ≥ γ 2 ⇒ γ 2 ≥ γ 1 ⇒ γ 3 ≥ γ 1 ≥ 3 • ≥ refl =≥ 3 ≥ refl • ≥ 2 =≥ 2 (≥ cons ≥ 3 )• ≥ 2 =≥ cons (≥ 3 • ≥ 2 )
In this definition, and henceforth, the notation ≥ n will be used to denote a (hypothetical) proof of γ n ≥ γ k . For example, given a proof ≥ 2 of γ 2 ≥ σ; γ 1 , one can prove γ 2 ≥ γ 1 by the denotation ≥ 2 • ≥ cons ≥ refl .

We can now define precisely the forcing set γ σ. This is done simultaneously with the strong forcing set γ s σ, itself defined inductively following the construction of the type σ.

γ σ = ∀γ 1 ≥ γ (∀γ 2 ≥ γ 1 (γ 2 s σ ⇒ γ 2 ⊢ r N) ⇒ γ 1 ⊢ r N) γ s N = γ ⊢ r N γ s (σ → τ ) = ∀γ ′ ≥ γ(γ ′ σ ⇒ γ ′ τ ) γ s (σ * τ ) = γ σ × γ τ
We will also need γ ′ γ, the component-wise extension of the forcing relation defined as follows ([] denotes the empty context).

γ ′ [] = ⊤ γ ′ (σ; γ) = (γ ′ σ) × (γ ′ γ)
The first equation defines the forcing of the empty context to be the singleton set ⊤, whose unique inhabitant is denoted tt. The symbol × constructs a Cartesian product i.e. pair type in the ambient type theory; the components of a Cartesian product can be accessed by the projection operations proj 1 and proj 2 .

The following operations (lemmas) show that ⊢ r , ⊢ e , , s , are all monotone with respect to the prefix preorder. The last two operations are defined by induction on types and contexts, respectively.

(-) (-) :

γ 2 ≥ γ 1 ⇒ γ 1 ⊢ r σ ⇒ γ 2 ⊢ r σ H ≥ refl = H H ≥cons≥2 = e(wkn( H ≥2 )) (-) (-) : γ 2 ≥ γ 1 ⇒ γ 1 ⊢ e σ ⇒ γ 2 ⊢ e σ H ≥ refl = H H ≥cons≥2 = wkn(e( H ≥2 )) ⌈(-)⌉ (-) : γ 2 ≥ γ 1 ⇒ γ 1 σ ⇒ γ 2 σ ⌈H⌉ ≥ refl = H ⌈H⌉ ≥cons≥2 =≥ 3 → H(≥ 3 • ≥ cons ≥ 2 ) ⌊(-)⌋ σ (-) : γ 2 ≥ γ 1 ⇒ γ 1 s σ ⇒ γ 2 s σ ⌊H⌋ σ→τ ≥2 =≥ 3 → H(≥ 3 • ≥ 2 ) ⌊(H 1 , H 2 )⌋ σ * τ ≥2 = ⌈H 1 ⌉ ≥2 , ⌈H 2 ⌉ ≥2 ⌊H⌋ N ≥2 = H ≥2 ⌈ ⌈(-)⌉ ⌉ (-) γ2 : γ 2 ≥ γ 1 ⇒ γ 1 γ ⇒ γ 2 γ ⌈ ⌈H⌉ ⌉ ≥2 [] = H ⌈ ⌈H⌉ ⌉ ≥2 σ;γ = ⌈proj 1 H⌉ ≥2 , ⌈ ⌈proj 2 H⌉ ⌉ ≥2 γ
Finally, we also need lemmas relating the forcing sets and derivability, the return (η) and run (µ) operations.

η(-) : γ s σ ⇒ γ σ µ(-) : γ N ⇒ γ s N ηH =≥ 1 κ → κ ≥ refl ⌊H⌋ ≥1 µH = H ≥ refl (≥ 1 α → α)
Return shows that we can always lift a member of the strong forcing set to a member of the forcing set. Run shows that, whenever we have a member of a set forcing type N, we can actually obtain a term of System T in normal form from it; note that by definition the sets γ s N and γ ⊢ r N are the same.

The reify function ↓ (-) shows that we can actually run any forcing set, for any type σ, and not just for σ = N. It is defined by induction on the type.

γ ↓ σ (-) : γ σ ⇒ γ ⊢ r σ γ ↓ N H = µH γ ↓ σ→τ H = lam( γ ↓ τ (≥ 1 κ → H(≥ 1 • ≥ cons ≥ refl ) (≥ 2 φ → φ ≥ refl (⌈ σ;γ ↑ σ hyp⌉ ≥2•≥1 ) ≥ refl (≥ 3 → κ(≥ 3 • ≥ 2 ))))) γ ↓ σ * τ H = pair α ↓ σ (≥ 1 κ → H ≥ 1 (≥ 2 α → proj 1 α ≥ refl (≥ 3 → κ(≥ 3 • ≥ 2 )))) α ↓ τ (≥ 1 κ → H ≥ 1 (≥ 2 α → proj 2 α ≥ refl (≥ 3 → κ(≥ 3 • ≥ 2 ))))
The case of arrow type forces us to define, at the same time with the reify function, the reflect function ↑ (-):

γ ↑ σ (-) : γ ⊢ e σ ⇒ γ σ γ ↑ N p = η(e p) γ ↑ σ→τ p = η(≥ 2 α → γ ↑ τ app( p ≥2 , γ ↓ σ α)) γ ↑ σ * τ p = η( γ ↑ σ fst p, γ ↑ τ snd p)
Note that this function needs as domain only the neutral terms.

Finally, we are ready to define the evaluation functionthat constructs a member of the forcing set for any input term of System T + . The definition is by recursion on the construction of the term p.

γ (-) σ (-) : γ ⊢ σ ⇒ ∀γ ′ γ(γ ′ σ) hyp ρ = proj 1 ρ wkn p ρ = p proj 2 ρ lam p ρ = η(≥ 1 α → p (α,⌈ ⌈ρ⌉ ⌉ ≥ 1 ) ) app(p, q) ρ =≥ 1 κ → p ρ ≥ 1 (≥ 2 φ → φ ≥ refl ( q ⌈ ⌈ρ⌉ ⌉ ≥ 2 •≥ 1 ) ≥ refl (≥ 3 → κ(≥ 3 • ≥ 2 ))) pair(p, q) ρ = η( p ρ , q ρ ) fst p ρ =≥ 1 κ → p ρ ≥ 1 (≥ 2 α → proj 1 α ≥ refl (≥ 3 → κ(≥ 3 • ≥ 2 ))) snd p ρ =≥ 1 κ → p ρ ≥ 1 (≥ 2 α → proj 2 α ≥ refl (≥ 3 → κ(≥ 3 • ≥ 2 ))) shift p ρ =≥ 1 κ → µ p η(≥2ν →η(≥3α →η(α≥ refl (≥4 →κ(≥4•≥3•≥2))))),⌈ ⌈ρ⌉ ⌉ ≥ 1 zero ρ = η(zero) succ p ρ = η(succ (µ p ρ )) rec(n, a, f ) ρ =≥ 1 κ → n ρ ≥ 1 (≥ 2 ν → {ν} ⌈ ⌈ρ⌉ ⌉ ≥ 2 •≥ 1 ≥ refl (≥ 3 → κ(≥ 3 • ≥ 2 )))
where

{zero} ρ ′ = a ρ ′ {succ r} ρ ′ =≥ 1 κ → f ⌈ ⌈ρ ′ ⌉ ⌉ ≥ 1 ≥ refl (≥ 2 γ → γ ≥ refl (η r ≥2•≥1 ) ≥ refl (≥ 3 δ → {r} ρ ′ (≥ 3 • ≥ 2 • ≥ 1 )(≥ 4 α → δ ≥ 4 (ηα) ≥ refl (≥ 5 → κ(≥ 5 • ≥ 4 • ≥ 3 • ≥ 2 ))))) {e e} ρ ′ = ↑ rec(e, ↓ a ρ ′ , ↓ f ρ ′ )
Note that the argument ρ is of type γ ′ γ.

For γ ′ = γ, such a ρ can always be constructed by reflecting the term hyp:

⇑ γ : γ γ ⇑ [] = tt ⇑ σ; γ = (↑ σ hyp), ⌈ ⌈⇑ γ⌉ ⌉ ≥cons≥ refl
We have therefore shown that, given p : γ ⊢ σ of System T + , there is a term in normal form ↓ p ρ : γ ⊢ r σ of System T, for every ρ, and in particular one such term is ↓ p ⇑γ .

The following proposition characterizes the equational theory generated by the normalization procedure. It will be used in the proof of Soundness Theorem of Section 3. This has also been machine checked and is available in Agda notation from [START_REF] Ilik | Formal proof of normalization of System T+ in Agda[END_REF]. Proposition 1. The following definitional equalities hold,

↓ wkn p α,ρ = ↓ p ρ for α ∈ τ ; γ τ (1) ↓ hyp α,ρ = ↓ α for α ∈ γ τ (2) ↓ fst pair(p, q) ρ = ↓ p ρ (3) ↓ snd pair(p, q) ρ = ↓ q ρ (4) ↓ app(lam p, q) ρ = ↓ p q ρ ,ρ (5)
↓ rec(zero, p, q) ρ = ↓ p ρ [START_REF] Danvy | Type-directed partial evaluation[END_REF] ↓ rec(succ r, p, q) ρ = ↓ app(app(q, r), rec(r, p, q)) ρ (7)

↓ N shift p ρ = ↓ N p φ,ρ (8)
↓ N app(app(hyp, x), y) φ,ρ = ↓ N y φ,ρ (9)
where for the last two equations,

φ := η(≥ 2 ν → η(≥ 3 α → η(µα))),
and x, y : N → N → N ⊢ N.

Proof. Equations ( 1)-( 7) follow from the ones that hold already of the -(-) function. This is because, as an argument to the ↓ (-) function, the evaluation function is always applied to some ≥ 1 and κ.

p ρ ≥ 1 κ = q ρ ≥ 1 κ wkn p α,ρ ≥ 1 κ = p ρ ≥ 1 κ hyp α,ρ ≥ 1 κ = α ≥ 1 κ fst pair(p, q) ρ ≥ 1 κ = p ρ ≥ 1 κ snd pair(p, q) ρ ≥ 1 κ = q ρ ≥ 1 κ app(lam p, q) ρ ≥ 1 κ = p q ρ ,ρ ≥ 1 κ rec(zero, p, q) ρ ≥ 1 κ = p ρ ≥ 1 κ
rec(succ r, p, q) ρ ≥ 1 κ = app(app(q, r), rec(r, p, q)) ρ ≥ 1 κ These equations come out by unfolding the definition and occasionally using an η-equality step of the form (α → φα) = φ.

Equations ( 8)-( 9) also follow by definition, this time reification being applied for only one concrete type, N.

A modified realizability interpretation of Analysis

By a logical theory sufficient to formalize proofs of Analysis we have in mind the System HA ω+ of Figure 1 together with the full axiom of choice schema AC = ∪ σ,τ ∈T AC στ ,

(AC στ ) ∀x σ ∃ τ yA(x, y) → ∃ σ→τ f ∀x σ A(x, f (x)).
This formulation of the axiom is strictly stronger than the Axiom of Dependent Choices which usually treated in the context of realizability interpretations for Analysis. One can also consider the axioms of Figure 2 to be part of HA ω+ . It is known that due to their logical form, the proof interpretation that we are going to

Γ ⊢ ∀x N A(x) ∀x N (A(x) → S(x)), Γ ⊢ S(r) Shift Γ ⊢ A(r) (A, S ∈ Σ 2 )
Figure 1: A natural deduction system for the theory HA ω+ employ has no modifying effect on them. On the other hand, they can indicate in which sense the realizability model supports extensionality.

HA ω+ is a first-order, predicate logic which is multi-sorted, that is, has variables and quantifiers that range over the types of System T. The system is "minimal" in the sense of Schwichtenberg [START_REF] Schwichtenberg | Proofs and Computations[END_REF] -one wants to know that the method works even if we do not have a special treatment of the absurdity symbol ⊥; one can work with any fixed formula N as if it were ⊥.

HA ω+ has explicit rules for dealing with the existential quantifier (disjunction has not been included for the sake of simplicity). This, together with the special Shift rule, justifies the plus superscript + the name. The rule Shift is a general form of the more usual double-negation elimination rule, restricted to Σ 2 -formulas, that is precisely suitable for a simple proof of the Soundness Theorem. It has previously been used by Nakata and the author in a semi-classical logic context [START_REF] Ilik | Delimited control operators prove double-negation shift[END_REF][START_REF] Ilik | A direct version of Veldman's proof of open induction on Cantor space via delimited control operators[END_REF].

The class of Σ 2 -formulas consists of formulas S of the following form,

S ::= N | ∃x N N | N → S | N ∧ S | S ∧ N,
where N stands for so called computationally irrelevant formulas [START_REF] Seisenberger | Program from proofs using classical dependent choice[END_REF], defined inductively by

N ::= P | N ∧ N | N ∨ N | ∀x τ N | A → N
, where P stands for prime formulas (predicates) and A has no restrictions on the form. As our interpretation we will use a version of Kreisel's so called modified realizability interpretation [START_REF] Troelstra | Metamathematical Investigations of Intuitionistic Arithmetic and Analysis[END_REF][START_REF] Kohlenbach | Applied Proof Theory: Proof Interpretations and Their Use in Mathematics[END_REF], optimised similarly to the work of Berger, Buchholz, Schwichtenberg, and Seisenberger [START_REF] Berger | Refined program extraction from classical proofs[END_REF][START_REF] Seisenberger | Program from proofs using classical dependent choice[END_REF]. However, the key addition is that the realizing terms will also be computed by normalized instances of the shift term. Note that Σ 2 -formulae are exactly those ones that are realized by a term of type N.

↓ r ⇑Γ = ↓ s ⇑Γ Refl Γ ⊢ r τ . = s τ Γ ⊢ A(r) Γ ⊢ r . = s Comp Γ ⊢ A(s) Γ ⊢ (succ r) . = zero Cont Γ ⊢ ⊥ Γ ⊢ ⊥ Efq Γ ⊢ A
Our main result is the following one.

Soundness Theorem. If HA ω+ +AC proves C 1 , C 2 , . . . , C n ⊢ A, and A is computationally relevant, then there exists a term p of System T + such that HA ω+ alone proves that, for every ρ :

|C 1 |, |C 2 |, . . . , |C n | |C 1 |, |C 2 |, . . . , |C n |, ↓ hyp ρ mr C 1 , ↓ wkn hyp ρ mr C 2 , . . . , ↓ wkn n hyp ρ mr C n ⊢ ↓ p ρ mr A.
Proof. The proof is by induction on the derivation of C 1 , C 2 , . . . , C n ⊢ A and provides the same realizing terms as Kreisel's modified realizability interpretation of HA ω +AC. The additional rule of Shift (treated in more detail below) is realized via the shift term of System T + , nevertheless normalized to System T using ↓ • .

We will denote by p realizing terms provided by the induction hypothesis for each proof rule. If there are two induction hypotheses, the term corresponding to the second, right premise of the proof rule will be denoted by q.

As a general guide, the elimination rules are enough to prove their own soundness, while the introduction rules and the rules AC, Wkn, Ind, and Shift also need to use the definitional equalities of Proposition 1.

In general, the axiom AC στ is realized by the term lam pair(lam app(fst wkn hyp, hyp), lam app(snd wkn hyp, hyp)).

When the formula A(x, y) is computationally irrelevant, the realizer is the term lam hyp. The proof in both cases is a trivial intuitionistic implication and does not require AC στ itself. Equations ( 1)-( 5) of Proposition 1 are nevertheless used.

Ax is realized by hyp.

Wkn is realized by wkn p and verified using equation ( 1) and ( 2). The general case of → I , when A from A → B is computationally relevant, is realized by lam p and verified using equations ( 5), [START_REF] Berger | Refined program extraction from classical proofs[END_REF], and (1). The induction hypothesis needs to be used with the context ρ := ( x ρ , ρ), where x comes from the unfolding of the mr-definition for implication. The special case, when A is computationally irrelevant, is rather realized by the term p only.

When A from A → B is computationally relevant, the case → E is realized by app(p, q). When A is irrelevant, the realizing term is just p.

∧ 1 E is realized using fst p, in general, while in the case where one of the conjuncts of A ∧ B is irrelevant, the realizer is just p.

∧ 2 E is realized using snd p, in general, while in the case where one of the conjuncts of A ∧ B is irrelevant, the realizer is just p.

In general, ∧ I is realized using pair(p, q) and verified via equations ( 3) and (4). When A from A ∧ B is irrelevant, the realizer is q, while when B is irrelevant, the realizer is p.

In general, ∃ I is realized by pair(p, q) and verified via equations ( 3) and (4). When A(x) from ∃xA(x) is computationally irrelevant, then the realizer is r, the witnessing term.

∃ E is realized by app(app(q, fst p), snd p), in general. When A(x) from ∃xA(x) is computationally irrelevant, then the realizer is app(q, p).

∀ I is realized by lam p. For verification, it is necessary to apply equation ( 5) and to use the induction hypothesis with context ρ := ( x ρ , ρ).

∀ E is realized by app(p, r).

Ind is realized by lam rec(hyp, p, q) and using equations ( 6) and [START_REF] Danvy | Abstracting control[END_REF].

Shift is realized by shift p (normalized to System T using ↓ -). The goal is to prove ↓ hyp ρ mr C 1 , . . . , ↓ wkn n hyp ρ mr C n ⊢ ↓ shift p ρ mr A(r).

Using equation [START_REF] Gabbay | Applications of trees to intermediate logics[END_REF], we obtain φ and the goal becomes ↓ hyp ρ mr C 1 , . . . , ↓ wkn n hyp ρ mr C n ⊢ ↓ p φ,ρ mr A(r).

We can now use the induction hypothesis with ρ := (φ, ρ), ↓ hyp φ,ρ mr ∀x N (A(x) → S(x)), ↓ wkn hyp φ,ρ mr C 1 , . . . , ↓ wkn n+1 hyp φ,ρ mr C n ⊢ ↓ p φ,ρ mr S(r).

Thanks to equation ( 1), the induction hypothesis becomes ↓ hyp φ,ρ mr ∀x N (A(x) → S(x)), ↓ hyp ρ mr C 1 , . . . , ↓ wkn n hyp ρ mr C n ⊢ ↓ p φ,ρ mr S(r).

Finally, thanks to equation ( 9), we can finish the proof by applying the Shift rule for:

S ′ (x, y) := ↓ y φ,ρ mr S(x) A ′ (x, y) := ↓ y φ,ρ mr A(x).
Remark 1. The Shift case in the proof of the Soundness Theorem only uses the case where shift is reified at type N. This use does not exhaust the possibilities of the realizability model. For example, one can prove the soundness of the Shift rule for A = A 1 ∧ A 2 or A = ∃z N A 2 (z), when A i ∈ Σ 2 , by using the equations

↓ τ * σ p ρ = pair(↓ τ fst p ρ , ↓ σ snd p ρ ) ↓ N * σ fst shift p ρ = ↓ N p φ1,ρ ↓ τ * N snd shift p ρ = ↓ N p φ2,ρ ↓ N app(app(hyp, x), y) φ1,ρ = ↓ N fst y φ1,ρ ↓ N app(app(hyp, x), y) φ2,ρ = ↓ N snd y φ2,ρ where x : N → N * N → N; γ ⊢ N y : N → N * N → N; γ ⊢ N * N φ 1 := η(≥ 2 ν → η(≥ 3 α → η(α ≥ refl (≥ 4 γ → (proj 1 γ))))) φ 2 := η(≥ 2 ν → η(≥ 3 α → η(α ≥ refl (≥ 4 γ → (proj 2 γ))))).
The induction hypothesis needs to be used twice, once for φ 1 and once for φ 2 .

Similar equations hold for function types:

γ ↓ N app(shift p, z) ρ = N→(N→N)→N;γ ↓ N p φ3,ρ φ 3 := η(≥ 2 ν → η(≥ 3 α → η(α ≥ refl (≥ 4 γ → µ(γ ≥ refl z ⌈ ⌈ρ⌉ ⌉ ≥ 4 •≥ 3 •≥ 2 )))))
Nevertheless, it does not appear to be possible to prove the soundness of the Shift rule even for the case |A| = N → N in general, since it is well known that there are already classically true Σ 0 3 -formulas which do not have a recursive realizer.

Still, it may be the case that the realizability model can be used to give a sound computational interpretation of particular Σ 0 3 (or more complex) formulas. Corollary 1. The Σ 2 -fragment of classical Analysis satisfies the Existence Property, Given a derivation of Γ ⊢ ∃x τ A(x), there exists a term p of type τ of System T such that Γ ⊢ A(p). and, consequently, the Weak Church's Rule, Given a (closed) derivation of ∅ ⊢ ∀x N ∃y N A(x, y), there exists a total recursive function f : N → N such that, for all n ∈ N, we have that ∅ ⊢ A(n, fn), where m denotes the term succ • • • succ m times zero.

Proof. The proof method is not new (see Corollary 5.24 of [START_REF] Kohlenbach | Applied Proof Theory: Proof Interpretations and Their Use in Mathematics[END_REF] and paragraph 1.11.7 of [START_REF] Troelstra | Metamathematical Investigations of Intuitionistic Arithmetic and Analysis[END_REF]). If the formula A is of the class Γ 1 [START_REF] Troelstra | Metamathematical Investigations of Intuitionistic Arithmetic and Analysis[END_REF][START_REF] Kohlenbach | Applied Proof Theory: Proof Interpretations and Their Use in Mathematics[END_REF],

Γ 1 ∋ G ::= N | G ∧ G | ∀xG | ∃xG | S → G,
(where S is a Σ 2 -formula and N is computationally irrelevant) then already intuitionistic logic shows that ⊢ (p mr A) → A. If A is outside this class, one first needs to define the "with truth" variant of modified realizability in which one replaces the clause for implication of mr-interpretation of Definition 1 by

p mrt A → B := ∀x([↓ x ρ mrt A] → [↓ app(p, x) ρ mrt B]) ∧ (A → B).
The Soundness Theorem is provable for mrt with the same realizing terms, but now we also have, for any formula A, (p mrt A) → A. This directly implies the Existence Property.

For the special case when Γ = ∅ and τ = N, we get the Numerical Existence Property:

Given a (closed) derivation of ∅ ⊢ ∃y N A(y), there exists n : N such that ∅ ⊢ A(n). This follows from the fact that a closed derivation has a realizer that is a closed term (does not have non-bound hyp subterms). Since the realizer is necessarily in normal form, and since it is not neutral (all neutral terms have at least one non-bound occurrence of hyp), then the realizer must be of the required form succ • • • succ n times zero.

To show the Weak Church's Rule, we use elementary Recursion Theory. Like all theories over countable languages, HA ω+ +AC is recursively axiomatizable, that is, there exists a recursive predicate Proof(k, l) formalizing the fact that k ∈ N is a code for a derivation of the formula coded by l ∈ N.

Let g(n) = min m Proof(j 1 m, A(n, j 2 m) ), where j 1 and j 2 are the projections of some surjective pairing function. As defined, g is a partial recursive function. Now, given ∅ ⊢ ∀x N ∃y N A(x, y) and n ∈ N, we obtain ∅ ⊢ ∃y N A(n, y), and by the Numerical Existence Property we obtain m ∈ N such that ⊢ A(n, m). We proved that, for every n, there exists m such that ∅ ⊢ A(n, m) which shows that the function g is total recursive. We may now take f (n) := j 2 (g(n)) and by definition we have that, for any n, ∅ ⊢ A(n, f (n)).

Note that the class Σ 2 includes the following schemata, (MP)

¬ N ¬ N ∃x τ M (x) → ∃x τ M (x), (DNS) ∀x N ¬ N ¬ N A(x) → ¬ N ¬ N ∀x N A(x),
where M, N denote computationally irrelevant formulas and ¬ N A denotes negation in minimal logic, that is A → N for a fixed N . The Existence Property implies that principles like MP and DNS can justly be considered as constructive even in presence of induction and the full Axiom of Choice, partly extending previous works [START_REF] Troelstra | Metamathematical Investigations of Intuitionistic Arithmetic and Analysis[END_REF][START_REF] Gabbay | Applications of trees to intermediate logics[END_REF][START_REF] Seldin | On the proof theory of the intermediate logic MH[END_REF][START_REF] Herbelin | An intuitionistic logic that proves Markov's principle[END_REF][START_REF] Ilik | Delimited control operators prove double-negation shift[END_REF]. Similar conclusions follow from the work of Rand Moschovakis that uses a version of Kleene's generalrecursive realizability [START_REF] Rand | Analyzing realizability by Troelstra's methods[END_REF].

Weak Church's Rule seems to justify why, even constructively, CT 0 deserves the name "the false Church's Thesis" [START_REF] Lombardi | Algèbre commutative -Méthodes constructives[END_REF].

  the Ackermann function of type N → N → N in lambda calculus notation, A := λm. R m(λn.n + 1)(λm ′ .λu.λn. R n(u1)(λn ′ .λw.uw)), where R is a constant such that R 0ab = a R(n + 1)ab = bn(R nab), is defined using the following term: lam (rec hyp(lam(succ hyp)) hyp(app(wkn hyp)(succ zero))(lam(lam(app(wkn(wkn(wkn hyp))) hyp)))))))).

  Proof of Normalization Theorem. Our goal is to define an evaluation function, (-) : γ ⊢ σ ⇒ γ σ that maps a term p of type γ ⊢ σ to a forcing 1 set γ σ, together with a reification function, ↓ (-) : γ σ ⇒ γ ⊢ r σ, that extracts normal forms (without shift!) from the forcing set. Composing the two function, p → ↓ p , gives a normalization procedure. (The notation a b c → d will be a compact form of a → b → c → d.)

Figure 2 :

 2 Figure 2: Additional rules for equality (computationally irrelevant)

Definition 1 .

 1 Given a context Γ and an interpretation of hypotheses ρ : |Γ| |Γ|, the modified realizability interpretation "p mr A" of a formula A by a term p of type |Γ| ⊢ r |A| of System T is defined by the following formula translation, p mr N := N (for any term p of type N) p mr N ∧ B := N ∧ (p mr B) p mr A ∧ N := (p mr A) ∧ N p mr A ∧ B := (↓ fst p ρ mr A) ∧ (↓ snd p ρ mr B) p mr N → B := N → (p mr B) p mr A → B := ∀x([↓ x ρ mr A] → [↓ app(p, x) ρ mr B]) p mr ∀x τ A(x) := ∀x τ (↓ app(p, x) ρ mr A(x)) p mr ∃x τ N (x) := N (p) p mr ∃x τ A(x) := ↓ snd p ρ mr A(↓ fst p ρ ), in which N denotes a computationally irrelevant formula, and where the type |A| of the realizing term p is computed as follows: |N | := N |N ∧ B| := |B| |A ∧ N | := |A| |A ∧ B| := |A| * |B| |N → B| := |B| |A → B| := |A| → |B| |∀x τ A| := τ → |A| |∃x τ N | := τ |∃x τ A| := τ * |A| The map | • | is extended to contexts Γ by |C 1 , . . . , C n | := |C 1 |; • • • ; |C n |.

The terminology "forcing" comes from similarity of our construction with Kripke models which does not intentionally refer to the forcing from Set Theory.

DANKO ILIK Ax A, Γ ⊢ A Γ ⊢ A Wkn B, Γ ⊢ A A, Γ ⊢ B →I Γ ⊢ A → B Γ ⊢ A → B Γ ⊢ A →E Γ ⊢ B Γ ⊢ A ∧ B ∧ 1 E Γ ⊢ A Γ ⊢ A ∧ B ∧ 2 E Γ ⊢ B Γ ⊢ A Γ ⊢ B ∧I Γ ⊢ A ∧ B Γ ⊢ A(r τ ) ∃I Γ ⊢ ∃x τ A(x) Γ ⊢ ∃x τ A(x) Γ ⊢ ∀x τ (A(x) → B) x ∈ FV(B) ∃E Γ ⊢ B Γ ⊢ A(x τ ) x ∈ FV(Γ) ∀I Γ ⊢ ∀x τ A(x) Γ ⊢ ∀x τ A(x) ∀E Γ ⊢ A(r τ ) Γ ⊢ A(zero) Γ ⊢ ∀x N (A(x) → A(succ x))Ind

Acknowledgments

This work was funded by Kurt Gödel Research Prize Fellowship 2011 and ERC Advanced Grant ProofCert. I would also like to thank Martín Escardó, Jaime Gaspar, Keiko and Dirk Pattinson for comments on an earlier version of this paper, and Dale Miller for providing scientific liberty.


We consider demand response solutions having the capability to monitor different variables at users' premises, like presence and temperature, and to control individual appliances. We focus on the optimal control of the appliances during time periods where the available capacity is not enough to satisfy the demand generated by houses operating freely. We propose an approach to define the utility of appliances as a function of monitored variables, as well as control schemes to optimize this utility. Global optimums can be reached when a centralized entity (i.e., an aggregator) can gather information from each user and control each individual appliance. This may not be always possible, for example for privacy and/or scalability reasons. We therefore consider, in addition, a system where decisions are taken partially at a centralized site (global power allocation per home) and partially at customer premises (sharing of the allocated power among local appliances). Performances of proposed control mechanisms are evaluated and compared. We show the potential value of introducing demand response mechanisms at fine granularity.

Advanced demand response solutions based on fine-grained load control Rim Kaddah * ,Daniel Kofman * and Michal Pioro † ‡

I. INTRODUCTION

Present trends in the eco-system of electricity operators, like the growing penetration of renewable intermittent energy sources and the increasing number of end-users playing active roles, have increased the requirement for advanced demand response solutions.

The Internet of Things paradigm and its specific implementations -for example in smart houses and smart buildings -enable new service models for electricity operators as well as innovative demand response approaches. This general idea is gaining momentum, as it is attested by the recent acquisition of Nest by Google (and by the related business models established with electricity operators).

In the present paper we introduce an approach for implementing advanced demand response solutions at a potentially broad geographical scope that: i) can work at the level of users' appliances, ii) can take into consideration data monitored at user premises, like presence and temperature and iii) based on this information, optimizes the total provided utility (e.g. at a neighborhood scale) under fairness constraints. Definitions of "utility" and "fairness" for this specific context are provided in the paper, as well as the way to model them.

In [START_REF] Kofman | New service models for electricity distribution during energy crises[END_REF] the authors have introduced a family of new service models for the provision of electricity, in particular to face *This author has carried out the work presented in this paper at LINCS (www.lincs.fr) periods of time during which it is not possible to cope with all the demand, either because of technical or economic reasons. The proposed service models allow significantly limiting the impact on quality of experience during such time periods by avoiding coarse-grained control mechanisms (like rolling blackouts) or high costs. Based on the general architecture proposed in the document, available power can be distributed in a smarter way, at a fine granularity, taking into consideration the relevance of each appliance for the end-users. In particular, the proposed architecture leverages the capabilities of the Internet of Things paradigm. The mechanisms we propose in the present paper can be embedded on this general framework as an implementation of one of its key building blocks, but their scope of application is much broader.

The methodology proposed in this paper is motivated as follows. In case of scarcity of resources, the general target is to minimize the impact on quality of experience. In order to translate this general statement into autonomous taken decisions leading to optimal power allocation and appliances control, we need first to model the utility, from the end user point of view, of receiving a certain amount of power. Therefore, in this paper we first provide a typology of appliances and define their utility as a function of different relevant variables (like ambient temperature for the control of a heating system). We also model the evolution of these variables as a function of the provided power in order to be able to represent how the decisions taken at a given time will impact the user perceived utility in the future.

Based on the proposed model of utility and on the dynamics of the system variables (e.g. evolution of temperature as a function of the power provided to the heating system), we propose different approaches for allocating power to the various appliances of the different clients of a given geographical zone characterized by the electric network infrastructure. We consider control systems that work at different granularities, ranging from power allocation to individual appliances to total power allocation to end-users. We also consider ahead of time and real-time approaches. Supposing time is slotted, we call ahead of time those approaches where the decisions are taken at the beginning of a time period for its whole duration. We call real time approaches those where for a given time period, control decisions are taken at each time slot without knowledge of how exogenous variables (like total available capacity) will evolve in future time slots.

For specific use cases, we optimize the control system for the various proposed control approaches and compare the results. We show the potential high impact of the presented solution.

The paper is organized as follows: Section II presents related work. Section III introduces the problem and presents the general framework as well as the taxonomy of appliances, utility definitions and control schemes we propose. In Section IV, we instantiate a specific system and propose a model that allow us, for this specific system, to evaluate and compare the performances of the various control schemes we propose. In Section V, we present a numerical analysis of the model which outcomes provide insight on the behavior of the proposed control schemes. Conclusions and future work are presented in Section VI.

II. RELATED WORK

The topic of Demand Response has motivated a large set of contributions during the last years. Demand Response approaches can be grouped in two categories: pricing based and direct load control. The approaches in the first category try to induce the expected users' behavior through dynamic pricing incentives and provide no strict guaranties on the outcome. On this group we can cite [START_REF] Li | Optimal demand response based on utility maximization in power networks[END_REF], [START_REF] Gatsis | Cooperative multi-residence demand response scheduling[END_REF], [START_REF] Joe-Wong | Optimized day-ahead pricing for smart grids with device-specific scheduling flexibility[END_REF], [START_REF] Mohsenian-Rad | Autonomous demand-side management based on game-theoretic energy consumption scheduling for the future smart grid[END_REF]). In [START_REF] Li | Optimal demand response based on utility maximization in power networks[END_REF], the authors propose a taxonomy of appliances and a pricing scheme that takes into account utility functions of the appliances being served. In the present paper we propose a different taxonomy of services that we consider better adapted for the definition of utility functions, as explained in Section III-D. In particular, it enables taking into account in a simple way the criticality of a given appliance as seen by a given user. We also propose a related general approach for defining utility functions.

The approaches in the second category, in which we are interested, enables Distribution System Operator (DSO) or aggregators to directly control the load. Load can be controlled at different granularities, e.g. per user or per appliance. Previous works on direct per appliance load control focus on specific types of appliances. For instance, the authors in [START_REF] Bapat | User-sensitive scheduling of home appliances[END_REF] consider the control of shiftable loads. In [START_REF] Srikantha | An analysis of peak demand reductions due to elasticity of domestic appliances[END_REF], [START_REF] Srikantha | Distributed control for reducing carbon footprint in the residential sector[END_REF], the authors show the high value of exploiting the capability to reduce power allocated to elastic appliances. This last paper focuses on peaks reductions whereas we focus on complying with the available total capacity. A wide range of work focused on Thermostatically Controlled Loads (TLCs) ( [START_REF] Molderink | Management and control of domestic smart grid technology[END_REF], [START_REF] Mathieu | Energy arbitrage with thermostatically controlled loads[END_REF], [START_REF] Nayyar | Aggregate flexibility of a collection of loads π[END_REF], [START_REF] Sanandaji | Improved battery models of an aggregation of thermostatically controlled loads for frequency regulation[END_REF], [START_REF] Karmakar | Coordinated scheduling of thermostatically controlled realtime systems under peak power constraint[END_REF]). The approach presented in this paper is generic, and applies to any control granularity and any type of appliances.

To our knowledge, no generic framework was proposed that allows joint control of different types of appliances in case of direct load control involving an aggregation of homes. In this work, we choose to use utility functions to model the flexibility (e.g., shifting capabilities, payback effect) and relevance for the users of all types of controlled appliances. Utility functions were previously used in the literature to measure social welfare when designing pricing schemes and are generally considered as (convex) functions of power (e.g., [START_REF] Samadi | Optimal real-time pricing algorithm based on utility maximization for smart grid[END_REF]). Our approach is similar to [START_REF] Li | Optimal demand response based on utility maximization in power networks[END_REF] but more general: utility is represented as a function of several relevant variables (endogenous and exogenous to clients' environment), which in particular enable evaluating the impact on quality of experience of the allocated power, and we differentiate appliance usage from its operation constraints.

In [START_REF] Agnetis | Optimization models for consumer flexibility aggregation in smart grids: The address approach[END_REF] the authors focus on how aggregators can leverage in the energy market the flexibility that can be provided by clusters of users. For this and other contributions that have been published on the topic, our proposals enable increasing the available aggregated flexibility.

III. PROBLEM STATEMENT AND PROPOSED SOLUTIONS

A. Problem statement

Power grids are evolving fast but are still lacking mechanisms for fine-grained control of power allocation. In this paper we consider advanced frameworks, like the one presented in [START_REF] Kofman | New service models for electricity distribution during energy crises[END_REF], which enable controlling the demand at different granularities, including at a per appliance level, during periods of generation shortage.

We consider two functional groups in charge of demand control, one located at a Distribution System Operator (DSO) or aggregator site and the other one at user premises. The design of the demand-response mechanisms implemented through these two functional groups targets energy efficiency as well as satisfying users' expectations. Complexity arises because, on the one side, those two global objectives could be contradictory and, on the other hand, theoretic optimal solutions may not be feasible (e.g. for scalability reasons) and several non-technical factors have to be considered (e.g. privacy issues may constrain the data that can be made available to the DSO or aggregator).

We can summarize our problem statement as follows: Under the hypotheses that an advanced architecture enabling demand control at fine granularity is deployed and that a set of variables are monitored at user premises, we search demand control mechanisms for energy efficiency and users' satisfaction under different constraints of scalability and of the users' data dissemination scope.

B. Solutions framework

We focus on time periods where the global demand exceeds the available capacity. We call DE a and DE u the functional groups at the DSO/aggregator side and at the user side, respectively. DE u is aware of the state of the variables monitored at user premises and receives control decisions from DE a . When relevant to a specific control case, DE u can transmit all or part of the data he gathered to DE a . We consider different demand control approaches. They can be classified in two families. In the first family, DE a decisions are taken at the granularity of users, without any knowledge on individual appliances nor on the state of monitored variables. At each decision time, it allocates to each user a maximum power (which could be different for different users) for a certain time period. Based on this limit, DE u controls the demand of each appliance. In the second family, DE a has full information and directly controls the appliances. In order to quantify energy efficiency and users satisfaction, we define for each appliance a utility function. The utility may depend on the monitored variables (like presence or temperature) and on exogenous variables (like outside temperature).

The models we introduce in the following section target maximizing the total utility under different types of system constraints and taking into account fairness considerations. We do not directly focus on the revenues of the players. Nevertheless, one can expect that if well performing pricing models are defined, reaching maximum users' utility leads to maximum gains.

C. Proposed control schemes

In the following, we propose different control schemes and we compare their performances. The choice of a scheme will depend as well on the different service models and corresponding tariff schemes that can be associated to them.

1) Global Maximum Utility:

The Maximum Utility scheme supposes DE a has full information and decides how much power to allocate to each appliance in order to maximize the total utility, means the sum of the utilities of each appliance of each user. We call this scheme M U

2) Global Maximum Utility under fairness constraints:

This scheme, that we name F M U , also supposes that DE a has full information. It maximizes the total utility in a restricted domain where the minimum of the utilities of all users is maximized (see Section IV-B for a formal definition). We consider this scheme in order to introduce fairness. In fact we assume here a specific fairness definition1 , which seems in particular appropriate for the case of homogeneous users (homes with similar characteristics). For the case of heterogeneous users, depending on different considerations that we will not treat here, it can be argued that a scheme where max-min is applied to the utility divided by the number of inhabitants (or square meters) would be fairer.

3) Local maximum utility under homogeneous capacity constraints:

In this scheme, users are grouped into classes. Each class receives a certain amount of power based on a parameter that is associated to the class at the configuration time of the system (for example, the allocation may be a function of the maximum power authorized for the users of the class in nominal conditions). At each decision time, DE a allocates to each user the power allocated its class divided by the number of users in the class and transmits the corresponding information to each DE u that, based on this limi, takes control decisions in order to maximize local utility. We name this scheme LM H.

4) Rolling Black-Outs:

In this scheme, the power allocated to each user by DE a is either the maximum subscribed power or zero. We analyze a simple approach to introduce fairness in power allocation, which will be explained in the section devoted to presenting the optimization models. As in the previous schemes, each DE u controls the appliances in order to maximize local utility and to respect the allocated power. We call this scheme RB.

5) Decisions time:

The DSO or aggregator may be able to forecast the starting time and duration of a starvation time period (e.g. predicted extreme weather conditions). In this case, the power allocation may be done at the beginning of the time period for its whole duration. In other cases, starvation periods are not known a priori. Moreover, optimizing the system for the whole period under the studied constraints that take into account the dynamics of different variables (like the temperature in the house) may not be scalable in certain contexts.

Therefore, we analyze and compare the 2 first abovepresented schemes both in the cases of ahead of time and real-time optimization.

D. Appliances' Taxonomy and Utility Functions

In this section, we first present a taxonomy of appliances from which one can derive the type of control that can be applied to each given appliance (its flexibility). The taxonomy also provides the rationale for the utility functions we propose afterward.

1) Taxonomy :

We consider that, for the purpose of modeling demand control mechanisms and users satisfaction, appliances should be classified based on the 3 following criteria.

a) Criterion 1 -Usage:

We propose grouping appliances based on 3 general types of usage:

• Interactive demands

Interactive demands are those that are directly triggered by end users and, when possible, should be served immediatly. Obviously, the utility of those appliances depends directly on the presence of inhabitants. Lighting and TV are typical examples of interactive loads.

• Background loads

Background loads are those in charge of controlling value of variables like the temperature in a room, in the water-heater or inside the fridge. They are usually shiftable, which means that shifting (up to a certain limit) the time at which the expected energy is provided do not significantly affect the quality of experience. They may depend on presence but also on exogeneous variables (e.g. related with the weather). The value of feeding such loads depends on the distance between the targeted and present values of the variables being controlled and also on the dynamics of the variable (how the variables evolve in time as a function of the power provided to the appliance). Subclasses can be defined depending on the level of inertia of the controlled variables. For example, a heating system has more inertia than an air-conditioning cooling system.

• Program based loads

Program based loads are those that have well defined cycles that can be programmed. The value of feeding these appliances is related with the capacity of completing a program. They are usually shiftable, but in most cases they are not elastic. They can be classified on those than can be stopped before of the end of the cycle and those for witch such an event may generate some damage. Typical examples of this category are washing machines and charging systems for electric vehicles. The quality of experience depends, in particular, in the distance between the expected and actual start time and termination time of an operation cycle, as well as on the level of respect of the constraints on acceptable interruptions and on the total provided service (e.g. charging) during the cycle.

b) Criterion 2 -Criticality and preferences: Appliances can be differentiated by their criticality. We can define three levels of criticality namely, "Critical", "Basic" and "Others". The first category comprises demands that have to be accommodated under any circumstances (e.g., home medical equipment that have to operate when needed). Basic demands are generated to accommodate important needs that will significantly affect users' well-being. (e.g., a certain level of lighting, space heating during especially cold weather). Demands that fall into the "Others" category are those that can be abandoned without significantly affecting home residents' well being (e.g. entertainment). Moreover, may provide a priority ordering of loads depending on their own perception of the importance of the appliances.

c) Criterion 3 -Electrical characteristics and power flexibility:

This category describes electrical characteristics of loads (e.g., resistive, inductive, storage) that may impose operation constraints. For resistive loads, reducing power will affect the quality of experience but not avoid functioning. In many cases resistive loads are elastic and therefore reducing allocated power will just delay the provision of the service (for example, a water-heater will take longer time to reach the desired water temperature). Inductive loads are usually less flexible.

2) Utility Functions : As mentioned, the general approach we propose relies on the definition of utility functions. Based on the presented taxonomy, we propose a 3 steps methodology to derive utility functions and adequate control decisions for any type of appliances.

1) Define normalized utility functions for the different types of usages (Criterion 1). The following are just examples of functions that could be used. Since for interactive loads utility depends directly on power allocated and the presence of inhabitants, it can be defined as an increasing in power and piecewise linear function with slopes that decrease since the marginal utility decreases after having satisfied a group of houses needs. For background loads, utility is dependent on the value of some controlled variables; it can therefore be defined as a monotone piecewise linear function in these variables with different slopes between minimum, preferred and maximum tolerable thresholds of the controlled variables. Since for Program based loads, utility is related with the completion of a program, it can be expressed as a function of total required energy to complete a program and of the distribution in time of this energy in order to evaluate the amount of shift. Dependence to presence of inhabitants can be expressed by a multiplying factor. This factor can linear with the expected value of inhabitants or sublinear as usually the 1st inhabitant trigger requirements that are shared by additional inhabitants. 2) Take into account the level of importance (Criterion 2) by multiplying the normalized function by a factor that indicates the level of criticality as perceived by the user. This provides the flexibility for the utility of the same appliance being different for different users. 3) Based on Criterion 3, identify the type of control that can be applied, which has also to consider issues introduced in Criterion 1, like shiftability and tolerance to interruptions.

We now define the utility functions for the specific appliances we use in the rest of the paper. These definitions should be considered in this section just as two examples of possible utility functions defined through the general approach introduced above. We consider two appliances: Lighting system and Heater system. a) Lighting System: A lighting system is an interactive load for which power drawn depends on the number of bulbs powered on and on the power they consume. To model the utility of a lighting system, we first define the minimum, acceptable and maximum required power.

• The minimum power is chosen as the power required by the bulb at home that consumes the less.

• We suppose an acceptable required power of 1.6W/m 2 multiplied by the size of the home (or the sum of the sizes of the N largest rooms in the home, where N is the number of present residents).

For the present paper, we do not consider the daylight factor; in other words, we consider a day where natural sunlight is not enough.

• The maximum required power is given by the sum of the power required by all bulbs in the home. Figure 1 presents our model, where we denote by U 1 ht the normalized utility of the lighting system at home h at time t, π(h, t) the expected value of the number of people present at home h at time t divided by the maximum number residents, P 1 max (h) the maximum required power, α a coefficient that takes value in [0,1], P 1 min (h) the minimum required power, P 1 acc (h) the acceptable required power and X 1 ht the power allocated by the control system to the lighting system of home h at time t.

b) Heater System: A heater system is a background load for which we consider that power drawn can be reduced from its nominal value P max (h) to a minimal value P min (h). The utility derived from the usage of this appliance depends on the temperature indoor, that we denote by Y 2 ht , and on users presence or probability of presence, that we denote by π(h, t) (see figure 2). Temperature evolution dynamics are modeled by the following equation:

Y 2 ht = Y 2 h(t-1) + A(h)X 2 ht + B(h)(T 0 (t) -Y 2 h(t-1) ) where Y 2
ht is the temperature in home h at time t, A(h) and B(h) are coefficients for heating and insulation in home h and T 0 (t) is the exterior temperature at time t.

IV. STUDIED SYSTEM AND CORRESPONDING MODEL

In this section we first introduce the specific system we study by making some assumptions on the general system proposed in Section III-B. Then, we present the model we define for this specific system in order evaluate and compare the performances of the different control approaches introduced in Section III-C.

A. System Assumptions

We focus on the functional groups introduced in Section III-B and we make the following assumptions:

• The system has no storage capabilities (neither at DSO/aggregator infrastructure nor at user premises).

• Power losses introduced by the distribution network are considered similar for all the users and hence the location of a user doesn't affect the decisions related to his power share.

• The decision element DE a knows the available generation capacity as a function of time.

• Only non critical loads are considered; capacity is supposed to be large enough to accommodate all critical demands. Available capacity therefore denotes remaining capacity after power has been allocated to all critical loads.

• Required exogenous information is known (either only by DE u or by both DE u and DE a depending on the analyzed control scheme).

• The state of the appliances that are part of the system, their electric characteristics and the values of relevant variables (e.g. temperature at a home) at the beginning of the crisis are known (either only by DE u or by both DE u and DE a depending on the analyzed control scheme).

• For the control schemes where DE a works at a user granularity, DE a is configured with the set of maximum power level each user has subscribed to.

• Time is slotted and the power consumed by an appliance is supposed to be constant in a time slot.

Technologies for deploying autonomic capabilities for DE u to self-discover part of the required data are today mature.

B. Model

The target of the system is to offer the highest possible quality of experience while complying with system capacity constraints C(t) for all time instants t.

Next, we present a set of optimization problems that expresses the previous sentence and the system constraints in a formal language for each of the control schemes we have introduced. We denote by T the duration of the starvation period in number of time slots, by H the number of homes and by A the number of appliances per home. Table I

max X a ht ,x a ht T t=1 H h=1 A a=1 U a ht (1a) s.t. H h=1 A a=1 X a ht ≤ C(t), ∀ t (1b) p a (h)x a ht ≤ X a ht ≤ P a (h)x a ht , ∀ t, ∀ h, ∀ a (1c) x a ht binary (1d)
Through the binary variable x a ht (see Table 1), Equation (1c) indicates that the power assigned to appliance a is either 0, either bounded between minimum and maximum. This excludes allocating a positive amount of power lower the the minimum; indeed, for some appliances, receiving less than the minimum possible power not only provides no utility but also can create some damage.

Please remark that the utility functions may depend on the dynamics of different variables, as introduced in Section III-D2), and therefore power allocations at one time slot will impact the utility in future time slots. d) Global Maximum Utility, real time: Although the decisions are taken here per time slot, the dynamics of the system are still considered. For example, we don't suppose an independent temperature measure at each time slot but temperature is calculated based on the modeled temperature dynamics, exogeneous variables and previously taken decisions. This enables to compare the performances of this scheme with those of the previous one. Indeed, although designed for usage in real-time, this scheme can also be used ahead of time, as it reduces the computation time and therefore increases scalability compared with the previous one (of course, such approach will lead to poorer performances). The constraints are the same as in the previous case and we have now T problems to solve consecutively:

max H h=1 A a=1 U a ht f or t = 1..T (2)
e) Global Maximum Utility under fairness constraints: We present the ahead of time case; from which it is trivial to derive the real-time one.

The following problem computes the domain of the variables where the minimum of the users utility is maximized.

max X a ht ,x a ht U (3a) s.t. T t=1 A a=1 U a ht ≥ U, ∀ h (3b) H h=1 A a=1 X a ht ≤ C(t), ∀ t (3c) p a (h)x a ht ≤ X a ht ≤ P a (h)x a ht , ∀ t, ∀ h, ∀ a (3d) x a ht binary (3e)
Let's denote buy U M the solution of the previous problem. The following problem maximizes the global utility inside the domain computed by the previous one.

max X a ht ,x a ht T t=1 H h=1 A a=1 U a ht s.t. (4a) s.t. H h=1 A a=1 X a ht ≤ C(t), ∀ t (4b) p a (h)x a ht ≤ X a ht ≤ P a (h)x a ht , ∀ t, ∀ h, ∀ a (4c) T t=1 A a=1 U a ht ≥ U M , ∀ h (4d) x a ht binary (4e)
1) Local maximum utility under homogeneous capacity constraints: For this control scheme, the optimization problem is divided into 2 steps. First DE a decides the capacity to be allocated to each user and then, at each user, DE u decides the corresponding allocation per appliance by solving the M U problem with H = 1. DE a takes decisions based on the outcome of the following problem. For simplicity we present it for 2 levels of possible positive allocated capacities, but it is straight forward to generalize to M levels.

Lets denote by K the number of classes, by g k the number of houses in class k and by C 2 (k) the maximum power subscribed by users of class k. The power allocated to each home of class k by DE a equals C(t)C 2 (k) k g k .C 2 (k) . 2) Rolling Black-Outs: The only difference between this scheme and the previous one is the way DE a computes the power it allocates to users. In this scheme, houses are ordered randomly. DE a allocates to each house either 0 or the maximum subscribed power. During the first two hours, the first users in the list are served. Then the users are disconnected and the available power is provided for the next two hours to the next users in the list. DE a iterates this process and once all users are served, it starts again from the beginning of the list and continues until the end of the optimization period T .

V. NUMERICAL ANALYSIS

A. Analyzed System

In this section we fix several system parameters and exogenous variables and we focus on the behavior of the presented control schemes as a function of the available capacity.

• We select a slot duration of τ = 5 minutes

• We consider a starvation period of 15 hours, so T = 180 slots.

• We suppose that the total available power during the starvation period is constant, C(t) = C and we analyze the model for different values of C.

• H = 50 houses are considered for two cases: homogeneous and heterogeneous. For the heterogeneous case we suppose two classes of 25 houses each.

• We consider two types of appliances, A = 2, which are lighting (index a = 1) and heating (index a = 2). We use the corresponding utility functions defined in Section III-D2. For lighting, we consider a particular case where the utility function is linear between p 1 (P min ) and P 1 (P max ). The rest of the curve is unchanged.

• For all cases we suppose that the external and preferred temperatures are supposed constant and equal, respectively, T 0 (t) = 10 • C ∀t and T 2 (h) = 20 • C ∀h • We suppose that the expected value of the number of persons in the houses is constant during the whole studied period and we assume that both types of appliances are of equal importance for users. We therefore work with the normalized utility functions.

The numerical analysis of the various presented mixed integer linear problems has been carried out using ILOG CPLEX Interactive Optimizer. Additional constraints have been introduced to the optimization problems to make them tractable in terms of time, without impacting the results.

B. Numerical results

Since it is based on direct control and the largest set of data, scheme M U provides the maximum total utility over the optimization horizon. We therefore take it as the benchmark to compare all the schemes. Figure 3 shows the results for the homogeneous case with the following minimum and maximum accepted power for each appliance (in Watts): Lighting system [50, 1000], Heater system [1000, 4000].

Please observe that for facilitating the analysis we represent the total utility divided by the number of houses, which means that the absolute gain of the M U scheme compared with the others is 50 times larger than what is shown in the figures. Since utilities have been normalized per appliances (see Section III-D2), the maximum utility per slot equals 2 and therefore the total maximum utility per user equals 360. Performance is expressed by the average utility it provides to homes over the whole optimization period.

The extreme left and right points on the x-axis correspond to the power values at which, respectively, the total utility for the LM H scheme reaches zero and the total utility for the M U scheme reaches the maximum possible utility.

Only the points in the graphs have been computed, the lines have been drawn facilitate reading.

As expected, the gain of all schemes is important compared to the RB scheme, except under very hard crises when scheme LM H fails at providing any utility.

The gains for schemes M U and F M U are significant, at least at certain levels of starvation, which may justify introducing the complexity induced by fine-grained control.

Scheme LM H reaches the performances of Scheme M U for two specific values of the available capacity. The first one corresponds to the minimum power that can be allocated to the heating system of a given house (1000W). The fact that at this point, for Scheme LM H, all Heating Systems may be activated at certain times slots (even if not necessary at the same time slots) explains the rapid increase of the total utility at this specific total available capacity. The second one is trivial, it corresponds to the point where the capacity is enough to absorb the maximum possible demand.

The performances of Scheme LM H do not reach those of Scheme M U in all cases. As an example, we consider the Back to Figure 3, it is interesting to see that the real-time M U scheme significantly under performs scheme M U for most values of C. This is explained by the fact that, since the approach has no vision on the future, DE a doesn't allocate enough power to the Heating system (it doesn't predict the utility that can be generated in the future). Therefore, for low values of C, even when it can allocate power for the Heating system of some houses, it prefers to allocate the whole power to the Lighting system. On the contrary of the scheme LM H , the real-time M U scheme can provide power to the Heating systems of some houses for values of C smaller than 50000W, but as it has been designed, it decides not to do it. This shows that the real-time M U mechanism is not well designed and that additional intelligence is needed when a real-time approach is required.

Figure 3 shows that in the homogeneous case, for this particular configuration, introducing fairness do not affect the total utility (F M U and M U have the same performances). This is not always the case, as shown in Figure 4 for the heterogeneous case.

VI. CONCLUSION

We propose a general approach for demand response solutions based on the possibility of extending visibility and control to users' premises, and more precisely, having the capability to gather relevant information on existing appliances, to monitor relevant variables at users' premises and to control individual appliances. These capabilities enable DSOs and aggregators to evaluate the utility for end users of the allocated power. The possibility to take into consideration the evaluation of this utility enables new service and business models.

In order to leverage the above-listed capabilities, it is necessary to relate the targeted behavior of the controlled system with the services it provides. To cope with this requirement, we have proposed a taxonomy of appliances and a related approach for defining the utility of any king of appliances, as perceived by the users, as a function of the gathered information.

We propose and analyze a set of control schemes tending to maximize the total users utility under system technical and non-technical constraints (e.g. fairness constrains and constrains on data dissemination due to privacy issues). We consider ahead of time and real-time control schemes.

The analysis shows the high value of demand response mechanisms acting at fine granularity (e.g. per appliance visibility and control), specially when the period of power starvation is known ahead of time. We consider two cases in order to cover two different service models: in the first one a service provider takes control on the whole system (on individual appliances), in the second one, control is split in such a way that no sensitive data will be disclosed out of the houses and no control on local appliances will be delegated to an external entity. For both cases the proposed ahead of time mechanisms performances seems to justify the complexity induced by the fine-grained approach. A technical analysis to estimate the costs of an implementable solution is under development in the context of a joint program between EDF and Telecom ParisTech (Seido Lab).

When the starvation periods are not known ahead of time, the control mechanisms we propose act in a per slot basis; they keep traces of the past through the dynamics of the system, but have no view on the future, which induces poor performances. Such control schemes are not able to predict that allocating power at present time to a given appliance (e.g. Heater system) will create value in the future. For these schemes, additional intelligence has to be added to the system, which is a topic for further study.

Finally, we plan to combine the potentiality of the studied approach with a separate work we are carrying on possible participation of users to specific energy markets.

Fig. 1 .

 1 Fig. 1. Utility of lighting as a function of the power

Fig. 2 .

 2 Fig. 2. Utility of space heater as a function of the indoor temperature

Fig. 3 .Fig. 4 .

 34 Fig. 3. Average utility perceived per user for different values of the capacity considering homogeneous homes

  summarizes the notation we use.

	System Parameters and Exogeneous Variables
	τ	Duration of a time slot
	C(t)	Available power capacity at time slot t
	p a (h)	Minimum power consumed by appliance a in home h
	P a (h)	Maximum power consumed by appliance a in home h
	π(h, t)	Expected value of presence in home h at time t
	t 2 (h)	Minimum acceptable indoor temperature for home h
	T 2 (h)	Preferred indoor temperature for home h
	T 2	Maximum acceptable indoor temperature
	T0(h)	Initial indoor temperature for home h
	A(h), B(h) Coefficients for temperature dynamics in home h
	T 0 (t)	Outside temperature at time t
	C i (h)	Power limits for home h in increasing order
	Control Variables and Controlled Variables
	U a ht X a ht x a ht	Utility of appliance a in home h at time t Power consumed by appliance a in home h at time t = 1 when appliance a in home h at time t is active and
		= 0 otherwise
	Y 2 ht	Temperature of home h at time t (continuous)
	y 2

ht Equals 0 when temperature of home h at time t is less than or equal to t 2 (h) and 1 otherwise L ht Power limit for home h at time slot t (continuous) z i ht Equals 1 when power limit is equal to C i (h) and 0 otherwise TABLE I. NOMENCLATURE c) Global Maximum Utility, ahead of time:

Notice that this is not max-min fairness; nevertheless, the minimum utility provided to a given user will be the same as in max-min fairness. We do not introduce max-min fairness because max-min fair solutions of the problem we define may not exist, as can be understood from the formal problem stated in Section IV-B