Discover Top Posts Tagged with #incrementalization

Paolo G. Giarrusso - A Theory of Changes for Higher-Order Languages - Incrementalizing λ-calculi by Static Differentiation

Paolo motivates incrementalization, and walks through an example of incrementalizing a sum operation. In the presentation, he uses special "circle" operators (circle plus and circle plus) to represent calculating the diff, and applying the result of the differential to the old result. The language here is pretty suggestive.

So as it turns out, these operators are going to play a key role in the algebraic theory they're interested in. Types: V (base set), delta v (change set for v), (+) : (v : V) -> delta v -> V, (-) : (v : V) -> V -> delta v, obeying some laws (e.g. cancellation)

NB: change set might be different from base set. Example: for natural numbers, delta v is integers z such that z + x is a nat. (-4 is not delta 3)

How to incrementalize? Static differentiation? (ezyang: Is this the same as symbolic differentiation?) Correctness: [[ f (a (+) da) ]] = [[ f a (+) Derive(f) f da ]]

Well, actually, we don't have dependent types

Well, watch out: it's not derivatives, but function changes. Not f' x dx = f x2 (-) f x1 = y2 (-) y1, but df x dx = f2 x2 (-) f1 x1 = ... Function changes are necessary for application, since the function could change. delta (T -> U) = T -> delta T -> delta U

Setting: language plugins which define datatypes and change structures / primitives.

They did a case study on map reduce

Correctness proof uses logical relations!

Q: How do you compute the derivative of a function? E.g. for a fold function, it has to assume the input is a valid group.

A: We provide a primitive which assumes that the it gets a group operation, then the designer of the language plugin provides the derivative. (So fold is a primitive?) Yes, fold is a primitive. Since we are a higher order language, we can have a few primitives, such as fold, and then other operations can be derived from it.

Q: For some functions, derivatives won't be defined. Does your system allow the developer to recognize them? Or does this have to be recognized. (I.e. mathematical derivative?)

A: Well, watch out, this is different from mathematics. Actually, the derivative always exists, the real question is whether or not it is efficient. Sometimes this is impossible. But you can often provide more general primitives. We are limited to simple examples. We don't have support yet for caching intermediate results.

Q: Could you say more about the description of change in datatype? You have support for bag and map. Can I have changes for the values contained?

A: Something better to do, a change to a bag, is add/remove/change, and the change is just the change type for T. This is more efficient. We did not do it in the case study, since it still requires (indistinct), there is past work which we should reuse, Liu&Teitelbaum '95

Q: What is the programming interface. Can I use this to take derivatives in my program?

A: Our language is embedded as a DSL. Inside the DSL, you don't, but outside you can take derivatives and apply changes. So... yes.

#pldi #pldi14 #incrementalization