Paolo G Giarrusso

Yann Régis-Gianas

Philipp Schuster

Incremental λ-Calculus in Cache-Transfer Style Static Memoization by Program Transformation

, propagate changes but do not reuse intermediate results, leading to wasteful recomputation. As a solution, we introduce conversion to Cache-Transfer-Style, an additional program transformations producing purely incremental functional programs that create and maintain nested tuples of intermediate results. To prove CTS conversion correct, we extend the correctness proof of static differentiation from STLC to untyped λ-calculus via step-indexed logical relations, and prove sound the additional transformation via simulation theorems. To show ILC-based languages can improve performance relative to fromscratch recomputation, and that CTS conversion can extend its applicability, we perform an initial performance case study. We provide derivatives of primitives for operations on collections and incrementalize selected example programs using those primitives, confirming expected asymptotic speedups.

Introduction

After computing a base output from some base input, we often need to produce updated outputs corresponding to updated inputs. Instead of rerunning the same base program on the updated input, incremental computation transforms the input change to an output change, potentially reducing asymptotic time complexity and significantly improving efficiency, especially for computations running on large data sets.

Incremental λ-Calculus (ILC) is a recently introduced framework [START_REF] Cai | A theory of changes for higher-order languages -incrementalizing λ-calculi by static differentiation[END_REF] for higher-order incremental computation. ILC represents changes from a base value v 1 to an updated value v 2 as a first-class change value dv . Since functions are firstclass values, change values include function changes.

ILC also statically transforms base programs to incremental programs or derivatives, that are functions mapping input changes to output changes. Incremental language designers can then provide their language with (higher-order) primitives (with their derivatives) that efficiently encapsulate incrementalizable computation skeletons (such as tree-shaped folds), and ILC will incrementalize higher-order programs written in terms of these primitives.

Alas, ILC only incrementalizes efficiently self-maintainable computations [START_REF] Cai | A theory of changes for higher-order languages -incrementalizing λ-calculi by static differentiation[END_REF]Sec. 4.3], that is, computations whose output changes can be computed using only input changes, but not the inputs themselves [START_REF] Gupta | Maintenance of materialized views: problems, techniques, and applications[END_REF]. Few computations are self-maintainable: for instance, mapping self-maintainable functions on a sequence is self-maintainable, but dividing numbers is not! Cai et al. [START_REF] Cai | A theory of changes for higher-order languages -incrementalizing λ-calculi by static differentiation[END_REF] already hint at this problem; we elaborate on it in Section 2.1. In this paper, we extend ILC to non-self-maintainable computations. To this end, we must enable derivatives to reuse intermediate results created by the base computation.

Many incrementalization approaches rely on some forms of dynamic memoization to remember intermediate results: they typically use hashtables to memoize function results, or dynamic dependence graphs [START_REF] Acar | Self-Adjusting Computation[END_REF] to remember the computation trace. However, looking up intermediate results in such dynamic data structure has a cost in time, and typical general-purpose optimizers cannot predict results from memoization lookups. Besides, reasoning on dynamic dependence graphs and computation traces is often complex. Instead, ILC aims to produce purely functional programs that are suitable for further optimizations and equational reasoning.

To that end, we eschew standard dynamic memoization in favor of static memoization: we transform programs to cache-transfer style (CTS), following ideas from Liu and Teitelbaum [START_REF] Liu | Caching intermediate results for program improvement[END_REF]. CTS functions output caches of intermediate results along with their primary results. Caches are just nested tuples whose structure is derived from code, and accessing them does not involve looking up keys depending on inputs. On the contrary, intermediate results can be fetched from these tuples using statically known locations. We also extend differentiation to produce CTS derivatives, which can extract from caches any intermediate results they need and which are responsible for updating the caches for the next computation step. This approach was inspired and pioneered by Liu and Teitelbaum [START_REF] Liu | Caching intermediate results for program improvement[END_REF] for untyped first-order functional languages; we integrate it with ILC and extend it to higher-order languages.

The correctness proof of static differentiation in CTS is quite challenging. First, it requires to show a forward simulation relation between two triples of reduction traces (the first triple being made of the source base evaluation, the source updated evaluation and the source derivative evaluation; the second triple being made of the corresponding CTS-translated evaluations). Dealing with six distinct evaluation environments at the same time was error prone on paper and for this reason, we conducted the proof using Coq [START_REF]The Coq development team: The Coq proof assistant reference manual[END_REF]. Second, the simulation relation must not only track values but also caches, which are only partially updated while in the middle of the evaluation of derivatives. Finally, we study the translation for an untyped λ-calculus, while previous ILC correctness proofs were restricted to simply-typed λ-calculus. Hence, we define which changes are valid via a logical relation and show its fundamental property. Being in an untyped setting, our logical relations are step-indexed, not indexed by types. We study an untyped language with the intention to make it applicable to the erasure of typed languages. Formalizing a type-preserving translation is left for future work because giving a type to CTS programs is challenging, as we shall explain.

In addition to the correctness proof, we present preliminary experimental results from three case studies. We obtain efficient incremental programs even on non self-maintainable functions.

Our contributions are presented as follows. First, we summarize ILC and illustrate the need to extend it to remember intermediate results via CTS (Sec. 2). Second, in our mechanized formalization (Sec. 3), we give a novel proof of correctness for ILC differentiation for untyped λ-calculus, based on step-indexed logical relations (Sec. 3.4). Third, building on top of ILC differentiation, we show how to transform untyped higher-order programs to CTS (Sec. 3.5) and we show that CTS functions and derivatives simulate correctly their non-CTS counterparts (Sec. 3.7). Finally, in our case studies (Sec. 4), we compare the performance of the generated code to the base programs. Sec. 4.4 discusses limitations and future work. Sec. 5 discusses related work and Sec. 6 concludes.

ILC and CTS Primer

In this section we exemplify ILC by applying it on an average function, show why the resulting incremental program is asymptotically inefficient, and use CTS conversion and differentiation to incrementalize our example efficiently and speed it up asymptotically (as confirmed by benchmarks in Sec. 4.1). Further examples in Sec. 4 apply CTS to higher-order programs and suggest that CTS enables incrementalizing efficiently some core database primitives such as joins.

Incrementalizing average via ILC

Our example computes the average of a bag of numbers. After computing the base output y 1 of the average function on the base input bag xs 1 , we want to update the output in response to a stream of updates to the input bag. For simplicity, we assume we have two updated inputs xs 2 and xs 3 and want to compute two updated outputs y 2 and y 3 , so the overall program can be described in Haskell as: Throughout the paper, we contrast base vs updated inputs and outputs. We also have base and updated values, computations, inputs, outputs, and so on.

We want to compute the updated outputs y 2 and y 3 in average 3 faster using ILC. For that, we assume that we receive not only updated inputs xs 2 and xs 3 but also input change dxs 1 from xs 1 to xs 2 and input change dxs 2 from xs 2 to xs 3 . An input change dx from x 1 to x 2 describes the changes from base input x 1 to updated input x 2 , so that x 2 can be computed via the update operator ⊕ as x 1 ⊕ dx .

We use ILC to automatically transform average to its derivative daverage :: Bag Z → ∆(Bag Z) → ∆Z. A derivative is guaranteed to map input changes to output changes. In this example, this means that dy 1 = daverage xs 1 dxs 1 is a change from base output y 1 = average xs 1 to updated output y 2 = average xs 2 , hence y 2 = y 1 ⊕ dy 1 .

Thanks to daverage's correctness, we can avoid expensive calls to average on updated inputs, and use daverage instead. This lets us rewrite average 3 to incrementalAverage 3 :

incrementalAverage 3 :: (Z, Z, Z) incrementalAverage 3 = let y1 = average xs1; dy 1 = daverage xs1 dxs1 y2 = y1 ⊕ dy 1 ; dy 2 = daverage xs2 dxs2 y3 = y2 ⊕ dy 2 in (y1, y2, y3)
As shown in previous work [START_REF] Giarrusso | Optimizing and Incrementalizing Higher-order Collection Queries by AST Transformation[END_REF], the derivative df of a function f is the nil change of f since

(f ⊕ df ) (a ⊕ da) = f a ⊕ df a da = f (a ⊕ da)

Self-maintainability and efficiency of derivatives

Alas, derivatives are efficient only if they are self-maintainable, and daverage is not! So, incrementalAverage 3 is no faster than average 3 . Let us inspect the code generated by differentiating average. Since average combines sum, length, and div , its derivative daverage combines those functions and their derivatives accordingly. It recomputes s, n and r just like average, but r is not used anywhere so its recomputation could be avoided. On the other hand, expensive intermediate results s and n are passed to ddiv . If ddiv does not actually use its inputs s and n, then their computation could be avoided too. Cai et al. [START_REF] Cai | A theory of changes for higher-order languages -incrementalizing λ-calculi by static differentiation[END_REF] call a derivative self-maintainable if it does not inspect its base inputs, but only its change inputs. Derivatives produced by ILC are only efficient if they do not compute inputs of self-maintainable derivatives. Cai et al. [START_REF] Cai | A theory of changes for higher-order languages -incrementalizing λ-calculi by static differentiation[END_REF] leave efficient support for non-self-maintainable derivatives for future work. But ddiv is not self-maintainable! Consider its implementation:

ddiv :: Z → ∆Z → Z → ∆Z → ∆Z ddiv a da b db = div (a ⊕ da) (b ⊕ db) -div a b
Function ddiv computes the difference between the updated and the original result. It uses its base inputs a and b, hence is not self-maintainable, and a derivative calling it, such as daverage, will not be efficient.

But not all is lost: executing daverage xs dxs will compute exactly the same s and n as executing average xs, so to avoid recomputation we must simply save and reuse them. Hence, we CTS-convert each function f to a CTS function fC and a CTS derivative dfC : CTS function fC produces, together with its final result, a cache containing intermediate results, that the caller must pass to CTS derivative dfC . CTS-converting our example produces the following code, which requires no wasteful recomputation.

type AverageC = (Z, SumC , Z, LengthC , Z, DivC ) averageC :: Bag Z → (Z, AverageC ) averageC xs = let (s, cs1) = sumC xs; (n, cn1) = lengthC xs; (r , cr 1) = divC s n in (r , (s, cs1, n, cn1, r , cr 1)) daverageC :: Bag Z → ∆(Bag Z) → AverageC → (∆Z, AverageC ) daverageC xs dxs (s, cs1, n, cn1, r , cr 1) = let (ds, cs2) = dsumC xs dxs cs1 (dn, cn2) = dlengthC xs dxs cn1 (dr , cr 2) = ddivC s ds n dn cr 1 in (dr , ((s ⊕ ds), cs2, (n ⊕ dn), cn2, (r ⊕ dr ), cr 2))
For each function f , we introduce a type FC for its cache, such that a CTS function fC has type A → (B , FC ) and CTS derivative dfC has type A → ∆A → FC → (∆B , FC ). Crucially, CTS derivatives like daverageC must return an updated cache to ensure correct incrementalization, so that application of further changes works correctly. In general, if (y 1 , c 1 ) = fC x 1 and (dy, c 2 ) = dfC x 1 dx c 1 , then (y 1 ⊕ dy, c 2 ) must equal the result of the base function fC applied to the updated input x 1 ⊕ dx , that is (y 1 ⊕ dy, c 2 ) = fC (x 1 ⊕ dx ).

