Documentation

SE.Transformation.Domain.Operator.Semantics

Operator Semantics #

SE.Transformation.Domain.Operator.Semantics

Authoritative semantic classification for transformation operators.

operatorFamily is the sole operator-to-family mapping. familyKind is the sole family-to-kind mapping. operatorKind is derived from those two functions.

Reference artifacts and derived operator lists must mirror these mappings; they are not independent sources of taxonomy semantics.

The kind classification groups families by the principal structural dimension of change represented in this theory:

These classifications describe transformation structure only. They do not determine persistence.

OperatorInFamily and OperatorInKind are the Prop-valued membership predicates for downstream proofs, for example statements of the form "every operator in family f satisfies P". They are definitionally the equations operatorFamily op = family and operatorKind op = kind, and are decidable. operatorsInFamily, operatorsInKind and familiesInKind in SE.Transformation.Registry are the computational counterparts.

source
def SE.Transformation.operatorFamily :
OperatorCode → TransformationFamily

The transformation family for each operator code.

Each operator belongs to exactly one family. This definition is the authoritative operator-to-family mapping.

Equations
Instances For
    source
    def SE.Transformation.familyKind :
    TransformationFamily → TransformationKind

    The transformation kind for each family.

    Each family belongs to exactly one kind. This definition is the authoritative family-to-kind mapping.

    Equations
    Instances For
      source
      def SE.Transformation.operatorKind (op : OperatorCode) :
      TransformationKind

      The transformation kind for an operator code.

      The result is derived transitively through operatorFamily and familyKind; it is not an independent classification.

      Equations
      Instances For
        source
        def SE.Transformation.OperatorInFamily (op : OperatorCode) (family : TransformationFamily) :
        Prop

        Predicate asserting that operator op belongs to family family.

        This is the Prop-valued form of the authoritative mapping operatorFamily: it holds exactly when operatorFamily op = family (operatorInFamily_iff). Downstream proofs should state "for every operator in family family" with this predicate, so the statement does not depend on how the mapping is represented. It is decidable (see the instance below).

        Equations
        Instances For
          source
          def SE.Transformation.OperatorInKind (op : OperatorCode) (kind : TransformationKind) :
          Prop

          Predicate asserting that operator op belongs to kind kind.

          This is the Prop-valued form of the derived mapping operatorKind: it holds exactly when operatorKind op = kind (operatorInKind_iff). Membership in a kind follows from membership in a family of that kind (operatorInKind_of_operatorInFamily). It is decidable (see the instance below).

          Equations
          Instances For
            source
            theorem SE.Transformation.operatorInFamily_iff {op : OperatorCode} {f : TransformationFamily} :
            OperatorInFamily op f ↔ operatorFamily op = f

            OperatorInFamily op family unfolds to operatorFamily op = family.

            source
            theorem SE.Transformation.operatorInKind_iff {op : OperatorCode} {k : TransformationKind} :
            OperatorInKind op k ↔ operatorKind op = k

            OperatorInKind op kind unfolds to operatorKind op = kind.

            source
            theorem SE.Transformation.operatorInKind_of_operatorInFamily {op : OperatorCode} {f : TransformationFamily} {k : TransformationKind} (hf : OperatorInFamily op f) (hk : familyKind f = k) :
            OperatorInKind op k

            An operator in a family is in the kind of that family.

            This is the operator, family and kind layering stated as a lemma: if op is in family and familyKind family = kind, then op is in kind.

            source
            @[implicit_reducible]
            instance SE.Transformation.instDecidableOperatorInFamily (op : OperatorCode) (f : TransformationFamily) :
            Decidable (OperatorInFamily op f)

            Family membership is decidable, so finite statements about operators in a family can be checked with decide.

            Equations
            source
            @[implicit_reducible]
            instance SE.Transformation.instDecidableOperatorInKind (op : OperatorCode) (k : TransformationKind) :
            Decidable (OperatorInKind op k)

            Kind membership is decidable, so finite statements about operators in a kind can be checked with decide.

            Equations