Hom commutation, token and annotation layer

The value-level content of “compile once, evaluate many” for the general evaluator: every ingredient of a row's annotation is an ⊕/⊗/⊖/δ-polynomial in the occurrence annotations, so it commutes with every SemiringWithMonusHom:

• GenAnn.finalize_mapHom – the finalized factored annotation commutes (this is where map_delta enters, for the pending group factors);
• AggValue.predProv_mapAnn – the predicate provenance of a comparison against a token commutes: the world annotations are ⊗/⊖-polynomials and the characteristic values χ are {𝟘,𝟙}-valued, with the aggregate values themselves untouched by the pushforward;
• GenPred.predsem_mapAnn – the predicate provenance of a whole generalized predicate commutes (∧ ↦ ⊗, ∨ ↦ ⊕ through map_mul and map_add, ¬ by polarity).

These are unconditional, but they do not by themselves give the evaluator-level commutation AggQuery.evaluateAnnotated_hom at the bottom of this file: the evaluator's supersede and cashing decisions compare annotation lists for equality, which a non-injective hom can conflate (licensing supersedes on the target side that the source side does not take), and the ≼-order's annotation tie-break in havingGroup need not be preserved. Both divergences are value-neutral, so the theorem holds with no hypothesis on the hom, the query or the m-semiring:

• an extra supersede only drops a group guard standing next to an annotation that already contains an occurrence of that group, which delta_absorb makes redundant;
• a changed tie-break only permutes occurrences carrying the same tuple part, hence the same aggregated-term value, and the tie-block congruence of Provenance.AggValueCongr shows such a permutation leaves the predicate provenance alone. GenRow.Sim below carries that slack row by row through the evaluator, and GenRow.Sim.toAnnotated_eq cashes it into an equality of finalized annotated tuples.

The annotation pushforward

