We want to maintain the sequence of iterations of some function f,
f: I × S → S
I: “input” from external world - list of edges, for example S: “state” of iteration, needs an initial value - a frontier, for example
iterate : I × S → Stream S iterate (input, state) = state :: iterate (input, f (input, state))
iterate –> state :: f (input, state) :: f (input, f (input, state)) :: …
how do we maintain this with respect to changes in input, I?
figure out how f responds to changes, eg.
f : I × S → S f’ : I × S → ΔI × ΔS → ΔS
s0 –f–> s1 –f–> s2 –f–> s3 –f–> …
– maybe it’s this???
iterate : I × S → Stream S iterate (input, state) = state :: iterate (input, f (input, state))
iterate’ : I × S → ΔI × ΔS → Stream ΔS iterate’ (input, state) (δinput, δstate) = δstate :: (iterate’ (input, f (input, state)) (δinput, f’ (input, state) (δinput, δstate)))
iterate’ : I × Stream S → ΔI × ΔS → Stream ΔS iterate’ (input, state :: states) (δinput, δstate) = δstate :: (iterate’ (input, states) (δinput, f’ (input, state) (δinput, δstate)))
Δ(A × B) = ΔA × ΔB Δ(A + B) = ΔA + ΔB
Δ(A + B)(inl x) ~= ΔA Δ(A + B)(inr x) ~= ΔB inl (x: A) inr (dy: ΔB)
Change Structure
M: “intermediate state” saved b/w initial run & delta update
f1 : I × S → S × M fΔ : M → ΔI × ΔS → ΔS × M
Intermediate state for “iterate” is (Stream M).
iterate1 : I × S → Stream S × Stream M iterateΔ : Stream M → ΔI × ΔS → Stream ΔS × Stream M