useful-notes/hassan/002-geolog-glossary.md

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.