src/autograd/backward_PROOF.bend
bendtorch-core@0.1.0.0 · 549 lines · 30 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/autograd/backward.bend as Backward
3import bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend as Laws
4
5def truth(value: Bool) -> Data:
6 match value:
7 case True{}:
8 Unit
9 case False{}:
10 Empty
11
12def true_false(equal: {True{} == False{} : Bool}) -> Empty:
13 %equal : truth(_)
14 Unit{}
15
16def eq_refl(+number: Nat) -> {True{} == Nat.is_eq(number, number) : Bool}:
17 match number:
18 case 0n:
19 {==}
20 case 1n+rest:
21 eq_refl(rest)
22
23def add_succ(+left: Nat, +right: Nat) -> {Nat.add(left, 1n+right) == 1n+Nat.add(left, right) : Nat}:
24 match left:
25 case 0n:
26 {==}
27 case 1n+rest:
28 Equal.cong(Nat, Nat, number => 1n+number, Nat.add(rest, 1n+right), 1n+Nat.add(rest, right), add_succ(rest, right))
29
30def succ_add_ne(+left: Nat, +right: Nat) -> {False{} == Nat.is_eq(1n+Nat.add(left, right), right) : Bool}:
31 match right:
32 case 0n:
33 {==}
34 case 1n+rest:
35 %Equal.sym(Nat, Nat.add(left, 1n+rest), 1n+Nat.add(left, rest), add_succ(left, rest)) :
36 {False{} == Nat.is_eq(1n+_, 1n+rest) : Bool}
37 succ_add_ne(left, rest)
38
39def length_append(-A: Data, +xs: List<&2, A>, +ys: List<&2, A>) ->
40 {List.length(&2, A, List.append(&2, A, xs, ys)) == Nat.add(List.length(&2, A, xs), List.length(&2, A, ys)) : Nat}:
41 match xs:
42 case Nil{}:
43 {==}
44 case Con{head, tail}:
45 Equal.cong(Nat, Nat, number => 1n+number, List.length(&2, A, List.append(&2, A, tail, ys)),
46 Nat.add(List.length(&2, A, tail), List.length(&2, A, ys)), length_append(A, tail, ys))
47
48def append_ne(-A: Data, +xs: List<&2, A>, +item: A, +rest: List<&2, A>) ->
49 {False{} == Nat.is_eq(List.length(&2, A, List.append(&2, A, xs, item <> rest)), List.length(&2, A, rest)) : Bool}:
50 %Equal.sym(Nat, List.length(&2, A, List.append(&2, A, xs, item <> rest)),
51 Nat.add(List.length(&2, A, xs), 1n+List.length(&2, A, rest)), length_append(A, xs, item <> rest)) :
52 {False{} == Nat.is_eq(_, List.length(&2, A, rest)) : Bool}
53 %Equal.sym(Nat, Nat.add(List.length(&2, A, xs), 1n+List.length(&2, A, rest)),
54 1n+Nat.add(List.length(&2, A, xs), List.length(&2, A, rest)), add_succ(List.length(&2, A, xs), List.length(&2, A, rest))) :
55 {False{} == Nat.is_eq(_, List.length(&2, A, rest)) : Bool}
56 succ_add_ne(List.length(&2, A, xs), List.length(&2, A, rest))
57
58def not_lt_succ_ne(+id: Nat, +bound: Nat, outside: {Nat.is_lt(id, 1n+bound) == False{} : Bool}) ->
59 {False{} == Nat.is_eq(bound, id) : Bool}:
60 match id bound:
61 case 0n bound:
62 Empty.absurd({False{} == Nat.is_eq(bound, 0n) : Bool}, true_false(outside))
63 case 1n+rest 0n:
64 {==}
65 case 1n+rest 1n+smaller:
66 not_lt_succ_ne(rest, smaller, outside)
67
68def not_lt_succ_lt(+id: Nat, +bound: Nat, outside: {Nat.is_lt(id, 1n+bound) == False{} : Bool}) ->
69 {Nat.is_lt(id, bound) == False{} : Bool}:
70 match id bound:
71 case 0n bound:
72 Empty.absurd({Nat.is_lt(0n, bound) == False{} : Bool}, true_false(outside))
73 case 1n+rest 0n:
74 {==}
75 case 1n+rest 1n+smaller:
76 not_lt_succ_lt(rest, smaller, outside)
77
78def Laws.vjp_leaf(g):
79 {==}
80
81def Laws.vjp_add(a, b, g):
82 {==}
83
84def Laws.vjp_sub(a, b, g):
85 {==}
86
87def Laws.vjp_mul(a, b, left, right, g):
88 {==}
89
90def Laws.vjp_neg(a, g):
91 {==}
92
93def Laws.backward_add(x, y):
94 {==}
95
96def Laws.backward_sub(x, y):
97 {==}
98
99def Laws.backward_mul(x, y):
100 {==}
101
102def Laws.backward_neg(x):
103 {==}
104
105def Laws.seed_selected_output(newer, node, rest):
106 match newer:
107 case Nil{}:
108 %eq_refl(List.length(&2, Backward.Node, rest)) :
109 {Backward.chosen(node, rest, List.length(&2, Backward.Node, rest),
110 unit => Backward.pass(rest, List.length(&2, Backward.Node, rest), List.length(&2, Backward.Node, rest)), _) ==
111 Some{1.0} <> Backward.sweep(rest,
112 Backward.contribute(node, Some{1.0}, List.length(&2, Backward.Node, rest), Backward.nones(List.length(&2, Backward.Node, rest))),
113 List.length(&2, Backward.Node, rest)) : List<&2, Maybe<&2, F32>>}
114 {==}
115 case Con{head, tail}:
116 %append_ne(Backward.Node, tail, node, rest) :
117 {Backward.chosen(head, List.append(&2, Backward.Node, tail, node <> rest),
118 List.length(&2, Backward.Node, List.append(&2, Backward.Node, tail, node <> rest)),
119 unit => Backward.pass(List.append(&2, Backward.Node, tail, node <> rest),
120 List.length(&2, Backward.Node, List.append(&2, Backward.Node, tail, node <> rest)), List.length(&2, Backward.Node, rest)), _) ==
121 None{} <> List.append(&2, Maybe<&2, F32>, Backward.nones(List.length(&2, Backward.Node, tail)),
122 Some{1.0} <> Backward.sweep(rest,
123 Backward.contribute(node, Some{1.0}, List.length(&2, Backward.Node, rest), Backward.nones(List.length(&2, Backward.Node, rest))),
124 List.length(&2, Backward.Node, rest))) : List<&2, Maybe<&2, F32>>}
125 Equal.cong(List<&2, Maybe<&2, F32>>, List<&2, Maybe<&2, F32>>, xs => None{} <> xs,
126 Backward.pass(List.append(&2, Backward.Node, tail, node <> rest),
127 List.length(&2, Backward.Node, List.append(&2, Backward.Node, tail, node <> rest)), List.length(&2, Backward.Node, rest)),
128 List.append(&2, Maybe<&2, F32>, Backward.nones(List.length(&2, Backward.Node, tail)),
129 Some{1.0} <> Backward.sweep(rest,
130 Backward.contribute(node, Some{1.0}, List.length(&2, Backward.Node, rest), Backward.nones(List.length(&2, Backward.Node, rest))),
131 List.length(&2, Backward.Node, rest))),
132 Laws.seed_selected_output(tail, node, rest))
133
134def is_some_accumulate(slot: Maybe<&2, F32>, +value: F32) ->
135 {Maybe.is_some(&2, F32, Backward.accumulate(slot, Some{value})) == True{} : Bool}:
136 match slot:
137 case None{}:
138 {==}
139 case Some{held}:
140 {==}
141
142def somes_bumped(slot: Maybe<&2, F32>, +rest: List<&2, Maybe<&2, F32>>, +below: Nat, +target: Nat, +value: F32, flag: Bool,
143 ih: {Laws.somes(Backward.bump(rest, below, target, value)) == Laws.mark(Laws.somes(rest), below, target) : List<&2, Bool>}) ->
144 {Laws.somes(Backward.bumped(slot, rest, value, unit => Backward.bump(rest, below, target, value), flag)) ==
145 Laws.marked(Maybe.is_some(&2, F32, slot), Laws.somes(rest), unit => Laws.mark(Laws.somes(rest), below, target), flag) : List<&2, Bool>}:
146 match flag:
147 case True{}:
148 Equal.cong(Bool, List<&2, Bool>, found => found <> Laws.somes(rest),
149 Maybe.is_some(&2, F32, Backward.accumulate(slot, Some{value})), True{}, is_some_accumulate(slot, value))
150 case False{}:
151 Equal.cong(List<&2, Bool>, List<&2, Bool>, xs => Maybe.is_some(&2, F32, slot) <> xs,
152 Laws.somes(Backward.bump(rest, below, target, value)), Laws.mark(Laws.somes(rest), below, target), ih)
153
154def somes_bump(slots: List<&2, Maybe<&2, F32>>, +count: Nat, +target: Nat, +value: F32) ->
155 {Laws.somes(Backward.bump(slots, count, target, value)) == Laws.mark(Laws.somes(slots), count, target) : List<&2, Bool>}:
156 match slots count:
157 case Nil{} count:
158 {==}
159 case Con{slot, rest} 0n:
160 {==}
161 case Con{slot, +rest} 1n+below:
162 somes_bumped(slot, rest, below, target, value, Nat.is_eq(below, target), somes_bump(rest, below, target, value))
163
164def contribution_targets(contributions: List<&2, Backward.Contribution>) -> List<&2, Nat>:
165 match contributions:
166 case Nil{}:
167 Nil{}
168 case Con{Backward.Contribution{target, value}, rest}:
169 target <> contribution_targets(rest)
170
171def somes_deliver(contributions: List<&2, Backward.Contribution>, +count: Nat, +slots: List<&2, Maybe<&2, F32>>) ->
172 {Laws.somes(Backward.deliver(contributions, count, slots)) ==
173 Laws.mark_all(contribution_targets(contributions), count, Laws.somes(slots)) : List<&2, Bool>}:
174 match contributions:
175 case Nil{}:
176 {==}
177 case Con{Backward.Contribution{+target, +value}, rest}:
178 %somes_bump(slots, count, target, value) :
179 {Laws.somes(Backward.deliver(rest, count, Backward.bump(slots, count, target, value))) ==
180 Laws.mark_all(contribution_targets(rest), count, _) : List<&2, Bool>}
181 somes_deliver(rest, count, Backward.bump(slots, count, target, value))
182
183def vjp_targets(node: Backward.Node, +g: F32) -> {contribution_targets(Backward.vjp(node, g)) == Laws.targets(node) : List<&2, Nat>}:
184 match node:
185 case Backward.Leaf{}:
186 {==}
187 case Backward.Add{a, b}:
188 {==}
189 case Backward.Sub{a, b}:
190 {==}
191 case Backward.Mul{a, b, left, right}:
192 {==}
193 case Backward.Neg{a}:
194 {==}
195
196def somes_contribute(+node: Backward.Node, gradient: Maybe<&2, F32>, +count: Nat, +slots: List<&2, Maybe<&2, F32>>) ->
197 {Laws.somes(Backward.contribute(node, gradient, count, slots)) ==
198 Laws.spread(node, Maybe.is_some(&2, F32, gradient), count, Laws.somes(slots)) : List<&2, Bool>}:
199 match gradient:
200 case None{}:
201 {==}
202 case Some{+value}:
203 %vjp_targets(node, value) :
204 {Laws.somes(Backward.deliver(Backward.vjp(node, value), count, slots)) == Laws.mark_all(_, count, Laws.somes(slots)) : List<&2, Bool>}
205 somes_deliver(Backward.vjp(node, value), count, slots)
206
207def sweep_reach(nodes: List<&2, Backward.Node>, gradients: List<&2, Maybe<&2, F32>>, +count: Nat) ->
208 {Laws.somes(Backward.sweep(nodes, gradients, count)) == Laws.reach(nodes, Laws.somes(gradients), count) : List<&2, Bool>}:
209 match nodes gradients count:
210 case Nil{} gradients count:
211 {==}
212 case Con{node, rest} Nil{} count:
213 {==}
214 case Con{node, rest} Con{gradient, pending} 0n:
215 {==}
216 case Con{+node, rest} Con{+gradient, +pending} 1n+below:
217 %somes_contribute(node, gradient, below, pending) :
218 {Maybe.is_some(&2, F32, gradient) <> Laws.somes(Backward.sweep(rest, Backward.contribute(node, gradient, below, pending), below)) ==
219 Maybe.is_some(&2, F32, gradient) <> Laws.reach(rest, _, below) : List<&2, Bool>}
220 Equal.cong(List<&2, Bool>, List<&2, Bool>, xs => Maybe.is_some(&2, F32, gradient) <> xs,
221 Laws.somes(Backward.sweep(rest, Backward.contribute(node, gradient, below, pending), below)),
222 Laws.reach(rest, Laws.somes(Backward.contribute(node, gradient, below, pending)), below),
223 sweep_reach(rest, Backward.contribute(node, gradient, below, pending), below))
224
225def somes_nones(+count: Nat) -> {Laws.somes(Backward.nones(count)) == Laws.falses(count) : List<&2, Bool>}:
226 match count:
227 case 0n:
228 {==}
229 case 1n+rest:
230 Equal.cong(List<&2, Bool>, List<&2, Bool>, xs => False{} <> xs, Laws.somes(Backward.nones(rest)), Laws.falses(rest), somes_nones(rest))
231
232def chosen_reached(+node: Backward.Node, +rest: List<&2, Backward.Node>, +below: Nat, +output: Nat, flag: Bool,
233 ih: {Laws.somes(Backward.pass(rest, below, output)) == Laws.reached(rest, below, output) : List<&2, Bool>}) ->
234 {Laws.somes(Backward.chosen(node, rest, below, unit => Backward.pass(rest, below, output), flag)) ==
235 Laws.reached_chosen(node, rest, below, unit => Laws.reached(rest, below, output), flag) : List<&2, Bool>}:
236 match flag:
237 case True{}:
238 %somes_nones(below) :
239 {Laws.somes(Backward.sweep(node <> rest, Some{1.0} <> Backward.nones(below), 1n+below)) ==
240 Laws.reach(node <> rest, True{} <> _, 1n+below) : List<&2, Bool>}
241 sweep_reach(node <> rest, Some{1.0} <> Backward.nones(below), 1n+below)
242 case False{}:
243 Equal.cong(List<&2, Bool>, List<&2, Bool>, xs => False{} <> xs,
244 Laws.somes(Backward.pass(rest, below, output)), Laws.reached(rest, below, output), ih)
245
246def pass_reached(nodes: List<&2, Backward.Node>, +count: Nat, +output: Nat) ->
247 {Laws.somes(Backward.pass(nodes, count, output)) == Laws.reached(nodes, count, output) : List<&2, Bool>}:
248 match nodes count:
249 case Nil{} count:
250 {==}
251 case Con{node, rest} 0n:
252 {==}
253 case Con{+node, +rest} 1n+below:
254 chosen_reached(node, rest, below, output, Nat.is_eq(below, output), pass_reached(rest, below, output))
255
256def Laws.reached_exactly(graph, output):
257 pass_reached(graph, List.length(&2, Backward.Node, graph), output)
258
259def Laws.unused_leaf_none(x, y, z):
260 {==}
261
262def Laws.accumulate_moves_in(contribution):
263 {==}
264
265def Laws.accumulate_adds_total_first(held, value):
266 {==}
267
268def Laws.accumulate_keeps_without_contribution(held):
269 {==}
270
271def Laws.bump_target(newer, slot, rest, value):
272 match newer:
273 case Nil{}:
274 %eq_refl(List.length(&2, Maybe<&2, F32>, rest)) :
275 {Backward.bumped(slot, rest, value,
276 unit => Backward.bump(rest, List.length(&2, Maybe<&2, F32>, rest), List.length(&2, Maybe<&2, F32>, rest), value), _) ==
277 Backward.accumulate(slot, Some{value}) <> rest : List<&2, Maybe<&2, F32>>}
278 {==}
279 case Con{head, tail}:
280 %append_ne(Maybe<&2, F32>, tail, slot, rest) :
281 {Backward.bumped(head, List.append(&2, Maybe<&2, F32>, tail, slot <> rest), value,
282 unit => Backward.bump(List.append(&2, Maybe<&2, F32>, tail, slot <> rest),
283 List.length(&2, Maybe<&2, F32>, List.append(&2, Maybe<&2, F32>, tail, slot <> rest)), List.length(&2, Maybe<&2, F32>, rest), value), _) ==
284 head <> List.append(&2, Maybe<&2, F32>, tail, Backward.accumulate(slot, Some{value}) <> rest) : List<&2, Maybe<&2, F32>>}
285 Equal.cong(List<&2, Maybe<&2, F32>>, List<&2, Maybe<&2, F32>>, xs => head <> xs,
286 Backward.bump(List.append(&2, Maybe<&2, F32>, tail, slot <> rest),
287 List.length(&2, Maybe<&2, F32>, List.append(&2, Maybe<&2, F32>, tail, slot <> rest)), List.length(&2, Maybe<&2, F32>, rest), value),
288 List.append(&2, Maybe<&2, F32>, tail, Backward.accumulate(slot, Some{value}) <> rest),
289 Laws.bump_target(tail, slot, rest, value))
290
291def Laws.fan_out_arrival_order(x, a, b, c):
292 {==}
293
294def Laws.lookup_exact(A, newer, item, rest):
295 match newer:
296 case Nil{}:
297 %eq_refl(List.length(&2, A, rest)) :
298 {Backward.picked(A, item, unit => Backward.find(A, rest, List.length(&2, A, rest), List.length(&2, A, rest)), _) ==
299 Some{item} : Maybe<&2, A>}
300 {==}
301 case Con{head, tail}:
302 %append_ne(A, tail, item, rest) :
303 {Backward.picked(A, head, unit => Backward.find(A, List.append(&2, A, tail, item <> rest),
304 List.length(&2, A, List.append(&2, A, tail, item <> rest)), List.length(&2, A, rest)), _) == Some{item} : Maybe<&2, A>}
305 Laws.lookup_exact(A, tail, item, rest)
306
307def find_unknown(-A: Data, +xs: List<&2, A>, +id: Nat, +outside: {Nat.is_lt(id, List.length(&2, A, xs)) == False{} : Bool}) ->
308 {Backward.find(A, xs, List.length(&2, A, xs), id) == None{} : Maybe<&2, A>}:
309 match xs:
310 case Nil{}:
311 {==}
312 case Con{head, tail}:
313 %not_lt_succ_ne(id, List.length(&2, A, tail), outside) :
314 {Backward.picked(A, head, unit => Backward.find(A, tail, List.length(&2, A, tail), id), _) == None{} : Maybe<&2, A>}
315 find_unknown(A, tail, id, not_lt_succ_lt(id, List.length(&2, A, tail), outside))
316
317def Laws.lookup_unknown(A, items, id, outside):
318 find_unknown(A, items, id, outside)
319
320def Laws.bump_unknown(gradients, target, value, outside):
321 match gradients:
322 case Nil{}:
323 {==}
324 case Con{slot, tail}:
325 %not_lt_succ_ne(target, List.length(&2, Maybe<&2, F32>, tail), outside) :
326 {Backward.bumped(slot, tail, value,
327 unit => Backward.bump(tail, List.length(&2, Maybe<&2, F32>, tail), target, value), _) == slot <> tail : List<&2, Maybe<&2, F32>>}
328 Equal.cong(List<&2, Maybe<&2, F32>>, List<&2, Maybe<&2, F32>>, xs => slot <> xs,
329 Backward.bump(tail, List.length(&2, Maybe<&2, F32>, tail), target, value), tail,
330 Laws.bump_unknown(tail, target, value, not_lt_succ_lt(target, List.length(&2, Maybe<&2, F32>, tail), outside)))
331
332def Laws.value_unknown(entries, id, outside):
333 %Equal.sym(Maybe<&2, Backward.Entry>, Backward.lookup(Backward.Entry, entries, id), None{},
334 find_unknown(Backward.Entry, entries, id, outside)) :
335 {Backward.entry_value(_) == Fail{Backward.UnknownNode{}} : Result<&2, &2, Backward.Error, F32>}
336 {==}
337
338def Laws.grad_unknown(entries, id, outside):
339 %Equal.sym(Maybe<&2, Backward.Entry>, Backward.lookup(Backward.Entry, entries, id), None{},
340 find_unknown(Backward.Entry, entries, id, outside)) :
341 {Backward.entry_grad(_) == Fail{Backward.UnknownNode{}} : Result<&2, &2, Backward.Error, Maybe<&2, F32>>}
342 {==}
343
344def Laws.record_unknown_left(entries, kind, a, b, outside):
345 %Equal.sym(Result<&2, &2, Backward.Error, F32>, Backward.value(Backward.Tape{entries}, a), Fail{Backward.UnknownNode{}},
346 Laws.value_unknown(entries, a, outside)) :
347 {Backward.operands(entries, kind, a, b, _, Backward.value(Backward.Tape{entries}, b)) ==
348 (Backward.Tape{entries}, Fail{Backward.UnknownNode{}}) : Backward.Tape & Result<&2, &2, Backward.Error, Nat>}
349 {==}
350
351def operands_right(+entries: List<&2, Backward.Entry>, kind: Backward.Binary, +a: Nat, +b: Nat, left: Result<&2, &2, Backward.Error, F32>) ->
352 {Backward.operands(entries, kind, a, b, left, Fail{Backward.UnknownNode{}}) ==
353 (Backward.Tape{entries}, Fail{Backward.UnknownNode{}}) : Backward.Tape & Result<&2, &2, Backward.Error, Nat>}:
354 match left:
355 case Fail{error}:
356 {==}
357 case Done{x}:
358 {==}
359
360def Laws.record_unknown_right(entries, kind, a, b, outside):
361 %Equal.sym(Result<&2, &2, Backward.Error, F32>, Backward.value(Backward.Tape{entries}, b), Fail{Backward.UnknownNode{}},
362 Laws.value_unknown(entries, b, outside)) :
363 {Backward.operands(entries, kind, a, b, Backward.value(Backward.Tape{entries}, a), _) ==
364 (Backward.Tape{entries}, Fail{Backward.UnknownNode{}}) : Backward.Tape & Result<&2, &2, Backward.Error, Nat>}
365 operands_right(entries, kind, a, b, Backward.value(Backward.Tape{entries}, a))
366
367def Laws.neg_unknown(entries, a, outside):
368 %Equal.sym(Result<&2, &2, Backward.Error, F32>, Backward.value(Backward.Tape{entries}, a), Fail{Backward.UnknownNode{}},
369 Laws.value_unknown(entries, a, outside)) :
370 {Backward.negated(entries, a, _) ==
371 (Backward.Tape{entries}, Fail{Backward.UnknownNode{}}) : Backward.Tape & Result<&2, &2, Backward.Error, Nat>}
372 {==}
373
374def nodes_length(+entries: List<&2, Backward.Entry>) ->
375 {List.length(&2, Backward.Entry, entries) == List.length(&2, Backward.Node, Backward.nodes(entries)) : Nat}:
376 match entries:
377 case Nil{}:
378 {==}
379 case Con{Backward.Entry{node, value, slot}, rest}:
380 Equal.cong(Nat, Nat, number => 1n+number, List.length(&2, Backward.Entry, rest),
381 List.length(&2, Backward.Node, Backward.nodes(rest)), nodes_length(rest))
382
383def Laws.backward_unknown(entries, output, outside):
384 %nodes_length(entries) :
385 {Backward.merged(entries, Backward.checked(Backward.nodes(entries), _, output, Nat.is_lt(output, _),
386 Backward.wired(Backward.nodes(entries), _))) == Fail{Backward.UnknownNode{}} : Result<&2, &2, Backward.Error, Backward.Tape>}
387 %Equal.sym(Bool, Nat.is_lt(output, List.length(&2, Backward.Entry, entries)), False{}, outside) :
388 {Backward.merged(entries, Backward.checked(Backward.nodes(entries), List.length(&2, Backward.Entry, entries), output, _,
389 Backward.wired(Backward.nodes(entries), List.length(&2, Backward.Entry, entries)))) ==
390 Fail{Backward.UnknownNode{}} : Result<&2, &2, Backward.Error, Backward.Tape>}
391 {==}
392
393def Laws.backward_dangling(entries, output, inside, unsound):
394 %nodes_length(entries) :
395 {Backward.merged(entries, Backward.checked(Backward.nodes(entries), _, output, Nat.is_lt(output, _),
396 Backward.wired(Backward.nodes(entries), _))) == Fail{Backward.DanglingOperand{}} : Result<&2, &2, Backward.Error, Backward.Tape>}
397 %Equal.sym(Bool, Nat.is_lt(output, List.length(&2, Backward.Entry, entries)), True{}, inside) :
398 {Backward.merged(entries, Backward.checked(Backward.nodes(entries), List.length(&2, Backward.Entry, entries), output, _,
399 Backward.wired(Backward.nodes(entries), List.length(&2, Backward.Entry, entries)))) ==
400 Fail{Backward.DanglingOperand{}} : Result<&2, &2, Backward.Error, Backward.Tape>}
401 %Equal.sym(Bool, Backward.wired(Backward.nodes(entries), List.length(&2, Backward.Entry, entries)), False{}, unsound) :
402 {Backward.merged(entries, Backward.checked(Backward.nodes(entries), List.length(&2, Backward.Entry, entries), output, True{}, _)) ==
403 Fail{Backward.DanglingOperand{}} : Result<&2, &2, Backward.Error, Backward.Tape>}
404 {==}
405
406def Laws.backward_success(entries, output, inside, sound):
407 %nodes_length(entries) :
408 {Backward.merged(entries, Backward.checked(Backward.nodes(entries), _, output, Nat.is_lt(output, _),
409 Backward.wired(Backward.nodes(entries), _))) ==
410 Done{Backward.Tape{Backward.merge(entries, Backward.pass(Backward.nodes(entries), List.length(&2, Backward.Entry, entries), output))}} :
411 Result<&2, &2, Backward.Error, Backward.Tape>}
412 %Equal.sym(Bool, Nat.is_lt(output, List.length(&2, Backward.Entry, entries)), True{}, inside) :
413 {Backward.merged(entries, Backward.checked(Backward.nodes(entries), List.length(&2, Backward.Entry, entries), output, _,
414 Backward.wired(Backward.nodes(entries), List.length(&2, Backward.Entry, entries)))) ==
415 Done{Backward.Tape{Backward.merge(entries, Backward.pass(Backward.nodes(entries), List.length(&2, Backward.Entry, entries), output))}} :
416 Result<&2, &2, Backward.Error, Backward.Tape>}
417 %Equal.sym(Bool, Backward.wired(Backward.nodes(entries), List.length(&2, Backward.Entry, entries)), True{}, sound) :
418 {Backward.merged(entries, Backward.checked(Backward.nodes(entries), List.length(&2, Backward.Entry, entries), output, True{}, _)) ==
419 Done{Backward.Tape{Backward.merge(entries, Backward.pass(Backward.nodes(entries), List.length(&2, Backward.Entry, entries), output))}} :
420 Result<&2, &2, Backward.Error, Backward.Tape>}
421 {==}
422
423def and_true(+value: Bool) -> {Bool.and(value, True{}) == value : Bool}:
424 match value:
425 case True{}:
426 {==}
427 case False{}:
428 {==}
429
430def and_false(+value: Bool) -> {Bool.and(value, False{}) == False{} : Bool}:
431 match value:
432 case True{}:
433 {==}
434 case False{}:
435 {==}
436
437def operands_bounded(+node: Backward.Node, +bound: Nat) ->
438 {Backward.operands_below(node, bound) == Laws.bounded(Laws.targets(node), bound) : Bool}:
439 match node:
440 case Backward.Leaf{}:
441 {==}
442 case Backward.Add{a, b}:
443 Equal.cong(Bool, Bool, flag => Bool.and(Nat.is_lt(a, bound), flag), Nat.is_lt(b, bound), Bool.and(Nat.is_lt(b, bound), True{}),
444 Equal.sym(Bool, Bool.and(Nat.is_lt(b, bound), True{}), Nat.is_lt(b, bound), and_true(Nat.is_lt(b, bound))))
445 case Backward.Sub{a, b}:
446 Equal.cong(Bool, Bool, flag => Bool.and(Nat.is_lt(a, bound), flag), Nat.is_lt(b, bound), Bool.and(Nat.is_lt(b, bound), True{}),
447 Equal.sym(Bool, Bool.and(Nat.is_lt(b, bound), True{}), Nat.is_lt(b, bound), and_true(Nat.is_lt(b, bound))))
448 case Backward.Mul{a, b, left, right}:
449 Equal.cong(Bool, Bool, flag => Bool.and(Nat.is_lt(a, bound), flag), Nat.is_lt(b, bound), Bool.and(Nat.is_lt(b, bound), True{}),
450 Equal.sym(Bool, Bool.and(Nat.is_lt(b, bound), True{}), Nat.is_lt(b, bound), and_true(Nat.is_lt(b, bound))))
451 case Backward.Neg{a}:
452 Equal.sym(Bool, Bool.and(Nat.is_lt(a, bound), True{}), Nat.is_lt(a, bound), and_true(Nat.is_lt(a, bound)))
453
454def Laws.wired_matches_operand_bounds(graph):
455 match graph:
456 case Nil{}:
457 {==}
458 case Con{node, rest}:
459 %Equal.sym(Bool, Backward.operands_below(node, List.length(&2, Backward.Node, rest)),
460 Laws.bounded(Laws.targets(node), List.length(&2, Backward.Node, rest)), operands_bounded(node, List.length(&2, Backward.Node, rest))) :
461 {Bool.and(_, Backward.wired(rest, List.length(&2, Backward.Node, rest))) ==
462 Bool.and(Laws.bounded(Laws.targets(node), List.length(&2, Backward.Node, rest)), Laws.well_formed(rest)) : Bool}
463 Equal.cong(Bool, Bool, flag => Bool.and(Laws.bounded(Laws.targets(node), List.length(&2, Backward.Node, rest)), flag),
464 Backward.wired(rest, List.length(&2, Backward.Node, rest)), Laws.well_formed(rest), Laws.wired_matches_operand_bounds(rest))
465
466def wired_entries(+entries: List<&2, Backward.Entry>) ->
467 {Backward.wired(Backward.nodes(entries), List.length(&2, Backward.Entry, entries)) == Laws.well_formed(Backward.nodes(entries)) : Bool}:
468 %Equal.sym(Nat, List.length(&2, Backward.Entry, entries), List.length(&2, Backward.Node, Backward.nodes(entries)), nodes_length(entries)) :
469 {Backward.wired(Backward.nodes(entries), _) == Laws.well_formed(Backward.nodes(entries)) : Bool}
470 Laws.wired_matches_operand_bounds(Backward.nodes(entries))
471
472def head_ill_formed(+entry: Backward.Entry, +rest: List<&2, Backward.Entry>,
473 unbound: {Laws.bounded(Laws.targets(Laws.entry_node(entry)), List.length(&2, Backward.Entry, rest)) == False{} : Bool}) ->
474 {Laws.well_formed(Backward.nodes(entry <> rest)) == False{} : Bool}:
475 match entry:
476 case Backward.Entry{node, value, slot}:
477 %nodes_length(rest) :
478 {Bool.and(Laws.bounded(Laws.targets(node), _), Laws.well_formed(Backward.nodes(rest))) == False{} : Bool}
479 %Equal.sym(Bool, Laws.bounded(Laws.targets(node), List.length(&2, Backward.Entry, rest)), False{}, unbound) :
480 {Bool.and(_, Laws.well_formed(Backward.nodes(rest))) == False{} : Bool}
481 {==}
482
483def unbound_ill_formed(+newer: List<&2, Backward.Entry>, +entry: Backward.Entry, +rest: List<&2, Backward.Entry>,
484 +unbound: {Laws.bounded(Laws.targets(Laws.entry_node(entry)), List.length(&2, Backward.Entry, rest)) == False{} : Bool}) ->
485 {Laws.well_formed(Backward.nodes(List.append(&2, Backward.Entry, newer, entry <> rest))) == False{} : Bool}:
486 match newer:
487 case Nil{}:
488 head_ill_formed(entry, rest, unbound)
489 case Con{Backward.Entry{node, value, slot}, tail}:
490 %Equal.sym(Bool, Laws.well_formed(Backward.nodes(List.append(&2, Backward.Entry, tail, entry <> rest))), False{},
491 unbound_ill_formed(tail, entry, rest, unbound)) :
492 {Bool.and(Laws.bounded(Laws.targets(node), List.length(&2, Backward.Node, Backward.nodes(List.append(&2, Backward.Entry, tail, entry <> rest)))), _) ==
493 False{} : Bool}
494 and_false(Laws.bounded(Laws.targets(node), List.length(&2, Backward.Node, Backward.nodes(List.append(&2, Backward.Entry, tail, entry <> rest)))))
495
496def Laws.backward_rejects_unbound_operand(newer, entry, rest, output, inside, unbound):
497 Laws.backward_dangling(List.append(&2, Backward.Entry, newer, entry <> rest), output, inside,
498 Equal.trans(Bool, Backward.wired(Backward.nodes(List.append(&2, Backward.Entry, newer, entry <> rest)),
499 List.length(&2, Backward.Entry, List.append(&2, Backward.Entry, newer, entry <> rest))),
500 Laws.well_formed(Backward.nodes(List.append(&2, Backward.Entry, newer, entry <> rest))), False{},
501 wired_entries(List.append(&2, Backward.Entry, newer, entry <> rest)),
502 unbound_ill_formed(newer, entry, rest, unbound)))
503
504def Laws.backward_accepts_bound_operands(entries, output, inside, bound):
505 Laws.backward_success(entries, output, inside,
506 Equal.trans(Bool, Backward.wired(Backward.nodes(entries), List.length(&2, Backward.Entry, entries)),
507 Laws.well_formed(Backward.nodes(entries)), True{}, wired_entries(entries), bound))
508
509def nodes_merge(+entries: List<&2, Backward.Entry>, +gradients: List<&2, Maybe<&2, F32>>) ->
510 {Backward.nodes(entries) == Backward.nodes(Backward.merge(entries, gradients)) : List<&2, Backward.Node>}:
511 match entries gradients:
512 case Nil{} gradients:
513 {==}
514 case Con{Backward.Entry{node, value, slot}, rest} Nil{}:
515 {==}
516 case Con{Backward.Entry{node, value, slot}, rest} Con{gradient, more}:
517 Equal.cong(List<&2, Backward.Node>, List<&2, Backward.Node>, xs => node <> xs,
518 Backward.nodes(rest), Backward.nodes(Backward.merge(rest, more)), nodes_merge(rest, more))
519
520def Laws.backward_twice_accumulates(entries, output, found, computed):
521 %Equal.sym(Result<&2, &2, Backward.Error, List<&2, Maybe<&2, F32>>>, Backward.gradients(Backward.Tape{entries}, output), Done{found}, computed) :
522 {Laws.again(Backward.merged(entries, _), output) ==
523 Done{Backward.Tape{Backward.merge(Backward.merge(entries, found), found)}} : Result<&2, &2, Backward.Error, Backward.Tape>}
524 %nodes_merge(entries, found) :
525 {Backward.merged(Backward.merge(entries, found), Backward.planned(_, output)) ==
526 Done{Backward.Tape{Backward.merge(Backward.merge(entries, found), found)}} : Result<&2, &2, Backward.Error, Backward.Tape>}
527 %Equal.sym(Result<&2, &2, Backward.Error, List<&2, Maybe<&2, F32>>>, Backward.gradients(Backward.Tape{entries}, output), Done{found}, computed) :
528 {Backward.merged(Backward.merge(entries, found), _) ==
529 Done{Backward.Tape{Backward.merge(Backward.merge(entries, found), found)}} : Result<&2, &2, Backward.Error, Backward.Tape>}
530 {==}
531
532def Laws.backward_twice_mul(x, y):
533 {==}
534
535def Laws.zero_grad_empties(entries):
536 match entries:
537 case Nil{}:
538 {==}
539 case Con{Backward.Entry{node, value, slot}, rest}:
540 Equal.cong(List<&2, Maybe<&2, F32>>, List<&2, Maybe<&2, F32>>, xs => None{} <> xs,
541 Laws.slots(Backward.cleared(rest)), Backward.nones(List.length(&2, Backward.Entry, rest)), Laws.zero_grad_empties(rest))
542
543def Laws.zero_grad_keeps_nodes(entries):
544 match entries:
545 case Nil{}:
546 {==}
547 case Con{Backward.Entry{node, value, slot}, rest}:
548 Equal.cong(List<&2, Backward.Node>, List<&2, Backward.Node>, xs => node <> xs,
549 Backward.nodes(Backward.cleared(rest)), Backward.nodes(rest), Laws.zero_grad_keeps_nodes(rest))