commit 1d25c9d217f9b9a57b70d57867ceae91a8523c6a Author: Hassan Abedi Date: Fri Feb 27 13:05:58 2026 +0100 The base commit diff --git a/.editorconfig b/.editorconfig new file mode 100644 index 0000000..f41e0e7 --- /dev/null +++ b/.editorconfig @@ -0,0 +1,27 @@ +# https://EditorConfig.org + +root = true + +[*] +charset = utf-8 +end_of_line = lf +indent_style = space +indent_size = 4 +insert_final_newline = true +trim_trailing_whitespace = true + +[*.py] +max_line_length = 100 + +[*.md] +max_line_length = 150 +trim_trailing_whitespace = false + +[*.sh] +indent_size = 2 + +[*.{yaml,yml,json}] +indent_size = 2 + +[*.toml] +indent_size = 2 diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..2bfb9c4 --- /dev/null +++ b/.gitignore @@ -0,0 +1,42 @@ +.idea +*.swp +**/*.whl +*.egg-info +**/__pycache__ +.DS_Store +venv +.venv + +.vscode +.zed +rust/target + +site + +.pytest_cache +.ruff_cache + +python/build +python/dist + +**/.ipynb_checkpoints + +**/.hypothesis + +# Compiled Dynamic libraries +*.so +*.dylib +*.dll + +## Javascript +*.node +**/node_modules +**/.DS_Store +nodejs/lancedb/native* +dist + +## Rust +target + +## Misc +*.log diff --git a/hassan/001-similar-projects.md b/hassan/001-similar-projects.md new file mode 100644 index 0000000..16aa5a1 --- /dev/null +++ b/hassan/001-similar-projects.md @@ -0,0 +1,49 @@ +## Projects Related to Geolog + +### Chase-Based & Geometric Logic Tools + +| Project | Language | Description | Key Features | Link | +|--------------------------------------------------------------------|----------|-------------------------------------------------------------------------------------------------------------------------------|----------------------------------------------------------------------------------------------------------------------|-----------------------------------------------------------------------------------| +| **Chase** (Ramsdell) | OCaml | Model finder for finitary geometric logic. Uses an input syntax called "Geolog" — likely the direct namesake of this project. | Minimal model finding, partial functions, tree visualization of chase output, Prolog-like input syntax (`.gl` files) | [github.com/ramsdell/chase]() | +| **Rusty Razor** | Rust | First-order model finder using the chase algorithm. Converts arbitrary FOL to geometric normal form. | Homomorphically minimal models, no upfront bound required, model space exploration, provenance tracking | [github.com/salmans/rusty-razor]() | +| **Geometric Logic for Policy Analysis** (Sagha, Naumov, Dougherty) | Haskell | Chase-based prototype for analyzing access control policies as geometric theories. | Jointly universal model sets, policy verification, comparison with SAT-based tools like Kodkod/Margrave | [Paper (PDF)]() | + +### Applied Category Theory Tools + +| Project | Language | Description | Key Features | Link | +|--------------------------------|-------------------|----------------------------------------------------------------------------------------------------------------------|-------------------------------------------------------------------------------------------------------------|------------------------------------------------------------------------------------------------------------------------------| +| **Catlab.jl** | Julia | Framework for applied and computational category theory. The most mature library in this space. | Generalized algebraic theories (GATs), C-sets/acsets, chase algorithm, wiring diagrams, limits/colimits | [github.com/AlgebraicJulia/Catlab.jl]() | +| **CatColab** (Topos Institute) | Rust + TypeScript | Collaborative web environment for formal, interoperable conceptual modeling. Closest in *spirit* to Geolog's vision. | Notebook UI, multiple domain-specific logics, collaborative editing, double-theory framework, visualization | [github.com/ToposInstitute/CatColab]() / [catcolab.org]() | +| **AlgebraicJulia** (ecosystem) | Julia | Broader ecosystem around Catlab for scientific computing with category theory. | Agent-based modeling, differential equations, epidemiological modeling, Petri nets | [algebraicjulia.org]() | + +### Relational/Formal Specification Tools (Broader Family) + +| Project | Language | Description | Key Features | Link | +|--------------------|----------|--------------------------------------------------------------------------------------------------------|-----------------------------------------------------------------------------------------------------------------------|--------------------------------------------------------------------------------------------------------------| +| **Alloy Analyzer** | Java | The most well-known lightweight formal methods tool. Relational logic + bounded model finding via SAT. | Signatures/relations, SAT-based Kodkod engine, bounded scope checking, graphical counterexamples, temporal logic (v6) | [alloytools.org]() / [GitHub]() | + +### Theoretical Foundations + +| Work | Author(s) | Description | Link | +|------------------------------------------------------|----------------|--------------------------------------------------------------------------------------------------------------------------------|--------------------------------------------------------------------------------------------------------------------------------| +| *Geometric Logic as a Specification Language* (1994) | Steven Vickers | Seminal paper proposing geometric logic as the basis for a Z-like specification language. The intellectual ancestor of Geolog. | [Springer]() / [PDF]() | +| *Geometric Logic in Computer Science* (1993) | Steven Vickers | Introduction to geometric logic, categorical logic, toposes, and their applications in computer science. | [Springer]() | + +--- + +### What Makes Geolog Distinctive + +Compared to the above projects, Geolog combines several features that no single existing tool offers together: + +* **Typed theories with geometric axioms** (like Chase/Razor) but with a richer **sort/function/relation** vocabulary (closer to Catlab) +* **Dependent/parameterized theories** — theories can take instances of other theories as parameters (e.g. `theory (N : PetriNet instance) Marking`) +* **Nested instances** — instances can contain instances of parameterized theories inline +* **Chase + equality saturation** — not just model finding but collapsing equivalent terms (as in the Category example) +* **Persistent, append-only storage** with version control — designed as infrastructure, not just a one-shot tool +* **Interactive REPL** — explore and mutate instances dynamically, unlike batch-mode model finders +* **Constructive proof witnesses** — the Petri net showcase demonstrates solutions as typed diagrammatic objects, not just boolean answers + + +## Changelog + +* **Feb 27, 2026** -- The first version was created. diff --git a/hassan/002-geolog-glossary.md b/hassan/002-geolog-glossary.md new file mode 100644 index 0000000..36b954c --- /dev/null +++ b/hassan/002-geolog-glossary.md @@ -0,0 +1,45 @@ +## 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. diff --git a/pyproject.toml b/pyproject.toml new file mode 100644 index 0000000..975fe0e --- /dev/null +++ b/pyproject.toml @@ -0,0 +1,10 @@ +[project] +name = "useful-notes" +version = "0.1.0" +description = "Python environment for the `useful-notes` project" + +requires-python = ">=3.10,<4.0" +dependencies = [ + "pre-commit (>=4.2.0,<5.0.0)", + "icecream (>=2.1.4,<3.0.0)", +]