From 4d1044b0af545919a9539dda8a3a652ed6f3a445 Mon Sep 17 00:00:00 2001 From: Hassan Abedi Date: Thu, 19 Mar 2026 14:17:59 +0100 Subject: [PATCH] Adding more notes on the project --- notes/qa-session.md | 61 ++++++++++++++++++++++++++++++++++ notes/summary.md | 81 +++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 142 insertions(+) create mode 100644 notes/summary.md diff --git a/notes/qa-session.md b/notes/qa-session.md index c69f560..00d6b5e 100644 --- a/notes/qa-session.md +++ b/notes/qa-session.md @@ -90,3 +90,64 @@ The mechanisms handle all standard geometric logic axioms: - Category laws, Petri net rules, graph reachability The gaps only matter for axioms with complex record/product operations in conclusions. + +--- + +## Q3: Is Geolog inspired by an existing tool or software? + +**Answer: Geolog is an AI-generated project that combines ideas from several fields. No single tool is its direct ancestor.** + +### Origin + +The README states: + +> "This README was synthesized automatically by Claude Opus 4.5. As was this entire project, really." + +Geolog was created by Claude Opus 4.5, Anthropic's AI model. + +### Technical Influences + +The project draws from several established areas: + +**Egglog / Egg** +- Uses `egglog-union-find` and `egglog-numeric-id` crates +- Equality saturation and e-graph techniques for congruence closure + +**Database Theory** +- Chase algorithm: a classical method for computing fixpoints in databases +- Relational algebra for query compilation + +**SMT Solvers** +- Model enumeration follows SMT solver patterns +- Automated search with forward chaining and equation propagation + +**Category Theory / Topos Theory** +- Geometric logic with semantics in topoi +- Lean4 formalization uses the `model-theory-topos` library + +**Formal Verification** +- Petri net reachability (similar to model checking) +- Diagrammatic rewriting + +### No Single Predecessor + +The codebase doesn't name a specific tool as direct inspiration. Geolog is a novel combination of: + +| Concept | Source Field | +|---------|--------------| +| Geometric logic | Mathematical logic | +| Chase algorithm | Database theory | +| Tensor algebra | Linear algebra / sparse computation | +| Equality saturation | Program optimization (egg/egglog) | +| Congruence closure | Automated theorem proving | + +### Related Tools (for context) + +While not cited as inspirations, similar tools exist in adjacent spaces: +- **Alloy** - relational logic model finder +- **Datalog** - logic programming for databases +- **CQL** - categorical query language +- **Z3** - SMT solver +- **Egg** - equality saturation toolkit + +Geolog occupies a unique niche: geometric logic with topos semantics applied to practical problems like workflow orchestration and Petri nets. diff --git a/notes/summary.md b/notes/summary.md new file mode 100644 index 0000000..0fe58d3 --- /dev/null +++ b/notes/summary.md @@ -0,0 +1,81 @@ +# Geolog Summary + +*Date: 2026-03-19* + +## What Is Geolog? + +Geolog is a **Geometric Logic REPL** — a reasoning engine written in Rust that implements type theory with semantics in topoi. It was AI-generated by Claude Opus 4.5. + +## Core Concepts + +### Axioms + +An axiom is an "if-then" rule: "If premises are true, then conclusion must be true." + +``` +forall x, y, z. friends(x,y), friends(y,z) |- knows(x,z) +``` + +Similar to Datalog rules, but extended with: +- Existentials in conclusions (`|- exists x. R(x)`) +- Disjunctions (`|- A \/ B`) +- Equality conclusions (`|- x = y`) + +### Chase Algorithm + +Repeatedly applies axioms until no new facts can be derived (fixpoint). Basic blocks: + +1. **Axioms** — the rules to apply +2. **Structure** — carriers (element sets), functions, relations +3. **Bindings** — variable-to-element mappings +4. **Tensor system** — finds violations (premises true, conclusion false) +5. **Fire conclusion** — adds relations, defines functions, creates elements, adds equations +6. **Congruence closure** — union-find for tracking element equality + +### Union-Find + +Data structure for tracking equivalence classes. Used for congruence closure when axioms conclude `x = y`. More efficient than naive dictionary + sets approach: +- Naive: O(n) per union +- Union-find: O(1) amortized per union + +### Language Syntax + +Geolog's syntax is not based on any single existing language. Influences: +- **Postfix application** (`x f` not `f(x)`) — category theory +- **Sequent notation** (`premises |- conclusion`) — proof theory +- **Path separators** (`/` not `.`) — unique to Geolog + +## Skeptical Assessment of Applications + +### Claimed Use Cases +- Business process workflow orchestration +- Formal verification +- Database query design +- Petri net reachability + +### Reality + +| Claim | Assessment | +|-------|------------| +| Workflow orchestration | No APIs, no integrations, no distributed execution — just a REPL | +| Formal verification | Lean4 proofs "in progress"; not comparable to Coq/Lean/TLA+ | +| Database query design | Not a database — no persistence at scale, no SQL, no transactions | +| Petri net reachability | Toy examples only, not industrial-scale | + +### What It Actually Is + +A **research/educational tool** for: +- Learning geometric logic and chase algorithms +- Experimenting with category-theoretic ideas +- Prototyping constraint systems +- Academic exploration + +**Not suitable for:** Production systems, real workflow orchestration, industrial formal verification, or database replacement. + +## Project Status + +- Version: 0.1.0 +- 30,000+ lines of Rust +- 168 tests (all passing) +- 30 example files +- Well-documented but unproven in real-world use