For CTS-converted functions, the cache type FC is a tuple of intermediate results and caches of subcalls. For primitive functions like div , the cache type DivC could contain information needed for efficient computation of output changes. In the case of div , no additional information is needed. The definition of divC uses div and produces an empty cache, and the definition of ddivC follows the earlier definition for ddiv , except that we now pass along an empty cache.

data DivC = DivC divC :: Z → Z → (Z, DivC ) divC a b = (div a b, DivC ) ddivC :: Z → ∆Z → Z → ∆Z → DivC → (∆Z, DivC ) ddivC a da b db DivC = (div (a ⊕ da) (b ⊕ db) -div a b, DivC )
Finally, we can rewrite average 3 to incrementally compute y 2 and y 3 :

ctsIncrementalAverage 3 :: (Z, Z, Z) ctsIncrementalAverage 3 = let (y1, c1) = averageC xs1; (dy 1 , c2) = daverageC xs1 dxs1 c1 y2 = y1 ⊕ dy 1 ; (dy 2 , c3) = daverageC xs2 dxs2 c2 y3 = y2 ⊕ dy 2 in (y1, y2, y3)
Since functions of the same type translate to functions of different types, the translation does not preserve well-typedness in a higher-order language in general, but it works well in our case studies (Sec. 4); Sec. 4.1 shows how to map such functions. Step indexes Fig. 1: Our language λ L of lambda-lifted programs. Tuples can be nullary.

We now formalize CTS-differentiation for an untyped Turing-complete λcalculus, and formally prove it sound with respect to differentiation. We also give a novel proof of correctness for differentiation itself, since we cannot simply adapt Cai et al. [START_REF] Cai | A theory of changes for higher-order languages -incrementalizing λ-calculi by static differentiation[END_REF]'s proof to the new syntax: Our language is untyped and Turingcomplete, while Cai et al. [START_REF] Cai | A theory of changes for higher-order languages -incrementalizing λ-calculi by static differentiation[END_REF]'s proof assumed a strongly normalizing simplytyped λ-calculus and relied on its naive set-theoretic denotational semantics. Our entire formalization is mechanized using Coq [START_REF]The Coq development team: The Coq proof assistant reference manual[END_REF]. For reasons of space, some details are deferred to the appendix.

Transformations We introduce and prove sound three term transformations, namely differentiation, CTS translation and CTS differentiation, that take a function to its corresponding (non-CTS) derivative, CTS function and CTS derivative. Each CTS function produces a base output and a cache from a base input, while each CTS derivative produces an output change and an updated cache from an input, an input change and a base cache.

Proof technique To show soundness, we prove that CTS functions and derivatives simulate respectively non-CTS functions and derivatives. In turn, we formalize (non-CTS) differentiation as well, and we prove differentiation sound with respect to non-incremental evaluation. Overall, this shows that CTS functions and derivatives are sound relatively to non-incremental evaluation. Our presentation proceeds in the converse order: first, we present differentiation, formulated as a variant of Cai et al. [START_REF] Cai | A theory of changes for higher-order languages -incrementalizing λ-calculi by static differentiation[END_REF]'s definition; then, we study CTS differentiation.

By using logical relations, we simplify significantly the setup of Cai et al. [START_REF] Cai | A theory of changes for higher-order languages -incrementalizing λ-calculi by static differentiation[END_REF].

To handle an untyped language, we employ step-indexed logical relations. Besides, we conduct our development with big-step operational semantics because that choice simplifies the correctness proof for CTS conversion.

Structure of the formalization Sec. 3.1 introduces the syntax of the language λ L we consider in this development, and introduces its four sublanguages λ AL , λ IAL , λ CAL and λ ICAL . Sec. 3.2 presents the syntax and the semantics of λ AL , the source language for our transformations. Sec. 3.3 defines differentiation and its target language λ IAL , and Sec. 3.4 proves differentiation correct. Sec. 3.5 defines CTS conversion, comprising CTS translation and CTS differentiation, and their target languages λ CAL and λ ICAL . Sec. 3.6 presents the semantics of λ CAL . Finally, Sec. 3.7 proves CTS conversion correct.

Notations We write X for a sequence of X of some unspecified length X 1 , . . . , X m .

Syntax for λ L

A superlanguage To simplify our transformations, we require input programs to have been lambda-lifted [START_REF] Johnsson | Lambda lifting: transforming programs to recursive equations[END_REF] and converted to A'-normal form (A'NF). Lambdalifted programs are convenient because they allow us to avoid a specific treatment for free variables in transformations. A'NF is a minor variant of ANF [START_REF] Sabry | Reasoning about programs in continuation-passing style[END_REF], where every result is bound to a variable before use; unlike ANF, we also bind the result of the tail call. Thus, every result can thus be stored in a cache by CTS conversion and reused later (as described in Sec. 2). This requirement is not onerous: A'NF is a minimal variant of ANF, and lambda-lifting and ANF conversion are routine in compilers for functional languages. Most examples we show are in this form.

In contrast, our transformation's outputs are lambda-lifted but not in A'NF. For instance, we restrict base functions to take exactly one argument-a base input. As shown in Sec. 2.1, CTS functions take instead two arguments -a base input and a cache -and CTS derivatives take three arguments -an input, an input change, and a cache. We could normalize transformation outputs to inhabit the source language and follow the same invariants, but this would complicate our proofs for little benefit. Hence, we do not prescribe transformation outputs to satisfy the same invariants, and we rather describe transformation outputs through separate grammars.

