Orthogonality

SE.Transformation.Relation.Orthogonality

Vocabulary for structural-independence relationships among transformation operators.

This module defines the possible relation values only. The canonical known pairs are supplied by the explicitly partial, symmetric lookup in SE.Transformation.Reference.Orthogonality.

Orthogonality describes independence.

inductive SE.Transformation.OrthogonalityRelation : Type

Relationship describing the degree of structural independence between two transformation operators.

inverseLike is intentionally not an orthogonality value: inverse direction is a sequencing or transformation relationship, not a degree of independence.

Absence of a canonical rule is represented by none in the lookup, not by a relation constructor.

• conflicting : OrthogonalityRelation

  The operators cannot be applied in the same context without contradiction.

• dependent : OrthogonalityRelation

  One operator's applicability depends on the other.

• orthogonal : OrthogonalityRelation

  The operators have no shared effect domain and do not interfere.

• overlapping : OrthogonalityRelation

  The operators share at least one effect dimension, including when one operator's effect domain contains the other's.

@[instance_reducible]

instance SE.Transformation.instDecidableEqOrthogonalityRelation : DecidableEq OrthogonalityRelation

Equations

• SE.Transformation.instDecidableEqOrthogonalityRelation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def SE.Transformation.instReprOrthogonalityRelation.repr : OrthogonalityRelation → Nat → Std.Format

Equations

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

@[instance_reducible]

instance SE.Transformation.instReprOrthogonalityRelation : Repr OrthogonalityRelation

Equations

• SE.Transformation.instReprOrthogonalityRelation = { reprPrec := SE.Transformation.instReprOrthogonalityRelation.repr }