src/tensor/reduction_LAWS.bend
bendtorch-core@0.1.0.0 · 191 lines · 30 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
4import bendtorch-core@0.1.0.0/src/tensor/reduction.bend as Reduction
5import bendtorch-core@0.1.0.0/src/tensor/math_totality.bend as Totality
6
7def LogicalValues(+fuel: Nat, -shape: Shape.Shape, -tensor: Core.Tensor<shape>, +cursor: Nat,
8 values: List<&2, F32>) -> Data:
9 match fuel values:
10 case 0n Nil{}:
11 Unit
12 case 1n+tail value <> values:
13 LogicalStep<tail, shape, tensor, cursor, value, values>
14 case 0n value <> values:
15 Empty
16 case 1n+tail Nil{}:
17 Empty
18
19type LogicalStep<-fuel: Nat, -shape: Shape.Shape, -tensor: Core.Tensor<shape>, -cursor: Nat,
20 -value: F32, -values: List<&2, F32>> is Data:
21 LogicalStep{-exact: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat},
22 -observed: {Core.checked_observe(shape, tensor, U32.from_nat(cursor)) == Some{value} : Maybe<&2, F32>},
23 -remaining: LogicalValues(fuel, shape, tensor, 1n+cursor, values)}
24
25type SumMeaning<-fuel: Nat, -shape: Shape.Shape, -tensor: Core.Tensor<shape>, -cursor: Nat,
26 -accumulator: F32, -value: F32> is Data:
27 SumMeaning{-values: List<&2, F32>, -logical: LogicalValues(fuel, shape, tensor, cursor, values),
28 -fold: {value == Reduction.sequential_sum(values, accumulator) : F32}}
29
30def LoopMeaning(-fuel: Nat, -shape: Shape.Shape, -original: Core.Tensor<shape>, -cursor: Nat, -accumulator: F32,
31 result: Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>) -> Data:
32 match result:
33 case Fail{error}:
34 Unit
35 case Done{pair}:
36 (tensor, value) = pair
37 SumMeaning<fuel, shape, original, cursor, accumulator, value>
38
39type SourceSum<-fuel: Nat, -shape: Shape.Shape, -original: Core.Tensor<shape>, -cursor: Nat, -accumulator: F32,
40 -result: Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>> is Data:
41 SourceSum{-meaning: @unit: Unit -> LoopMeaning(fuel, shape, original, cursor, accumulator, result)}
42
43law successful_loop_interpretation:
44 for +fuel: Nat
45 for -shape: Shape.Shape
46 for tensor: Core.Tensor<shape>
47 for +cursor: Nat
48 for +accumulator: F32
49 SourceSum<fuel, shape, tensor, cursor, accumulator, Reduction.natural_sum_loop(fuel, shape, tensor, cursor, accumulator)>
50
51def loop_value(-shape: Shape.Shape, result: Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>) -> Maybe<&2, F32>:
52 match result:
53 case Fail{error}:
54 None{}
55 case Done{pair}:
56 (tensor, value) = pair
57 Some{value}
58
59def retained_observe(-shape: Shape.Shape, result: Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>, +other: U32) -> Maybe<&2, F32>:
60 match result:
61 case Fail{error}:
62 None{}
63 case Done{pair}:
64 (tensor, value) = pair
65 Core.checked_observe(shape, tensor, other)
66
67def successful_observe(-shape: Shape.Shape, original: Core.Tensor<shape>,
68 result: Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>, +other: U32) -> Maybe<&2, F32>:
69 match result:
70 case Fail{error}:
71 None{}
72 case Done{pair}:
73 Core.checked_observe(shape, original, other)
74
75type Preserved<-shape: Shape.Shape, -original: Core.Tensor<shape>,
76 -result: Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>> is Data:
77 Preserved{-kept: @+other: U32 ->
78 {retained_observe(shape, result, other) == successful_observe(shape, original, result, other) : Maybe<&2, F32>}}
79
80type Interpretation<-actual: Maybe<&2, F32>, -expected: Maybe<&2, F32>> is Data:
81 Interpretation{-proof: @unit: Unit -> {actual == expected : Maybe<&2, F32>}}
82
83law ordered_loop_interpretation:
84 for +fuel: Nat
85 for -shape: Shape.Shape
86 for tensor: Core.Tensor<shape>
87 for +cursor: Nat
88 for +accumulator: F32
89 for +values: List<&2, F32>
90 for logical: LogicalValues(fuel, shape, tensor, cursor, values)
91 Interpretation<loop_value(shape, Reduction.natural_sum_loop(fuel, shape, tensor, cursor, accumulator)),
92 Some{Reduction.sequential_sum(values, accumulator)}>
93
94law ordered_loop_preservation:
95 for +fuel: Nat
96 for -shape: Shape.Shape
97 for tensor: Core.Tensor<shape>
98 for +cursor: Nat
99 for +accumulator: F32
100 Preserved<shape, tensor, Reduction.natural_sum_loop(fuel, shape, tensor, cursor, accumulator)>
101
102law ordered_sum_interpretation:
103 for +shape: Shape.Shape
104 for tensor: Core.Tensor<shape>
105 for +values: List<&2, F32>
106 for logical: LogicalValues(Shape.logical_numel(Shape.dimensions(shape)), shape, tensor, 0n, values)
107 Interpretation<Reduction.sum_observation(shape, Reduction.sum(shape, tensor)), Some{Reduction.sequential_sum(values, 0.0)}>
108
109type SumResult<-shape: Shape.Shape, -original: Core.Tensor<shape>, -retained: Core.Tensor<shape>,
110 -scalar: Core.Tensor<Reduction.scalar_shape()>> is Data:
111 SumResult{-values: List<&2, F32>, -logical: LogicalValues(Shape.logical_numel(Shape.dimensions(shape)), shape, original, 0n, values),
112 -meaning: {Core.observe(Reduction.scalar_shape(), scalar, 0) == Some{Reduction.sequential_sum(values, 0.0)} : Maybe<&2, F32>},
113 -kept: @+index: U32 -> {Core.checked_observe(shape, retained, index) == Core.checked_observe(shape, original, index) : Maybe<&2, F32>}}
114
115def SumResultMeaning(-shape: Shape.Shape, -original: Core.Tensor<shape>,
116 result: Result<&2, &1, Core.Error, Core.Tensor<shape> & Core.Tensor<Reduction.scalar_shape()>>) -> Data:
117 match result:
118 case Fail{error}:
119 Unit
120 case Done{pair}:
121 (retained, scalar) = pair
122 SumResult<shape, original, retained, scalar>
123
124type SourceSumResult<-shape: Shape.Shape, -original: Core.Tensor<shape>,
125 -result: Result<&2, &1, Core.Error, Core.Tensor<shape> & Core.Tensor<Reduction.scalar_shape()>>> is Data:
126 SourceSumResult{-meaning: @unit: Unit -> SumResultMeaning(shape, original, result)}
127
128law successful_sum_interpretation:
129 for +shape: Shape.Shape
130 for tensor: Core.Tensor<shape>
131 SourceSumResult<shape, tensor, Reduction.sum(shape, tensor)>
132
133type DynamicSumSuccess<-original: Core.Dynamic, -retained: Core.Dynamic, -scalar: Core.Dynamic> is Data:
134 DynamicSumSuccess{-shape: Shape.Shape, -input: Core.Tensor<shape>, -owner: Core.Tensor<shape>, -output: Core.Tensor<Reduction.scalar_shape()>,
135 -input_exact: {original == Core.Packed{shape, input} : Core.Dynamic}, -owner_exact: {retained == Core.Packed{shape, owner} : Core.Dynamic},
136 -scalar_exact: {scalar == Core.Packed{Reduction.scalar_shape(), output} : Core.Dynamic}, -source: SumResult<shape, input, owner, output>}
137
138def DynamicSumMeaning(-original: Core.Dynamic, result: Result<&2, &1, Core.Error, Core.Dynamic & Core.Dynamic>) -> Data:
139 match result:
140 case Fail{error}:
141 Unit
142 case Done{pair}:
143 (retained, scalar) = pair
144 DynamicSumSuccess<original, retained, scalar>
145
146type SourceDynamicSum<-original: Core.Dynamic, -result: Result<&2, &1, Core.Error, Core.Dynamic & Core.Dynamic>> is Data:
147 SourceDynamicSum{-meaning: @unit: Unit -> DynamicSumMeaning(original, result)}
148
149law successful_dynamic_sum_interpretation:
150 for tensor: Core.Dynamic
151 SourceDynamicSum<tensor, Reduction.sum_dynamic(tensor)>
152
153law empty_accumulation:
154 for -shape: Shape.Shape
155 for tensor: Core.Tensor<shape>
156 for +index: U32
157 for accumulator: F32
158 {Reduction.sum_loop(0n, shape, tensor, index, accumulator) == Done{(tensor, accumulator)} : Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>}
159
160law empty_sum_identity:
161 for +shape: Shape.Shape
162 for tensor: Core.Tensor<shape>
163 for empty: {Shape.logical_numel(Shape.dimensions(shape)) == 0n : Nat}
164 {Reduction.sum_observation(shape, Reduction.sum(shape, tensor)) == Some{0.0} : Maybe<&2, F32>}
165
166law sum_valid_success:
167 for +shape: Shape.Shape
168 for tensor: Core.Tensor<shape>
169 Totality.Success<Core.Error, Core.Tensor<shape> & Core.Tensor<Reduction.scalar_shape()>, Reduction.sum(shape, tensor)>
170
171law sum_dynamic_valid_success:
172 for tensor: Core.Dynamic
173 Totality.Success<Core.Error, Core.Dynamic & Core.Dynamic, Reduction.sum_dynamic(tensor)>
174
175type TotalSum<-shape: Shape.Shape, -original: Core.Tensor<shape>,
176 -result: Result<&2, &1, Core.Error, Core.Tensor<shape> & Core.Tensor<Reduction.scalar_shape()>>> is Data:
177 TotalSum{-done: Totality.Success<Core.Error, Core.Tensor<shape> & Core.Tensor<Reduction.scalar_shape()>, result>,
178 -interpretation: SourceSumResult<shape, original, result>}
179
180type TotalDynamicSum<-original: Core.Dynamic, -result: Result<&2, &1, Core.Error, Core.Dynamic & Core.Dynamic>> is Data:
181 TotalDynamicSum{-done: Totality.Success<Core.Error, Core.Dynamic & Core.Dynamic, result>,
182 -interpretation: SourceDynamicSum<original, result>}
183
184law sum_valid_result:
185 for +shape: Shape.Shape
186 for tensor: Core.Tensor<shape>
187 TotalSum<shape, tensor, Reduction.sum(shape, tensor)>
188
189law sum_dynamic_valid_result:
190 for tensor: Core.Dynamic
191 TotalDynamicSum<tensor, Reduction.sum_dynamic(tensor)>