An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

Semantics of higher-order incremental computation
Mario Alvarez-Picallo

Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

Acknowledgements
This research is funded by the EPSRC and the Oxford Computer
Science department, and supervised by professors Luke Ong andSamson Abramsky.

Part of this research was performed while I was working for
Semmle Ltd. and in close collaboration with the team there, inparticular Michael Peyton-Jones and Alex Eyers-Taylor.

Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

Outline1

An overview of incremental computation2

Difference algebras and differentiable maps

3

Higher-order derivatives

4

The future

Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

What is incremental computation?

We want to compute the value of some (expensive) function f
on some input x
The value of x changes over time, taking a sequence of values
x1 , x2 , . . .
We want to update the value of f (x) as xi changes...
...but it may be very expensive to compute f (xi ) from scratch!

Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

What is incremental computation?
Interpret the xi as applying successive “updates” ∆xi to an
initial value x1 :x2 = x1 + ∆x1x3 = x2 + ∆x2 . . .
Find ∆yi such that:f (x2 ) = f (x1 + ∆x1 ) = f (x1 ) + ∆y1
f (x3 ) = f (x2 + ∆x2 ) = f (x2 ) + ∆y2 . . .
(Optional) Make sure computing f (xi ) + ∆yi is cheaper thancomputing f (xi+1 )How to find the ∆yi ? Many approaches!
Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

The compositional approach to incremental computation
A general approach is to seek a function f 0 of the base state xi andthe update ∆xi that allows us to compute the ∆yi .
Most approaches make some restrictions on the kind of function f 0
is, most commonly it’s required that it depends only on ∆xi .
Ideally, we know g 0 for all the primitives of our language.
Then we only need a way to obtain (g ◦ f )0 from f 0 and g 0 !

Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

Cai and Giarrusso’s approach
In a recent paper, Cai, Giarrusso et al.1 introduce a theoreticalframework for making these ideas precise.
They introduce the notion of change structure, which provides asemantics for a type X whose elemnts can be updated with“changes” of type ∆X .
Their work also introduces compositional ways of obtaining
incrementalized versions (“derivatives”) of functions
compositionally, as a source-to-source transformation.
1. Cai, Giarrusso et al, PLDI 2016

Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

Change structures in detail
Change structures
A change structure is a tuple (A, ∆A, ⊕, ) such that:
A is a set
For every a ∈ A, ∆Aa is a set⊕ is a (dependent) function of type (x : A) → ∆Aa → A
is a (dependent) function of type A → (x : A) → ∆Axx ⊕ (yx) = yIntuition: ∆Aa is the type of changes that are applicable to somevalue a.
Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