As a result of this design choice, we consider languages for base programs, derivatives, CTS programs and CTS derivatives. In our Coq mechanization, we formalize those as four separate languages, saving us many proof steps to check the validity of required structural invariants. For simplicity, in the paper we define a single language called λ L (for λ-Lifted). This language satisfies invariants common to all these languages (including some of the A'NF invariants). Then, we define λ L sublanguages. We do not formalize the semantics of λ L itself, preferring to describe it informally; we only formalize the semantics of its sublanguages.

Syntax for terms

The λ L language is a relatively conventional lambda-lifted λcalculus with a limited form of pattern matching on tuples. The syntax for terms and values is presented in Fig. 1. We separate terms and values in two distinct syntactic classes because we use big-step operational semantics. Our let-bindings are non-recursive as usual, and support shadowing. Terms cannot contain λexpressions directly, but only refer to closures through the environment, and similarly for literals and primitives; we elaborate on this in Sec. 3.2. We do not introduce case expressions, but only bindings that destructure tuples, both in let-bindings and λ-expressions of closures. Our semantics does not assign meaning to match failures, but pattern-matchings are only used in generated programs and our correctness proofs ensure that the matches always succeed. We allow tuples to contain terms of form x ⊕ dx , which update base values x with changes in dx , because A'NF-converting these updates is not necessary to the transformations. We often inspect the result of a function call "f x ", which is not a valid term in our syntax. Hence, we write "@(f , x )" as a syntactic sugar for "let y = f x in y" with y chosen fresh.

Syntax for closed values A closed value is either a closure, a tuple of values, a literal, a primitive, a nil change for a primitive or a replacement change. A closure is a pair of an evaluation environment E and a λ-abstraction closed with respect to E. The set of available literals is left abstract. It may contain usual first-order literals like integers. We also leave abstract the primitives p like if-then-else or projections of tuple components. Each primitive p comes with a nil change, which is its derivative as explained in Sec. 2. A change value can also represent a replacement by some closed value a v . Replacement changes are not produced by static differentiation but are useful for clients of derivatives: we include them in the formalization to make sure that they are not incompatible with our system. As usual, environments E map variables to closed values.

Sublanguages of λ L The source language for all our transformations is a sublanguage of λ L named λ AL , where A stands for A'NF. To each transformation we associate a target language, which matches the transformation image. The target language for CTS conversion is named λ CAL , where "C" stands for CTS. The target languages of differentiation and CTS differentiation are called, respectively, λ IAL and λ ICAL , where the "I" stands for incremental.

The source language λ AL

We show the syntax of λ AL in Fig. 2. As said above, λ AL is a sublanguage of λ L denoting lambda-lifted base terms in A'NF. With no loss of generality, we assume that all bound variables in λ AL programs and closures are distinct. The step-indexed big-step semantics (Fig. 3) for base terms is defined by the judgment written E t ⇓ n v (where n can be omitted) and pronounced "Under environment E, base term t evaluates to closed value v in n steps." Intuitively, our

Term differentiation dt = D ι (t) D ι (x ) = dx D ι (let y = f x in t) = let y = f x , dy = df x dx in D ι (t) D ι (let y = (x ) in t) = let y = (x ), dy = (dx ) in D ι (t) Value differentiation dv = D ι (v ) D ι ((v )) = (D ι (v )) D ι (E f [λx . t]) = D ι (E f )[λx dx . D ι (t)] D ι ( ) = nil D ι (p) = 0p Environment differentiation dE = D ι (E) D ι (•) = • D ι (E; x = v ) = D ι (E); x = v ; dx = D ι (v ) Base/updated environment E = dE i • i = • i = 1, 2 dE ; x = v ; dx = dv i = dE 1; x = v v = v if i = 1 or v = v ⊕ dv if i = 2
λIAL change terms

dt ::= dx | let y = f x , dy = df x dx in dt | let y = (x ), dy = (dx ) in dt λIAL change values dv ::= (dv ) | dE [λx dx . dt] | d | 0p | !v λIAL change environments dE ::= • | dE ; x = v ; dx = dv λAL base terms t ::= x | let y = f x in t | let y = (x ) in t λAL closed values v ::= (v ) | E[λx . t] | | p λAL value environments E ::= • | E; x = v Fig. 2: Static differentiation D ι (-)
; syntax of its target language λ IAL , tailored to the output of differentiation; syntax of its source language λ AL . We assume that in λ IAL the same let binds both y and dy and that α-renaming preserves this invariant. We also define the base environment dE 1 and the updated environment dE 2 of a change environment dE .

step-indexes count the number of "nodes" of a big-step derivation. 4 As they are relatively standard, we defer the explanations of these rules to the appendix B.

Expressiveness A closure in the base environment can be used to represent a top-level definition. Since environment entries can point to primitives, we need no syntax to directly represent calls of primitives in the syntax of base terms. To encode in our syntax a program with top-level definitions and a term to be evaluated representing the entry point, one can produce a term t representing the entry point together with an environment E containing as values any top-level definitions, primitives and literals used in the program. Semi-formally, given an environment E 0 mentioning needed primitives and literals, and a list of top-level function definitions D = f = λx . t defined in terms of E 0 , we can produce a base environment E = L(D), with L defined by:

L(•) = E 0 and L(D, f = λx . t) = E, f = E[λx . t] where L(D) = E [SVar] E x ⇓1 E(x ) [STuple] E; y = (E(x )) t ⇓n v E let y = (x ) in t ⇓n+1 v [SPrimitiveCall] E(f ) = p E; y = δp(E(x )) t ⇓n v E let y = f x in t ⇓n+1 v [SClosureCall] E(f ) = E f [λx . t f ] E f ; x = E(x ) t f ⇓m vy E; y = vy t ⇓n v E let y = f x in t ⇓m+n+1 v
Fig. 3: Step-indexed big-step semantics for base terms of source language λ AL .

Correspondingly, we extend all our term transformations to values and environments to transform such encoded top-level definitions.

Our mechanization can encode n-ary functions "λ(x 1 , x 2 , . . . , x n ). t" through unary functions that accept tuples; we encode partial application using a curry primitive such that, essentially, curry f x y = f (x, y); suspended partial applications are represented as closures. This encoding does not support currying efficiently, we further discuss this limitation in Sec. 4.4.

Control operators, like recursion combinators or branching, can be introduced as primitive operations as well. If the branching condition changes, expressing the output change in general requires replacement changes. Similarly to branching we can add tagged unions.

To check the assertions of the last two paragraphs, the Coq development contains the definition of a curry primitive as well as a primitive for a fixpoint combinator, allowing general recursion and recursive data structures as well.

Static differentiation from λ AL to λ IAL

Previous work [START_REF] Cai | A theory of changes for higher-order languages -incrementalizing λ-calculi by static differentiation[END_REF] defines static differentiation for simply-typed λ-calculus terms. Fig. 2 transposes differentiation as a transformation from λ AL to λ IAL and defines λ IAL 's syntax.

Differentiating a base term t produces a change term D ι (t), its derivative. Differentiating final result variable x produces its change variable dx . Differentiation copies each binding of an intermediate result y to the output and adds a new binding for its change dy. If y is bound to tuple (x ), then dy will be bound to the change tuple (dx ). If y is bound to function application "f x ", then dy will be bound to the application of function change df to input x and its change dx . We explain differentiation of environments D ι (E) later in this section.

Evaluating D ι (t) recomputes all intermediate results computed by t. This recomputation will be avoided through cache-transfer style in Sec. 3.5. A comparison with the original static differentiation [START_REF] Cai | A theory of changes for higher-order languages -incrementalizing λ-calculi by static differentiation[END_REF] can be found in Appendix A.

Semantics for λ IAL We move on to define how λ IAL change terms evaluate to change values. We start by defining necessary definitions and operations on An evaluation environment dE follows the same structure as let-bindings of change terms: it binds variables to closed values and each variable x is immediately followed by a binding for its associated change variable dx . As with let-bindings of change terms, α-renamings in an environment dE must rename dx into dy if x is renamed into y. We define the update operator ⊕ to update a value with a change. This operator is a partial function written "v ⊕ dv ", defined as follows:

[SDVar] dE dx ⇓1 dE (dx ) [SDTuple] dE (x , dx ) = v x , dv x dE ; y = (v x ); dy = (dv x ) dt ⇓n dv dE let y = (x ), dy = (dx ) in dt ⇓n+1 dv [SDReplaceCall] dE 1 @(f , x ) ⇓m vy dE 2 @(f , x ) ⇓n vy dE (df ) = !v f dE ; y = vy ; dy = !vy dt ⇓p dv dE let y = f x , dy = df x dx in dt ⇓m+n+p+1 dv [SDPrimitiveNil] dE (f , df ) = p, 0p dE (x , dx ) = vx , dv x dE ; y = δp(vx ); dy = ∆p(vx , dv x ) dt ⇓n dv dE let y = f x , dy = df x dx in dt ⇓n+1 dv [SDClosureChange] dE (f , df ) = E f [λx . t f ], dE f [λx dx . dt f ] dE (x , dx ) = vx , dv x E f ; x = vx t f ⇓m vy dE f ; x = vx ; dx = dv x dt f ⇓n dv y dE ; y = vy ; dy = dv y dt ⇓p dv dE let y = f x , dy = df x dx in dt ⇓m+n+p+1 dv
v 1 ⊕ !v 2 = v 2 ⊕ d = δ ⊕ ( , d ) E[λx . t] ⊕ dE [λx dx . dt] = (E ⊕ dE )[λx . t] (v 1 , . . . , v n ) ⊕ (dv 1 , . . . , dv n ) = (v 1 ⊕ dv 1 , . . . , v n ⊕ dv n ) p ⊕ 0 p = p
where

(E; x = v ) ⊕ (dE ; x = v ; dx = dv ) = ((E ⊕ dE ); x = (v ⊕ dv )).
Replacement changes can be used to update all values (literals, tuples, primitives and closures), while tuple changes can only update tuples, literal changes can only update literals, primitive nil can only update primitives and closure changes can only update closures. A replacement change overrides the current value v with a new one v . On literals, ⊕ is defined via some interpretation function δ ⊕ , which takes a literal and a literal change to produce an updated literal. Change update for a closure ignores dt instead of computing something like dE[t ⊕ dt]. This may seem surprising, but we only need ⊕ to behave well for valid changes (as shown by Theorem 3.1): for valid closure changes, dt must behave anyway similarly to D ι (t), which Cai et al. [START_REF] Cai | A theory of changes for higher-order languages -incrementalizing λ-calculi by static differentiation[END_REF] show to be a nil change. Hence, t ⊕ D ι (t) and t ⊕ dt both behave like t, so ⊕ can ignore dt and only consider environment updates. This definition also avoids having to modify terms at runtime, which would be difficult to implement safely. We could also implement f ⊕ df as a function that invokes both f and df on its argument, as done by Cai et al. [START_REF] Cai | A theory of changes for higher-order languages -incrementalizing λ-calculi by static differentiation[END_REF], but we believe that would be less efficient when ⊕ is used at runtime. As we discuss in Sec. 3.4, we restrict validity to avoid this runtime overhead.

Having given these definitions, we show in Fig. 4 a step-indexed big-step semantics for change terms, defined through judgment dE dt ⇓ n dv (where n can be omitted). This judgment is pronounced "Under the environment dE , the change term dt evaluates into the closed change value dv in n steps." Rules Closure changes with non-nil environment changes represent partial application of derivatives to non-nil changes; for instance, if f takes a pair and dx is a non-nil change, 0 curry f df x dx constructs a closure change containing dx , using the derivative of curry mentioned in Sec. 3.2. In general, such closure changes do not arise from the rules we show, only from derivatives of primitives.

A new soundness proof for static differentiation

In this section, we show that static differentiation is sound (Theorem 3.3) and that Eq. ( 1) holds:

f a 2 = f a 1 ⊕ D ι (f ) a 1 da (1)
whenever da is a valid change from a 1 to a 2 (as defined later). One might want to prove this equation assuming only that a 1 ⊕ da = a 2 , but this is false in general.

A direct proof by induction on terms fails in the case for application (ultimately because f 1 ⊕df = f 2 and a 1 ⊕da = a 2 do not imply that f 1 a 1 ⊕df a 1 da = f 2 a 2 ). Fig. 5: Step-indexed validity, through judgments for values and for terms.

• d n → δ⊕( , d ) • !v2 n v1 → v2 • 0p n p → p • (dv
As usual, this can be fixed by introducing a logical relation. We call ours validity: a function change is valid if it turns valid input changes into valid output changes.

Static differentiation is only sound on input changes that are valid. Cai et al. [START_REF] Cai | A theory of changes for higher-order languages -incrementalizing λ-calculi by static differentiation[END_REF] show this for a strongly normalizing simply-typed λ-calculus using denotational semantics. Using an operational semantics, we generalize this result to an untyped and Turing-complete language, so we must turn to a step-indexed logical relation [START_REF] Ahmed | Step-indexed syntactic logical relations for recursive and quantified types[END_REF][START_REF] Acar | Imperative self-adjusting computation[END_REF].

Alert readers might wonder why we use a big-step semantics for a Turingcomplete language. We indeed focus on incrementalizing computations that terminate on both old and new inputs. Our choice follows Acar et al. [START_REF] Acar | Imperative self-adjusting computation[END_REF] (compared with in Sec. 5).

Validity as a step-indexed logical relation We say that "dv is a valid change from v 1 to v 2 , up to k steps" and write

dv k v 1 → v 2
to mean that dv is a change from v 1 to v 2 and that dv is a valid description of the differences between v 1 and v 2 , with validity tested with up to k steps. This relation approximates validity; if a change dv is valid at all approximations, it is simply valid (between v 1 and v 2 ); we write then dv v 1 → v 2 (omitting the step-index k) to mean that validity holds at all step-indexes. We similarly omit step-indexes k from other step-indexed relations when they hold for all k.

To justify this intuition of validity, we show that a valid change from v 1 to v 2 goes indeed from v 1 to v 2 (Theorem 3.1), and that if a change is valid up to k steps, it is also valid up to fewer steps (Lemma 3.2).

Theorem 3.1 (⊕ agrees with validity).

If

dv k v 1 → v 2 holds for all k > 0, then v 1 ⊕ dv = v 2 . Lemma 3.2 (Downward-closure). If N ≥ n, then dv N v 1 → v 2 implies dv n v 1 → v 2 .
Crucially, Theorem As usual with step-indexing, validity is defined by well-founded induction over naturals ordered by <; to show well-foundedness we observe that evaluation always takes at least one step.

Validity for values, terms and environments is formally defined by cases in Fig. 5. First, a literal change d is a valid change from to ⊕ d = δ ⊕ ( , d ). Since the function δ ⊕ is partial, the relation only holds for the literal changes d which are valid changes for . Second, a replacement change !v 2 is always a valid change from any value v 1 to v 2 . Third, a primitive nil change is a valid change between any primitive and itself. Fourth, a tuple change is valid up to step n, if each of its components is valid up to any step strictly less than n. Fifth, we define validity for closure changes. Roughly speaking, this statement means that a closure change is valid if (i) its environment change dE is valid for the original closure environment E 1 and for the new closure environment E 2 ; and (ii) when applied to related values, the closure bodies t are related by dt, as defined by the auxiliary judgment (dE dt) n (E 1 t 1 ) → (E 2 t 2 ) for validity between terms under related environments (defined in C). As usual with step-indexed logical relations, in the definition for this judgment about terms, the number k of steps required to evaluate the term t 1 is subtracted from the number of steps n that can be used to relate the outcomes of the term evaluations.

Soundness of differentiation

We can state a soundness theorem for differentiation without mentioning step-indexes; thanks to this theorem, we can compute the updated result v 2 not by rerunning a computation, but by updating the base result v 1 with the result change dv that we compute through a derivative on the input change. A corollary shows Eq. (1).

Theorem 3.3 (Soundness of differentiation in λ AL ). If dE is a valid change environment from base environment E 1 to updated environment E 2 , that is dE E 1 → E 2
, and if t converges both in the base and updated environment, that is

E 1 t ⇓ v 1 and E 2 t ⇓ v 2 , then D ι (t) evaluates under the change environment dE to a valid change dv between base result v 1 and updated result v 2 , that is dE D ι (t) ⇓ dv , dv v 1 → v 2 and v 1 ⊕ dv = v 2 .
We must first show that derivatives map input changes valid up to k steps to output changes valid up to k steps, that is, the fundamental property of our step-indexed logical relation:

Lemma 3.4 (Fundamental Property). For each n, if dE n E 1 → E 2 then (dE D ι (t)) n (E 1 t) → (E 2 t).
Translation of terms M = Tt(t )

Tt(let y = f x in t ) = let y, c y fx = f x in Tt(t ) Tt(let y = (x ) in t ) = let y = (x ) in Tt(t ) Tt(x ) = (x , C (t))
Cache of a term C = C (t) Syntax definitions for the target languages λ CAL and λ ICAL Terms of λ CAL follow again λ-lifted A'NF, like λ AL , except that a let-binding for a function application "f x " now binds an extra cache identifier c y fx besides output y. Cache identifiers have non-standard syntax: it can be seen as a triple that refers to the value identifiers f , x and y. Hence, an α-renaming of one of these three identifiers must refresh the cache identifier accordingly. Result terms explicitly return cache C through syntax (x , C). Caches are encoded through nested tuples, but they are in fact a tree-like data structure that is isomorphic to an execution trace. This trace contains both immediate values and the execution traces of nested function calls.

C (let y = f x in t) = ((C (t), y), c y fx ) C (let y = (x ) in t) = (C (t), y) C (x) = ()
Translation of values V = T (v ) T ((v )) = (T (v )) T (E[λx . t]) = T (E)[λx . Tt(t)] T ( ) = T (p) = p

CTS conversion

The syntax for λ ICAL matches the image of the CTS derivative and witnesses the CTS discipline followed by the derivatives: to determine dy, the derivative of f evaluated at point x with change dx expects the cache produced by evaluating y in the base term. The derivative returns the updated cache which contains the intermediate results that would be gathered by the evaluation of f (x ⊕ dx ). The result term of every change term returns the computed change and a cache update dC , where each value identifier x of the input cache is updated with its corresponding change dx .

Differentiation of terms dM = Dt(t )

Dt(let y = f x in t ) = let dy, c y fx = df x dx c y fx in Dt(t ) Dt(let y = (x ) in t ) = let dy = (dx ) in Dt(M ) Dt(x ) = (dx , U (t))
Cache update of a term dC = U (t)

U (let y = f x in t) = ((U (t), y ⊕ dy), c y fx ) U (let y = (x ) in t) = (U (t), y ⊕ dy) U (x) = ()
Differentiation of change values dV = T (dv )

T ((dv )) = (T (dv )) T (dE [λx dx . D ι (t)]) = T (dE )[λx dx (C (t)). Dt(t)] T (!v ) = !T (v ) T (d ) = d T (0p) = 0p

CTS conversion and differentiation

These translations use two auxiliary functions: C (t) which computes the cache term of a λ AL term t, and U (t), which computes the cache update of t's derivative.

CTS translation on terms, T t (t ), accepts as inputs a global term t and a subterm t of t. In tail position (t = x ), the translation generates code to return both the result x and the cache C (t) of the global term t. When the transformation visits let-bindings, it outputs extra bindings for caches c y fx on function calls and visits the let-body.

Similarly to T t (t ), CTS derivation D t (t ) accepts a global term t and a subterm t of t. In tail position, the translation returns both the result change dx and the cache update U (t). On let-bindings, it does not output bindings for y but for dy, it outputs extra bindings for c y fx as in the previous case and visits the let-body.

To handle function definitions, we transform the base environment E through T (E) and T (D ι (E)) (translations of environments are done pointwise, see D). Since D ι (E) includes E, we describe T (D ι (E)) to also cover T (E). Overall, T (D ι (E)) CTS-converts each source closure f = E[λx . t] to a CTS-translated function, with body T t (t), and to the CTS derivative df of f . This CTS derivative pattern matches on its input cache using cache pattern C (t). That way, we make sure that the shape of the cache expected by df is consistent with the shape of the cache produced by f . The body of derivative df is computed by CTS-deriving f 's body via D t (t). Base terms of the language are evaluated using a conventional big-step semantics, consisting of two judgments. Judgment "F M ⇓ (V, V c )" is read "Under evaluation environment F , base term M evaluates to value V and cache V c ". The semantics follows the one of λ AL ; since terms include extra code to produce and carry caches along the computation, the semantics evaluates that code as well. For space reasons, we defer semantic rules to the appendix. Auxiliary judgment "F C ⇓ V c " evaluates cache terms into cache values: It traverses a cache term and looks up the environment for the values to be cached.

Change terms of λ ICAL are also evaluated using a big-step semantics, which resembles the semantics of λ IAL and λ CAL . Unlike those semantics, evaluating cache updates (dC , x ⊕ dx ) is evaluated using the ⊕ operator (overloaded on λ CAL values and λ ICAL changes). By lack of space, its rules are deferred to Appendix E. This semantics relies on three judgments. Judgment "dF dM ⇓ (dV , V c )" is read "Under evaluation environment F , change term dM evaluates to change value dV and updated cache V c ". The first auxiliary judgment "dF dC ⇓ V c " defines evaluation of cache update terms. The final auxiliary judgment "V c ∼ C → dF " describes a limited form of pattern matching used by CTS derivatives: namely, how a cache pattern C matches a cache value V c to produce a change environment dF .

Soundness of CTS conversion

The proof is based on a simulation in lock-step, but two subtle points emerge. First, we must relate λ AL environments that do not contain caches, with λ CAL environments that do. Second, while evaluating CTS derivatives, the evaluation environment mixes caches from the base computation and updated caches computed by the derivatives.

Theorem 3.7 follows because differentiation is sound (Theorem 3.3) and evaluation commutes with CTS conversion; this last point requires two lemmas. First, CTS translation of base terms commutes with our semantics:

Lemma 3.5 (Commutation for base evaluations).

For all E, t and v , if

E t ⇓ v , there exists V c , T (E) T t (t) ⇓ (T (v ), V c ).
Second, we need a corresponding lemma for CTS translation of differentiation results: intuitively, evaluating a derivative and CTS translating the resulting change value must give the same result as evaluating the CTS derivative. But to formalize this, we must specify which environments are used for evaluation, and this requires two technicalities.

Assume derivative D ι (t) evaluates correctly in some environment dE . Evaluating CTS derivative D t (t) requires cache values from the base computation, but they are not in T (dE )! Therefore, we must introduce a judgment to complete a CTS-translated environment with the appropriate caches (see Appendix F).

Next, consider evaluating a change term of the form dM = C[dM ], where C is a standard single-hole change-term context-that is, for λ ICAL , a sequence of let-bindings. When evaluating dM , we eventually evaluate dM in a change environment dF updated by C: the change environment dF contains both the updated caches coming from the evaluation of C and the caches coming from the base computation (which will be updated by the evaluation of dM ). Again, a new judgment, given in Appendix F, is required to model this process.

With these two judgments, the second key Lemma stating the commutation between evaluation of derivatives and evaluation of CTS derivatives can be stated. We give here an informal version of this Lemma, the actual formal version can be found in Appendix F.

Lemma 3.6 (Commutation for derivatives evaluation).

If the evaluation of D ι (t) leads to an environment dE 0 when it reaches the differentiated context D ι (C) where t = C[t ], and if the CTS conversion of t under this environment completed with base (resp. changed) caches evaluates into a base value T (v ) (resp. a changed value T (v )) and a base cache value V c (resp. an updated cache value V c ), then under an environment containing the caches already updated by the evaluation of D ι (C) and the base caches to be updated, the CTS derivative of t evaluates to T (dv ) such that v ⊕ dv = v and to the updated cache V c .

Finally, we can state soundness of CTS differentiation. This theorem says that CTS derivatives not only produce valid changes for incrementalization but that they also correctly consume and update caches.

Theorem 3.7 (Soundness of CTS differentiation).

If the following hypotheses hold:

1. dE E → E 2. E t ⇓ v 3. E t ⇓ v
then there exists dv , V c , V c and F 0 such that:

1. T (E) T (t) ⇓ (T (v ), V c ) 2. T (E ) T (t) ⇓ (T (v ), V c ) 3. C (t) ∼ V c → F 0 4. T (dE ); F 0 D t (t) ⇓ (T (dv ), V c ) 5. v ⊕ dv = v

Incrementalization case studies

In this section, we investigate two questions: whether our transformations can target a typed language like Haskell and whether automatically transformed programs can perform well. We implement by hand primitives on sequences, bags and maps in Haskell. The input terms in all case studies are written in a deep embedding of λ AL into Haskell. The transformations generate Haskell code that uses our primitives and their derivatives.

We run the transformations on three case studies: a computation of the average value of a bag of integers, a nested loop over two sequences and a more involved example inspired by Koch et al. [START_REF] Koch | DBToaster: higher-order delta processing for dynamic, frequently fresh views[END_REF]'s work on incrementalizing database queries. For each case study, we make sure that results are consistent between from scratch recomputation and incremental evaluation; we measure the execution time for from scratch recomputation and incremental computation as well as the space consumption of caches. We obtain efficient incremental programs, that is ones for which incremental computation is faster than from scratch recomputation. The measurements indicate that we do get the expected asymptotic improvement in time of incremental computation over from scratch recomputation by a linear factor while the caches grows in a similar linear factor.

Our benchmarks were compiled by GHC 8.2.2 and run on a 2.20GHz hexa core Intel(R) Xeon(R) CPU E5-2420 v2 with 32GB of RAM running Ubuntu 14.04. We use the criterion [START_REF] O'sullivan | criterion: a Haskell microbenchmarking library[END_REF] benchmarking library.

Averaging bags of integers

Sec. 2.1 motivates our transformation with a running example of computing the average over a bag of integers. We represent bags as maps from elements to (possibly negative) multiplicities. Earlier work [START_REF] Cai | A theory of changes for higher-order languages -incrementalizing λ-calculi by static differentiation[END_REF][START_REF] Koch | DBToaster: higher-order delta processing for dynamic, frequently fresh views[END_REF] represents bag changes as bags of removed and added elements. We use a different representation of bag changes that takes advantage of the changes to elements and provide primitives on bags and their derivatives. The CTS variant of map, that we call mapC , takes a function fC in CTS and a bag as and produces a bag and a cache. The cache stores for each invocation of fC , and therefore for each distinct element in as, the result of fC of type b and the cache of type c.

Inspired by Rossberg et al. [START_REF] Rossberg | F-ing modules[END_REF], all higher-order functions (and typically, also their caches) are parametric over cache types of their function arguments. Here, functions mapC and dmapC and cache type MapC are parametric over the cache type c of fC and dfC .

map :: (a → b) → Bag a → Bag b data MapC a b c = MapC (Map a (b, c)) mapC :: (a → (b, c)) → Bag a → (Bag b, MapC a b c) dmapC :: (a → (b, c)) → (a → ∆a → c → (∆b, c)) → Bag a → ∆(Bag a) → MapC a b c → (∆(Bag b), MapC a b c)
We wrote the length and sum functions used in our benchmarks in terms of primitives map and foldGroup and had their CTS function and CTS derivative generated automatically. We evaluate whether we can produce an updated result with daverageC shown in Sec. 2.1 faster than by from scratch recomputation with average. We expect the speedup of daverageC to depend on the size of the input bag n. We fix an input bag of size n as the bag containing the numbers from 1 to n. We define a change that inserts the integer 1 into the bag. To measure execution time of from scratch recomputation, we apply average to the input bag updated with the change. To measure execution time of the CTS function averageC , we apply averageC to the input bag updated with the change. To measure execution time of the CTS derivative daverageC , we apply daverageC to the input bag, the change and the cache produced by averageC when applied to the input bag. In all three cases we ensure that all results and caches are fully forced so as to not hide any computational cost behind laziness.

The plot in Fig. 8a shows execution time versus the size n of the base input. To produce the base result and cache, the CTS transformed function averageC takes longer than the original average function takes to produce just the result. Producing the updated result incrementally is slower than from scratch recomputation for small input sizes, but because of the difference in time complexity becomes faster as the input size grows. The size of the cache grows linearly with the size of the input, which is not optimal for this example. We leave optimizing the space usage of examples like this to future work.

Nested loops over two sequences

Next, we consider CTS differentiation on a higher-order example. To incrementalize this example efficiently, we have to enable detecting nil function changes at runtime by representing function changes as closures that can be inspected by incremental programs. Our example here is the Cartesian product of two sequences computed in terms of functions map and concat. We implemented incremental sequences and related primitives following Firsov and Jeltsch [START_REF] Firsov | Purely functional incremental computing[END_REF]: our change operations and first-order operations (such as concat) reuse their implementation. On the other hand, we must extend higher-order operations such as map to handle non-nil function changes and caching. A correct and efficient CTS derivative dmapC has to work differently depending on whether the given function change is nil or not: For a non-nil function change it has to go over the input sequence; for a nil function change it has to avoid that.

Cai et al. [START_REF] Cai | A theory of changes for higher-order languages -incrementalizing λ-calculi by static differentiation[END_REF] use static analysis to conservatively approximate nil function changes as changes to terms that are closed in the original program. But in this example the function argument (λy → (x , y)) to map in cartesianProduct is not a closed term. It is, however, crucial for the asymptotic improvement that we avoid looping over the inner sequence when the change to the free variable x in the change environment is 0 x .

To enable runtime nil change detection, we apply closure conversion to the original program and explicitly construct closures and changes to closures. While the only valid change for closed functions is their nil change, for closures we can have non-nil function changes. A function change df , represented as a closure change, is nil exactly when all changes it closes over are nil.

We represent closed functions and closures as variants of the same type. Correspondingly we represent changes to a closed function and changes to a closure as variants of the same type of function changes. We inspect this representation at runtime to find out if a function change is a nil change. We use the same benchmark setup as in the benchmark for the average computation on bags. The input of size n is a pair of sequences (xs, ys). Each sequence initially contains the integers from 1 to n. Updating the result in reaction to a change dxs to the outer sequence xs takes less time than updating the result in reaction to a change dys to the inner sequence ys. While a change to the outer sequence xs results in an easily located change in the output sequence, a change for the inner sequence ys results in a change that needs a lot more calculation to find the elements it affects. We benchmark changes to the outer sequence xs and the inner sequence ys separately where the change to one sequence is the insertion of a single integer 1 at position 1 and the change for the other one is the nil change. Fig. 9 shows execution time versus input size. In this example again preparing the cache takes longer than from scratch recomputation alone. The speedup of incremental computation over from scratch recomputation increases with the size of the base input sequences because of the difference in time complexity. Eventually we do get speedups for both kinds of changes (to the inner and to the outer sequence), but for changes to the outer sequence we get a speedup

Indexed joins of two bags

Our goal is to show that we can compose primitive functions into larger and more complex programs and apply CTS differentiation to get a fast incremental program. We use an example inspired from the DBToaster literature [START_REF] Koch | DBToaster: higher-order delta processing for dynamic, frequently fresh views[END_REF]. In this example we have a bag of orders and a bag of line items. An order is a pair of an order key and an exchange rate. A line item is a pair of an order key and a price. We build an index mapping each order key to the sum of all exchange rates of the orders with this key and an index from order key to the sum of the prices of all line items with this key. We then merge the two maps by key, multiplying corresponding sums of exchange rates and sums of prices. We compute the total price of the orders and line items as the sum of those products. Unlike DBToaster, we assume our program is already transformed to explicitly use indexes, as above. Because our indexes are maps, we implemented a change structure, CTS primitives and their CTS derivatives for maps.

To build the indexes, we use a groupBy function built from primitive functions foldMapGroup on bags and singleton for bags and maps respectively. The CTS function groupByC and the CTS derivative dgroupByC are automatically generated. While computing the indexes with groupBy is self-maintainable, merging them is not. We need to cache and incrementally update the intermediately created indexes to avoid recomputing them.

We evaluate the performance in the same way we did in the other case studies. The input of size n is a pair of bags where both contain the pairs (i , i ) for i between 1 and n. The change is an insertion of the order (1, 1) into the orders bag. For sufficiently large inputs, our CTS derivative of the original program produces updated results much faster than from scratch recomputation, again because of a difference in time complexity as indicated by Fig. 8b. The size of the cache grows linearly with the size of the input in this example. This is unavoidable, because we need to keep the indexes.

Limitations and future work

Typing of CTS programs Functions of the same type f 1 , f 2 :: A → B can be transformed to CTS functions f 1 :: A → (B , C 1 ), f 2 :: A → (B , C 2 ) with different cache types C 1 , C 2 , since cache types depend on the implementation. This heterogeneous typing of translated functions poses difficult typing issues, e.g. what is the translated type of a list (A → B )? We cannot hide cache types behind existential quantifiers because they would be too abstract for derivatives, which only work on very specific cache types. We can fix this problem with some runtime overhead by using a single type Cache, defined as a tagged union of all cache types or, maybe with more sophisticated type systems -like first-class translucent sums, open existentials or Typed Adapton's refinement types [START_REF] Hammer | Typed Adapton: refinement types for incremental computations with precise names[END_REF] that could be able to correctly track down cache types properly.

In any case, we believe that these machineries would add a lot of complexity without helping much with the proof of correctness. Indeed, the simulation relation is more handy here because it maintains a global invariant about the whole evaluations (typically the consistency of cache types between base computations and derivatives), not many local invariants about values as types would.

One might wonder why caches could not be totally hidden from the programmer by embedding them in the derivatives themselves; or in other words, why we did not simply translate functions of type A → B into functions of type A → B × (∆A → ∆B). We tried this as well; but unlike automatic differentiation, we must remember and update caches according to input changes (especially when receiving a sequence of such changes as in Sec. 2.1). Returning the updated cache to the caller works; we tried closing over the caches in the derivative, but this ultimately fails (because we could receive function changes to the original function, but those would need access to such caches).

Comprehensive performance evaluation This paper focuses on theory and we leave benchmarking in comparison to other implementations of incremental computation to future work. The examples in our case study were rather simple (except perhaps for the indexed join). Nevertheless, the results were encouraging and we expect them to carry over to more complex examples, but not to all programs. A comparison to other work would also include a comparison of space usage for auxiliary data structure, in our case the caches.

Cache pruning via absence analysis

To reduce memory usage and runtime overhead, it should be possible to automatically remove from transformed programs any caches or cache fragments that are not used (directly or indirectly) to compute outputs. Liu [START_REF] Liu | Efficiency by incrementalization: an introduction[END_REF] performs this transformation on CTS programs by using absence analysis, which was later extended to higher-order languages by Sergey et al. [START_REF] Sergey | Modular, higher-order cardinality analysis in theory and practice[END_REF]. In lazy languages, absence analysis removes thunks that are not needed to compute the output. We conjecture that the analysis could remove unused caches or inputs, if it is extended to not treat caches as part of the output.

Unary vs n-ary abstraction

We only show our transformation correct for unary functions and tuples. But many languages provide efficient support for applying curried functions such as div :: Z → Z → Z. Naively transforming such a curried function to CTS would produce a function divC of type Z → (Z → (Z, DivC 2 )), DivC 1 ) with DivC 1 = (), which adds excessive overhead. In Sec. 2 and our evaluation we use curried functions and never need to use this naive encoding, but only because we always invoke functions of known arity.

Related work

Cache-transfer-style Liu [START_REF] Liu | Efficiency by incrementalization: an introduction[END_REF]'s work has been the fundamental inspiration to this work, but her approach has no correctness proof and is restricted to a first-order untyped language. Moreover, while the idea of cache-transfer-style is similar, it's unclear if her approach to incrementalization would extend to higher-order programs. Firsov and Jeltsch [START_REF] Firsov | Purely functional incremental computing[END_REF] also approach incrementalization by code transformation, but their approach does not deal with changes to functions. Instead of transforming functions written in terms of primitives, they provide combinators to write CTS functions and derivatives together. On the other hand, they extend their approach to support mutable caches, while restricting to immutable ones as we do might lead to a logarithmic slowdown.

Finite differencing Incremental computation on collections or databases by finite differencing has a long tradition [START_REF] Paige | Finite differencing of computable expressions[END_REF][START_REF] Blakeley | Efficiently updating materialized views[END_REF]. The most recent and impressive line of work is the one on DBToaster [START_REF] Koch | Incremental query evaluation in a ring of databases[END_REF][START_REF] Koch | DBToaster: higher-order delta processing for dynamic, frequently fresh views[END_REF], which is a highly efficient approach to incrementalize queries over bags by combining iterated finite differencing with other program transformations. They show asymptotic speedups both in theory and through experimental evaluations. Changes are only allowed for datatypes that form groups (such as bags or certain maps), but not for instance for lists or sets. Similar ideas were recently extended to higher-order and nested computation [START_REF] Koch | Incremental view maintenance for collection programming[END_REF], though only for datatypes that can be turned into groups. Koch et al. [START_REF] Koch | Incremental view maintenance for collection programming[END_REF] emphasize that iterated differentiation is necessary to obtain efficient derivatives; however, ANF conversion and remembering intermediate results appear to address the same problem, similarly to the field of automatic differentiation [START_REF] Wang | Demystifying differentiable programming: Shift/reset the penultimate backpropagator (????[END_REF].

Logical relations To study correctness of incremental programs we use a logical relation among base values v 1 , updated values v 2 and changes dv . To define a logical relation for an untyped λ-calculus we use a step-indexed logical relation, following Appel and McAllester [5], Ahmed [START_REF] Ahmed | Step-indexed syntactic logical relations for recursive and quantified types[END_REF]; in particular, our definitions are closest to the ones by Acar et al. [START_REF] Acar | Imperative self-adjusting computation[END_REF], who also work with an untyped language, big-step semantics and (a different form of) incremental computation. However, they do not consider first-class changes. Technically, we use environments rather than substitution, and index our big-step semantics differently.

Dynamic incrementalization

The approaches to incremental computation with the widest applicability are in the family of self-adjusting computation [START_REF] Acar | Self-Adjusting Computation[END_REF][START_REF] Acar | Self-adjusting computation: (an overview)[END_REF], including its descendant Adapton [START_REF] Hammer | Adapton: composable, demand-driven incremental computation[END_REF]. These approaches incrementalize programs by combining memoization and change propagation: after creating a trace of base computations, updated inputs are compared with old ones in O(1) to find corresponding outputs, which are updated to account for input modifications. Compared to self-adjusting computation, Adapton only updates results that are demanded. As usual, incrementalization is not efficient on arbitrary programs, but only on programs designed so that input changes produce small changes to the computation trace; refinement type systems have been designed to assist in this task [START_REF] Çiçek | A type theory for incremental computational complexity with control flow changes[END_REF][START_REF] Hammer | Typed Adapton: refinement types for incremental computations with precise names[END_REF]. To identify matching inputs, Nominal Adapton [START_REF] Hammer | Incremental computation with names[END_REF] replaces input comparisons by pointer equality with first-class labels, enabling more reuse.

Conclusion

We have presented a program transformation which turns a functional program into its derivative and efficiently shares redundant computations between them thanks to a statically computed cache. This work has been mechanized using Coq and the corresponding proof is available online, together with the case study material. 5Although our first practical case studies show promising results, this paper focused on putting CTS differentiation on solid theoretical ground. For the moment, we only have scratched the surface of the incrementalization opportunities opened by CTS primitives and their CTS derivatives: in our opinion, exploring the design space for cache data structures will lead to interesting new results in purely functional incremental programming.

A Comparison with original static differentiation

Cai et al. [START_REF] Cai | A theory of changes for higher-order languages -incrementalizing λ-calculi by static differentiation[END_REF]'s static differentiation for λ-terms [START_REF] Cai | A theory of changes for higher-order languages -incrementalizing λ-calculi by static differentiation[END_REF] is defined instead as follows:

Derive(x ) = dx Derive(t u) = (Derive(t)) u (Derive(u)) Derive(λx . t) = λx dx . Derive(t)
Even though the first two cases of Cai et al. [START_REF] Cai | A theory of changes for higher-order languages -incrementalizing λ-calculi by static differentiation[END_REF]'s differentiation map into the two cases of our differentiation variant, one may ask where the third case is realized now. Actually, this third case occurs while we transform the base environment E. Indeed, we will assume that the closures of the environment of the source program have been adjoined a nil change or derivative, as defined by D ι (E). Change value D ι (v ) represents a nil change for v ; if v is a closure, its nil change is also its derivative [START_REF] Cai | A theory of changes for higher-order languages -incrementalizing λ-calculi by static differentiation[END_REF]. Computing D ι (v ) requires a meta-level function nil which computes a nil change for every literal . The existence of such a function is generally assumed in previous work [START_REF] Cai | A theory of changes for higher-order languages -incrementalizing λ-calculi by static differentiation[END_REF] as it is always valid to use the change ! . Yet, since this triggers recomputation, it can be more efficient to pick nil changes appropriate to the domain and to the definition of ⊕.

B Description of the semantic rules for λ AL Rule [SVar] looks variable x up in environment E. Other rules evaluate letbinding "let y = . . . in t" in environment E: Each rule computes y's new value v y (taking m steps) and evaluates in n steps the body t to a value v , using environment E extended by binding y to v y . The overall let-binding evaluates to v in m + n + 1 steps. But different rules compute the value of y differently.

[STuple] looks each variable in x up in E to evaluate tuple (x ) (in m = 0 steps).

[SPrimitiveCall] evaluates function calls where variable f is bound in E to a primitive p, evaluated as specified by a function δ p (-) from closed values to closed values. To evaluate such a primitive call, this rule applies δ p (-) to x 's value (in m = 0 steps). [SClosureCall] evaluates function calls where variable f is bound in E to closure E f [λx . t f ]: this rule evaluates the closure body t f in m steps, using the closure environment E f extended with the value of x in E. The rules for the evaluation of λ CAL change terms are similar to the evaluation rules of λ AL change terms except that (i) caches are carried along the computation and updated at return sites; (ii) there is no recomputation of base values since they are now extracted from the caches. Rule [TDResult] returns the final change value of a computation as well as a updated cache resulting from the evaluation of the cache update term dC . Rule [TDTuple] resembles its counterpart in the source language, but the tuple for y is not built as it has already been pushed in the environment by the cache. As for λ AL , there are three rules to deal with let-bindings depending on the shape of the change bound to df in the environment:

C Validity relation over environments

• k • → • dE k E 1 → E 2 dv k v 1 → v 2 dE ; x = v 1 ; dx = dv k E 1 ; x = v 1 → E 2 ; x = v 2

D CTS translation of environments

-If df is bound to a replacement, the rule [TDReplaceCall] applies. In that case, we reevaluate the function call in the updated environment dF 2 (defined similarly as in the source language). This evaluation leads to a new value V which replaces the original one as well as an updated cache for c y fx .

-If df is bound to a nil change and f is bound to primitive p, the rule [TD-PrimitiveNil] applies. The derivative of p is invoked with the value of x , its change value and the cache of the original call to p. The semantics of p's derivative is given by builtin function ∆ p (-), as in the source language. -If df is bound to a closure change and f is bound to a closure, the rule [TD-ClosureChange] applies. The body of the closure change is evaluated under the closure change environment extended with the value of the formal argument x , its change dx and with the environment resulting from the binding of the original cache value to the variables occuring in the cache C. This evaluation leads to a change and an updated cache bound in the environment to continue with the evaluation of the rest of the term.

F Soundness proof of CTS conversion

This section gives complementary technical details about the homonymous section of the paper.

The proof requires a judgment to relate source change environments with CTS change environments that appear during the evaluation of λ CAL change terms under context. Assuming that dF is a change environment with no cache, this judgment is written dF dF 0 ↑ C → k dF k and is read "Under the change environment dF , the change environment with no cache dF is completed into the change environment dF k with the caches produced by C in the base computation if k = 1 or in the updated computation if k = 2".

The rules for this judgment are given in Fig. 12.

[CompleteNil] is a straightforward base case. [CompleteTuple] does not introduce any cache since only function calls do produce caches. [CompleteWithBaseCall] (resp. [Complete-WithUpdatedCall]) computes a cache V c by evaluating @(f , x ) under the base (resp. updated) environment dF 1 (resp. dF 2 ). In [CompleteWithUpdated-Call], one might wonder why the recursive call which evaluates the remaining context C is not performed under an environment where y = V . Actually, this is consistent with the fact that in the CTS derivatives base values are only updated at the end of the computation when the updated cache is returned. This is necessary since derivatives calls in C still need values from the base computation, not the ones from the updated computation. base (resp. updated) computations. The hypothesis (5) (resp. ( 6)) evaluates t under the base (resp. updated) change environment equipped with caches to get the cached values for the whole base (resp. updated) computation. Finally, the hypothesis [START_REF] Cai | A theory of changes for higher-order languages -incrementalizing λ-calculi by static differentiation[END_REF] extracts from V c only the base cached values that are needed to evaluate D t (t ): the operation V ↑|C| c removes the |C| first elements from the cache V c . Indeed, these cached values have already been updated by the evaluation of C and they are present in dF 2 . The conclusion of this lemma states that T (dE ) (the CTS version of dE ), extended with the F 0 , the not-yet-updated cache values from the base computation, and with the updated change environment dF 2 , is a sound environment to evaluate the CTS derivative to the CTS version of dv and to the updated cache V c .

G Space usage measurements

  average :: Bag Z → Z average xs = let s = sum xs; n = length xs; r = div s n in r average 3 = let y1 = average xs1; y2 = average xs2; y3 = average xs3 in (y1, y2, y3)

  daverage :: Bag Z → ∆(Bag Z) → ∆Z daverage xs dxs = let s = sum xs; ds = dsum xs dxs; n = length xs; dn = dlength xs dxs; r = div s n; dr = ddiv s ds n dn in dr

Fig. 4 :

 4 Fig. 4: Step-indexed big-step semantics for the change terms of λ IAL .

  [SDVar] and[SDTuple] are unsurprising. To evaluate function calls in letbindings "let y = f x , dy = df x dx in dt" we have three rules, depending on the shape of dE (df ). These rules all recompute the value v y of y in the original environment, but compute differently the change dy to y. If dE (df ) replaces the value of f , [SDReplaceCall] recomputes v y = f x from scratch in the new environment, and bind dy to !v y when evaluating the let body. If dE (df ) is the nil change for primitive p,[SDPrimitiveNil] computes dy by running p's derivative through function ∆ p (-). If dE (df ) is a closure change,[SDClosureChange] invokes it normally to compute its change dv y . As we show, if the closure change is valid, its body behaves like f 's derivative, hence incrementalizes f correctly.

Fig. 6 :

 6 Fig. 6: Cache-Transfer Style translation and syntax of its target language λ CAL .

Fig. 6

 6 Fig. 6 and 7 define both the syntax of λ CAL and λ ICAL and CTS conversion. The latter comprises CTS differentiation D(-), from λ AL to λ ICAL , and CTS translation T (-), from λ AL to λ CAL .

  Change terms dM ::= let dy, c y fx = df x dx c y fx in dM | let dy = (dx ) in dM | , dC ) Cache updates dC ::= (dC , c y fx ) | (dC , x ⊕ dx ) | () Change values dV ::= (dV ) | dF [λx dx C. dM ] | d | 0p | !V Change environments dF ::= • | dF ; dDv Change environment entries dDv ::= Dv | dx = dV

Fig. 7 :

 7 Fig. 7: CTS differentiation and syntax of its target language λ ICAL . Beware T (dE [λx dx . D ι (t)]) applies a left-inverse of D ι (t) during pattern matching.

3. 6

 6 Semantics of λ CAL and λ ICAL An evaluation environment F of λ CAL contains both values and cache values. Values V resemble λ AL values v , cache values V c match cache terms C and change values dV match λ IAL change values dv . Evaluation environments dF for change terms must also bind change values, so functions in change closures take not just a base input x and an input change dx , like in λ IAL , but also an input cache C. By abuse of notation, we reuse the same syntax C to both deconstruct and construct caches.

Fig. 8 :

 8 Fig. 8: Benchmark results for average and totalPrice

cartesianProduct : :

 : Sequence a → Sequence b → Sequence (a, b) cartesianProduct xs ys = concatMap (λx → map (λy → (x , y)) ys) xs concatMap :: (a → Sequence b) → Sequence a → Sequence b concatMap f xs = concat (map f xs)

data

  Fun a b c where Closed :: (a → (b, c)) → Fun a b c Closure :: (e → a → (b, c)) → e → Fun a b c data ∆(Fun a b c) where DClosed :: (a → ∆a → c → (∆b, c)) → ∆(Fun a b c) DClosure :: (e → ∆e → a → ∆a → c → (∆b, c)) → e → ∆e → ∆(Fun a b c)

  Benchmark results for Cartesian product changing inner sequence. Benchmark results for Cartesian product changing outer sequence.

Fig. 9 :

 9 Fig. 9: Benchmark results for cartesianProduct

type

  Order = (Z, Z) type LineItem = (Z, Z) totalPrice :: Bag Order → Bag LineItem → Z totalPrice orders lineItems = let orderIndex = groupBy fst orders orderSumIndex = Map.map (Bag.foldMapGroup snd ) orderIndex lineItemIndex = groupBy fst lineItems lineItemSumIndex = Map.map (Bag.foldMapGroup snd ) lineItemIndex merged = Map.merge orderSumIndex lineItemSumIndex total = Map.foldMapGroup multiply merged in total groupBy :: (a → k ) → Bag a → Map k (Bag a) groupBy keyOf bag = Bag.foldMapGroup (λa → Map.singleton (keyOf a) (Bag.singleton a)) bag

Fig. 10 :

 10 Fig. 10: Target language λ CAL (semantics of base terms and caches).

Fig. 10 and

 10 Fig. 10 and 11 have been omitted from the paper: they contains the operational semantics for λ CAL and λ ICAL .The rules for the evaluation of λ CAL change terms are similar to the evaluation rules of λ AL change terms except that (i) caches are carried along the computation and updated at return sites; (ii) there is no recomputation of base

  1, . . . , dv m) n (v1, . . . , vm) → (v 1 , . . . , v m ) if and only if (v1, . . . , vm) ⊕ (dv 1, . . . , dv m)= (v 1 , . . . , v m ) and ∀k < n, ∀i ∈ [1 . . . m], dv i k vi → v i • dE [λx dx . dt] n E1[λx . t] → E2[λx . t] if and only if E2 = E1 ⊕ dE and ∀k < n, v1, dv , v2, if dv k v1 → v2 then (dE ; x = v1; dx = dv dt) k (E1; x = v1 t) → (E2; x = v2 t) • (dE dt) n (E1 t1) → (E2 t2) if and only if ∀k < n, v1, v2, E1 t1 ⇓ k v1 and E2 t2 ⇓ v2implies that ∃dv , dE dt ⇓ dv ∧ dv n-k v1 → v2

  3.1 enables (a) computing v 2 from a valid change and its source, and (b) showing Eq. (1) through validity. As discussed, ⊕ ignores changes to closure bodies to be faster, which is only sound if those changes are nil; to ensure Theorem 3.1 still holds, validity on closure changes must be adapted accordingly and forbid non-nil changes to closure bodies. This choice, while unusual, does not affect our results: if input changes do not modify closure bodies, intermediate changes will not modify closure bodies either. Logical relation experts might regard this as a domain-specific invariant we add to our relation. Alternatives are discussed by Giarrusso [10, App. C].

