The same equations can produce a typed state program instead of evaluating
numbers immediately. Positions are supplied by the state's owner. Assigning
the accumulator first makes its new value available to the parameter update;
the compiler must preserve that dependency and each separate rounding.
Writable slots are independent of each other and of the read-only inputs;
otherwise the first assignment could overwrite a later equation's input.
58def scaledGradientAssignments =
59 (lambda erased word : Type 0 .
60 (lambda erased slots : Nat .
61 (lambda unrestricted parameter : (family StdFin slots) .
62 (lambda unrestricted accumulator : (family StdFin slots) .
63 (lambda unrestricted gradient : (family StdFin slots) .
64 (lambda unrestricted decay : (family StdFin slots) .
65 (lambda unrestricted rate : (family StdFin slots) .
66 (lambda erased independent : (equal Nat (scaledGradientSlotsIndependent slots parameter accumulator gradient decay rate) 1) .
67 (let unrestricted input =
68 (lambda unrestricted slot : (family StdFin slots) .
69 (constructor PointwiseExpression PointwiseInput word slots slot))
70 in
71 (let unrestricted multiply =
72 (pointwiseBinary word slots (constructor PointwiseBinary PointwiseMultiply))
73 in
74 (constructor
75 StdList
76 StdListCons
77 (family PointwiseAssignment word slots)
78 (constructor
79 PointwiseAssignment
80 PointwiseAssign
81 word
82 slots
83 accumulator
84 (accumulateScaledGradient
85 (family PointwiseExpression word slots)
86 (pointwiseBinary word slots (constructor PointwiseBinary PointwiseAdd))
87 multiply
88 (input decay)
89 (input accumulator)
90 (input gradient)))
91 (constructor
92 StdList
93 StdListCons
94 (family PointwiseAssignment word slots)
95 (constructor
96 PointwiseAssignment
97 PointwiseAssign
98 word
99 slots
100 parameter
101 (subtractScaledUpdate
102 (family PointwiseExpression word slots)
103 (pointwiseBinary
104 word
105 slots
106 (constructor PointwiseBinary PointwiseSubtract))
107 multiply
108 (input rate)
109 (input parameter)
110 (input accumulator)))
111 (constructor StdList StdListEmpty (family PointwiseAssignment word slots))))))))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.