Permutations as data

A permutation of the entries of a vector of length n is a sequence of steps (PermS), each a numpy operation on the vector reshaped, row-major, to a shape dims with n entries:

step	numpy
tr dims axes	x.reshape(dims).transpose(axes).reshape(-1)
flip dims k	jnp.flip(x.reshape(dims), k).reshape(-1)
roll dims k s	jnp.roll(x.reshape(dims), s, axis=k).reshape(-1)

The steps apply in order. Each acts as a gather: output position i reads input position idx i, so the sequence [p₁, p₂, …] reads p₁.idx (p₂.idx (… i)) (PermS.idx). The squeezes and patchings of the models are transposes, their channel and token reversals flips, and their rotations rolls.

Nothing here uses Mathlib: the flow signature (Flow.Basic) reads PermS.idx as an Equiv.Perm, and the printer (Flow.Print) prints the steps.

inductive RoleFlow.Flow.PermStep : Type

One step of a permutation, on the vector reshaped to dims.

• tr (dims axes : List Nat) : PermStep

  Permute the axes: output axis j is input axis axes[j].

• flip (dims : List Nat) (k : Nat) : PermStep

  Reverse axis k.

• roll (dims : List Nat) (k s : Nat) : PermStep

  Rotate axis k by s: output index j reads j - s (mod the axis length).

@[implicit_reducible]

instance RoleFlow.Flow.instDecidableEqPermStep : DecidableEq PermStep

Equations

• RoleFlow.Flow.instDecidableEqPermStep = RoleFlow.Flow.instDecidableEqPermStep.decEq

def RoleFlow.Flow.instDecidableEqPermStep.decEq (x✝ x✝¹ : PermStep) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• RoleFlow.Flow.instDecidableEqPermStep.decEq (RoleFlow.Flow.PermStep.tr dims axes) (RoleFlow.Flow.PermStep.flip dims_1 k) = isFalse ⋯
• RoleFlow.Flow.instDecidableEqPermStep.decEq (RoleFlow.Flow.PermStep.tr dims axes) (RoleFlow.Flow.PermStep.roll dims_1 k s) = isFalse ⋯
• RoleFlow.Flow.instDecidableEqPermStep.decEq (RoleFlow.Flow.PermStep.flip dims k) (RoleFlow.Flow.PermStep.tr dims_1 axes) = isFalse ⋯
• RoleFlow.Flow.instDecidableEqPermStep.decEq (RoleFlow.Flow.PermStep.flip dims k) (RoleFlow.Flow.PermStep.roll dims_1 k_1 s) = isFalse ⋯
• RoleFlow.Flow.instDecidableEqPermStep.decEq (RoleFlow.Flow.PermStep.roll dims k s) (RoleFlow.Flow.PermStep.tr dims_1 axes) = isFalse ⋯
• RoleFlow.Flow.instDecidableEqPermStep.decEq (RoleFlow.Flow.PermStep.roll dims k s) (RoleFlow.Flow.PermStep.flip dims_1 k_1) = isFalse ⋯

@[implicit_reducible]

instance RoleFlow.Flow.instReprPermStep : Repr PermStep

Equations

• RoleFlow.Flow.instReprPermStep = { reprPrec := RoleFlow.Flow.instReprPermStep.repr }

def RoleFlow.Flow.instReprPermStep.repr : PermStep → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance RoleFlow.Flow.instInhabitedPermStep : Inhabited PermStep

Equations

• RoleFlow.Flow.instInhabitedPermStep = { default := RoleFlow.Flow.instInhabitedPermStep.default }

@[reducible, inline]

abbrev RoleFlow.Flow.PermS : Type

A permutation: its steps, applied in order.

Equations

• RoleFlow.Flow.PermS = List RoleFlow.Flow.PermStep

def RoleFlow.Flow.PermStep.digits (dims : List Nat) (i : Nat) : List Nat

The row-major digits of i in the shape dims.

Equations

• RoleFlow.Flow.PermStep.digits dims i = (List.foldr (fun (d : Nat) (x : List Nat × Nat) => match x with | (acc, j) => (j % d :: acc, j / d)) ([], i) dims).fst

def RoleFlow.Flow.PermStep.undigits (dims ds : List Nat) : Nat

The position of the digits ds in the shape dims.

Equations

• RoleFlow.Flow.PermStep.undigits dims ds = List.foldl (fun (acc : Nat) (x : Nat × Nat) => match x with | (d, x) => acc * d + x) 0 (dims.zip ds)

def RoleFlow.Flow.PermStep.dims : PermStep → List Nat

Equations

• (RoleFlow.Flow.PermStep.tr a a_1).dims = a
• (RoleFlow.Flow.PermStep.flip a a_1).dims = a
• (RoleFlow.Flow.PermStep.roll a a_1 a_2).dims = a

def RoleFlow.Flow.PermStep.idx : PermStep → Nat → Nat

