Component.Linear

1module Component.Linear
2
3import Std.Foundation
4import Std.Natural
5import Std.List
6import Representation.Schema
7
8-- PRD 19 P3/P4: a linear map is a MECHANISM. It declares what it computes and
9-- which parameters it owns; the parameter schema is DERIVED from that
10-- declaration, keyed by the structural component path, so no definition
11-- anywhere carries a hand-written parameter list (POC-001, LIB-003, REG-014).
12-- Bias is a field of the map rather than a separate component: PRD 19 L25's
13-- variants turn it on and off, and a bias without its map has no meaning.
14family LinearComponent : Type 0
15constructor LinearComponentOf
16field unrestricted linearComponentName : Bytes
17field unrestricted linearComponentInputs : Nat
18field unrestricted linearComponentOutputs : Nat
19field unrestricted linearComponentBias : (family StdBool)
20
21end-family
22
23def linearComponentNameOf =
24  (lambda unrestricted component : (family LinearComponent) .
25    (eliminate
26      LinearComponent
27      (lambda unrestricted current : (family LinearComponent) . Bytes)
28      component
29      (branch LinearComponentOf name inputs outputs bias . name)))
30
31-- the weight's logical extent is inputs x outputs elements of the representation
32def linearWeightStorage =
33  (lambda unrestricted inputs : Nat .
34    (lambda unrestricted outputs : Nat .
35      (constructor
36        LogicalStorage
37        LogicalStorageOf
38        (nat-multiply inputs outputs)
39        4
40        (constructor LogicalOwnership LogicalOwned)
41        (constructor LogicalLifetime LogicalPersistent))))
42
43def linearBiasStorage =
44  (lambda unrestricted outputs : Nat .
45    (constructor
46      LogicalStorage
47      LogicalStorageOf
48      outputs
49      4
50      (constructor LogicalOwnership LogicalOwned)
51      (constructor LogicalLifetime LogicalPersistent)))
52
53def linearParameterAt =
54  (lambda unrestricted path : (family StdList Bytes) .
55    (lambda unrestricted shape : (family StdList Nat) .
56      (lambda unrestricted storage : (family LogicalStorage) .
57        (constructor
58          ParameterSchema
59          ParameterSchemaOf
60          (constructor ParameterIdentity ParameterIdentityOf path)
61          (constructor ParameterShape ParameterShapeOf shape)
62          b"f32"
63          storage))))
64
65def componentPath =
66  (lambda unrestricted prefix : (family StdList Bytes) .
67    (lambda unrestricted name : Bytes .
68      (lambda unrestricted leaf : Bytes .
69        (stdListAppend
70          Bytes
71          prefix
72          (constructor
73            StdList
74            StdListCons
75            Bytes
76            name
77            (constructor StdList StdListCons Bytes leaf (constructor StdList StdListEmpty Bytes)))))))
78
79-- The parameters a linear map owns under a path prefix: its weight, and its
80-- bias exactly when the map declares one.
81def linearParameters =
82  (lambda unrestricted prefix : (family StdList Bytes) .
83    (lambda unrestricted component : (family LinearComponent) .
84      (eliminate
85        LinearComponent
86        (lambda unrestricted current : (family LinearComponent) .
87          (family StdList (family ParameterSchema)))
88        component
89        (branch
90          LinearComponentOf
91          name
92          inputs
93          outputs
94          bias
95          .
96          (constructor
97            StdList
98            StdListCons
99            (family ParameterSchema)
100            (linearParameterAt
101              (componentPath prefix name b"weight")
102              (constructor
103                StdList
104                StdListCons
105                Nat
106                inputs
107                (constructor StdList StdListCons Nat outputs (constructor StdList StdListEmpty Nat)))
108              (linearWeightStorage inputs outputs))
109            (eliminate
110              StdBool
111              (lambda unrestricted current : (family StdBool) .
112                (family StdList (family ParameterSchema)))
113              bias
114              (branch
115                StdTrue
116                .
117                (constructor
118                  StdList
119                  StdListCons
120                  (family ParameterSchema)
121                  (linearParameterAt
122                    (componentPath prefix name b"bias")
123                    (constructor
124                      StdList
125                      StdListCons
126                      Nat
127                      outputs
128                      (constructor StdList StdListEmpty Nat))
129                    (linearBiasStorage outputs))
130                  (constructor StdList StdListEmpty (family ParameterSchema))))
131              (branch StdFalse . (constructor StdList StdListEmpty (family ParameterSchema)))))))))
132
133def linearComponentInputsOf =
134  (lambda unrestricted component : (family LinearComponent) .
135    (eliminate
136      LinearComponent
137      (lambda unrestricted current : (family LinearComponent) . Nat)
138      component
139      (branch LinearComponentOf name inputs outputs bias . inputs)))
140
141def linearComponentOutputsOf =
142  (lambda unrestricted component : (family LinearComponent) .
143    (eliminate
144      LinearComponent
145      (lambda unrestricted current : (family LinearComponent) . Nat)
146      component
147      (branch LinearComponentOf name inputs outputs bias . outputs)))