Learning.ScaledProductUpdate

1module Learning.ScaledProductUpdate
2
3import Component.Pointwise
4import Std.Fin
5import Std.List
6import Std.Natural
7
8-- A local correlation update (often called a Hebbian update). The arithmetic
9-- order is explicit: form the observation product, scale it, then add to state.
10-- No derivative, objective, optimizer state or target realization is required.
11def accumulateScaledProduct =
12  (lambda erased scalar : Type 0 .
13    (lambda unrestricted add : (pi unrestricted left : scalar . (pi unrestricted right : scalar . scalar)) .
14      (lambda unrestricted multiply : (pi unrestricted left : scalar . (pi unrestricted right : scalar . scalar)) .
15        (lambda unrestricted coefficient : scalar .
16          (lambda unrestricted previous : scalar .
17            (lambda unrestricted left : scalar .
18              (lambda unrestricted right : scalar .
19                (add previous (multiply coefficient (multiply left right))))))))))
20
21def scaledProductSlotsIndependent =
22  (lambda erased slots : Nat .
23    (lambda unrestricted state : (family StdFin slots) .
24      (lambda unrestricted coefficient : (family StdFin slots) .
25        (lambda unrestricted left : (family StdFin slots) .
26          (lambda unrestricted right : (family StdFin slots) .
27            (naturalAnd
28              (pointwiseSlotsSeparate slots state coefficient)
29              (naturalAnd
30                (pointwiseSlotsSeparate slots state left)
31                (pointwiseSlotsSeparate slots state right))))))))
32
33-- Read-only observations may alias each other; they must not alias the state
34-- being mutated. The same independent-slot obligation used by scaled-gradient
35-- compositions prevents a placement from silently changing the local rule.
36def scaledProductAssignments =
37  (lambda erased word : Type 0 .
38    (lambda erased slots : Nat .
39      (lambda unrestricted state : (family StdFin slots) .
40        (lambda unrestricted coefficient : (family StdFin slots) .
41          (lambda unrestricted left : (family StdFin slots) .
42            (lambda unrestricted right : (family StdFin slots) .
43              (lambda erased independent : (equal Nat (scaledProductSlotsIndependent slots state coefficient left right) 1) .
44                (let unrestricted input =
45                  (lambda unrestricted index : (family StdFin slots) .
46                    (constructor PointwiseExpression PointwiseInput word slots index))
47                  in
48                  (constructor
49                    StdList
50                    StdListCons
51                    (family PointwiseAssignment word slots)
52                    (constructor
53                      PointwiseAssignment
54                      PointwiseAssign
55                      word
56                      slots
57                      state
58                      (accumulateScaledProduct
59                        (family PointwiseExpression word slots)
60                        (pointwiseBinary word slots (constructor PointwiseBinary PointwiseAdd))
61                        (pointwiseBinary word slots (constructor PointwiseBinary PointwiseMultiply))
62                        (input coefficient)
63                        (input state)
64                        (input left)
65                        (input right)))
66                    (constructor StdList StdListEmpty (family PointwiseAssignment word slots)))))))))))