46 lines
4.8 KiB
Markdown
46 lines
4.8 KiB
Markdown
|
## Geolog Glossary
|
||
|
|
|
||
|
|
* **Sort** — A sort is just a named type of thing. It's the most primitive declaration: "there exists a kind of thing called X." In the Graph theory,
|
||
|
|
`V : Sort` says "there is a kind of thing called vertices" and `E : Sort` says "there is a kind of thing called edges." Sorts don't have any
|
||
|
|
structure on their own — they're just labels for categories of elements.
|
||
|
|
* **Function** — A function maps elements of one sort to elements of another. `src : E -> V` says "every edge has a source vertex." For binary
|
||
|
|
operations, you use product domains: `mul : [x: M, y: M] -> M` says "given two monoid elements, multiplication produces a third." Functions must be
|
||
|
|
total — every element of the domain sort must be assigned a value.
|
||
|
|
* **Relation** — A relation is like a function but instead of producing a value, it's a proposition that is either true or false.
|
||
|
|
`completed : Item -> Prop` says "for any item, it either is or isn't completed." Binary relations like `leq : [lo: X, hi: X] -> Prop` express
|
||
|
|
relationships between pairs of elements. Relations are essentially database tables — a set of tuples for which the predicate holds.
|
||
|
|
* **Axiom** — An axiom is a rule that must hold in any valid instance. It takes the form of a geometric sequent: some premises on the left of `|-`, a
|
||
|
|
conclusion on the right. For example, `ax/trans` in the Preorder theory says "if x ≤ y and y ≤ z, then x ≤ z." The "geometric" restriction means
|
||
|
|
conclusions can only use conjunction (and), existential quantification (there exists), and disjunction (or) — no negation or universal
|
||
|
|
quantification on the right side. This is what makes the chase algorithm work.
|
||
|
|
* **Theory** — A theory is a complete package: a collection of sorts, functions, relations, and axioms that together define a *vocabulary and laws*
|
||
|
|
for some domain. The theory of `Graph` says "there are vertices and edges, and every edge has a source and target vertex." The theory of `Category`
|
||
|
|
adds composition, identities, and axioms for associativity and unit laws. A theory doesn't describe any particular graph or category — it describes
|
||
|
|
what it *means* to be one.
|
||
|
|
* **Instance** — An instance is a concrete, finite model that satisfies a theory. If the theory is the blueprint, the instance is a specific building.
|
||
|
|
`Triangle : Graph` says "here is a specific graph: it has vertices A, B, C, edges ab, bc, ca, and these specific source/target assignments." Every
|
||
|
|
function must be defined for every element, and every axiom must evaluate to true.
|
||
|
|
* **The Chase** — The chase is the key algorithmic idea. You provide some base facts and the chase automatically derives everything that logically
|
||
|
|
follows from the axioms. In the transitive closure example, you declare edges A→B, B→C, C→D, and the chase computes all six reachable pairs. You
|
||
|
|
write `= chase { ... }` instead of `= { ... }` to trigger this. It repeatedly scans for axioms that aren't yet satisfied and adds the necessary
|
||
|
|
facts until everything is consistent — a fixpoint computation.
|
||
|
|
* **Equality Saturation** — In the Category example, composing identity morphisms with themselves could produce infinite chains (id∘id∘id∘...).
|
||
|
|
Equality saturation collapses these by recognizing that id∘id = id (from the unit laws), merging equivalent elements rather than generating new ones
|
||
|
|
forever. This is what keeps the chase terminating in theories with equations.
|
||
|
|
* **Parameterized (Dependent) Theory** — A theory can take an instance of another theory as a parameter. `theory (N : PetriNet instance) Marking`
|
||
|
|
means "given some specific Petri net N, a Marking assigns tokens to N's places." This is the dependent types angle — the *type* of a marking depends
|
||
|
|
on the *value* of a specific net. You can't talk about markings in the abstract; they're always markings *of* something.
|
||
|
|
* **Nested Instance** — Inside an instance, you can define sub-instances of parameterized theories inline. In `ReachabilityProblem`, the
|
||
|
|
`initial_marking` and `target_marking` are instances of `Marking` defined right there inside the problem instance, using the `= { ... }` syntax
|
||
|
|
within the outer braces.
|
||
|
|
* **Proof Witness / Solution** — This is the Petri net showcase's central idea. A `Solution` isn't a boolean "yes, it's reachable." It's a *data
|
||
|
|
structure* — containing a trace (sequence of firings), wires (how tokens flow between firings), terminals (how tokens connect to initial/target
|
||
|
|
markings), and isomorphisms (proving the token counts match exactly). The fact that you can construct a well-typed instance of `Solution` *is* the
|
||
|
|
proof. If the types check and all axioms are satisfied, reachability is proven. This is the "propositions as types, proofs as programs" idea from
|
||
|
|
type theory, applied to diagrammatic reasoning.
|
||
|
|
|
||
|
|
|
||
|
|
## Changelog
|
||
|
|
|
||
|
|
* **Feb 27, 2026** -- The first version was created.
|