Applications.lidr 10.6 KB
Newer Older
Nicola Botta's avatar
Nicola Botta committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
% -*-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.