The input position that output position i reads.

Equations

• One or more equations did not get rendered due to their size.

def RoleFlow.Flow.PermStep.inv : PermStep → PermStep

The step that undoes this one.

Equations

• (RoleFlow.Flow.PermStep.tr a a_1).inv = RoleFlow.Flow.PermStep.tr (List.map (fun (a_2 : Nat) => a.getD a_2 1) a_1) (List.map (fun (a : Nat) => List.idxOf a a_1) (List.range a_1.length))
• (RoleFlow.Flow.PermStep.flip a a_1).inv = RoleFlow.Flow.PermStep.flip a a_1
• (RoleFlow.Flow.PermStep.roll a a_1 a_2).inv = RoleFlow.Flow.PermStep.roll a a_1 ((a.getD a_1 1 - a_2 % a.getD a_1 1) % a.getD a_1 1)

def RoleFlow.Flow.PermStep.ok (n : Nat) (p : PermStep) : Bool

The step is well formed on vectors of length n: its shape has n entries, axes is a permutation of the axes, and k is an axis.

Equations

• One or more equations did not get rendered due to their size.
• RoleFlow.Flow.PermStep.ok n (RoleFlow.Flow.PermStep.flip a a_1) = (List.foldl (fun (x1 x2 : Nat) => x1 * x2) 1 (RoleFlow.Flow.PermStep.flip a a_1).dims == n && decide (a_1 < a.length))
• RoleFlow.Flow.PermStep.ok n (RoleFlow.Flow.PermStep.roll a a_1 a_2) = (List.foldl (fun (x1 x2 : Nat) => x1 * x2) 1 (RoleFlow.Flow.PermStep.roll a a_1 a_2).dims == n && decide (a_1 < a.length))

def RoleFlow.Flow.PermStep.embed (outer inner : Nat) (p : PermStep) : PermStep

The step on the middle of the shape [outer] ++ dims ++ [inner] (an axis of length 1 is left out).

Equations

• One or more equations did not get rendered due to their size.

def RoleFlow.Flow.PermStep.isId : PermStep → Bool

The step does nothing: a transpose with the axes in order, a flip of an axis of length at most 1, a roll by a multiple of the axis length.

Equations

• (RoleFlow.Flow.PermStep.tr a a_1).isId = (a_1 == List.range a_1.length)
• (RoleFlow.Flow.PermStep.flip a a_1).isId = decide (a.getD a_1 1 ≤ 1)
• (RoleFlow.Flow.PermStep.roll a a_1 a_2).isId = (a_2 % a.getD a_1 1 == 0)

def RoleFlow.Flow.PermStep.text : PermStep → String

The step in the surface syntax of the webapp, before its argument: tr<[2, 3], [1, 0]>.

Equations

• (RoleFlow.Flow.PermStep.tr a a_1).text = toString "tr<" ++ toString a ++ toString ", " ++ toString a_1 ++ toString ">"
• (RoleFlow.Flow.PermStep.flip a a_1).text = toString "flip<" ++ toString a ++ toString ", " ++ toString a_1 ++ toString ">"
• (RoleFlow.Flow.PermStep.roll a a_1 a_2).text = toString "roll<" ++ toString a ++ toString ", " ++ toString a_1 ++ toString ", " ++ toString a_2 ++ toString ">"

def RoleFlow.Flow.PermS.text (x : String) (ps : PermS) : String

The steps applied to x, in the surface syntax of the webapp.

Equations

• RoleFlow.Flow.PermS.text x ps = List.foldl (fun (x : String) (p : RoleFlow.Flow.PermStep) => toString p.text ++ toString "(" ++ toString x ++ toString ")") x ps

def RoleFlow.Flow.PermS.idx (ps : PermS) (i : Nat) : Nat

The input position that output position i reads.

Equations

• ps.idx i = List.foldr RoleFlow.Flow.PermStep.idx i ps

def RoleFlow.Flow.PermS.inv (ps : PermS) : PermS

The steps that undo ps.

Equations

• ps.inv = List.map RoleFlow.Flow.PermStep.inv (List.reverse ps)

def RoleFlow.Flow.PermS.ok (n : Nat) (ps : PermS) : Bool

Every step is well formed on vectors of length n.

Equations

• RoleFlow.Flow.PermS.ok n ps = List.all ps (RoleFlow.Flow.PermStep.ok n)

def RoleFlow.Flow.PermS.idxList (n : Nat) (ps : PermS) : List Nat

The index list [idx 0, …, idx (n - 1)].

Equations

• RoleFlow.Flow.PermS.idxList n ps = List.map ps.idx (List.range n)

def RoleFlow.Flow.PermS.valid (n : Nat) (ps : PermS) : Bool

ps is a permutation of 0, …, n - 1: well formed, and its index list is one.

Equations

• One or more equations did not get rendered due to their size.