Effect Dimensions #

Effect dimensions name the aspects of a transformation configuration that an operator step may change.

A step is the intrinsic effect of one application of one named operator. Incidental changes belong to separate operator steps. Properties a result may later acquire are not effects of the operator that produced it.

footprint op is a conservative upper bound on the dimensions that a step of op may change. A dimension outside it is preserved by every step.
requirements op is a lower bound: a finite collection of clauses. Every clause must be satisfied by every step, and a clause is satisfied when at least one of its dimensions changes. Requirements are conjunctions of disjunctions.
characteristic op is the single dimension that op is defined by changing, when its complete requirement is exactly one singleton clause.

Footprints and clauses are lists read as finite sets. Only membership matters: order and repetition have no semantic significance.

source

inductive SE.Transformation.Dimension :

Type

An aspect of a transformation configuration.

content is multiplicity-insensitive: its agreement compares the sets of distinct content descriptions the participants carry, so a faithful duplicate of an already-present description does not by itself change it, while a new distinct description may. arrangement and composition are structures compared modulo the model's agreement equivalence for each.

content : Dimension
The set of distinct content descriptions the participants carry.
arrangement : Dimension
The ordering and relative-position structure among components.
composition : Dimension
The part-whole structure of the configuration.
referentPopulation : Dimension
Which referents and structural participants exist.
representationPopulation : Dimension
Which representations of a referent exist.
containment : Dimension
Which enclosing structure each participant is placed in.
binding : Dimension
Associations with contexts, bearers, scopes, and applicability settings.
association : Dimension
Relations among participants other than containment, binding, composition, and lineage.
lineage : Dimension
Derivational ancestry, continuation and version relations, including copy-of, derived-from, successor and version relations, branch continuation, and a participant's position in a version chain.
evidence : Dimension
Claims, verification, and attestation metadata attached to participants.
standing : Dimension
Permission, authority, or normative standing, including its holder and scope.

Instances For

source

@[instance_reducible]

instance SE.Transformation.instDecidableEqDimension :

DecidableEq Dimension

Equations

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

source

@[instance_reducible]

instance SE.Transformation.instReprDimension :

Repr Dimension

Equations

SE.Transformation.instReprDimension = { reprPrec := SE.Transformation.instReprDimension.repr }

source

def SE.Transformation.instReprDimension.repr :

Dimension → Nat → Std.Format

Equations

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

Instances For

source

def SE.Transformation.referenceDimensions :

List Dimension

All effect dimensions in canonical reference order.

Equations

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

Instances For

source

theorem SE.Transformation.referenceDimensions_nodup :

referenceDimensions.Nodup

referenceDimensions has no duplicates.

source

theorem SE.Transformation.referenceDimensions_complete (d : Dimension) :

d ∈ referenceDimensions

Every dimension occurs in referenceDimensions.

source

def SE.Transformation.footprint :

OperatorCode → List Dimension

The dimensions that a step of an operator may change.

A dimension omitted here is a substantive assertion that every step of the operator preserves it. MG and RV carry the widest footprints: MG because consuming its inputs removes the facts about them, and RV because restoring a prior version reaches whatever a version captures.

Equations

Instances For

source

def SE.Transformation.requirements :

OperatorCode → List (List Dimension)

The required-change condition of an operator: a collection of clauses.

Every step of the operator must satisfy every clause, and a clause is satisfied by a step that changes at least one of its dimensions. A single multi-member clause is a genuine alternative; separate clauses are independently mandatory.

Equations

Instances For

source

def SE.Transformation.characteristic (op : OperatorCode) :

Option Dimension

The single dimension that an operator is defined by changing.

It exists exactly when the complete required-change condition is the one clause {d}. A singleton clause alongside other mandatory clauses does not yield a characteristic.

Equations