Exercise 1.8: Implementation of inline_formula not implemented
(require [sicmutils.env :refer :all])
Part A: Implement inline_formula not implemented
The goal here is to implement inline_formula not implemented as a procedure. Explicitly:
Suppose we have a procedure
f
that implements a path-dependent function: for pathq
and timet
it has the value((f q) t)
. The procedure delta computes the variation inline_formula not implemented as the value of the expression((((delta eta) f) q) t)
. Complete the definition ofdelta
:
After laboriously proving all of the properties above, the actual implementation feels so simple.
The key is equation 1.22 in the book:
formula not implementedGiven inline_formula not implemented. Through the magic of automatic differentiation we can simply write:
(defn delta [eta]
(fn [f]
(fn [q]
(letfn [(g [eps]
(f (+ q (* eps eta))))]
((D g) 0)))))
It's almost spooky, that inline_formula not implemented can somehow figure out what to do here.
Part B: Check inline_formula not implemented's properties
Part B's problem description gave us a path-dependent function similar to this one:
(defn litfn [sym]
(fn [q]
(let [Local (UP Real (UP* Real 2) (UP* Real 2))
F (literal-function sym (list -> Local Real))]
(compose F (Gamma q)))))
I've modified it slightly to take in a symbol, since we'll need to generate multiple functions for a few of the rules.
inline_formula not implemented takes a symbol like inline_formula not implemented and a path function – a function from inline_formula not implemented to any number of coordinates (see the UP*
?) – and returns a generic expression for a path dependent function inline_formula not implemented that acts via inline_formula not implemented. inline_formula not implemented might be a Lagrangian, for example.
The textbook also gives us this function from inline_formula not implemented to test out the properties above. I've added an inline_formula not implemented of the same type signature that we can use to add variation to the path.
(def q (literal-function q (-> Real (UP Real Real))))
(def eta (literal-function eta (-> Real (UP Real Real))))
These weren't easy to write down, but they really do constitute proofs. If you trust the system managing the algebra, then the equalities here are general. This is an area of computing I haven't worked with much, but I'm left with the eery feeling that these are more powerful than any tests I might have decided to write, if I weren't guided by this exercise.
Variation Product Rule
Equation \eqref{eq:var-prod} states the product rule for variations. Here it is in code. I've implemented the right and left sides and subtracted them. As expected, the result is 0:
(let [f (litfn f)
g (litfn g)
de (delta eta)
left ((de (* f g)) q)
right (+ (* (g q) ((de f) q))
(* (f q) ((de g) q)))]
((- left right) t))
Variation Sum Rule
The sum rule is similar. Here's the Scheme implementation of equation \eqref{eq:var-sum}:
(let [f (litfn f)
g (litfn g)
de (delta eta)
left ((de (+ f g)) q)
right (+ ((de f) q)
((de g) q))]
((- left right) t))
Variation Scalar Multiplication
Here's equation \eqref{eq:var-scalar} in code. The sides are equal, so their difference is 0:
(let [g (litfn g)
de (delta eta)
left ((de (* c g)) q)
right (* c ((de g) q))]
((- left right) t))
Chain Rule for Variations
To compute the chain rule we'll need a version of fn
that takes the derivative of the inner function:
(defn Dfn [sym]
(fn [q]
(let [Local (UP Real (UP* Real 2) (UP* Real 2))
F (literal-function sym [-> Local Real])]
(compose (D F) (Gamma q)))))
For the Scheme implementation, remember that both fn
and Dfn
have inline_formula not implemented baked in. The inline_formula not implemented in equation \eqref{eq:var-chain} is hardcoded to inline_formula not implemented in the function below.
Here's a check that the two sides of equation \eqref{eq:var-chain} are equal:
(let [h (litfn F)
dh (Dfn F)
de (delta eta)
left (de h)
right (* dh (de Gamma))]
(((- left right) q) t))
inline_formula not implemented commutes with inline_formula not implemented
Our final test. Here's equation \eqref{eq:var-commute} in code, showing that the derivative commutes with the variation operator:
(let [f (litfn f)
g (compose D f)
de (delta eta)
left (D ((de f) q))
right ((de g) q)]
((- left right) t))