Adding more notes on the project
This commit is contained in:
Hassan Abedi
parent
ac2d363737
commit
4d1044b0af
@ -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.
|
||||
|
||||
81
notes/summary.md
Normal file
81
notes/summary.md
Normal file
@ -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
|
||||
Loading…
x
Reference in New Issue
Block a user