89 lines
2.2 KiB
Markdown
89 lines
2.2 KiB
Markdown
|
# Key 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`
|
||
|
|
|
||
|
|
Datalog is limited to Horn clauses (single atom in head). Geolog supports geometric sequents.
|
||
|
|
|
||
|
|
---
|
||
|
|
|
||
|
|
## Chase Algorithm
|
||
|
|
|
||
|
|
Repeatedly applies axioms until no new facts can be derived (fixpoint).
|
||
|
|
|
||
|
|
### Building Blocks
|
||
|
|
|
||
|
|
1. **Axioms** — 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
|
||
|
|
6. **Congruence closure** — tracks element equality via union-find
|
||
|
|
|
||
|
|
### Loop
|
||
|
|
|
||
|
|
```
|
||
|
|
repeat until no changes:
|
||
|
|
for each axiom:
|
||
|
|
find violations (tensor system)
|
||
|
|
fire conclusion for each violation
|
||
|
|
propagate equations (congruence closure)
|
||
|
|
```
|
||
|
|
|
||
|
|
---
|
||
|
|
|
||
|
|
## Union-Find
|
||
|
|
|
||
|
|
Data structure for tracking equivalence classes. Inputs are elements (IDs), not sets.
|
||
|
|
|
||
|
|
```
|
||
|
|
union(3, 7) // "3 and 7 are now equivalent"
|
||
|
|
union(7, 12) // "7 and 12 are now equivalent"
|
||
|
|
find(3) // Returns same representative as find(12)
|
||
|
|
```
|
||
|
|
|
||
|
|
### Why Not Dictionary + Sets?
|
||
|
|
|
||
|
|
| Approach | Union Cost |
|
||
|
|
|----------|------------|
|
||
|
|
| Dict + Sets | O(n) — must update all elements in merged set |
|
||
|
|
| Union-Find | O(1) amortized — just one pointer update |
|
||
|
|
|
||
|
|
Used for congruence closure when axioms conclude `x = y`.
|
||
|
|
|
||
|
|
---
|
||
|
|
|
||
|
|
## Language Syntax
|
||
|
|
|
||
|
|
Not based on any single existing language. Influences:
|
||
|
|
|
||
|
|
| Feature | Source |
|
||
|
|
|---------|--------|
|
||
|
|
| Postfix application (`x f` not `f(x)`) | Category theory |
|
||
|
|
| Sequent notation (`premises \|- conclusion`) | Proof theory |
|
||
|
|
| Path separators (`/` not `.`) | Unique to Geolog |
|
||
|
|
| Theory/Instance structure | Algebraic specification languages |
|
||
|
|
|
||
|
|
---
|
||
|
|
|
||
|
|
## Geometric Logic Restrictions
|
||
|
|
|
||
|
|
By design, Geolog excludes:
|
||
|
|
- Negation (no `not R(x)`)
|
||
|
|
- Classical implication (no `if A then B`)
|
||
|
|
- Arithmetic (no `x + 1 = y`)
|
||
|
|
|
||
|
|
These are intentional limits for topos-theoretic semantics, not missing features.
|