main.bend

mlbend-preprocess@0.1.0.0 · 306 lines · 40 definitions

1# mlbend-preprocess: the transformers of scikit-learn, over bend-ml's matrix.
2#
3#   import mlbend-preprocess@0.1.0.0/main.bend as P
4#
5# A transformer takes a matrix and gives a matrix of the same shape. The
6# matrix is bend-ml's: `Mat<r, c>` from `bend-ml-tensor`, the one
7# bend-ml's autodiff takes, so the estimators that follow can be handed
8# to a model without a copy. MLBend writes no matrix of its own.
9#
10# The standardiser is bend-ml's own arithmetic: a column-wise
11# normalisation is a transpose, then `Mat.layernorm` (which centres a
12# row and scales it by its own standard deviation), then a transpose
13# back. The min-max scaler and the normalisers use `Vec.dot`,
14# `Vec.scale` and `Mat.to_rows`.
15#
16# What is proved: the number of rows of a one-hot matrix, and the shape
17# of every result (the type says it, and the checker verifies it in
18# every operation). What is tested: the numbers, against NumPy and
19# scikit-learn (reference/test_preprocess.py). F32 is not a real
20# number, so a value is never proved, only tested.
21
22import Base
23import bend-ml-tensor@0.1.0.0/main.bend as T
24
25# The standardiser: every column centred on its mean and scaled by its
26# own standard deviation.
27
28
29# LAW (one_hot_count_length): the one-hot matrix has one row for every
30# label.
31law one_hot_count_length:
32  for ys: List<&2, Nat>
33  {one_hot_count_of(ys) == List.length(&2, Nat, ys) : Nat}
34
35# The extremes of every column: the smallest and the largest.
36type Bounds is Data:
37  Bounds{mins: List<&2, F32>, maxs: List<&2, F32>}
38
39# The largest of two rows, cell by cell.
40def bounds_max_go(maxs: List<&2, F32>, row: List<&2, F32>, +acc: List<&2, F32>) -> List<&2, F32>:
41  match maxs:
42    case Nil{}:
43      acc
44    case Con{a, ta}:
45      match row:
46        case Con{b, tb}:
47          bounds_max_go(ta, tb, List.append(&2, F32, acc, Con{F32.max(a, b), Nil{}}))
48        case Nil{}:
49          acc
50
51# The largest of two rows, cell by cell.
52def bounds_max(maxs: List<&2, F32>, row: List<&2, F32>) -> List<&2, F32>:
53  bounds_max_go(maxs, row, Nil{})
54
55# The smallest of two rows, cell by cell.
56def bounds_min_go(mins: List<&2, F32>, row: List<&2, F32>, +acc: List<&2, F32>) -> List<&2, F32>:
57  match mins:
58    case Nil{}:
59      acc
60    case Con{a, ta}:
61      match row:
62        case Con{b, tb}:
63          bounds_min_go(ta, tb, List.append(&2, F32, acc, Con{F32.min(a, b), Nil{}}))
64        case Nil{}:
65          acc
66
67# The smallest of two rows, cell by cell.
68def bounds_min(mins: List<&2, F32>, +row: List<&2, F32>) -> List<&2, F32>:
69  bounds_min_go(mins, row, Nil{})
70
71# The extremes of every column, row by row.
72def bounds_of_go(+rows: List<&2, List<&2, F32>>, +mins: List<&2, F32>, +maxs: List<&2, F32>) ->
73  Bounds:
74  match rows:
75    case Nil{}:
76      Bounds{mins, maxs}
77    case Con{+row, t}:
78      bounds_of_go(t, bounds_min(mins, row), bounds_max(maxs, row))
79
80# The extremes of every column, row by row.
81def bounds_of_rows(+rows: List<&2, List<&2, F32>>) -> Bounds:
82  match rows:
83    case Nil{}:
84      Bounds{Nil{}, Nil{}}
85    case Con{+row, t}:
86      bounds_of_go(t, row, row)
87
88# The extremes of every column of a matrix.
89def bounds_of(+r: Nat, +c: Nat, a: T.Mat<r, c>) -> Bounds:
90  bounds_of_rows(T.Mat.to_rows(r, c, a))
91
92# The row, divided, cell by cell.
93def l1_finish_go(acc: List<&2, F32>, +k: F32, +out: List<&2, F32>) -> List<&2, F32>:
94  match acc:
95    case Nil{}:
96      out
97    case Con{h, t}:
98      l1_finish_go(t, k, List.append(&2, F32, out, Con{F32.mul(h, k), Nil{}}))
99
100# The row, divided.
101def l1_finish(acc: List<&2, F32>, total: F32) -> List<&2, F32>:
102  l1_finish_go(acc, (1.0 / F32.max(total, 0.00000001) : F32), Nil{})
103
104# One row divided by the sum of its absolute values, cell by cell.
105def l1_row_go(+row: List<&2, F32>, +acc: List<&2, F32>, +total: F32) -> List<&2, F32>:
106  match row:
107    case Nil{}:
108      l1_finish(acc, total)
109    case Con{+h, t}:
110      l1_row_go(t, List.append(&2, F32, acc, Con{h, Nil{}}), F32.add(total, F32.abs(h)))
111
112# One row divided by the sum of its absolute values.
113def l1_row(+row: List<&2, F32>) -> List<&2, F32>:
114  l1_row_go(row, Nil{}, 0.0)
115
116# The rows of a matrix, each divided by the sum of its absolute values.
117def l1_normalize_go(+rows: List<&2, List<&2, F32>>, +acc: List<&2, List<&2, F32>>) ->
118  List<&2, List<&2, F32>>:
119  match rows:
120    case Nil{}:
121      acc
122    case Con{row, t}:
123      l1_normalize_go(t, List.append(&2, List<&2, F32>, acc, Con{l1_row(row), Nil{}}))
124
125# A matrix of r rows of c numbers, when there is one.
126def mat_of_(+r: Nat, +c: Nat, m: Maybe<&2, T.Mat<r, c>>) -> T.Mat<r, c>:
127  match m:
128    case Some{v}:
129      v
130    case None{}:
131      T.Mat.fill(r, c, 0.0)
132
133# A matrix of r rows of c numbers. When the rows do not fit, the
134# matrix is empty: a shape that does not hold is not a matrix.
135def mat_of(+r: Nat, +c: Nat, +rows: List<&2, List<&2, F32>>) -> T.Mat<r, c>:
136  mat_of_(r, c, T.Mat.of(r, c, rows))
137
138# The L1 normaliser: every row divided by the sum of its absolute
139# values.
140def l1_normalize(+r: Nat, +c: Nat, a: T.Mat<r, c>) -> T.Mat<r, c>:
141  mat_of(r, c, l1_normalize_go(T.Mat.to_rows(r, c, a), Nil{}))
142
143# The row, divided, cell by cell.
144def l2_finish_go(acc: List<&2, F32>, +norm: F32, +out: List<&2, F32>) -> List<&2, F32>:
145  match acc:
146    case Nil{}:
147      out
148    case Con{h, t}:
149      l2_finish_go(t, norm, List.append(&2, F32, out, Con{(h / F32.max(norm, 0.00000001) : F32), Nil{}}))
150
151# The length of a row, cell by cell.
152def l2_norm_go(acc: List<&2, F32>, +acc_sum: F32) -> F32:
153  match acc:
154    case Nil{}:
155      F32.sqrt(acc_sum)
156    case Con{+h, t}:
157      l2_norm_go(t, F32.add(acc_sum, F32.mul(h, h)))
158
159# The length of a row.
160def l2_norm(acc: List<&2, F32>) -> F32:
161  l2_norm_go(acc, 0.0)
162
163# The row, divided by its length.
164def l2_finish(+acc: List<&2, F32>) -> List<&2, F32>:
165  l2_finish_go(acc, l2_norm(acc), Nil{})
166
167# One row divided by the length of its arrow, cell by cell.
168def l2_row_go(+row: List<&2, F32>, +acc: List<&2, F32>) -> List<&2, F32>:
169  match row:
170    case Nil{}:
171      l2_finish(acc)
172    case Con{h, t}:
173      l2_row_go(t, List.append(&2, F32, acc, Con{h, Nil{}}))
174
175# One row divided by the length of its arrow.
176def l2_row(+row: List<&2, F32>) -> List<&2, F32>:
177  l2_row_go(row, Nil{})
178
179# The rows of a matrix, each divided by the length of its arrow.
180def l2_normalize_go(+rows: List<&2, List<&2, F32>>, +acc: List<&2, List<&2, F32>>) ->
181  List<&2, List<&2, F32>>:
182  match rows:
183    case Nil{}:
184      acc
185    case Con{row, t}:
186      l2_normalize_go(t, List.append(&2, List<&2, F32>, acc, Con{l2_row(row), Nil{}}))
187
188# The L2 normaliser: every row divided by the length of its arrow.
189def l2_normalize(+r: Nat, +c: Nat, +a: T.Mat<r, c>) -> T.Mat<r, c>:
190  mat_of(r, c, l2_normalize_go(T.Mat.to_rows(r, c, a), Nil{}))
191
192# One row scaled column by column, cell by cell.
193def scale_row_go(+row: List<&2, F32>, mins: List<&2, F32>, maxs: List<&2, F32>,
194  +acc: List<&2, F32>) -> List<&2, F32>:
195  match row:
196    case Nil{}:
197      acc
198    case Con{h, t}:
199      match mins:
200        case Nil{}:
201          acc
202        case Con{+m, ms}:
203          match maxs:
204            case Nil{}:
205              acc
206            case Con{mx, mxs}:
207              scale_row_go(t, ms, mxs,
208                List.append(&2, F32, acc,
209                  Con{((h - m : F32) / F32.max((mx - m : F32), 0.00000001) : F32), Nil{}}))
210
211# One row scaled column by column.
212def scale_row(+row: List<&2, F32>, mins: List<&2, F32>, maxs: List<&2, F32>) -> List<&2, F32>:
213  scale_row_go(row, mins, maxs, Nil{})
214
215# A matrix scaled column by column, row by row.
216def scaled_go(+rows: List<&2, List<&2, F32>>, +mins: List<&2, F32>, +maxs: List<&2, F32>,
217  +acc: List<&2, List<&2, F32>>) -> List<&2, List<&2, F32>>:
218  match rows:
219    case Nil{}:
220      acc
221    case Con{row, t}:
222      scaled_go(t, mins, maxs,
223        List.append(&2, List<&2, F32>, acc, Con{scale_row(row, mins, maxs), Nil{}}))
224
225# A matrix scaled column by column.
226def scaled_of(+r: Nat, +c: Nat, a: T.Mat<r, c>, +b: Bounds) -> List<&2, List<&2, F32>>:
227  match b:
228    case Bounds{mins, maxs}:
229      scaled_go(T.Mat.to_rows(r, c, a), mins, maxs, Nil{})
230
231# A matrix scaled column by column: every cell is (x - min) / (max - min).
232def scaled(+r: Nat, +c: Nat, a: T.Mat<r, c>, +b: Bounds) -> List<&2, List<&2, F32>>:
233  scaled_of(r, c, a, b)
234
235# The min-max scaler: every column mapped onto [0, 1].
236def min_max(+r: Nat, +c: Nat, +a: T.Mat<r, c>) -> T.Mat<r, c>:
237  mat_of(r, c, scaled(r, c, a, bounds_of(r, c, a)))
238
239# A list with its nth element replaced, element by element.
240def replace_at_go(+xs: List<&2, F32>, +n: Nat, +v: F32, +acc: List<&2, F32>) -> List<&2, F32>:
241  match xs:
242    case Nil{}:
243      acc
244    case Con{h, +t}:
245      match n:
246        case 0n:
247          List.append(&2, F32, acc, Con{v, t})
248        case _:
249          replace_at_go(t, Nat.sub(n, 1n), v, List.append(&2, F32, acc, Con{h, Nil{}}))
250
251# A list with its nth element replaced.
252def replace_at(+xs: List<&2, F32>, n: Nat, v: F32) -> List<&2, F32>:
253  replace_at_go(xs, n, v, Nil{})
254
255# One row of a one-hot matrix: a zero in every column but the label's.
256def one_hot_row(+label: Nat, k: Nat) -> List<&2, F32>:
257  replace_at(List.replicate(F32, k, 0.0), label, 1.0)
258
259# The rows of a one-hot matrix, label by label.
260def one_hot_rows_go(+labels: List<&2, Nat>, +k: Nat, +acc: List<&2, List<&2, F32>>) ->
261  List<&2, List<&2, F32>>:
262  match labels:
263    case Nil{}:
264      acc
265    case Con{h, t}:
266      one_hot_rows_go(t, k, List.append(&2, List<&2, F32>, acc, Con{one_hot_row(h, k), Nil{}}))
267
268# The rows of a one-hot matrix, one for every label.
269def one_hot_rows(+labels: List<&2, Nat>, +k: Nat) -> List<&2, List<&2, F32>>:
270  one_hot_rows_go(labels, k, Nil{})
271
272# The one-hot encoding: a row of k numbers for every label, with a one
273# in the column of the label. It is Nothing when there are not exactly
274# n labels.
275def one_hot(+k: Nat, +n: Nat, labels: List<&2, Nat>) -> Maybe<&2, T.Mat<n, k>>:
276  T.Mat.of(n, k, one_hot_rows(labels, k))
277
278# The number of rows of a one-hot matrix, counted.
279def one_hot_count_go(+labels: List<&2, Nat>, +acc: Nat) -> Nat:
280  match labels:
281    case Nil{}:
282      acc
283    case Con{h, t}:
284      one_hot_count_go(t, Nat.add(acc, 1n))
285
286# The number of rows of a one-hot matrix.
287def one_hot_count_of(ys: List<&2, Nat>) -> Nat:
288  match ys:
289    case Nil{}:
290      0n
291    case Con{h, t}:
292      (1n + one_hot_count_of(t) : Nat)
293
294# the one-hot matrix has one row for every label
295def one_hot_count_length(ys):
296  match ys:
297    case Nil{}:
298      {==}
299    case Con{h, +t}:
300      %one_hot_count_length(t) : {1n+one_hot_count_of(t) == 1n+_ : Nat}
301      {==}
302
303def standardize(+r: Nat, +c: Nat, a: T.Mat<r, c>) -> T.Mat<r, c>:
304  T.Mat.transpose(c, r,
305    T.Mat.layernorm(c, r, 0.00000001, T.Vec.fill(r, 1.0), T.Vec.fill(r, 0.0),
306      T.Mat.transpose(r, c, a)))