LocalCorrelation.System

1module LocalCorrelation.System
2
3import Component.Pointwise
4import Learning.IndependentState
5import Learning.ScaledProductUpdate
6import Model.Parameter
7import Std.Fin
8import Std.Float
9import Std.List
10import Std.Word
11
12-- Two coordinates of one associative state. Each coordinate learns from an
13-- immutable local observation pair. Evaluation sums the complete saved state;
14-- dropping either owner changes the result and prevents valid publication.
15def correlationState =
16  (stdFinFirst 3)
17
18def correlationRate =
19  (stdFinNextOf 3 (stdFinFirst 2))
20
21def correlationLeft =
22  (stdFinNextOf 3 (stdFinNextOf 2 (stdFinFirst 1)))
23
24def correlationRight =
25  (stdFinNextOf 3 (stdFinNextOf 2 (stdFinNextOf 1 (stdFinFirst 0))))
26
27def correlationAssignments =
28  (scaledProductAssignments
29    StdU64
30    4
31    correlationState
32    correlationRate
33    correlationLeft
34    correlationRight
35    (refl Nat 1))
36
37def correlationRow =
38  (lambda unrestricted state : F64 .
39    (lambda unrestricted rate : F64 .
40      (lambda unrestricted left : F64 .
41        (lambda unrestricted right : F64 .
42          (constructor
43            StdList
44            StdListCons
45            StdU64
46            (stdF64ToWord64 state)
47            (constructor
48              StdList
49              StdListCons
50              StdU64
51              (stdF64ToWord64 rate)
52              (constructor
53                StdList
54                StdListCons
55                StdU64
56                (stdF64ToWord64 left)
57                (constructor
58                  StdList
59                  StdListCons
60                  StdU64
61                  (stdF64ToWord64 right)
62                  (constructor StdList StdListEmpty StdU64)))))))))
63
64def correlationSystemWith =
65  (lambda unrestricted rate : F64 .
66    (constructor
67      IndependentStateSystem
68      IndependentStateSystemOf
69      4
70      1
71      correlationAssignments
72      (constructor
73        StdList
74        StdListCons
75        (family StdList StdU64)
76        (correlationRow 1.0 rate 2.0 3.0)
77        (constructor
78          StdList
79          StdListCons
80          (family StdList StdU64)
81          (correlationRow 2.0 rate 4.0 1.0)
82          (constructor StdList StdListEmpty (family StdList StdU64))))))
83
84def correlationSystem =
85  (correlationSystemWith 0.5)
86
87def correlationEvaluation =
88  (constructor
89    StdList
90    StdListCons
91    (family PointwiseAssignment StdU64 2)
92    (constructor
93      PointwiseAssignment
94      PointwiseAssign
95      StdU64
96      2
97      (stdFinFirst 1)
98      (pointwiseBinary
99        StdU64
100        2
101        (constructor PointwiseBinary PointwiseAdd)
102        (constructor PointwiseExpression PointwiseInput StdU64 2 (stdFinFirst 1))
103        (constructor PointwiseExpression PointwiseInput StdU64 2 (stdFinNextOf 1 (stdFinFirst 0)))))
104    (constructor StdList StdListEmpty (family PointwiseAssignment StdU64 2)))