Change structures, continued
Derivatives
Given a function f : A → B and change structures on A and B, aderivative for f is a function f 0 : (a : A) → (da : ∆Ax ) → ∆Bf (a)such that:f (a ⊕ da) = (f a) ⊕ (f 0 a da)Note that every function is differentiable, because
λ x dx.f (x ⊕ dx) (f x) is a derivative.
Given some λ-term Γ ` t : B, Giarrusso and Cai provide asource-to-source transformation Derive to find a derivative.

Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

Problems in paradise
Some problems with Cai and Giarrusso’s approach.
Every function is differentiable!
Requires dependent types!
More complicated theory (can’t use simply-typed λ-calculus)
In practice: either limiting or just ignored...
Always working with sets, not adequate for domains!
⊥ ⊕ (a⊥) = aDerive is not first-class
In some cases, not clear what
Mario Alvarez-Picalloshould be, e.g. lists!
Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

Outline1

An overview of incremental computation2

Difference algebras and differentiable maps

3

Higher-order derivatives

4

The future

Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

An alternative to change structures

Difference algebra
A difference algebra A is a tuple (A, ∆A, ⊕, +, 0) such that:(∆A, +, 0) is a monoid⊕ : A → ∆A → A is an action of ∆A on A, i.e.:
1
2

a⊕0=a
a ⊕ (da + db) = (a ⊕ da) ⊕ db

Fulfills same purpose as a change structure, but! No dependent
types, no .

Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

An alternative to change structures

Derivatives between difference algebras
Given a function f : A → B and difference algebras on A and B, aderivative for f is a function f 0 : A → ∆A → ∆B such that:f (a ⊕ da) = (f a) ⊕ (f 0 a da)Same as with change structures, minus the dependent types!
Note that all functions are no longer differentiable!

Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

The chain rule
Theorem
Given f : A → B, g : B → C differentiable maps with derivatives
f 0 , g 0 , then the following is a derivative for g ◦ f :(g ◦ f )0 (a)(da) = g 0 (f a, f 0 a da)
This is in fact the same as the chain rule from multivariate
calculus! If Da f is the differential of f at a, then:Da (g ◦ f ) = Df (a) g ◦ Da f
But unlike in calculus, here derivatives may not be unique!
Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

A category of difference algebras
The category DAlg
We define a category DAlg of difference algebras as follows:
The objects of DAlg are difference algebras
A = (A, ∆A, ⊕, +, 0)
The morphisms in DAlg are differentiable functions.
Identities and composition are as in Set

The chain rule guarantees that composition behaves well!

Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

The structure of DAlg

DAlg is a well-behaved category, it has:
Products (nice!)
Coproducts (nice!)
Exponentials (evil!)

Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

Products in DAlg
Product of difference algebras
Given difference algebras A, B, their product difference algebra
A × B is given by:
A × B = (A × B, ∆A × ∆B, ⊕× , +× , 0× )(a, b) ⊕× (da, db) = (a ⊕ da, b ⊕ db)(da1 , db1 ) +× (da2 , db2 ) = (da1 + da2 , db1 + db2 )0× = (0, 0)This is, in fact, the categorical product in DAlg!

Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

Coproducts in DAlg

Coproduct of difference algebras
Given difference algebras A, B, their coproduct difference algebra
A + B is given by:
A + B = (A + B, ∆A × ∆B, ⊕+ , ++ , 0+ )a ⊕+ (da, db) = a ⊕ dab ⊕+ (da, db) = b ⊕ db
(da1 , db1 ) ++ (da2 , db2 ) = (da1 + da2 , db1 + db2 )0+ = (0, 0)

Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

Exponentials in DAlg

Theorem
The category DAlg is equivalent to the category PreOrd ofpreorders and monotone functions.

...

...and PreOrd is a CCC, therefore so is DAlg.

Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

Exponentials in DAlg
Second attempt:
Exponential difference algebras
Given difference algebras A, B, the exponential A ⇒ B is given by:
A ⇒ B = (A ⇒ B, A ⇒ ∆B, ⊕⇒ , +⇒ , 0⇒ )(f ⊕⇒ df )(a) = f (a) ⊕ df (a)(df +⇒ dg )(a) = df (a) + dg (a)0⇒ (a) = 0
This almost works!
The problems: can’t guarantee f ⊕⇒ df is differentiable, ev isn’t
differentiable.
Requires higher derivatives!
Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

Another category of difference algebras
The category DAlg?
We define the category DAlg? of difference algebras as follows:
The objects of DAlg are difference algebras
A = (A, ∆A, ⊕, +, 0)
The morphisms in DAlg are pairs f = (f , f 0 ) where f is adifferentiable function and f 0 is a derivative of it.
The identity maps are Id = (Id, π2 )Composition is given by:(g , g 0 ) ◦ (f , f 0 ) = (g ◦ f , g 0 ◦ f ◦ π1 , f 0 )Products and coproducts are like in DAlg, but no exponentials!
Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

Outline1

An overview of incremental computation2

Difference algebras and differentiable maps

3

Higher-order derivatives

4

The future

Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

Higher-order derivatives

The problems with DAlg and DAlg? come from a lack ofhigher-order derivatives.

To get higher-order derivatives, we require:
A difference algebra structure on the difference sets ∆A
A suitable definition of smoothness of a function f

Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

Higher-order derivatives, the easy way

Let (A, ∆A, ⊕, +, 0) be a difference algebra.
Higher difference algebras
There’s a natural difference algebra structure on ∆A given by(∆A, ∆A, +, +, 0).
Whenever + is commutative and ⊕ is differentiable w.r.t. its firstargument, we will say (A, ∆A, ⊕, +, 0) is smooth.

Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

Higher-order derivatives, the easy way

Smooth functions between difference algebras
Let A, B be smooth difference algebras. We say that f : A → B issmooth whenever its derivative f 0 exists and it is a smooth map
when considered as a function f 0 : A × ∆A → ∆B

Essentially, a smooth function f is one for which all higher
derivatives f 0 , f 00 , . . . exist (with respect to the higher difference
algebras described before).

Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

Higher-order derivatives, the easy way
We’re not quite there yet. To obtain a CCC, we need to ensure
functions have a unique derivative.
Fortunately, there’s a very simple condition to impose on adifference algebra to ensure uniqueness of derivatives!
Thin difference algebras
A difference algebra is thin if whenever a ⊕ da = a ⊕ db, it is thecase that da = db.
Lemma
Let B be a difference algebra. Then the following are equivalent:
B is thin.
For every difference algebra A and every funciton f : A → B,
f has at most one derivative.
Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

Higher-order derivatives, the easy way

The category DAlg∆
We define the category DAlg∆ of difference algebras as follows:
The objects of DAlg∆ are smooth, thin difference algebras.
The morphisms between A and B in DAlg∆ are smoothfunctions f : A → B.
Identity maps and composition are as in Set.

It can be shown that DAlg∆ is a CCC, with products andexponentials as described previously for DAlg!

Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

Higher-order derivatives, the hard way
The previous category imposes too many requirements its objects.
It’s possible to generalize it in three ways:
The difference algebra structure on ∆A does not need to be
the one that arises from its monoid structure.
Derivatives do not need to be unique, as long as every map
carries its own derivative.
The monoid operation + does not need to be commutative,
as long as it is smooth.
One would expect that it is possible to relax these three conditions
and still obtain a CCC.

Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

Higher-order derivatives, the hard way

Difference stacks
A difference stack Â is a sequence (Ai ) where:
Every Ai is a difference algebra.
∆Ai = Ai+1

A sequence of functions (fi ) is called a smooth map wheneverf0 : A0 → B0 and fi+1 is a derivative of fi .
This generalizes difference algebras in the first and second points!

Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

Higher-order derivatives, the hard way
Projection of difference stacks
Given a difference stack Â = (Ai ), its n-th projection Πn Â is thedifference stack (Πn Â)i = (Ai+n )Smooth difference stacks
A difference stack Â is smooth whenever every one of its structuremaps ⊕i , +i is a smooth map between the relevant difference
stacks, i.e.
⊕i is a smooth map from Πi Â × Πi+1 Â into Πi Â
+i is a smooth map from Πi+1 Â × Πi+1 Â into Πi+1 Â
This generalizes difference algebras in the third point!
Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

Higher-order derivatives, the hard way
The category of smooth difference stacks
We define the category DStack? of difference stacks as follows:
The objects of DStack? are smooth difference stacks.
The morphisms between Â and B̂ in DAlg? are smooth mapsfˆ = (fi ).
Theorem
The category DStack is Cartesian closed.
Theorem (Internalization)
There is a smooth map ∂ : Â ⇒ B̂ → Â ⇒ ∆B̂ that sends every
map to its first derivative.
Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

Outline1

An overview of incremental computation2

Difference algebras and differentiable maps

3

Higher-order derivatives

4

The future

Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

Categorifying DAlg
All these constructions so far are on Set, but the category DAlg?
can be built on top of any Cartesian category C
What’s more, DAlg? can be raised to an endofunctor on the
category of Cartesian categories and product-preserving maps!
Question: does DStack? arise as a projective limit?
DStack? (C)C

DAlg? (C)DAlg? (DAlg? (C))...

And is such a construction always a CCC whenever C is?
Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

The differential geometry of difference algebras
There seems to be a connection between difference algebras andnotions in differential geometry.
Derivatives, the chain rule, smoothness, etc. are suggestive names.
Can the connection be made precise?
Conjecture: the Kleisli category of the tangent bundle monad on a
Cartesian differential category is a category of difference algebras.
Conjecture: certain categories of difference algebras (whena ⊕ da = a +  da) where  is a nilpotent homomorphism) aremodels of synthetic differential geometry
Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

Change structures on domains, recursion and PCF
Change structures can be defined on domains. Is the fixpoint
combinator smooth? What is its derivative?
Most of the work already done, answer is (under suitableconditions, like continuity of ⊕) yes!
Can this be a model of incremental PCF?
Most importantly: derivatives up-to the domain order:f (x) ⊕ f 0 (x, dx) v f (x ⊕ dx)(with a reasonable maximality condition on f 0 (x, dx))
Mario Alvarez-Picallo

Semantics of higher-order incremental computation

An overview of incremental computation
Difference algebras and differentiable maps
Higher-order derivatives
The future

Mario Alvarez-Picallo

Semantics of higher-order incremental computation