Instead, Ahmed[START_REF] Ahmed | Step-indexed syntactic logical relations for recursive and quantified types[END_REF] and Acar et al.[START_REF] Acar | Imperative self-adjusting computation[END_REF] count the number of steps that small-step evaluation would take, but our choice simplifies some proof steps and makes a minor difference in others.

https://github.com/yurug/cts

The definition of this judgment (resp. the differentiation of term contexts) is omitted, but it mimicks the evaluation of terms (resp. the differentiation of terms).

Acknowledgments We are grateful to reviewers of previous versions of this paper: they made important suggestions to help us improve our technical presentation. This work was partially supported by DFG project 282458149.

Evaluation of change terms dF dM ⇓ (dV , Vc)

[TDResult] dF (dx ) = dV dF dC ⇓ Vc dF (dx , dC ) ⇓ (dV , Vc)

[TDTuple] dF ; dy = dF (dx ) dM ⇓ (dV , Vc)

dF let dy = (dx ) in dM ⇓ (dV , Vc)

Fig. 11: Target language λ ICAL (semantics of change terms and cache updates).

[CompleteNil] Thanks to this judgment, we can state the following key technical lemma whose proof represents a large part of our Coq formalization.

Lemma F.1 (Evaluation of derivatives commutes with evaluation of CTS derivatives).

