src/tensor/transpose_LAWS.bend

bendtorch-core@0.1.0.0 · 45 lines · 4 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/axis_spec.bend as Axis
4import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
5import bendtorch-core@0.1.0.0/src/tensor/transpose_spec.bend as Transpose
6import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Values
7
8law transpose_axes_requested:
9  for +shape: Shape.Shape
10  for +a: U32
11  for +b: U32
12  for +inside: {True{} == Transpose.valid(shape, a, b) : Bool}
13  {Layout.transpose_axes(Shape.dimensions(shape), a, b, 0) ==
14    Transpose.requested_axes(Shape.rank_dimensions(Shape.dimensions(shape)), U32.to_nat(a), U32.to_nat(b)) : List<&2, U32>}
15
16law transpose_axes_valid:
17  for +shape: Shape.Shape
18  for +a: U32
19  for +b: U32
20  for +inside: {True{} == Transpose.valid(shape, a, b) : Bool}
21  {True{} == Layout.bijective(shape, Layout.transpose_axes(Shape.dimensions(shape), a, b, 0)) : Bool}
22
23law transpose_axes_self_inverse:
24  for +shape: Shape.Shape
25  for +a: U32
26  for +b: U32
27  for +inside: {True{} == Transpose.valid(shape, a, b) : Bool}
28  {Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(shape)), Shape.naturals(Layout.transpose_axes(Shape.dimensions(shape), a, b, 0))) ==
29    Shape.naturals(Layout.transpose_axes(Shape.dimensions(shape), a, b, 0)) : List<&2, Nat>}
30
31# The index map of a rank-2 transpose reads the transposed cell. For an input
32# of dimensions [rows, columns], output cell [j, l] of the [columns, rows]
33# transpose sits at j * rows + l, and `permute_source` with axes [1, 0] sends
34# it to input index l * columns + j, the input cell [l, j].
35law permute_source_transposed:
36  for +input: Shape.Shape
37  for +rows: U32
38  for +columns: U32
39  for matrix: {Shape.dimensions(input) == [rows, columns] : List<&2, U32>}
40  for +j: Nat
41  for j_below: {Nat.is_lt(j, U32.to_nat(columns)) == True{} : Bool}
42  for +l: Nat
43  for l_below: {Nat.is_lt(l, U32.to_nat(rows)) == True{} : Bool}
44  {Values.permute_source(input, [1, 0], U32.from_nat(Nat.add(Nat.mul(j, U32.to_nat(rows)), l))) ==
45    Some{U32.from_nat(Nat.add(Nat.mul(l, U32.to_nat(columns)), j))} : Maybe<&2, U32>}