401 lines
15 KiB
Plaintext
401 lines
15 KiB
Plaintext
|
// GeologMeta: A homoiconic representation of geolog theories
|
||
|
|
//
|
||
|
|
// An instance of GeologMeta IS a collection of geolog theories, complete with
|
||
|
|
// signatures, axioms, and well-formedness constraints.
|
||
|
|
//
|
||
|
|
// Key design principles:
|
||
|
|
// - All elements identified by UUID; human-readable names in separate NamingIndex
|
||
|
|
// - Child pointers go from parent to children (no products in domains)
|
||
|
|
// - Binding uses upward pointers from variable to binder
|
||
|
|
// - Transitive closure (ancestor) via Datalog-style axioms
|
||
|
|
// - Srt/theory, Func/theory enables multi-theory instances and theory parameters
|
||
|
|
//
|
||
|
|
// Naming convention: DomainSort/descriptor
|
||
|
|
// - Embeddings: VarT/term, EqF/formula (target sort)
|
||
|
|
// - Parent pointers: Srt/theory, Field/prod (container sort)
|
||
|
|
// - Projections: EqF/lhs, ProjT/field (field reference)
|
||
|
|
|
||
|
|
theory GeologMeta {
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// THEORIES
|
||
|
|
// ============================================================
|
||
|
|
|
||
|
|
Theory : Sort;
|
||
|
|
|
||
|
|
// Theory parameters: (N : PetriNet) means N is a Param
|
||
|
|
Param : Sort;
|
||
|
|
Param/theory : Param -> Theory; // which theory has this parameter
|
||
|
|
Param/type : Param -> Theory; // must instantiate this theory
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// SORTS (renamed to Srt to avoid keyword conflict)
|
||
|
|
// ============================================================
|
||
|
|
|
||
|
|
Srt : Sort;
|
||
|
|
Srt/theory : Srt -> Theory;
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// DERIVED SORTS (Base | Product)
|
||
|
|
// ============================================================
|
||
|
|
|
||
|
|
DSort : Sort;
|
||
|
|
|
||
|
|
// Base case: wraps a Sort
|
||
|
|
BaseDS : Sort;
|
||
|
|
BaseDS/dsort : BaseDS -> DSort;
|
||
|
|
BaseDS/srt : BaseDS -> Srt;
|
||
|
|
|
||
|
|
// Product case: [x: A, y: B, ...]
|
||
|
|
ProdDS : Sort;
|
||
|
|
ProdDS/dsort : ProdDS -> DSort;
|
||
|
|
|
||
|
|
// Product fields (recursive: field type is DSort)
|
||
|
|
Field : Sort;
|
||
|
|
Field/prod : Field -> ProdDS;
|
||
|
|
Field/type : Field -> DSort;
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// FUNCTION SYMBOLS
|
||
|
|
// ============================================================
|
||
|
|
|
||
|
|
Func : Sort;
|
||
|
|
Func/theory : Func -> Theory;
|
||
|
|
Func/dom : Func -> DSort;
|
||
|
|
Func/cod : Func -> DSort;
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// RELATION SYMBOLS (predicates, no codomain)
|
||
|
|
// ============================================================
|
||
|
|
|
||
|
|
Rel : Sort;
|
||
|
|
Rel/theory : Rel -> Theory;
|
||
|
|
Rel/dom : Rel -> DSort;
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// BINDERS (for variable scoping)
|
||
|
|
// ============================================================
|
||
|
|
// Variables point UP to their binder. Binders are introduced by
|
||
|
|
// Exists quantifiers or context variables.
|
||
|
|
|
||
|
|
Binder : Sort;
|
||
|
|
Binder/type : Binder -> DSort;
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// TERMS
|
||
|
|
// ============================================================
|
||
|
|
|
||
|
|
Term : Sort;
|
||
|
|
|
||
|
|
// Variable reference (points to binder)
|
||
|
|
VarT : Sort;
|
||
|
|
VarT/term : VarT -> Term;
|
||
|
|
VarT/binder : VarT -> Binder; // UPWARD pointer to introducing binder
|
||
|
|
|
||
|
|
// Function application (unary - argument may be a record)
|
||
|
|
AppT : Sort;
|
||
|
|
AppT/term : AppT -> Term;
|
||
|
|
AppT/func : AppT -> Func;
|
||
|
|
AppT/arg : AppT -> Term;
|
||
|
|
|
||
|
|
// Record construction [x = t1, y = t2, ...]
|
||
|
|
RecordT : Sort;
|
||
|
|
RecordT/term : RecordT -> Term;
|
||
|
|
|
||
|
|
RecEntry : Sort;
|
||
|
|
RecEntry/record : RecEntry -> RecordT;
|
||
|
|
RecEntry/val : RecEntry -> Term;
|
||
|
|
RecEntry/field : RecEntry -> Field; // which field this entry is for
|
||
|
|
|
||
|
|
// Projection t.field
|
||
|
|
ProjT : Sort;
|
||
|
|
ProjT/term : ProjT -> Term;
|
||
|
|
ProjT/base : ProjT -> Term;
|
||
|
|
ProjT/field : ProjT -> Field; // which field to project
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// FORMULAS
|
||
|
|
// ============================================================
|
||
|
|
|
||
|
|
Formula : Sort;
|
||
|
|
|
||
|
|
// Relation application `t R`
|
||
|
|
RelF : Sort;
|
||
|
|
RelF/formula : RelF -> Formula;
|
||
|
|
RelF/arg : RelF -> Term;
|
||
|
|
RelF/rel : RelF -> Rel;
|
||
|
|
|
||
|
|
// Truth
|
||
|
|
TrueF : Sort;
|
||
|
|
TrueF/formula : TrueF -> Formula;
|
||
|
|
|
||
|
|
// Falsity
|
||
|
|
FalseF : Sort;
|
||
|
|
FalseF/formula : FalseF -> Formula;
|
||
|
|
|
||
|
|
// Equality t1 = t2
|
||
|
|
EqF : Sort;
|
||
|
|
EqF/formula : EqF -> Formula;
|
||
|
|
EqF/lhs : EqF -> Term;
|
||
|
|
EqF/rhs : EqF -> Term;
|
||
|
|
|
||
|
|
// Conjunction (n-ary via arms)
|
||
|
|
ConjF : Sort;
|
||
|
|
ConjF/formula : ConjF -> Formula;
|
||
|
|
|
||
|
|
ConjArm : Sort;
|
||
|
|
ConjArm/conj : ConjArm -> ConjF;
|
||
|
|
ConjArm/child : ConjArm -> Formula;
|
||
|
|
|
||
|
|
// Disjunction (n-ary via arms)
|
||
|
|
DisjF : Sort;
|
||
|
|
DisjF/formula : DisjF -> Formula;
|
||
|
|
|
||
|
|
DisjArm : Sort;
|
||
|
|
DisjArm/disj : DisjArm -> DisjF;
|
||
|
|
DisjArm/child : DisjArm -> Formula;
|
||
|
|
|
||
|
|
// Existential quantification
|
||
|
|
ExistsF : Sort;
|
||
|
|
ExistsF/formula : ExistsF -> Formula;
|
||
|
|
ExistsF/binder : ExistsF -> Binder; // introduces this binder
|
||
|
|
ExistsF/body : ExistsF -> Formula;
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// SEQUENTS (axioms)
|
||
|
|
// ============================================================
|
||
|
|
|
||
|
|
Sequent : Sort;
|
||
|
|
Sequent/theory : Sequent -> Theory;
|
||
|
|
Sequent/premise : Sequent -> Formula;
|
||
|
|
Sequent/conclusion : Sequent -> Formula;
|
||
|
|
|
||
|
|
// Context variables (universal quantification at sequent level)
|
||
|
|
CtxVar : Sort;
|
||
|
|
CtxVar/sequent : CtxVar -> Sequent;
|
||
|
|
CtxVar/binder : CtxVar -> Binder; // introduces this binder
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// NODE UNIVERSE (for ancestry/scoping)
|
||
|
|
// ============================================================
|
||
|
|
// Unified sort for tracking parent-child in formula trees
|
||
|
|
|
||
|
|
Node : Sort;
|
||
|
|
Term/node : Term -> Node;
|
||
|
|
Formula/node : Formula -> Node;
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// CHILD RELATION
|
||
|
|
// ============================================================
|
||
|
|
// child(p, c) means c is an immediate child of p in the AST
|
||
|
|
|
||
|
|
child : [parent: Node, child: Node] -> Prop;
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// ANCESTOR RELATION (transitive closure of child)
|
||
|
|
// ============================================================
|
||
|
|
|
||
|
|
ancestor : [anc: Node, desc: Node] -> Prop;
|
||
|
|
|
||
|
|
// Datalog-style transitive closure axioms
|
||
|
|
ax/anc/base : forall p : Node, c : Node.
|
||
|
|
[parent: p, child: c] child |- [anc: p, desc: c] ancestor;
|
||
|
|
|
||
|
|
ax/anc/step : forall a : Node, p : Node, c : Node.
|
||
|
|
[anc: a, desc: p] ancestor, [parent: p, child: c] child |- [anc: a, desc: c] ancestor;
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// CHILD AXIOMS (populate child from structure)
|
||
|
|
// ============================================================
|
||
|
|
|
||
|
|
// EqF children
|
||
|
|
ax/child/eq/lhs : forall e : EqF, t : Term.
|
||
|
|
e EqF/lhs = t |- [parent: e EqF/formula Formula/node, child: t Term/node] child;
|
||
|
|
ax/child/eq/rhs : forall e : EqF, t : Term.
|
||
|
|
e EqF/rhs = t |- [parent: e EqF/formula Formula/node, child: t Term/node] child;
|
||
|
|
|
||
|
|
// ExistsF body
|
||
|
|
ax/child/exists : forall e : ExistsF, f : Formula.
|
||
|
|
e ExistsF/body = f |- [parent: e ExistsF/formula Formula/node, child: f Formula/node] child;
|
||
|
|
|
||
|
|
// ConjF arms
|
||
|
|
ax/child/conj : forall a : ConjArm, c : ConjF, f : Formula.
|
||
|
|
a ConjArm/conj = c, a ConjArm/child = f |-
|
||
|
|
[parent: c ConjF/formula Formula/node, child: f Formula/node] child;
|
||
|
|
|
||
|
|
// DisjF arms
|
||
|
|
ax/child/disj : forall a : DisjArm, d : DisjF, f : Formula.
|
||
|
|
a DisjArm/disj = d, a DisjArm/child = f |-
|
||
|
|
[parent: d DisjF/formula Formula/node, child: f Formula/node] child;
|
||
|
|
|
||
|
|
// RelF argument
|
||
|
|
ax/child/rel : forall r : RelF, t : Term.
|
||
|
|
r RelF/arg = t |- [parent: r RelF/formula Formula/node, child: t Term/node] child;
|
||
|
|
|
||
|
|
// AppT argument
|
||
|
|
ax/child/app : forall a : AppT, t : Term.
|
||
|
|
a AppT/arg = t |- [parent: a AppT/term Term/node, child: t Term/node] child;
|
||
|
|
|
||
|
|
// ProjT base
|
||
|
|
ax/child/proj : forall p : ProjT, t : Term.
|
||
|
|
p ProjT/base = t |- [parent: p ProjT/term Term/node, child: t Term/node] child;
|
||
|
|
|
||
|
|
// RecEntry value
|
||
|
|
ax/child/rec : forall e : RecEntry, r : RecordT, t : Term.
|
||
|
|
e RecEntry/record = r, e RecEntry/val = t |-
|
||
|
|
[parent: r RecordT/term Term/node, child: t Term/node] child;
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// IN-SEQUENT RELATION (for context variable scoping)
|
||
|
|
// ============================================================
|
||
|
|
|
||
|
|
in_seq : [node: Node, seq: Sequent] -> Prop;
|
||
|
|
|
||
|
|
ax/in_seq/premise : forall s : Sequent, f : Formula.
|
||
|
|
s Sequent/premise = f |- [node: f Formula/node, seq: s] in_seq;
|
||
|
|
|
||
|
|
ax/in_seq/conclusion : forall s : Sequent, f : Formula.
|
||
|
|
s Sequent/conclusion = f |- [node: f Formula/node, seq: s] in_seq;
|
||
|
|
|
||
|
|
ax/in_seq/desc : forall n : Node, m : Node, s : Sequent.
|
||
|
|
[node: n, seq: s] in_seq, [anc: n, desc: m] ancestor |- [node: m, seq: s] in_seq;
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// BINDING WELL-FORMEDNESS CONSTRAINTS
|
||
|
|
// ============================================================
|
||
|
|
// These axioms ensure variables point to valid binders.
|
||
|
|
// An instance satisfies these iff scoping is correct.
|
||
|
|
|
||
|
|
// Exists-bound: binder's exists must be an ancestor of the var
|
||
|
|
ax/wf/exists : forall v : VarT, b : Binder, e : ExistsF.
|
||
|
|
v VarT/binder = b, e ExistsF/binder = b |-
|
||
|
|
[anc: e ExistsF/formula Formula/node, desc: v VarT/term Term/node] ancestor;
|
||
|
|
|
||
|
|
// Context-bound: var must be in the same sequent as the ctx var
|
||
|
|
ax/wf/ctx : forall v : VarT, b : Binder, cv : CtxVar, s : Sequent.
|
||
|
|
v VarT/binder = b, cv CtxVar/binder = b, cv CtxVar/sequent = s |-
|
||
|
|
[node: v VarT/term Term/node, seq: s] in_seq;
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// COMMITS (version control checkpoints)
|
||
|
|
// ============================================================
|
||
|
|
// Commits form a DAG. Each commit represents a point-in-time
|
||
|
|
// snapshot of all name bindings.
|
||
|
|
|
||
|
|
Commit : Sort;
|
||
|
|
Commit/parent : Commit -> Commit; // previous commit (optional for initial)
|
||
|
|
// Note: For merge commits, we'd need a relation for multiple parents
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// NAME BINDINGS (mutable pointers via append-only log)
|
||
|
|
// ============================================================
|
||
|
|
// A NameBinding records that, as of a given commit, a name
|
||
|
|
// points to a specific theory or instance version.
|
||
|
|
//
|
||
|
|
// Names are strings stored in NamingIndex (by UUID).
|
||
|
|
// The "current" binding for a name is the most recent one
|
||
|
|
// reachable from HEAD commit.
|
||
|
|
|
||
|
|
NameBinding : Sort;
|
||
|
|
NameBinding/commit : NameBinding -> Commit; // when this binding was made
|
||
|
|
|
||
|
|
// What the name points to (exactly one of these is defined):
|
||
|
|
NameBinding/theory : NameBinding -> Theory;
|
||
|
|
NameBinding/instance : NameBinding -> Instance;
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// INSTANCES (immutable, patch-based versioning)
|
||
|
|
// ============================================================
|
||
|
|
// An Instance is an immutable snapshot. "Modifying" an instance
|
||
|
|
// creates a new Instance with parent pointer and delta.
|
||
|
|
//
|
||
|
|
// To materialize: chase parent chain, union additions, apply retractions.
|
||
|
|
|
||
|
|
Instance : Sort;
|
||
|
|
Instance/parent : Instance -> Instance; // base version (optional for v0)
|
||
|
|
Instance/theory : Instance -> Theory; // which theory this instantiates
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// INSTANCE ELEMENTS (delta: additions)
|
||
|
|
// ============================================================
|
||
|
|
// Elements added in a specific instance version.
|
||
|
|
// The actual UUID is tracked via the element's Luid in Universe.
|
||
|
|
|
||
|
|
Elem : Sort;
|
||
|
|
Elem/instance : Elem -> Instance; // which version introduced this
|
||
|
|
Elem/sort : Elem -> Srt; // which sort of the theory
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// ELEMENT RETRACTIONS (delta: tombstones)
|
||
|
|
// ============================================================
|
||
|
|
// Marks an element as retracted in a specific version.
|
||
|
|
// The element still exists in the log, but is filtered from materialized view.
|
||
|
|
|
||
|
|
ElemRetract : Sort;
|
||
|
|
ElemRetract/instance : ElemRetract -> Instance; // which version retracted
|
||
|
|
ElemRetract/elem : ElemRetract -> Elem; // what was retracted
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// FUNCTION VALUES (delta: additions)
|
||
|
|
// ============================================================
|
||
|
|
// Records a function value: func(arg) = result
|
||
|
|
|
||
|
|
FuncVal : Sort;
|
||
|
|
FuncVal/instance : FuncVal -> Instance; // which version defined this
|
||
|
|
FuncVal/func : FuncVal -> Func; // which function
|
||
|
|
FuncVal/arg : FuncVal -> Elem; // domain element (or product elem)
|
||
|
|
FuncVal/result : FuncVal -> Elem; // codomain element
|
||
|
|
|
||
|
|
// NOTE: No FuncValRetract sort - function values are IMMUTABLE.
|
||
|
|
// To "change" a function value, retract the domain element and create a new one.
|
||
|
|
// This ensures the Monotonic Submodel Property (see incremental_index_design.md).
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// RELATION TUPLES (delta: additions)
|
||
|
|
// ============================================================
|
||
|
|
// Records a relation tuple: rel(args...) holds
|
||
|
|
//
|
||
|
|
// All relations use product-domain encoding uniformly (even unary).
|
||
|
|
// Each tuple has RelTupleArg entries for each position in the domain.
|
||
|
|
|
||
|
|
RelTuple : Sort;
|
||
|
|
RelTuple/instance : RelTuple -> Instance; // which version asserted this
|
||
|
|
RelTuple/rel : RelTuple -> Rel; // which relation
|
||
|
|
|
||
|
|
// Relation tuple argument components (one per domain field)
|
||
|
|
RelTupleArg : Sort;
|
||
|
|
RelTupleArg/tuple : RelTupleArg -> RelTuple; // which tuple this belongs to
|
||
|
|
RelTupleArg/elem : RelTupleArg -> Elem; // element value for this position
|
||
|
|
RelTupleArg/position : RelTupleArg -> Field; // which field of the domain product
|
||
|
|
|
||
|
|
// NOTE: No RelTupleRetract sort - relation tuples are IMMUTABLE.
|
||
|
|
// Relations are boolean-valued functions: R(a,b) is defined at element creation time.
|
||
|
|
// To "change" a relation value, retract the involved elements and create new ones.
|
||
|
|
// This ensures the Monotonic Submodel Property (see incremental_index_design.md).
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// THEORY VERSIONING (same pattern as instances)
|
||
|
|
// ============================================================
|
||
|
|
// Theories are also immutable and patch-based.
|
||
|
|
// Theory/parent allows incremental theory extension.
|
||
|
|
|
||
|
|
Theory/parent : Theory -> Theory; // base version (optional for v0)
|
||
|
|
|
||
|
|
// Theory element retractions (for removing sorts/funcs/rels)
|
||
|
|
SrtRetract : Sort;
|
||
|
|
SrtRetract/theory : SrtRetract -> Theory;
|
||
|
|
SrtRetract/srt : SrtRetract -> Srt;
|
||
|
|
|
||
|
|
FuncRetract : Sort;
|
||
|
|
FuncRetract/theory : FuncRetract -> Theory;
|
||
|
|
FuncRetract/func : FuncRetract -> Func;
|
||
|
|
|
||
|
|
RelRetract : Sort;
|
||
|
|
RelRetract/theory : RelRetract -> Theory;
|
||
|
|
RelRetract/rel : RelRetract -> Rel;
|
||
|
|
|
||
|
|
SequentRetract : Sort;
|
||
|
|
SequentRetract/theory : SequentRetract -> Theory;
|
||
|
|
SequentRetract/sequent : SequentRetract -> Sequent;
|
||
|
|
}
|