Specialization, Feature Typing, Redefinition, and Interpretation

Specialization（preorder）、FeatureTyping（置換補題）、 Redefinition（型のリファイン）、Interpretation（モデル理論的意味論）、 および健全性定理を定義する。

structure VerifiedMBSE.Core.Specialization : Type

Specialization: A が B を特殊化する ⟺ A の任意のインスタンスは B のインスタンスでもある。

注: 現時点の Specialization は (specific, general) のみを保持する syntactic な 構造体であり、chain の証拠は specializes 側の命題でのみ保持する。将来 witness を 構造体に埋め込む拡張を行う場合は、本注記を更新すること（F3 参照）。

• specific : KerMLType
• general : KerMLType

def VerifiedMBSE.Core.instReprSpecialization.repr : Specialization → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance VerifiedMBSE.Core.instReprSpecialization : Repr Specialization

Equations

• VerifiedMBSE.Core.instReprSpecialization = { reprPrec := VerifiedMBSE.Core.instReprSpecialization.repr }

def VerifiedMBSE.Core.Specialization.refl (t : KerMLType) : Specialization

Specialization は反射的。

Equations

• VerifiedMBSE.Core.Specialization.refl t = { specific := t, general := t }

def VerifiedMBSE.Core.specializes (a b : KerMLType) : Prop

specialization の命題的定式化。

Equations

• VerifiedMBSE.Core.specializes a b = ∃ (s : VerifiedMBSE.Core.Specialization), s.specific = a ∧ s.general = b

theorem VerifiedMBSE.Core.specializes_refl (a : KerMLType) : specializes a a

specializes は反射的。

theorem VerifiedMBSE.Core.specializes_trans {a b c : KerMLType} (_hab : specializes a b) (_hbc : specializes b c) : specializes a c

specializes は推移的。

Specialization は現時点では witness を持たない pair 構造体であるため、a ≤ c の 証拠は ⟨⟨a, c⟩, rfl, rfl⟩ として直接構成できる。仮説 hab, hbc は API 上は 受け取っているが、本体では使用しない（将来 Specialization に chain の witness を 追加する拡張に備えた API フック）。旧 Specialization.trans は仮説を受け取りながら 使わないデータ関数だったため削除した（F3）。

@[implicit_reducible]

instance VerifiedMBSE.Core.instPreorderKerMLType : Preorder KerMLType

Preorder インスタンス。

Equations

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

structure VerifiedMBSE.Core.FeatureTyping : Type

FeatureTyping: feature に型を割り当てる関係。 型付け判断 f : A に対応する。

• feature : Feature

  型付け対象の feature

• featureType : KerMLType

  割り当てられる型

@[implicit_reducible]

instance VerifiedMBSE.Core.instReprFeatureTyping : Repr FeatureTyping

Equations

• VerifiedMBSE.Core.instReprFeatureTyping = { reprPrec := VerifiedMBSE.Core.instReprFeatureTyping.repr }

def VerifiedMBSE.Core.instReprFeatureTyping.repr : FeatureTyping → ℕ → Std.Format

Equations

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

structure VerifiedMBSE.Core.TypedFeature : Type

TypedFeature: Feature と FeatureTyping の整合性を保証する束。

• feature : Feature
• typing : FeatureTyping
• wf : self.typing.feature = self.feature

  整合性: typing は同じ feature を参照する

def VerifiedMBSE.Core.FeatureTyping.widen (ft : FeatureTyping) (b : KerMLType) : ft.featureType ≤ b → FeatureTyping

置換補題による型の拡張（subsumption）。 A ≤ B, f : A ⊢ f : B

Equations

• ft.widen b x✝ = { feature := ft.feature, featureType := b }

theorem VerifiedMBSE.Core.FeatureTyping.widen_feature (ft : FeatureTyping) (b : KerMLType) (h : ft.featureType ≤ b) : (ft.widen b h).feature = ft.feature

widen は feature そのものを変えない。

theorem VerifiedMBSE.Core.FeatureTyping.widen_type (ft : FeatureTyping) (b : KerMLType) (h : ft.featureType ≤ b) : (ft.widen b h).featureType = b

widen 後の型は指定した b に一致する。

theorem VerifiedMBSE.Core.FeatureTyping.widen_trans (ft : FeatureTyping) (b c : KerMLType) (hab : ft.featureType ≤ b) (hbc : b ≤ c) : (ft.widen c ⋯).feature = ((ft.widen b hab).widen c hbc).feature

widen は推移的に合成できる（coherence）。

structure VerifiedMBSE.Core.Redefinition : Type

