Learning.IndependentState

1module Learning.IndependentState
2
3import Component.Pointwise
4import Component.PointwiseIdentity
5import Model.Parameter
6import Data.Bytes
7import Std.Fin
8import Std.List
9import Std.Natural
10import Std.Word
11
12-- A separable transition with a persistent prefix and immutable local inputs.
13-- Each owner's complete input vector is declared in logical owner order. The
14-- same typed assignment semantics serve gradient and non-gradient equations.
15-- A dependency on a remote statistic cannot be hidden in this representation:
16-- it requires a different composition with an explicit communication edge.
17family IndependentStateSystem : Type 0
18parameter erased independentSlots : Nat
19constructor IndependentStateSystemOf
20field unrestricted independentPersistent : Nat
21field unrestricted independentProgram : (family StdList (family PointwiseAssignment StdU64 independentSlots))
22field unrestricted independentInitial : (family StdList (family StdList StdU64))
23
24end-family
25
26def independentPersistentCount =
27  (lambda erased slots : Nat .
28    (lambda unrestricted system : (family IndependentStateSystem slots) .
29      (eliminate
30        IndependentStateSystem
31        (lambda unrestricted current : (family IndependentStateSystem slots) . Nat)
32        system
33        (branch IndependentStateSystemOf persistent program initial . persistent))))
34
35def independentAssignments =
36  (lambda erased slots : Nat .
37    (lambda unrestricted system : (family IndependentStateSystem slots) .
38      (eliminate
39        IndependentStateSystem
40        (lambda unrestricted current : (family IndependentStateSystem slots) .
41          (family StdList (family PointwiseAssignment StdU64 slots)))
42        system
43        (branch IndependentStateSystemOf persistent program initial . program))))
44
45def independentInitialValues =
46  (lambda erased slots : Nat .
47    (lambda unrestricted system : (family IndependentStateSystem slots) .
48      (eliminate
49        IndependentStateSystem
50        (lambda unrestricted current : (family IndependentStateSystem slots) .
51          (family StdList (family StdList StdU64)))
52        system
53        (branch IndependentStateSystemOf persistent program initial . initial))))
54
55def independentStateAdmitted =
56  (lambda unrestricted slots : Nat .
57    (lambda unrestricted system : (family IndependentStateSystem slots) .
58      (eliminate
59        IndependentStateSystem
60        (lambda unrestricted current : (family IndependentStateSystem slots) . Nat)
61        system
62        (branch
63          IndependentStateSystemOf
64          persistent
65          program
66          initial
67          .
68          (naturalAnd
69            (naturalBelowTwoPower 64 slots)
70            (naturalAnd
71              (naturalNonzero persistent)
72              (naturalAnd
73                (naturalLessOrEqual persistent slots)
74                (naturalAnd
75                  (naturalNonzero (stdListLength (family StdList StdU64) initial))
76                  (naturalAnd
77                    (stdListFold
78                      (family StdList StdU64)
79                      Nat
80                      (lambda unrestricted row : (family StdList StdU64) .
81                        (lambda unrestricted rest : Nat .
82                          (naturalAnd rest (naturalEqual (stdListLength StdU64 row) slots))))
83                      1
84                      initial)
85                    (stdListFold
86                      (family PointwiseAssignment StdU64 slots)
87                      Nat
88                      (lambda unrestricted assignment : (family PointwiseAssignment StdU64 slots) .
89                        (lambda unrestricted rest : Nat .
90                          (eliminate
91                            PointwiseAssignment
92                            (lambda unrestricted current : (family PointwiseAssignment StdU64 slots) .
93                              Nat)
94                            assignment
95                            (branch
96                              PointwiseAssign
97                              destination
98                              expression
99                              .
100                              (naturalAnd
101                                rest
102                                (naturalLess (stdFinToNatural slots destination) persistent))))))
103                      1
104                      program))))))))))
105
106def independentStateIdentity =
107  (lambda unrestricted slots : Nat .
108    (lambda unrestricted system : (family IndependentStateSystem slots) .
109      (eliminate
110        IndependentStateSystem
111        (lambda unrestricted current : (family IndependentStateSystem slots) . Bytes)
112        system
113        (branch
114          IndependentStateSystemOf
115          persistent
116          program
117          initial
118          .
119          (bytes-append
120            b"alpha-independent-state-v1;"
121            (bytes-append
122              (pointwiseIdentityWord persistent)
123              (bytes-append
124                (pointwiseProgramIdentity slots program)
125                (bytes-append
126                  (pointwiseIdentityWord (stdListLength (family StdList StdU64) initial))
127                  (stdListFold
128                    (family StdList StdU64)
129                    Bytes
130                    (lambda unrestricted row : (family StdList StdU64) .
131                      (lambda unrestricted rest : Bytes .
132                        (bytes-append
133                          (stdListFold
134                            StdU64
135                            Bytes
136                            (lambda unrestricted word : StdU64 .
137                              (lambda unrestricted tail : Bytes .
138                                (bytes-append (dataBytesWord64LE word) tail)))
139                            b""
140                            row)
141                          rest)))
142                    b""
143                    initial)))))))))