Let t = C[t ] be a term and dE be a change environment.

If the following hypotheses hold:

Then the following conclusion holds:

Let us explain this statement in detail. The hypothesis (1) simply states the existence of a converging computation for the standard derivative of t. The hypothesis (2) makes explicit the change environment dE 0 under which t is evaluated by using an evaluation judgment for the derivative of C. 6 The hypothesis (3) (resp. ( 4)) completes the CTS version of dE 0 with the caches of the


Eric Leclerc

Les enjeux d'un aménagement urbain : le cas des villes anciennes de Mauritanie

Keywords: 4 heures Thèmes : VILLES, LIEUX, DEVELOPPEMENT

39): p. 19. 1

1. Mesure de l'évolution de l'urbanité Déroulement de la séance :

1) La ville comme Lieu

La séance commence par un positionnement théorique à propos de l'objet de l'étude : la ville. Le TD permet de s'interroger sur le concept de ville, souvent évacué des analyses car trop évident au pro>t d'études sur le contenu de la ville. P. Claval, premier des géographes français à affronter cette tâche d'une dé>nition du concept de ville, met en avant l'interaction comme propriété majeure : « la ville est une organisation destinée à maximiser l'interaction sociale ». Les implications spatiales de cette dé>nition ont été reprises par J. Lévy, à travers sa théorie de l'urbanité générale (chap 10, La ville un concept). Pour ce dernier, la ville est un objet de nature spatiale car il est l'une des réponses trouvée par l'homme pour lutter contre la distance « celle de la concentration des éléments d'une société en un point, celle de la centralité » (p 314). En ce sens on peut considérer la ville comme un lieu lorsqu'elle forme une unité spatiale où la distance s'annule. La ville crée de la société en concentrant dans le minimum d'espace (densité), le maximum d'objets sociaux (diversité). J. Lévy désigne par urbanité l'ensemble des effets productifs de l'objet spatial ville. La mesure du degré d'urbanité est fonction de la combinatoire entre les deux caractéristiques de la ville (diversité, densité). On applique ensuite cette approche au cas des villes anciennes de Mauritanie a>n d'évaluer l'impact des projets de développements sur la dynamique urbaine.