Redefinition: サブタイプ文脈で feature を再定義する関係。 redefining.featureType ≤ redefined.featureType という refinement 条件を要求する。

• redefining : FeatureTyping

  再定義する feature（サブタイプ側）

• redefined : FeatureTyping

  再定義される feature（スーパータイプ側）

• typeRefinement : self.redefining.featureType ≤ self.redefined.featureType

  型の refinement 条件

def VerifiedMBSE.Core.Redefinition.toWidened (r : Redefinition) : FeatureTyping

Redefinition から widen 経由で FeatureTyping を復元する。

Equations

• r.toWidened = r.redefining.widen r.redefined.featureType ⋯

theorem VerifiedMBSE.Core.Redefinition.toWidened_type (r : Redefinition) : r.toWidened.featureType = r.redefined.featureType

widen 後の型は redefined の型に一致する。

theorem VerifiedMBSE.Core.Redefinition.toWidened_feature (r : Redefinition) : r.toWidened.feature = r.redefining.feature

feature 本体は widen 後も redefining のまま。

def VerifiedMBSE.Core.Redefinition.trans (r₁ r₂ : Redefinition) (h : r₁.redefined.featureType = r₂.redefining.featureType) : Redefinition

Redefinition の推移律。

Equations

• r₁.trans r₂ h = { redefining := r₁.redefining, redefined := r₂.redefined, typeRefinement := ⋯ }

def VerifiedMBSE.Core.Interpretation : Type 1

意味論的解釈: 各 KerMLType に担体型を割り当てる関数。 denotational semantics: ⟦ T ⟧_I := I T

Equations

• VerifiedMBSE.Core.Interpretation = (VerifiedMBSE.Core.KerMLType → Type)

def VerifiedMBSE.Core.extent (I : Interpretation) (T : KerMLType) : Type

解釈下での extent。

Equations

• VerifiedMBSE.Core.extent I T = I T

def VerifiedMBSE.Core.semanticSpecializes (I : Interpretation) (a b : KerMLType) : Prop

意味論的 specialization: I の下で A ≤_sem B ⟺ I A → I B の単射が存在する。

Equations

• VerifiedMBSE.Core.semanticSpecializes I a b = ∃ (f : I a → I b), Function.Injective f

theorem VerifiedMBSE.Core.semanticSpecializes_refl (I : Interpretation) (a : KerMLType) : semanticSpecializes I a a

意味論的 specialization は反射的。

theorem VerifiedMBSE.Core.semanticSpecializes_trans (I : Interpretation) {a b c : KerMLType} (hab : semanticSpecializes I a b) (hbc : semanticSpecializes I b c) : semanticSpecializes I a c

意味論的 specialization は推移的。

theorem VerifiedMBSE.Core.semanticSpecializes_preorder (I : Interpretation) (a b c : KerMLType) : semanticSpecializes I a b → semanticSpecializes I b c → semanticSpecializes I a c

意味論的 specialization は preorder を成す。

def VerifiedMBSE.Core.trivialInterpretation : Interpretation

単一点解釈（自明モデル）。

Equations

• VerifiedMBSE.Core.trivialInterpretation x✝ = Unit

def VerifiedMBSE.Core.stringInterpretation : Interpretation

文字列解釈（デバッグ用）。

Equations

• VerifiedMBSE.Core.stringInterpretation x✝ = String

theorem VerifiedMBSE.Core.trivial_semanticSpecializes_all (a b : KerMLType) : semanticSpecializes trivialInterpretation a b

自明モデル下では specialization は常に成立する。

def VerifiedMBSE.Core.InterpretationRespects (I : Interpretation) : Prop

解釈がモデル条件を満たす（すべての Specialization を尊重する）。

Equations

• VerifiedMBSE.Core.InterpretationRespects I = ∀ (s : VerifiedMBSE.Core.Specialization), VerifiedMBSE.Core.semanticSpecializes I s.specific s.general

theorem VerifiedMBSE.Core.soundness (I : Interpretation) (hI : InterpretationRespects I) {a b : KerMLType} (hab : specializes a b) : semanticSpecializes I a b

健全性定理: 統語的 specialization ⇒ 意味論的 specialization。

theorem VerifiedMBSE.Core.trivial_respects : InterpretationRespects trivialInterpretation

自明解釈はモデル条件を満たす。

theorem VerifiedMBSE.Core.soundness_trivial {a b : KerMLType} (hab : specializes a b) : semanticSpecializes trivialInterpretation a b

系: 自明モデルでは統語的 specialization は常に意味論的にも成立する。