Recognizing a parameter row's descriptor

The table of an apply's right side holds its rows under every descriptor, and the apply's left row has to pick out its own: the descriptor whose cells are the codes of its components. That is a predicate over the row and a descriptor's cells (Sym.matchSP): each cell is a value equal to the component, or a gap whose bounds enclose it; and the ranks recorded in the fresh cells of one gap are ordered as their components, without a hole below any of them. Over cells the cut can produce, it holds exactly of the row's own descriptor (Sym.eval3_matchSP).

Gaps and bounds

Truth of comparisons over columns

A component against its cell

def Sym.freshIn {T : Type} [ValueType T] {c N k : ℕ} (a : SA T c N) (x : Fin (7 + k) → SA T c N) : SP T c N

The component lies in the cell's gap.

Equations

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

def Sym.cellMatch {T : Type} [ValueType T] {c N k : ℕ} (a : SA T c N) (x : Fin (7 + k) → SA T c N) : SP T c N

The component is what the cell codes: the value itself, or a value of its gap.

Equations

• Sym.cellMatch a x = ((Sym.isZ (x (Sym.iF k))).and (Sym.SP.atom CompOp.syneq a (x (Sym.iV k)))).or ((Sym.isN (x (Sym.iF k))).and (Sym.freshIn a x))

def Sym.ShapeOK {T : Type} [ValueType T] (C : Finset T) (k : ℕ) : Code T → Prop

The codes a cell of a descriptor can hold.

Equations

• Sym.ShapeOK C k (Sym.Code.conc a) = (a ∈ C)
• Sym.ShapeOK C k (Sym.Code.fresh l r) = (Sym.GapOK C l ∧ r ≤ k)

def Sym.Fits {T : Type} [ValueType T] (C : Finset T) (v : T) : Code T → Prop

A value fits a code: it is the code's value, or a fresh value of the code's gap.

Equations

• Sym.Fits C v (Sym.Code.conc a) = (v = a)
• Sym.Fits C v (Sym.Code.fresh l r) = (Sym.IsFresh C v ∧ Sym.lo C v = l)

Ranks recorded consistently are the ranks

noncomputable def Sym.below' {T : Type} [ValueType T] {k : ℕ} (C : Finset T) (par : Fin k → T) (a : T) : Finset T

The fresh components of a row in a value's gap below it.

Equations

• Sym.below' C par a = {b ∈ Finset.image par Finset.univ | Sym.IsFresh C b ∧ Sym.lo C b = Sym.lo C a ∧ b < a}

Unary ranks up to k

The descriptor of a row, as a predicate

def Sym.sameGap {T : Type} {c N k : ℕ} (x y : Fin (7 + k) → SA T c N) : SP T c N

Two cells are of one gap.

Equations

• Sym.sameGap x y = (Sym.SP.atom CompOp.syneq (x (Sym.iB k)) (y (Sym.iB k))).and (Sym.SP.atom CompOp.syneq (x (Sym.iV k)) (y (Sym.iV k)))

def Sym.iffSP {T : Type} {c N : ℕ} (p q : SP T c N) : SP T c N

Two predicates agree.

Equations

• Sym.iffSP p q = (p.and q).or (p.not.and q.not)

def Sym.rankPair {T : Type} [ValueType T] {c N k : ℕ} (a b : SA T c N) (x y : Fin (7 + k) → SA T c N) : SP T c N

Two fresh cells of one gap record ranks ordered as their components.

Equations

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

def Sym.thZero {T : Type} [ValueType T] {c N k : ℕ} (x : Fin (7 + k) → SA T c N) : SP T c N

The rank is 0.

Equations

• Sym.thZero x = Sym.andAll (List.map (fun (m : Fin k) => Sym.isLo (x (Sym.iR m))) (List.finRange k))

def Sym.thSucc {T : Type} [ValueType T] {c N k : ℕ} (x y : Fin (7 + k) → SA T c N) : SP T c N

The second rank is the next of the first.

Equations

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

def Sym.contigSP {T : Type} [ValueType T] {c N k : ℕ} (d : Fin k → Fin (7 + k) → SA T c N) (i : Fin k) : SP T c N

A fresh cell's rank leaves no hole below it.

Equations

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

def Sym.matchSP {T : Type} [ValueType T] {c N k : ℕ} (u : Fin k → SA T c N) (d : Fin k → Fin (7 + k) → SA T c N) : SP T c N

The descriptor's cells are the codes of the row's components.

Equations

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

theorem Sym.eval3_matchSP_true {T : Type} [ValueType T] {C : Finset T} {c N k : ℕ} (u : Fin k → SA T c N) (d : Fin k → Fin (7 + k) → SA T c N) (r : Tuple T N) (γ : Fin c → T) (par : Fin k → T) (cd : Fin k → Code T) (hu : ∀ (i : Fin k), (u i).eval r γ = par i) (hd : ∀ (i : Fin k) (j : Fin (7 + k)), (d i j).eval r γ = enc C k (cd i) j) (hshape : ∀ (i : Fin k), ShapeOK C k (cd i)) : (matchSP u d).eval3 r γ = Kleene.true ↔ ∀ (i : Fin k), cd i = code C par i

Over cells the cut can produce, the predicate holds exactly of a row's own descriptor.

Reading an output cell back as a value

def Sym.cellEq {T : Type} {c N k : ℕ} (x y : Fin (7 + k) → SA T c N) : SP T c N

Two cells are equal, column by column.

Equations

• Sym.cellEq x y = Sym.andAll (List.map (fun (j : Fin (7 + k)) => Sym.SP.atom CompOp.syneq (x j) (y j)) (List.finRange (7 + k)))

def Sym.decCell {T : Type} [ValueType T] {c N k : ℕ} (w : SA T c N) (x : Fin (7 + k) → SA T c N) (u : Fin k → SA T c N) (d : Fin k → Fin (7 + k) → SA T c N) : SP T c N

A value is what an output cell codes: the cell's value, or the component whose descriptor cell the output cell is.

Equations

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

theorem Sym.eval3_decCell_true {T : Type} [ValueType T] {C : Finset T} {c N k : ℕ} (w : SA T c N) (x : Fin (7 + k) → SA T c N) (u : Fin k → SA T c N) (d : Fin k → Fin (7 + k) → SA T c N) (r : Tuple T N) (γ : Fin c → T) (par : Fin k → T) (v : T) (hu : ∀ (i : Fin k), (u i).eval r γ = par i) (hd : ∀ (i : Fin k) (j : Fin (7 + k)), (d i j).eval r γ = enc C k (code C par i) j) (hx : ∀ (j : Fin (7 + k)), (x j).eval r γ = enc C k (vcode C par v) j) : (decCell w x u d).eval3 r γ = Kleene.true ↔ w.eval r γ = v

An output cell decodes to the value it codes.

Home · Documentation · Publications · Contributors · Source · Cite