% -*-Latex-*-
%if False
> module Applications
> import Syntax.PreorderReasoning
> import Data.Vect
> import About
> import Functors
> import Monads
> %default total
> %auto_implicits off
> %access public export
> %hide Prelude.List.last
> DetSys : Type -> Type
> DetSys X = X -> X
> flowDet : {X : Type} -> DetSys X -> Nat -> DetSys X
> flowDet f Z = id
> flowDet f ( S n) = flowDet f n . f
> lastLemma : {A : Type} -> {n : Nat} ->
> (x : A) -> (xs : Vect (S n) A) -> last (x :: xs) = last xs
> lastLemma x (y :: ys) = Refl
%endif
\section{Applications in dynamical systems and control theory}
\label{section:applications}
In this section we discuss applications of the principle of preservation
of extensional equality to dynamical systems and control theory.
%
We have seen in section \ref{section:example} that time discrete
deterministic dynamical systems on a set |X| are functions of type |X -> X|
< DetSys : Type -> Type
< DetSys X = X -> X
and that generalizing this notion to systems with uncertainties leads to
monadic systems
> MonSys : (Type -> Type) -> Type -> Type
> MonSys M X = X -> M X
where |M| is an \emph{uncertainty} monad: |List|, |Maybe|, |Dist|
\citep{10.1017/S0956796805005721}, |SimpleProb|
\citep{2017_Botta_Jansson_Ionescu}, etc.
%
For monadic systems, one can derive a number of general results.
%
One is that every deterministic system can be embedded in a monadic
systems:
> embed : {X : Type} -> {M : Type -> Type} -> Fat.VeriMonadFat M => DetSys X -> MonSys M X
> embed f = pure . f
A more interesting result is that the flow of a monadic system is a monoid morphism from |(Nat, (+), 0)| to |(MonSys M X, (>=>),
pure)|.
%
As discussed in section~\ref{section:example}, |flowMonL <=>
flowMonR| and here we write just |flow|.
%if False
> flow : {M : Type -> Type} -> {X : Type} -> Fat.VeriMonadFat M =>
> MonSys M X -> Nat -> MonSys M X
> flow f Z = pure
> flow f ( S n) = f >=> flow f n
%endif
The two parts of the monoid morphism proof are
> flowLemma1 : {X : Type} -> {M : Type -> Type} -> Fat.VeriMonadFat M =>
> (f : MonSys M X) -> flow f Z <=> pure
>
> flowLemma2 : {X : Type} -> {M : Type -> Type} -> Fat.VeriMonadFat M => {m, n : Nat} ->
> (f : MonSys M X) -> flow f (m + n) <=> (flow f m >=> flow f n)
Proving |flowLemma1| is immediate (because |flow f Z = pure|):
> flowLemma1 f = reflEE
%
We prove |flowLemma2| by induction on |m| using the properties from
section \ref{section:monads}: |pure| is a left and right identity of
Kleisli composition and Kleisli composition is associative.
%
The base case is straightforward
> flowLemma2 {m = Z} {n} f x =
> ( flow f (Z + n) x ) ={ Refl }=
> ( flow f n x ) ={ sym (pureLeftIdKleisli (flow f n) x) }=
> ( (pure >=> flow f n) x ) ={ Refl }=
> ( (flow f Z >=> flow f n) x ) QED
but the induction step again relies on Kleisli composition preserving extensional equality.
> flowLemma2 f {m = S l} {n} x =
> ( flow f (S l + n) x ) ={ Refl }=
> ( (f >=> flow f (l + n)) x ) ={ kleisliPresEE f f (flow f (l + n)) (flow f l >=> flow f n)
> reflEE (flowLemma2 f) x }=
> ( (f >=> (flow f l >=> flow f n)) x ) ={ sym (kleisliAssoc f (flow f l) (flow f n) x) }=
> ( ((f >=> flow f l) >=> flow f n) x ) ={ Refl }=
> ( (flow f (S l) >=> flow f n) x ) QED
As seen in section \ref{section:monads}, this follows directly from
the monad ADT and from the preservation of extensional equality for
functors.
\paragraph*{A representation theorem.}
%
Another important result for monadic systems is a representation
theorem: any monadic system |f : MonSys M X| can be represented by
a deterministic system on |M X|. With
> repr : {X : Type} -> {M : Type -> Type} -> Fat.VeriMonadFat M => MonSys M X -> DetSys (M X)
> repr f = id >=> f
% in other symbols: repr f x = x >>= f
%
and for an arbitrary monadic system |f|, |repr f| is equivalent to |f|
in the sense that
% %format (flowDet f n) = f "^{" n "}"
> reprLemma : {X : Type} -> {M : Type -> Type} -> Fat.VeriMonadFat M =>
> (f : MonSys M X) -> (n : Nat) -> repr (flow f n) <=> flowDet (repr f) n
where |flowDet| is the flow of a deterministic system
< flowDet : {X : Type} -> DetSys X -> Nat -> DetSys X
< flowDet f Z = id
< flowDet f ( S n) = flowDet f n . f
As for |flowLemma2|, proving the representation lemma is straightforward
but crucially relies on associativity of Kleisli composition and thus, as
seen in section \ref{section:monads}, on preservation of extensional
equality:
% > reprLemma f Z mx =
% > ( (repr (flow f Z)) mx ) ={ Refl }=
% > ( (id >=> flow f Z) mx ) ={ Refl }=
% > ( (id >=> pure) mx ) ={ Fat.pureRightIdKleisli id mx }=
% > ( id mx ) ={ Refl }=
% > ( flowDet (repr f) Z mx ) QED
> reprLemma f Z mx = Fat.pureRightIdKleisli id mx
> reprLemma f (S m) mx =
> ( repr (flow f (S m)) mx ) ={ Refl }=
> ( (id >=> flow f (S m)) mx ) ={ Refl }=
> ( (id >=> (f >=> flow f m)) mx ) ={ sym (Fat.kleisliAssoc id f (flow f m) mx) }=
> ( ((id >=> f) >=> flow f m) mx ) ={ kleisliLeapfrog (id >=> f) (flow f m) mx }=
> ( (id >=> flow f m) ((id >=> f) mx) ) ={ Refl }=
> ( repr (flow f m) ((id >=> f) mx) ) ={ reprLemma f m ((id >=> f) mx) }=
> ( flowDet (repr f) m ((id >=> f) mx) ) ={ Refl }=
> ( flowDet (repr f) m (repr f mx) ) ={ Refl }=
> ( flowDet (repr f) (S m) mx ) QED
Notice also the application of |kleisliLeapfrog| to deduce |(id >=>
flow f m) ((id >=> f) mx)| from |((id >=> f) >=> flow f m) mx|.
%
If we had formulated the theory in terms of bind instead of Kleisli
composition, the two expressions would be intensionally equal.
\paragraph*{Flows and trajectories.}
%
The last application of preservation of extensional
equality in the context of dynamical systems theory is a result about
flows and trajectories.
%
For a monadic system |f|, the trajectories of length |n+1| starting at
state |x : X| are
> trj : {M : Type -> Type} -> {X : Type} -> Fat.VeriMonadFat M =>
> MonSys M X -> (n : Nat) -> X -> M (Vect (S n) X)
> trj f Z x = map (x ::) (pure Nil)
> trj f ( S n) x = map (x ::) ((f >=> trj f n) x)
In words, the trajectory obtained by making zero steps starting at |x|
is an |M|-structure containing just |[x]|.
%
To compute the trajectories for |S n| steps, we first bind the outcome
of a single step |f x : M X| into |trj f n|.
%
This results in an |M|-structure of vectors of length |S n|.
%
Finally, we prepend these possible trajectories with the initial state
|x|.
Since |trj f n x| is an |M|-structure of vectors of states, we can
compute the last state of each trajectory.
%
It turns out that this is point-wise equal to |flow f n|:
> flowTrjLemma : {X : Type} -> {M : Type -> Type} -> Fat.VeriMonadFat M =>
> (f : MonSys M X) -> (n : Nat) ->
> flow f n <=> map {A = Vect (S n) X} last . trj f n
To prove this result, we first derive the auxiliary lemma
> mapLastLemma : {F : Type -> Type} -> {X : Type} -> {n : Nat} -> VeriFunctor F =>
> (x : X) -> (mvx : F (Vect (S n) X)) ->
> (map last . map (x ::)) mvx = map last mvx
> mapLastLemma {X} {n} x mvx =
> ( map {A = Vect (S (S n)) X} last (map (x ::) mvx) )
> ={ sym (mapPresComp {A = Vect (S n) X} last (x ::) mvx) }=
> ( map (last . (x ::)) mvx )
> ={ mapPresEE (last . (x ::)) last (lastLemma x) mvx }=
> ( map last mvx ) QED
where |lastLemma x : last . (x ::) <=> last|.
In the implementation of |mapLastLemma| we have applied both
preservation of composition and preservation of extensional
equality.
%
With |mapLastLemma| in place, |flowTrjLemma| is readily implemented by
induction on the number of steps
%**PJ: Only added to avoid bad page-break
%\newpage
> flowTrjLemma {X} f Z x =
> ( flow f Z x ) ={ Refl }= (pure x) ={ Refl }=
> ( pure (last (x :: Nil)) ) ={ sym (Fat.pureNatTrans last (x :: Nil)) }=
> ( map last (pure (x :: Nil)) ) ={ cong {f = map last}
> (sym (Fat.pureNatTrans {A = Vect Z X} (x ::) Nil)) }=
> ( map last (map (x ::) (pure Nil)) ) ={ Refl }=
> ( map last (trj f Z x) ) QED
>
> flowTrjLemma f (S m) x =
> ( flow f (S m) x ) ={ Refl }=
> ( (f >=> flow f m) x ) ={ kleisliPresEE f f (flow f m) (map (last {len = m}) . trj f m)
> reflEE (flowTrjLemma f m) x }=
>
> ( (f >=> map (last {len = m}) . trj f m) x ) ={ sym (mapKleisliLemma f (trj f m) last x) }=
> ( map last ((f >=> trj f m) x) ) ={ sym (mapLastLemma x ((f >=> trj f m) x)) }=
> ( map last (map (x ::) ((f >=> trj f m) x)) ) ={ Refl }=
> ( map last (trj f (S m) x) ) QED
Again, preservation of extensional equality proves essential for the induction step.
\paragraph*{Dynamic programming (DP).} The relationship between the
flow and the trajectory of a monadic dynamical system also plays a
crucial role in the \emph{semantic verification} of dynamic
programming.
%
DP \citep{bellman1957} is a method for solving sequential decision
problems.
%
These problems are at the core of many applications in economics,
logistics and computer science and are, in principle, well
understood~\citep{bellman1957, de_moor1995, %de_moor1999,
gnesi1981dynamic, 2017_Botta_Jansson_Ionescu}.
Proving that dynamic programming is semantically correct boils down to
showing that the value function |val| that is at the core of the
backwards induction algorithm of DP is extensionally equal to a
specification |val'|.
The |val| function of DP takes |n| policies or decision rules and is
computed by iterating |n| times a monadic dynamical system similar to
the function argument of |flow| but with an additional \emph{control}
argument.
%
At each iteration, a \emph{reward} function is mapped on the states
%TiRi: can this be left out?: obtained by iterating the system
and the result is reduced with a \emph{measure} function.
%
In this computation, the measure function is applied a number of times
that is exponential in |n|.
By contrast, |val'| is computed by applying the measure function only
once, but to a structure of a size exponential in |n| that is obtained
by adding up the rewards along all the trajectories.
The equivalence between |val| and |val'| is established by structural
induction.
%
As in the |flowTrjLemma| discussed above, |map| preserving extensional
equality turns out to be pivotal in applying the induction hypothesis,
see \citep{brede2020} for details.