La Mauritanie est un Etat de l'Afrique de l'Ouest à la fois sahélien et ouvert sur l'océan Atlantique. Il se caractérise par un territoire immense, plus d'un million de km2, mais vide, un peu plus de 2 millions d'habitants en 1988. La population est concentrée dans le Sud, dans la vallée du Fleuve Sénégal, et de plus en plus dans les villes ce qui justi>e notre attention pour les évolutions divergentes de l'urbanisation dans ce pays, alors que 80% du territoire dans sa partie septentrionale est parcouru par les grands nomades Maures. Il faut également tenir compte de l'extrême discontinuité spatiale qui caractérise la Mauritanie et qui s'af>rme à travers les évolutions récentes.

La dé>nition de la ville en Mauritanie est mouvante, changeant à chaque enquête ou recensement. Seules les capitales régionales ont été retenues en 1962, indépendamment de leur taille démographique et de leur fonction économique. Le recensement de 1977 complète ce critère administratif par un seuil numérique : 5.000 habitants, maintenu en 1988.

2) La situation alarmante des villes anciennes

La transition urbaine en Mauritanie a été particulièrement brutale. Depuis l'Indépendance, le développement de l'Etat et la nouvelle gestion du territoire se sont appuyés sur la construction d'un réseau urbain pour parvenir à ce but quitte à multiplier les créations ex-nihilo dont Nouakchott est le prototype et l'aboutissement. S'y ajoutent un bouleversement démographique et une crise climatique pour enclencher un processus rapide d'urbanisation. Malgré leurs lacunes, les statistiques disponibles donnent une idée de la rapidité des évolutions. En 1965, l'enquête de la SEDES estimait le taux d'urbanisation à 7 % soit 76 000 citadins, alors qu'en 1950 la population urbaine était estimée à 25 000 personnes (3 % de la population totale). En 1988 les citadins, un peu plus de 700 000, sont devenus pratiquement aussi nombreux (40%) que les sédentaires ruraux (48%). Le nombre des villes administratives est passé de 16 en 1977 à 22 en 1988, puis 25 en 1995. Il s'agit dans un premier temps de replacer les villes anciennes qui sont au nombre de 4 (Ouadane, Chinguetti, Tichit, Oualata) dans le réseau urbain mauritanien actuel, a>n de mesurer l'ampleur de leur déclin récent. A partir des documents 1, 2 et 3, on peut souligner leur position périphérique et les risques de disparition de celles-ci. On assiste à la mort des villes par déclin de l'urbanité absolue suite à la disparition de l'activité principale, le commerce.