def GenAnn.mapHom {K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] (h : SemiringWithMonusHom K K') (a : GenAnn K) : GenAnn K'

Pushforward of a factored annotation along h.

Equations

• GenAnn.mapHom h a = { base := h.toRingHom a.base, pending := Multiset.map (List.map ⇑h.toRingHom) a.pending }

theorem chi_hom {T : Type} [ValueType T] {K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] (h : SemiringWithMonusHom K K') (op : CompOp) (a b : T) : h.toRingHom (Having.chi op a b) = Having.chi op a b

The characteristic value of a comparison commutes with any hom (χ is {𝟘,𝟙}-valued).

theorem worldAnn_hom {K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] (h : SemiringWithMonusHom K K') {N : ℕ} (α : Fin N → K) (W : Finset (Fin N)) : h.toRingHom (Having.worldAnn α W) = Having.worldAnn (fun (i : Fin N) => h.toRingHom (α i)) W

The factored world annotation commutes with any hom: it is an ⊗/⊖-polynomial in the occurrence annotations.

theorem GenAnn.finalize_mapHom {K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] (h : SemiringWithMonusHom K K') (a : GenAnn K) : (mapHom h a).finalize = h.toRingHom a.finalize

The finalized factored annotation commutes with any hom (the pending group factors through map_delta).

The token pushforward

theorem AggValue.length_mapAnn_occs {T K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] (h : SemiringWithMonusHom K K') (a : AggValue T K) : a.occs.length = (mapAnn (⇑h.toRingHom) a).occs.length

The occurrence payload keeps its length under the pushforward.

theorem AggValue.anns_mapAnn {T K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] (h : SemiringWithMonusHom K K') (a : AggValue T K) (i : Fin a.occs.length) : (mapAnn (⇑h.toRingHom) a).anns ((finCongr ⋯) i) = h.toRingHom (a.anns i)

The pushed-forward annotations, along the reindexing.

theorem AggValue.valOn_mapAnn {T K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] (h : SemiringWithMonusHom K K') (a : AggValue T K) (W : Finset (Fin a.occs.length)) : (mapAnn (⇑h.toRingHom) a).valOn (Finset.map (finCongr ⋯).toEmbedding W) = a.valOn W

The per-world aggregate value is untouched by the pushforward.

theorem AggValue.predProv_mapAnn {T : Type} [ValueType T] {K K' : Type} [CommSemiringWithMonus K] [DecidableEq K] [CommSemiringWithMonus K'] [DecidableEq K'] (h : SemiringWithMonusHom K K') (a : AggValue T K) (op : CompOp) (c : T) : (mapAnn (⇑h.toRingHom) a).predProv op c = h.toRingHom (a.predProv op c)

Token-level hom commutation. The predicate provenance of a comparison against a token commutes with every SemiringWithMonusHom: it is an ⊕/⊗/⊖-polynomial in the occurrence annotations, and the aggregate values compared are untouched by the pushforward.

The predicate pushforward

theorem TermG.eval_mapAnnSum {T : Type} [ValueType T] {K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] {n : ℕ} {κ : Fin n → ColKind} (h : SemiringWithMonusHom K K') (t : TermG T κ) (u : Tuple (GenValue T K) n) : (t.eval fun (k : Fin n) => AggValue.mapAnnSum (⇑h.toRingHom) (u k)) = t.eval u

Terms over regular columns are untouched by the pushforward (their token reads collapse, and collapse is annotation-independent).

theorem GenPred.predsem_mapAnn {T : Type} [ValueType T] {K K' : Type} [CommSemiringWithMonus K] [DecidableEq K] [CommSemiringWithMonus K'] [DecidableEq K'] {n : ℕ} {κ : Fin n → ColKind} (h : SemiringWithMonusHom K K') (φ : GenPred T κ) (neg : Bool) (u : Tuple (GenValue T K) n) : (φ.predsem neg fun (k : Fin n) => AggValue.mapAnnSum (⇑h.toRingHom) (u k)) = h.toRingHom (φ.predsem neg u)

Predicate-level hom commutation. The predicate provenance of a generalized predicate commutes with every SemiringWithMonusHom: regular atoms through χ, aggregate atoms through the token-level commutation, ∧ ↦ ⊗ and ∨ ↦ ⊕ through map_mul and map_add, and ¬ by polarity.

Guard absorption

The first substantive use of the delta_absorb axiom: an existence-entailing predicate provenance algebraically absorbs its group's δ-guard. Every monomial of the possible-world sum contains some occurrence annotation of the group (the worlds are non-empty), and delta_absorb lets that occurrence swallow δ of the whole group sum.

theorem AggValue.predProv_delta_absorb {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] (a : AggValue T K) (op : CompOp) (c : T) : a.predProv op c * SemiringWithMonus.delta (List.map Prod.snd a.occs).sum = a.predProv op c

A token's predicate provenance absorbs the δ-guard of its own group.

theorem GenPred.predsem_delta_absorb {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] {n : ℕ} {κ : Fin n → ColKind} (φ : GenPred T κ) (neg : Bool) (u : Tuple (GenValue T K) n) (ℓ₀ : List K) (huni : ∀ k ∈ φ.comparedCols, ∀ (a : AggValue T K), u k = Sum.inr a → List.map Prod.snd a.occs = ℓ₀) (hent : φ.entailsExistence neg = true) : φ.predsem neg u * SemiringWithMonus.delta ℓ₀.sum = φ.predsem neg u

Guard absorption for entailing predicates: when a predicate entails existence and all its compared tokens carry the annotation list ℓ₀, its predicate provenance absorbs δ(⊕ℓ₀).

The group sequence under the pushforward

Having.havingGroup sorts the group by the tuple part and breaks ties on equal tuple parts by the alternative order on the annotations. The pushforward changes the tie-break order, so the hom-side group sequence coincides with the mapped base-side group sequence only up to a permutation inside blocks of equal tuple parts – a TiePerm, which the congruence layer of Provenance.AggValueCongr renders invisible to every reading of the resulting tokens.

theorem havingGroup_tiePerm {T : Type} [ValueType T] {K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] [DecidableEq K'] {m n₁ : ℕ} [HasAltLinearOrder K] [HasAltLinearOrder K'] (h : SemiringWithMonusHom K K') (is : Tuple (Fin m) n₁) (r : AnnotatedRelation T K m) (g : Tuple T n₁) : TiePerm (fun (p q : AnnotatedTuple T K' m) => p.1 = q.1) (List.map (fun (p : AnnotatedTuple T K m) => (p.1, h.toRingHom p.2)) (Having.havingGroup is r g)) (Having.havingGroup is (Multiset.map (fun (p : AnnotatedTuple T K m) => (p.1, h.toRingHom p.2)) r) g)

The hom-side group sequence is a tie-block permutation of the mapped base-side group sequence: both are sorted by the tuple part and carry the same multiset of annotated occurrences.

theorem ofGroup_mapAnn_tiePerm {T : Type} [ValueType T] {K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] [DecidableEq K'] {m n₁ : ℕ} [HasAltLinearOrder K] [HasAltLinearOrder K'] (h : SemiringWithMonusHom K K') (f : SeqAggFunc T) (t : Term T m) (is : Tuple (Fin m) n₁) (r : AnnotatedRelation T K m) (g : Tuple T n₁) : TiePerm (fun (p q : T × K') => p.1 = q.1) (AggValue.mapAnn (⇑h.toRingHom) (AggValue.ofGroup f t (Having.havingGroup is r g))).occs (AggValue.ofGroup f t (Having.havingGroup is (Multiset.map (fun (p : AnnotatedTuple T K m) => (p.1, h.toRingHom p.2)) r) g)).occs

The occurrence payloads of the two group tokens – base-side pushed forward, and hom-side – differ by a tie-block permutation on equal values: occurrences with equal tuple parts have equal aggregated-term values.

theorem ofGroup_predProv_hom {T : Type} [ValueType T] {K K' : Type} [CommSemiringWithMonus K] [DecidableEq K] [CommSemiringWithMonus K'] [DecidableEq K'] {m n₁ : ℕ} [HasAltLinearOrder K] [HasAltLinearOrder K'] (h : SemiringWithMonusHom K K') (f : SeqAggFunc T) (t : Term T m) (is : Tuple (Fin m) n₁) (r : AnnotatedRelation T K m) (g : Tuple T n₁) (op : CompOp) (c : T) : (AggValue.ofGroup f t (Having.havingGroup is (Multiset.map (fun (p : AnnotatedTuple T K m) => (p.1, h.toRingHom p.2)) r) g)).predProv op c = h.toRingHom ((AggValue.ofGroup f t (Having.havingGroup is r g)).predProv op c)

Group-token hom commutation. The predicate provenance of a comparison against the token of a group of the pushed-forward relation is the image under the hom of the base-side predicate provenance: the two tokens differ by a tie-block permutation of the payload, which AggValue.predProv_congr makes invisible.

theorem havingGroup_annSum_hom {T : Type} [ValueType T] {K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] [DecidableEq K'] {m n₁ : ℕ} [HasAltLinearOrder K] [HasAltLinearOrder K'] (h : SemiringWithMonusHom K K') (is : Tuple (Fin m) n₁) (r : AnnotatedRelation T K m) (g : Tuple T n₁) : (List.map Prod.snd (Having.havingGroup is (Multiset.map (fun (p : AnnotatedTuple T K m) => (p.1, h.toRingHom p.2)) r) g)).sum = h.toRingHom (List.map Prod.snd (Having.havingGroup is r g)).sum

The pending group factor – the sum of the occurrence annotations of the group – commutes with the pushforward, the tie-block permutation being invisible to a sum.

The simulation relation

The evaluator-level commutation cannot be a per-row equality: the hom side may supersede more pending factors (a non-injective hom conflates the annotation-list equality tests) and its group sequences are only tie-block permutations of the mapped base-side ones. The right invariant is a row-wise simulation: regular values equal, tokens tie-block-equivalent to the pushed-forward tokens, and the finalized annotation equal to the image of the base-side finalized annotation. Both discrepancies are value- neutral at that level: extra supersedes by guard absorption (delta_absorb), tie-breaks by the congruence layer.

def GenValue.Equiv {T K : Type} : GenValue T K → GenValue T K → Prop

Equivalence of lifted values: equal regular values, or tokens with the same aggregate and tie-block-permuted payloads.

Equations

• GenValue.Equiv (Sum.inl v') (Sum.inl v) = (v' = v)
• GenValue.Equiv (Sum.inr a') (Sum.inr a) = (a'.agg = a.agg ∧ TiePerm (fun (p q : T × K) => p.1 = q.1) a'.occs a.occs)
• x✝¹.Equiv x✝ = False

theorem GenValue.Equiv.collapseSum_eq {T K : Type} {v' v : GenValue T K} (h : v'.Equiv v) : AggValue.collapseSum v' = AggValue.collapseSum v

Equivalent lifted values collapse to the same regular value.

theorem TermG.eval_equiv {T : Type} [ValueType T] {K : Type} {n : ℕ} {κ : Fin n → ColKind} (t : TermG T κ) {u' u : Tuple (GenValue T K) n} (hu : ∀ (k : Fin n), (u' k).Equiv (u k)) : t.eval u' = t.eval u

Terms evaluate equally on pointwise-equivalent tuples.

theorem GenPred.holds_equiv {T : Type} [ValueType T] {K : Type} {n : ℕ} {κ : Fin n → ColKind} (φ : GenPred T κ) {u' u : Tuple (GenValue T K) n} (hu : ∀ (k : Fin n), (u' k).Equiv (u k)) : φ.holds u' ↔ φ.holds u

Classical truth of a predicate is invariant on pointwise-equivalent tuples.

theorem GenPred.predsem_equiv {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] {n : ℕ} {κ : Fin n → ColKind} (φ : GenPred T κ) (neg : Bool) {u' u : Tuple (GenValue T K) n} (hu : ∀ (k : Fin n), (u' k).Equiv (u k)) : φ.predsem neg u' = φ.predsem neg u

The predicate provenance is invariant on pointwise-equivalent tuples: tokens are read only through their predicate provenance (AggValue.predProv_congr) and their collapse.

def GenRow.Sim {T K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] (h : SemiringWithMonusHom K K') {n : ℕ} (r' : GenRow T K' n) (r : GenRow T K n) : Prop

The row-wise simulation relation underlying the evaluator-level hom commutation: regular columns equal, token columns tie-block-equivalent to the pushed-forward base-side tokens, and the finalized annotation the image of the base-side finalized annotation.

Equations

• GenRow.Sim h r' r = ((∀ (k : Fin n), (r'.1 k).Equiv (AggValue.mapAnnSum (⇑h.toRingHom) (r.1 k))) ∧ r'.2.finalize = h.toRingHom r.2.finalize)

theorem GenRow.Sim.toAnnotated_eq {T K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] (h : SemiringWithMonusHom K K') {n : ℕ} {r' : GenRow T K' n} {r : GenRow T K n} (hs : Sim h r' r) : r'.toAnnotated = h.mapAnnotatedTuple r.toAnnotated

Simulated rows finalize to pushed-forward annotated tuples.

Per-side finalize identities

The three row transformations of the evaluator that rearrange the factored annotation are finalize-equivalent on each side separately: cashing a group factor moves δ between pending and base (projection), the supersede drop is licensed exactly by the guard-absorption condition of its filter (selection), and the product splits multiplicatively.

theorem GenAnn.finalize_cash {K : Type} [CommSemiringWithMonus K] [DecidableEq K] (b : K) (P kept : Multiset (List K)) (hle : kept ≤ P) : { base := b * (Multiset.map (fun (l : List K) => SemiringWithMonus.delta l.sum) (P - kept)).prod, pending := kept }.finalize = { base := b, pending := P }.finalize

Cashing any sub-multiset of pending factors does not change the finalized annotation.

theorem GenPred.predsem_absorb_prod {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] {n : ℕ} {κ : Fin n → ColKind} (φ : GenPred T κ) (u : Tuple (GenValue T K) n) (hent : φ.entailsExistence false = true) (D : Multiset (List K)) (hD : ∀ l ∈ D, ∀ k ∈ φ.comparedCols, ∀ (a : AggValue T K), u k = Sum.inr a → List.map Prod.snd a.occs = l) : φ.predsem false u * (Multiset.map (fun (l : List K) => SemiringWithMonus.delta l.sum) D).prod = φ.predsem false u

An existence-entailing predicate provenance absorbs the δ-guards of any collection of pending factors, each of which is the occurrence list of every compared token.

theorem GenAnn.finalize_sel {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] {n : ℕ} {κ : Fin n → ColKind} (φ : GenPred T κ) (u : Tuple (GenValue T K) n) (b : K) (P C : Multiset (List K)) (hC : ∀ k ∈ φ.comparedCols, ∀ (a : AggValue T K), u k = Sum.inr a → List.map Prod.snd a.occs ∈ C) : { base := b * φ.predsem false u, pending := if φ.entailsExistence false = true then Multiset.filter (fun (l : List K) => ¬(C ≠ 0 ∧ ∀ l' ∈ C, l' = l)) P else P }.finalize = φ.predsem false u * { base := b, pending := P }.finalize

Selection finalize identity. On each side separately, the annotation produced by an aggregate-atom selection finalizes to the predicate provenance times the input's finalized annotation: kept pending factors commute out, and each superseded factor is absorbed by the predicate provenance, its drop condition being exactly the absorption license. The compared-lists multiset C is abstract; the only fact used is that every compared token's occurrence list belongs to it.

theorem GenAnn.finalize_prod {K : Type} [CommSemiringWithMonus K] (b₁ b₂ : K) (P₁ P₂ : Multiset (List K)) : { base := b₁ * b₂, pending := P₁ + P₂ }.finalize = { base := b₁, pending := P₁ }.finalize * { base := b₂, pending := P₂ }.finalize

The product annotation finalizes to the product of the finalized annotations.

Multiset relation plumbing

theorem rel_map_of_forall {α γ δ' : Type} {R : γ → δ' → Prop} {s : Multiset α} {f : α → γ} {g : α → δ'} (hfg : ∀ x ∈ s, R (f x) (g x)) : Multiset.Rel R (Multiset.map f s) (Multiset.map g s)

Mapping a multiset with two functions related pointwise yields related multisets.

theorem rel_map_of_rel {α β γ δ' : Type} {R : α → β → Prop} {S : γ → δ' → Prop} {s : Multiset α} {t : Multiset β} {f : α → γ} {g : β → δ'} (hst : Multiset.Rel R s t) (hfg : ∀ (x : α) (y : β), R x y → S (f x) (g y)) : Multiset.Rel S (Multiset.map f s) (Multiset.map g t)

Push a relation through maps of related multisets.

theorem map_eq_of_rel {α β γ : Type} {R : α → β → Prop} {s : Multiset α} {t : Multiset β} {f : α → γ} {g : β → γ} (hst : Multiset.Rel R s t) (hfg : ∀ (x : α) (y : β), R x y → f x = g y) : Multiset.map f s = Multiset.map g t

Related multisets mapped by pointwise-equal-on-related-pairs functions are equal.

theorem rel_filter_of_iff {α β : Type} {R : α → β → Prop} {s : Multiset α} {t : Multiset β} {p : α → Prop} {q : β → Prop} [DecidablePred p] [DecidablePred q] (hst : Multiset.Rel R s t) (hpq : ∀ (x : α) (y : β), R x y → (p x ↔ q y)) : Multiset.Rel R (Multiset.filter p s) (Multiset.filter q t)

Filtering related multisets by predicates that agree on related pairs preserves the relation.

theorem rel_product {α β γ δ' : Type} {R : α → β → Prop} {S : γ → δ' → Prop} {s : Multiset α} {t : Multiset β} {s' : Multiset γ} {t' : Multiset δ'} (hst : Multiset.Rel R s t) (hst' : Multiset.Rel S s' t') : Multiset.Rel (fun (x : α × γ) (y : β × δ') => R x.1 y.1 ∧ S x.2 y.2) (s.product s') (t.product t')

Products of related multisets are related pairwise.

The evaluator-level commutation

The query syntax mentions no annotation values, so the same query evaluates over any annotation semiring; the database argument determines it. The main theorem relates the evaluation on the pushed-forward database to the base-side evaluation, row by row, through GenRow.Sim; finalizing both sides then yields the hypothesis-free hom commutation of evaluateAnnotated.

theorem GenPred.holds_mapAnnSum {T : Type} [ValueType T] {K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] {n : ℕ} {κ : Fin n → ColKind} (h : SemiringWithMonusHom K K') (φ : GenPred T κ) (u : Tuple (GenValue T K) n) : (φ.holds fun (k : Fin n) => AggValue.mapAnnSum (⇑h.toRingHom) (u k)) ↔ φ.holds u

Classical truth is invariant under the pushforward of the tuple.

theorem GenRow.sim_ofAnnotated {T K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] (h : SemiringWithMonusHom K K') {n : ℕ} (p : AnnotatedTuple T K n) : Sim h (ofAnnotated (h.mapAnnotatedTuple p)) (ofAnnotated p)

Embedded pushed-forward annotated tuples simulate the embedded base-side tuples.

theorem rel_ofAnnotated_map {T K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] (h : SemiringWithMonusHom K K') {n : ℕ} (X : AnnotatedRelation T K n) : Multiset.Rel (GenRow.Sim h) (Multiset.map GenRow.ofAnnotated (h.mapAnnotatedRelation X)) (Multiset.map GenRow.ofAnnotated X)

Embedding a pushed-forward annotated relation yields rows simulating the embedded base-side rows.

theorem groupByKey_mapAnnotatedRelation {T : Type} [ValueType T] {K K' : Type} [CommSemiringWithMonus K] [DecidableEq K] [CommSemiringWithMonus K'] [DecidableEq K'] (h : SemiringWithMonusHom K K') {n : ℕ} (X : AnnotatedRelation T K n) : ↑↑(groupByKey (h.mapAnnotatedRelation X)) = h.mapAnnotatedRelation ↑↑(groupByKey X)

groupByKey commutes with the annotation pushforward: keys are data-only and group values are annotation sums.

theorem AggQuery.evaluate_hom_rel {T : Type} [ValueType T] {K K' : Type} [CommSemiringWithMonus K] [DecidableEq K] [CommSemiringWithMonus K'] [DecidableEq K'] [HasAltLinearOrder K] [HasAltLinearOrder K'] (h : SemiringWithMonusHom K K') {n : ℕ} {κ : Fin n → ColKind} (q : AggQuery T n κ) (d : AnnotatedDatabase T K) : Multiset.Rel (GenRow.Sim h) (q.evaluate (h.mapAnnotatedDatabase d)) (q.evaluate d)

Row-wise simulation. Evaluating the transported query on the pushed-forward database produces, row for row, simulations of the base-side rows: same regular values, tie-block-equivalent tokens, and the pushed-forward finalized annotation.

theorem AggQuery.evaluateAnnotated_hom {T : Type} [ValueType T] {K K' : Type} [CommSemiringWithMonus K] [DecidableEq K] [CommSemiringWithMonus K'] [DecidableEq K'] [HasAltLinearOrder K] [HasAltLinearOrder K'] (h : SemiringWithMonusHom K K') {n : ℕ} {κ : Fin n → ColKind} (q : AggQuery T n κ) (d : AnnotatedDatabase T K) : q.evaluateAnnotated (h.mapAnnotatedDatabase d) = h.mapAnnotatedRelation (q.evaluateAnnotated d)

Evaluator-level hom commutation (hypothesis-free): the final annotated relation computed by the general evaluator commutes with every SemiringWithMonusHom, over every m-semiring. The extra supersedes a non-injective hom can trigger are value-neutral by guard absorption (delta_absorb), and the annotation tie-breaks of the group sort are value-neutral by the tie-block congruence layer.

Home · Documentation · Publications · Contributors · Source · Cite