§03-i Minerva — Semantic Binding — What this section covers
Mars® Spec › §03-i Minerva — Semantic Binding › What this section covers
Section index · Semantic binding →
Mars® Protocol — §03-i: Semantic Binding and Data Source
Version 1.0-draft
1. What this section covers
This section covers the semantic binding operation and its substrate: the characterization of data sources, the binding of data-source structure to the formal domain model, and the aspect-keyed query library that binding produces. It also specifies the two data-source client classes (Pymnemon and Impera) and the multi-locus gap report emitted by semantic binding.
Dependencies:
- §01 (modeling) — provides the domain model (one or more, composable and independently operable; see §01 §1) — its orders, perspectives, variants, and aspects — that governs all binding operations. Where multiple domain models are active, each carries its own registered artifact identity; semantic-map entries and query library entries are scoped to the domain model version under which they were produced.
- §02b §5 (delta-attestation lifecycle) — governs the amendment lifecycle for semantic-map artifacts, query library entries, and any registered artifacts referenced here
- §03-ii (knowledge base) — a previously-committed KB version may be provided as optional input to semantic binding (§2.1); the KB referenced must be version-identified per §03-ii §3.4
Produces: semantic-map artifact, aspect-keyed query library, multi-locus gap report — consumed by §03-iii (evidence-gathering verification) and by any analysis operation at use time via the reverse-path.
1.1 What semantic binding produces in the layer
Semantic binding takes a characterized data source and an order-decomposed domain model and produces a semantic-map artifact and an aspect-keyed query library. It also emits a multi-locus gap report.
Four artifact classes participate across all artifact-generating operations: model / formal specification / data source / knowledge base. Each is a first-class reinforcement target. The reinforcement mechanism is symmetric: any operation can surface a gap in any artifact class, and the resulting typed signal targets the matching class under a single declared reinforcement policy. No hierarchy exists among the four classes.
Derivation direction. A formal specification is the lowered output of a domain model produced by predicate lowering — it is downstream of the model, not a peer to it. An externally-provided specification (a protocol, standard, guideline, or rules document) is source material that can bootstrap a domain model (§01 §2.8); it is not itself a formal specification before that process and does not serve as a governing reference until it has been lowered through a domain model and enrolled in the delta-attestation lifecycle. Reversing a formal specification back into the domain model that generated it recovers at best the same model and is not a bootstrap path. The governing specification (§03-iii §2.2) is a dynamic active selection from one or more formal specifications and is likewise downstream of the model.