4) Le refus de l'abandon, le choix du développement

Pourtant le destin de ces 4 villes (Ouadane, Chinguetti, Tichit, Oualata) est remis en question avec la création de la Fondation Nationale pour la Sauvegarde des Villes Anciennes en 1993. Il s'agit de la transformation de ces 4 villes en éléments du patrimoine national et mondial (lancement d'une campagne de sauvegarde des villes anciennes sous l'égide de l'UNESCO en 1981). Ces villes deviennent des lieux de mémoire avec la valorisation de Chinguetti, 7° ville sainte de l'Islam. Ici la notion de lieu peut être d'abord considérée d'un simple point de vue géométrique (opposition point/surface). Mais certains lieux peuvent acquérir une valeur collective au point de se hisser (ou plutôt d'être hissé) au rang de symbole. Lieu acquiert une valeur patrimoniale = Lieux de mémoires. Cette valorisation s'accompagne d'une politique de développement. On cherche alors à faire comprendre aux étudiants les raisons de cette réintégration des villes anciennes dans le territoire national, au moins comme symbole. Mais dans un second temps, l'analyse critique du choix des opérations de développement doit permettre de véri>er si elles peuvent faire renaître des objets urbains, c'est à dire effacer la distance par la coprésence et favoriser les interactions.

Document 6 : Projet de développement

Les objectifs sont multiples : 1. Lieu de production = vers l'autosuf>sance alimentaire 2. Le développement d'infrastructures urbaines (adduction d'eau, ce que n'a même pas le cheflieu de région Néma).

3. Lieu de mémoire national (bibliothèque pour conserver les manuscrits)

Nouvelle position dans le tourisme mondial

On peut aussi interpréter le choix de ces lieux pour le développement par rapport à la politique d'arabisation entamée depuis 1973 avec l'adhésion à la Ligue arabe. Ancrage de l'identité du territoire au Nord et dans son passé Maure. Projet de développement = Momi>cation de la ville => >ger sa position.

5) Peut-on toujours parler de ville ?

Toutes les actions menées pour maintenir en vie, voir revitaliser les villes anciennes, visent à briser leur enclavement dans un soucis de réintégration dans le réseau urbain et le territoire national. On doit alors s'interroger sur le degré d'urbanité de ces villes en mesurant la somme des interactions des systèmes urbains (urbanité absolue) et en la comparant au potentiel des interactions (urbanité relative). Il ne s'agit pas de la mesure statistique de ces paramètres mais d'une évaluation qualitative réalisable avec les étudiants à partir de deux documents, l'un décrivant le maintien d'une activité commerciale (approche de la densité), l'autre portant sur les effets productifs de la ville sur la société (approche de la diversité).

