habedi-work/useful-notes
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

WIP

Browse Source
This commit is contained in:
Hassan Abedi 2026-03-30 10:45:39 +02:00
parent dc343be7ad
commit f6af3ab731
4 changed files with 129 additions and 82 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

40
hassan/008-chase-algorithm.md
View File

@ -9,33 +9,37 @@
### Algorithm Variants
| Variant | Output Size | Speed per Step | Satisfaction Check | Used By | Best For |
|:---------------|:------------|:---------------|:-------------------|:------------------|:----------------------------------------------|
| Oblivious | Largest | Fastest | None | — | Prototyping; when output size doesn't matter |
| Skolem | Medium | Fast | Implicit (Skolem terms) | VLog, Graal | Parallelism; data exchange; deterministic runs |
| Restricted | Smallest | Slower | Explicit (homomorphism check) | RDFox, VLog | Production use; query performance over large KGs |
| Core | Most compact | Slowest | Full core computation | — (theoretical) | Theoretical analysis; minimum representations |
| Variant | Output Size | Speed per Step | Satisfaction Check | Used By | Best For |
|:-----------|:-------------|:---------------|:------------------------------|:----------------|:-------------------------------------------------|
| Oblivious | Largest | Fastest | None | — | Prototyping; when output size doesn't matter |
| Skolem | Medium | Fast | Implicit (Skolem terms) | VLog, Graal | Parallelism; data exchange; deterministic runs |
| Restricted | Smallest | Slower | Explicit (homomorphism check) | RDFox, VLog | Production use; query performance over large KGs |
| Core | Most compact | Slowest | Full core computation | — (theoretical) | Theoretical analysis; minimum representations |
#### Variant Notes
**Oblivious Chase** fires every applicable rule without checking whether the conclusion already holds. Simple to implement but produces redundant facts and is the hardest to guarantee termination for.
**Oblivious Chase** fires every applicable rule without checking whether the conclusion already holds. Simple to implement but produces redundant
facts and is the hardest to guarantee termination for.
**Skolem Chase** uses deterministic Skolem functions to generate nulls — the same rule trigger always produces the same null. This makes it idempotent and easy to parallelize, with no need to track which rules have already fired.
**Skolem Chase** uses deterministic Skolem functions to generate nulls — the same rule trigger always produces the same null. This makes it idempotent
and easy to parallelize, with no need to track which rules have already fired.
**Restricted Chase** checks before firing whether the rule head is already satisfied via a homomorphism into the current database. Never adds redundant facts, producing the smallest universal solution. The homomorphism check is NP-hard in general but fast in practice with good indexing.
**Restricted Chase** checks before firing whether the rule head is already satisfied via a homomorphism into the current database. Never adds
redundant facts, producing the smallest universal solution. The homomorphism check is NP-hard in general but fast in practice with good indexing.
**Core Chase** goes further than the restricted chase, computing the logical core — the most compressed possible universal solution. Theoretically important but computationally expensive; not used in production engines.
**Core Chase** goes further than the restricted chase, computing the logical core — the most compressed possible universal solution. Theoretically
important but computationally expensive; not used in production engines.
### Chase Query Engines
| Engine | Organization | Chase Variant | Home Page |
|:---------|:-------------------------------|:-------------------|:-------------------------------------------------------------------------------------|
| RDFox | Oxford Semantic Technologies | Restricted | [oxfordsemantic.tech/rdfox](https://oxfordsemantic.tech/rdfox) |
| VLog | TU Dresden / VU Amsterdam | Restricted + Skolem | [github.com/karmaresearch/vlog](https://github.com/karmaresearch/vlog) |
| Graal | LIRMM, Montpellier | Skolem + Oblivious | [graphik-team.github.io/graal](https://graphik-team.github.io/graal) |
| Vadalog | University of Oxford / TU Wien | Warded (Restricted variant) | [vadalog-system.com](https://vadalog-system.com) |
| PDQ | University of Oxford | Skolem | [github.com/michaelbenedict/pdq](https://github.com/michaelbenedict/pdq) |
| Llunatic | University of Genova | Skolem | [github.com/donatellosantoro/Llunatic](https://github.com/donatellosantoro/Llunatic) |
| Engine | Organization | Chase Variant | Home Page |
|:---------|:-------------------------------|:----------------------------|:-------------------------------------------------------------------------------------|
| RDFox | Oxford Semantic Technologies | Restricted | [oxfordsemantic.tech/rdfox](https://oxfordsemantic.tech/rdfox) |
| VLog | TU Dresden / VU Amsterdam | Restricted + Skolem | [github.com/karmaresearch/vlog](https://github.com/karmaresearch/vlog) |
| Graal | LIRMM, Montpellier | Skolem + Oblivious | [graphik-team.github.io/graal](https://graphik-team.github.io/graal) |
| Vadalog | University of Oxford / TU Wien | Warded (Restricted variant) | [vadalog-system.com](https://vadalog-system.com) |
| PDQ | University of Oxford | Skolem | [github.com/michaelbenedict/pdq](https://github.com/michaelbenedict/pdq) |
| Llunatic | University of Genova | Skolem | [github.com/donatellosantoro/Llunatic](https://github.com/donatellosantoro/Llunatic) |
## Changelog

128
hassan/009-logic-primer.md
View File

@ -7,18 +7,23 @@ A reference for the core concepts of first-order logic and database theory.
## Building Blocks
### Constants
Specific known values — real things in your database.
```
Alice, Bob, Engineering, 42
```
### Variables
Placeholders for unknown values, usually written in uppercase or with `?`.
```
X, Y, ?person, ?dept
```
### Terms
A term is either a constant or a variable. Anything that can fill an argument slot in a predicate.
---
@ -26,6 +31,7 @@ A term is either a constant or a variable. Anything that can fill an argument sl
## Predicates and Atoms
A **predicate** is a named relation applied to a list of terms:
```
Employee(X, Y) -- predicate "Employee", arity 2
Likes(X, Y, Z) -- predicate "Likes", arity 3
@ -35,6 +41,7 @@ Person(Alice) -- predicate "Person", arity 1
The number of arguments a predicate takes is its **arity**.
An **atom** is a predicate applied to specific terms. When all terms are constants it is called a **ground atom** — a concrete fact in the database:
```
Employee(Alice, Engineering) -- ground atom
```
@ -49,45 +56,49 @@ A **rule** is an if-then statement built from atoms, split into two parts:
body → head
```
| Part | Also Called | Meaning |
|:-----|:------------|:--------|
| Body | Antecedent, LHS | Conditions that must hold |
| Part | Also Called | Meaning |
|:-----|:----------------|:--------------------------------|
| Body | Antecedent, LHS | Conditions that must hold |
| Head | Consequent, RHS | What must be true if body holds |
Example:
```
Employee(X, Y), Department(Y) → ∃Z. ManagedBy(Y, Z)
```
Variables in the head that do not appear in the body are **existential variables** — they represent unknown values that must exist, but whose identity is not known.
Variables in the head that do not appear in the body are **existential variables** — they represent unknown values that must exist, but whose identity
is not known.
---
## Quantifiers
| Symbol | Name | Meaning | Example |
|:-------|:-----|:--------|:--------|
| `∀` | Universal | "For all..." | `∀X. Person(X) → Mortal(X)` |
| `∃` | Existential | "There exists some..." | `∀X. Person(X) → ∃Y. MotherOf(X, Y)` |
| Symbol | Name | Meaning | Example |
|:-------|:------------|:-----------------------|:-------------------------------------|
| `∀` | Universal | "For all..." | `∀X. Person(X) → Mortal(X)` |
| `∃` | Existential | "There exists some..." | `∀X. Person(X) → ∃Y. MotherOf(X, Y)` |
---
## Connectives
| Symbol | Name | Meaning |
|:-------|:-----|:--------|
| `∧` | Conjunction | AND |
| `∨` | Disjunction | OR |
| `¬` | Negation | NOT |
| `→` | Implication | IF...THEN |
| `↔` | Biconditional | IF AND ONLY IF |
| Symbol | Name | Meaning |
|:-------|:--------------|:---------------|
| `∧` | Conjunction | AND |
| `∨` | Disjunction | OR |
| `¬` | Negation | NOT |
| `→` | Implication | IF...THEN |
| `↔` | Biconditional | IF AND ONLY IF |
---
## Key Concepts
### Substitution
A mapping from variables to terms. Written as `σ`:
```
σ = { X → Alice, Y → Engineering }
@ -95,55 +106,64 @@ Employee(X, Y) under σ = Employee(Alice, Engineering)
```
### Homomorphism
A substitution that maps one set of atoms into another, preserving structure. Used in the chase to check whether a rule head is already satisfied in the database.
A substitution that maps one set of atoms into another, preserving structure. Used in the chase to check whether a rule head is already satisfied in
the database.
### Ground Instance
An atom or rule with all variables replaced by constants — no variables remaining.
### Herbrand Universe
The set of all ground terms constructable from the constants and function symbols in a formula. Represents the "world" of all possible values.
### Skolem Term / Skolem Function
A named placeholder for an existentially quantified variable, constructed deterministically from the values that triggered it:
```
∀X. Person(X) → ∃Y. MotherOf(X, Y)
Skolemized: MotherOf(X, mother_of(X))
```
The Skolem term `mother_of(X)` means "the mother of X, whoever that is." Same input always produces the same term.
---
## Types of Dependencies (Rules)
| Type | Abbreviation | Form | Meaning |
|:-----|:-------------|:-----|:--------|
| Tuple-generating dependency | TGD | `body → ∃z. head` | If body holds, some new tuple must exist |
| Equality-generating dependency | EGD | `body → x = y` | If body holds, two values must be equal |
| Functional dependency | FD | Special EGD | A set of attributes uniquely determines another |
| Full dependency | — | TGD with no existentials | Head variables all appear in body |
| Type | Abbreviation | Form | Meaning |
|:-------------------------------|:-------------|:-------------------------|:------------------------------------------------|
| Tuple-generating dependency | TGD | `body → ∃z. head` | If body holds, some new tuple must exist |
| Equality-generating dependency | EGD | `body → x = y` | If body holds, two values must be equal |
| Functional dependency | FD | Special EGD | A set of attributes uniquely determines another |
| Full dependency | — | TGD with no existentials | Head variables all appear in body |
---
## Rule Classes and Termination
| Rule Class | Existentials | Termination Guarantee | Notes |
|:-----------|:-------------|:----------------------|:------|
| Datalog | No | Always | Core of logic programming |
| Weakly acyclic | Yes | Yes | No cyclic value propagation through existentials |
| Guarded | Yes | No (but decidable) | Existential vars "guarded" by a body atom |
| Frontier-one | Yes | No (but decidable) | At most one frontier variable per rule |
| General TGDs | Yes | Undecidable | No restrictions |
| Rule Class | Existentials | Termination Guarantee | Notes |
|:---------------|:-------------|:----------------------|:-------------------------------------------------|
| Datalog | No | Always | Core of logic programming |
| Weakly acyclic | Yes | Yes | No cyclic value propagation through existentials |
| Guarded | Yes | No (but decidable) | Existential vars "guarded" by a body atom |
| Frontier-one | Yes | No (but decidable) | At most one frontier variable per rule |
| General TGDs | Yes | Undecidable | No restrictions |
---
## Datalog
Datalog is a logic programming language and the most important rule class for the chase. It is a restriction of first-order logic with no function symbols and no existential variables in rule heads.
Datalog is a logic programming language and the most important rule class for the chase. It is a restriction of first-order logic with no function
symbols and no existential variables in rule heads.
### Syntax
A Datalog program consists of:
- **Facts** — ground atoms representing known data
- **Rules** — if-then statements deriving new facts from existing ones
@ -160,18 +180,19 @@ Colleague(X, Y) :- WorksIn(X, D), WorksIn(Y, D), X ≠ Y.
### Key Properties
| Property | Value |
|:---------|:------|
| Existentials in head | No |
| Function symbols | No |
| Negation | Stratified only |
| Termination | Always |
| Data complexity | PTIME |
| Evaluation strategy | Bottom-up (forward chaining) or top-down (backward chaining) |
| Property | Value |
|:---------------------|:-------------------------------------------------------------|
| Existentials in head | No |
| Function symbols | No |
| Negation | Stratified only |
| Termination | Always |
| Data complexity | PTIME |
| Evaluation strategy | Bottom-up (forward chaining) or top-down (backward chaining) |
### Evaluation
Datalog is evaluated by computing the **least fixed point** — repeatedly applying all rules until no new facts are derived. This is exactly the chase with no existentials:
Datalog is evaluated by computing the **least fixed point** — repeatedly applying all rules until no new facts are derived. This is exactly the chase
with no existentials:
```
Iteration 0: { Employee(alice, engineering), Employee(bob, marketing), Department(engineering) }
@ -182,7 +203,8 @@ Iteration 3: nothing new → stop
### Datalog vs SQL
Datalog can express **recursive queries** naturally, which SQL cannot without special extensions (like recursive CTEs). For example, computing transitive closure (all ancestors of a person) is trivial in Datalog:
Datalog can express **recursive queries** naturally, which SQL cannot without special extensions (like recursive CTEs). For example, computing
transitive closure (all ancestors of a person) is trivial in Datalog:
```
Ancestor(X, Y) :- Parent(X, Y).
@ -191,26 +213,29 @@ Ancestor(X, Y) :- Parent(X, Z), Ancestor(Z, Y).
### Datalog and the Chase
Pure Datalog evaluation is a restricted chase with no existential variables — all chase variants behave identically. The fixed point is always reached in at most O(n^k) steps.
Pure Datalog evaluation is a restricted chase with no existential variables — all chase variants behave identically. The fixed point is always reached
in at most O(n^k) steps.
---
## Geometric Logic
Geometric logic is a fragment of first-order logic that is particularly well-suited to the chase. It is the theoretical foundation for most modern chase-based reasoning engines.
Geometric logic is a fragment of first-order logic that is particularly well-suited to the chase. It is the theoretical foundation for most modern
chase-based reasoning engines.
### Definition
A formula is **geometric** if it uses only:
| Allowed | Not Allowed |
|:--------|:-----------|
| Conjunction `∧` | Universal quantifier `∀` in head |
| Disjunction `∨` | Negation `¬` |
| Existential quantifier `∃` | Implication `→` in head |
| Equality `=` | Infinite conjunctions in head |
| Allowed | Not Allowed |
|:---------------------------|:---------------------------------|
| Conjunction `∧` | Universal quantifier `∀` in head |
| Disjunction `∨` | Negation `¬` |
| Existential quantifier `∃` | Implication `→` in head |
| Equality `=` | Infinite conjunctions in head |
A **geometric sequent** (rule) has the form:
```
φ ⊢ ψ
@ -234,9 +259,11 @@ Employee(X) ∧ X = Y ⊢ Employee(Y)
### Why Geometric Logic Matters
Geometric logic has a special property: if a geometric formula is true in a model, it remains true in any **extension** of that model (adding more facts never makes it false). This is called **monotonicity** and is exactly what makes the chase work — the chase only adds facts, never removes them.
Geometric logic has a special property: if a geometric formula is true in a model, it remains true in any **extension** of that model (adding more
facts never makes it false). This is called **monotonicity** and is exactly what makes the chase work — the chase only adds facts, never removes them.
This property means:
- The chase directly computes models of geometric theories
- Every geometric theory has a **canonical model** — the one the chase builds
- Query answers over the chase result are guaranteed correct for any model of the theory
@ -260,7 +287,8 @@ Geometric sequent: Employee(X) ⊢ ∃Y. WorksIn(X, Y)
TGD: Employee(X) → ∃Y. WorksIn(X, Y)
```
The chase is the standard procedure for building models of geometric theories. Given a set of geometric axioms and an initial database, the chase constructs the minimal model satisfying all axioms — which is exactly the universal solution used for query answering.
The chase is the standard procedure for building models of geometric theories. Given a set of geometric axioms and an initial database, the chase
constructs the minimal model satisfying all axioms — which is exactly the universal solution used for query answering.
---

17
hassan/010-datomic-for-geolog.md
View File

@ -26,7 +26,8 @@ So the right mental model is:
### Why It Fits Part of the Problem
The notes describe Geolog as infrastructure with persistent, append-only storage and an interactive REPL, not just as a one-shot solver. Datomic's immutable fact model lines up well with that storage story.
The notes describe Geolog as infrastructure with persistent, append-only storage and an interactive REPL, not just as a one-shot solver. Datomic's
immutable fact model lines up well with that storage story.
Good candidates to store in Datomic:
@ -56,7 +57,8 @@ Geolog needs chase behavior that can:
* branch when a rule concludes a disjunction
* merge terms when equations force equality
Those are central to the chase-based model described in the notes, and they are not features Datomic gives you as a database. Datomic gives you a temporal fact store plus Datalog query tools; it does not give you a geometric-logic engine.
Those are central to the chase-based model described in the notes, and they are not features Datomic gives you as a database. Datomic gives you a
temporal fact store plus Datalog query tools; it does not give you a geometric-logic engine.
That means a Datomic-based Geolog would still need its own:
@ -72,7 +74,8 @@ Inference: Datomic is a reasonable substrate for storing models and derivation h
### Licensing and Stack Implications
As of March 26, 2026, Datomic's official docs say that all editions are free and that the binaries are licensed under Apache 2.0, while Datomic's own FAQ says it is not open source because the source is not published.
As of March 26, 2026, Datomic's official docs say that all editions are free and that the binaries are licensed under Apache 2.0, while Datomic's own
FAQ says it is not open source because the source is not published.
Official sources:
@ -96,12 +99,14 @@ That source-unavailable dependency has real engineering consequences:
* fully reproducible "build everything from source" workflows become weaker
* some contributors will reject the stack on principle because it is not fully open
So the licensing issue is not "can it legally coexist with open parts of the stack?" The answer there is mostly **yes**. The more important question is strategic:
So the licensing issue is not "can it legally coexist with open parts of the stack?" The answer there is mostly **yes**. The more important question
is strategic:
* does Geolog want a fully open, self-hostable, inspectable foundation
* or is it acceptable to place the storage layer on a free but closed-source binary
If Geolog wants the strongest possible open-source story, Datomic is a poor fit. If Geolog mainly wants a strong immutable fact store and accepts vendor dependence, Datomic remains viable.
If Geolog wants the strongest possible open-source story, Datomic is a poor fit. If Geolog mainly wants a strong immutable fact store and accepts
vendor dependence, Datomic remains viable.
---
@ -116,4 +121,4 @@ For Geolog as described in these notes:
## Changelog
* **Mar 26, 2026** -- Added note on whether Datomic could serve as a backend for Geolog, including licensing implications.
* **Mar 26, 2026** -- First version created.

22
hassan/011-geolog-intermediate-representation.md
View File

@ -3,7 +3,8 @@
This note summarizes the intermediate representation currently implemented in the Geolog repo on branch `ir-draft1`:
https://git.sgai.uk/creators/geolog/-/tree/ir-draft1?ref_type=heads
All file paths below are repo-relative, not local workspace paths. The main sources are `geolog-lang/src/Geolog/IR.hs` and `geolog-lang/src/Geolog/Lower.hs`.
All file paths below are repo-relative, not local workspace paths. The main sources are `geolog-lang/src/Geolog/IR.hs` and
`geolog-lang/src/Geolog/Lower.hs`.
## Where the IR sits
@ -40,7 +41,8 @@ The lowering entry point is `geolog-lang/src/Geolog/Lower.hs`, via `lowerTop`, w
The IR is intentionally relational. It turns theory structure into tables and rules.
- `Path = [QName]`: a hierarchical name like `["M","mul"]`, pretty-printed as `M.mul`.
- `ColType` is the type of a column. `EntityType Path` means the column refers to rows from another entity/table, `PrimType PrimInt | PrimString` covers builtin scalars, and `Tuple [(QName, ColType)]` supports structured values.
- `ColType` is the type of a column. `EntityType Path` means the column refers to rows from another entity/table, `PrimType PrimInt | PrimString`
covers builtin scalars, and `Tuple [(QName, ColType)]` supports structured values.
- `Table` contains `columns :: [ColType]` and `primaryKey :: Maybe [Int]`.
- `Term` supports literals, variables, projections like `x.field`, and record construction.
- `Atom` contains `table :: Path`, `rowId :: Maybe Term`, and `values :: Map Int Term`.
@ -86,7 +88,8 @@ This logic is in `finishTheory` in `geolog-lang/src/Geolog/Lower.hs`.
Lowering is not just flattening syntax. It also turns shared context into explicit columns.
`liftOnShared` copies shared outer variables into the current row shape so that dependencies become relationally explicit. This is why tables like `D.mul` contain both `M.car` arguments and displayed-car columns.
`liftOnShared` copies shared outer variables into the current row shape so that dependencies become relationally explicit. This is why tables like
`D.mul` contain both `M.car` arguments and displayed-car columns.
See `liftOnShared` in `geolog-lang/src/Geolog/Lower.hs`.
@ -158,7 +161,8 @@ The implemented IR is best understood as a relationalized, flattened theory:
- references become foreign-key-style laws
- total functions become tables plus totality laws
So the IR is not just an AST for queries. It is the bridge from elaborated dependent syntax to a database-shaped form that later evaluation code can consume.
So the IR is not just an AST for queries. It is the bridge from elaborated dependent syntax to a database-shaped form that later evaluation code can
consume.
## Status
@ -181,8 +185,14 @@ What still looks missing:
So the current IR is best seen as a lowered theory IR, not yet a full chase-runtime IR.
If the project keeps this design, the natural next step is probably a second layer above `FlatTheory` for runtime execution state. That layer would hold current facts, branch identity, fresh-name allocation, equality information, and evaluation metadata.
If the project keeps this design, the natural next step is probably a second layer above `FlatTheory` for runtime execution state. That layer would
hold current facts, branch identity, fresh-name allocation, equality information, and evaluation metadata.
## Note
`docs/lecture3.tex` has a `Query IR` section header but no content yet, so the code above is currently the most concrete description of the actual intermediate representation.
`docs/lecture3.tex` has a `Query IR` section header but no content yet, so the code above is currently the most concrete description of the actual
intermediate representation.
## Changelog
* **Mar 30, 2026** -- First version created.