Learning.Transition

1module Learning.Transition
2
3import Learning.Transformation
4import Std.Natural
5
6-- Epoch fences a replaced execution; version identifies one logical state.
7-- They are independent: restarting a worker need not advance the learner.
8family LearningRound : Type 0
9constructor LearningRoundOf
10field unrestricted learningMembershipEpoch : Nat
11field unrestricted learningStateVersion : Nat
12
13end-family
14
15-- A pure transition has no replay-sensitive external effect. Interaction is
16-- explicit and may only be replayed through the retained-boundary protocol.
17-- This vocabulary extends the existing transformation modes; it does not
18-- infer differentiation or invent an optimizer for a state evolution rule.
19family TransitionReplay : Type 0
20constructor ReplayPureTransition
21constructor ReplayRetainedInteraction
22constructor RestartExternalInteraction
23
24end-family
25
26family LearningTransition : Type 0
27parameter erased transitionState : Type 0
28parameter erased transitionInput : Type 0
29parameter erased transitionOutput : Type 0
30constructor LearningTransitionOf
31field unrestricted transitionMode : (family LearningTransformation)
32field unrestricted transitionReplay : (family TransitionReplay)
33field unrestricted transitionStep : (pi unrestricted state : transitionState . (pi unrestricted input : transitionInput . transitionOutput))
34
35end-family
36
37def learningRoundEqual =
38  (lambda unrestricted left : (family LearningRound) .
39    (lambda unrestricted right : (family LearningRound) .
40      (eliminate
41        LearningRound
42        (lambda unrestricted current : (family LearningRound) . Nat)
43        left
44        (branch
45          LearningRoundOf
46          leftEpoch
47          leftVersion
48          .
49          (eliminate
50            LearningRound
51            (lambda unrestricted current : (family LearningRound) . Nat)
52            right
53            (branch
54              LearningRoundOf
55              rightEpoch
56              rightVersion
57              .
58              (naturalAnd
59                (naturalEqual leftEpoch rightEpoch)
60                (naturalEqual leftVersion rightVersion))))))))
61
62def runLearningTransition =
63  (lambda erased state : Type 0 .
64    (lambda erased input : Type 0 .
65      (lambda erased output : Type 0 .
66        (lambda unrestricted transition : (family LearningTransition state input output) .
67          (eliminate
68            LearningTransition
69            (lambda unrestricted current : (family LearningTransition state input output) .
70              (pi unrestricted oldState : state . (pi unrestricted observation : input . output)))
71            transition
72            (branch LearningTransitionOf mode replay step . step))))))