Document 1 : Carte du réseau urbain mauritanien

  Kiffa-Néma. Oualata et les autres villes anciennes sont dans un angle mort du territoire national. A l'inverse Nouakchott est devenue en seulement 40 ans la principale ville du pays tant du point de vue démographique (passant d'un village de 500 âmes en 1950 à 393.325 habitants en 1988) que politique. Cette fantastique concentration qu'aucune ressource locale ne justi>e marque la profonde transformation de la société mauritanienne rassemblée aujourd'hui pour un quart dans une seule ville. Plus qu'une courante macrocéphalie, il faut ici souligner la cristallisation en un lieu d'une société en recomposition, au point de se demander si la Mauritanie ne se fond pas aujourd'hui dans sa capitale.Teghaza) contre l'or et les esclaves du Soudan. Ce sont des villes étapes qui assurent le repos et le ravitaillement des caravanes, mais également leur sécurité au point que les pistes prennent le nom des tribus qui en assurent le contrôle ainsi dès le IX° siècle la piste transsaharienne de l'Ouest devient la route des Lemtouna. L'histoire de cette route est celle d'un lent glissement vers l'Est commandé par l'évolution des têtes de pont situées au Maghreb et plus au Sud au Sahel sur les royaumes qui contrôlent le commerce de l'or. Ces villes de part et d'autre du Sahara sont le plus souvent également les capitales politiques des royaumes qui se succèdent. On peut suivre pour illustrer ces évolutions la position de Oualata  Sous le nom de Birou, Oualata l'une des grandes villes de l'Empire du Ghana VII°-XI°s iècles dont le centre de gravité est situé dans les Hodh. Koumbi saleh, la capitale de l'Empire qui n'est plus aujourd'hui qu'un vestige archéologique n'est qu'à 250 km au SW. Avec la chute de l'Empire sous les coups des almoravides (1077), Oualata récupère une partie de l'activité de l'ancienne capitale détruite. Dans l'Empire du Mali qui lui succède (XII°-XIV°), puis l'Empire songhaï (XIV°-XV°), Oualata a une position plus marginal (occidentale), son rôle politique décline au pro>t d'un rôle plus culturelle (élite intellectuelle).

	1988	393 325	10,7
	1995*	579 130	5,7
	2000*	728 635	4,7
	* projection
	Document 2 : ∆ démographique des villes mauritaniennes
	faiblesse de l'urbanisation en 1950 = 3%, 1962 = 7% avec une population à 78% nomade en 1965
	(1988 = 12%).
	Colonisation française par l'E, Oualata soumise en 1912, elle dépend alors de Tombouctou.
	Mais dès 1945 les Hodh sont rattachés à la Mauritanie. Dans ce nouveau territoire, Les villes anciennes dépérissent. Vont elles subir le même sort qu'Aoudagost ou Koumbi saleh, Oualata se trouve à plus de 1.000 km de la nouvelle capitale St Louis du Sénégal! ou plus disparaître ? tard Nouakchott (1960).
	3) Une position héritée
	Dans le nouvel Etat mauritanien, les deux axes de communication principaux sont vers le Nord-Une analyse diachronique va permettre de comprendre la genèse de ces 4 villes devenues Est Rosso-Nouakchott-Atar-Zouérate et ses mines de fer, et d'Ouest en Est le grand axe de la Population Accroissement annuel anciennes ainsi que le déclin de leur position dans le territoire. Il s'agit d'évaluer ici pour les villes anciennes, et plus particulièrement Oualata, la somme des interactions quelles sont capables route de l'espoir Nouakchott-Année de générer, ce qui revient à mesurer l'urbanité absolue de ces lieux.
	1962	5 807
	1977	138 530	23,5

 1962 : Les villes sont très petites, au maximum 10.000 habitants et la plus grande est Atar, capitale de l'Emirat de l'Adrar.

 1977 : Faiblesse des villes anciennes qui sont déjà sur le déclin avec une population inférieure à 3.000 habitants ce qui les exclues de la catégorie of>cielle des villes. Par contre évolution rapide au pro>t de la capitale avec déjà un phénomène de macrocéphalie.

 1988-95 : Poursuite des tendances précédentes, Nouakchott = 56 % de la population. Si les villes anciennes semblent freiner (Ouadane) voir inverser (Chinguetti, Oualata) l'évolution démographique, les valeurs de 1995 sont plus proches de la réalité car les données du recensement semblent surestimées. Document 3 :Plan de Oualata Agonie d'une ville :  émigration des populations. En 1912 elle ne comptait déjà plus que 1.600 habitants, aujourd'hui 931 of>ciellement (recensement électoral) mais plus près de 500 réellement d'après les études de terrain soit -70% en 80 ans!  abandon de l'habitat avec destruction et ensablement  nouvelle fonction peu peuplante : relégation des prisonniers politiques. Document 4 et 5 : Texte 4 / carte de l'évolution des routes transsahariennes Des villes très prospères par leur position de pivot, au contact du Sahel et du Sahara, tour à tour relais ou moteur dans le commerce transsaharien approvisionné au nord par des produits manufacturés (tissus, armes) auquel s'ajoute le sel extrait au coeur du Sahara (salines d'Idjil,  Le destin de Oualata dépend de sa place sur les routes transsahariennes. Déjà important à l'époque de l'Empire du Ghana, l'étape de Oualata devient incontournable lorsque les pistes les plus occidentales sont abandonnées à la suite de la conquête almoravide. Etape sur la route d'Idjil (salines) / Tombouctou. Ibn Battouta qui y fait étape la décrit en 1352 comme une place dynamique et prospère. La fortune de Oualata décroit avec le déplacement des routes vers l'E. Le retournement de la position :  Le déclin des villes sahéliennes résulte de celui des =ux transsahariens avec un double retournement :  1°) Vers le Sud (Soudan) --> côte avec la conquête européenne par l'océan Atlantique et le golfe de Guinée = Oualata trop au N.  2°) Vers l'Ouest : conquête par le =euve Sénégal, axe E --> W, qui permet d'atteindre directement les ressources en or = Oualata trop loin du =euve.

Document 7 : Texte sur commerce Côte d'Ivoire /Mauritanie

  L'étude de Oualata montre que l'enclavement n'est pas un obstacle. Il existe une forte activité des grands commerçants qui ont ré-orienté leurs activités commerciales. Il existe toujours un commerce d'envergure nationale et internationale dont le siège est situé à Oualata.  Commerce du bétail : Hodh grande région d'élevage (50% du PIB avant la sécheresse), vente des animaux au détail sur le marché de Nouakchott ou villes au Sud jusqu'à Abidjan! forts pro>ts car demande urbaine (grandes métropoles).  Commerce de produits manufacturés : achat à Nouakchott, Bamako ou Abidjan suivant les différences de prix entre les lieux. Ex : pièces détachées automobiles achetées à Bamako et revendues à Nouakchott.  Commerce de produits vivriers : achat au Mali ou auprès de l'aide internationale -> stockage à Oualata / Néma expédition à Nouakchott lorsque les prix sont + élevés. Oualata a réorganisé ses =ux commerciaux dans l'espace et les a adaptés aux nouvelles structures territoriales (Etat). Oualata joue toujours le rôle de centre dans le commerce international (virtuel lorsque la marchandise ne passe plus physiquement par la ville), avec des succursales dans les lieux d'approvisionnements et de vente. Oualata n'est pas enclavée! L'obstacle de la distance, souvent invoqué expliquer le déclin des villes anciennes n'est pas recevable. En ce sens, Oualata demeure une ville car elle a la capacité d'annuler la distance. L'urbanité absolue est cependant en déclin car le volume des interactions ici commerciales a diminué depuis son heure de gloire. Il reste à véri>er si le maintien d'une certaine activité commerciale produit encore de la société. Chorfa soit Oulad Dawud (c-a-d les tribus maraboutiques) qui constituent l'élite socio-politique de Oualata. Les tribus nomades représentées, Kounta (marabouts) / Oulad Bella (guerriers) sont en situation de dépendance. Or cette élite commerçante minimise les interactions sociales a>n de maintenir les positions acquises. Elles freinent le désenclavement de Oualata car celui-ci permet le maintien des relations de clientélisme (se sont les seules tribus à contrôler les haratines, 60% de la population). La réunion de tous ces groupes sociaux à Oualata (12 tribus) ne provoquent pas une plus grande interaction, il n'y pas d'effet productif sur la société, l'urbanité relative y est donc faible. Le facteur de l'enclavement souvent évoqué pour expliquer le déclin des villes anciennes dont Oualata est insuf>sant. En effet si le volume des activités commerciales a baissé, soit une perte d'urbanité absolue, il n'a pas totalement disparu. L'élite socio-politique organise toujours un Zawaya Les pourcentages sont effectués en colonne, les effectifs sont donnés entre parenthèse 102 = nombre de personnes interrogées 26 = nombre total de commerçants (activité principale)

	Document 8 : Tableau activités et tribus Rappel de la structure de la société Maure pour interpréter le tableau :  Ordres nobles  Guerriers (hassan)  Marabouts (zawaya)  Ordres soumis  Tributaires  Artisans  Hommes non libres (donc rattachés à une tribu appartenant à l'un des deux ordres nobles ci-dessus)  Affranchis (haratines)  Esclaves Cependant ces activités de grand commerce concernent une minorité de personnes (moins de 10) TRIBU/STATUT SOCIAL LIBRE FORGERON HARATINE TOTAL COMMERCANT CHORFA (Z) 20,8% ( 10) 16,7% ( 1) 52,1% ( 25) 35,0% ( 36) 26,9% ( 7) IDHEYLBA (Z) 16,7% ( 1) 1,0% ( 1) 3,8% ( 1) KOUNTA (Z) 10,4% ( 5) 2,1% ( 1) 5,8% ( 6) 3,8% ( 1) LAGHLAL (Z) 4,2% ( 2) 1,9% ( 2) 3,8% ( 1) LAGHMOUNAT (H) 10,4% ( 5) 4,9% ( 5) 3,8% ( 1) LEMTOUNA (Z) 2,1% ( 1) 1,0% ( 1) MEHAJIB (Z) 10,4% ( 5) 2,1% ( 1) 5,8% ( 6) 3,8% ( 1) NEMADI (H) 6,3% ( 3) 2,9% ( 3) 3,8% ( 1) OULAD BELLA (H) 10,4% ( 5) 4,9% ( 5) 11,5% ( 3) OULAD DAWUD (Z) 12,5% ( 6) 66,7% ( 4) 37,5% ( 18) 28,2% ( 28) 30,8% ( 8) OULAD NASSER (H) 4,2% ( 2) 1,9% ( 2) TEJEKANT (Z) 12,5% ( 6) 2,1% ( 1) 6,8% ( 7) 7,7% ( 2) TOTAL 100% ( 48) 100% ( 6) 100% ( 48) 100% (102) 100% ( 26) qui sont soit Document 8 (H) = Hassan (Z) =