strata-k - GitLite

KO | EN

gitlite — search

#cloud-native #large-language-models #tensorflow #containers #openai #json #monitoring #bash #security #rust

strata-k

(★ 9)

A stratified, semiring-parameterized Datalog and its reference engine — the symbolic core of a neuro-symbolic logic system. Bool/Trop semirings, stratified negation, aggregates, exact probabilistic (?prob) queries, and a stable-model (@asp) solver.

File Explorer

ZIP Download

- - book.yml
  - ci.yml
  - gpu.yml
- gbnf_consumer_check.sh
- preregistration.md
- README.md
- - 00-prologue.md
  - 01-the-idea.md
  - 02-two-winters-three-bets.md
  - 03-dissolved-not-dead.md
  - 04-autopsies.md
  - 05-converging-lines.md
  - 06-meet-strata-k.md
  - 07-change-one-word.md
  - 08-choices-under-constraints.md
  - 09-the-language-that-checks-itself.md
  - 10-iron.md
  - 11-the-road.md
  - 12-first-contact.md
  - SUMMARY.md
- .gitignore
- book.toml
- - Cargo.toml
- - Cargo.toml
- - Cargo.toml
- - Cargo.toml
- - Cargo.toml
- - Cargo.toml
  - README.md
- - Cargo.toml
- - Cargo.toml
  - README.md
- - Cargo.toml
  - README.md
- - build.rs
  - Cargo.toml
  - pyproject.toml
  - README.md
- - Cargo.toml
  - README.md
- contract-verdict.md
- grammar.ebnf
- ir-encoding.md
- language.md
- strata.gbnf
- - ch01-ownership.strata
  - ch06-trading-house.strata
  - ch07-routes.strata
  - ch07-shared-evidence.strata
  - ch08-portfolio.strata
  - ch09-vignette-draft.strata
  - ch09-vignette-draft2.strata
  - ch09-vignette.strata
  - ch11-neural.strata
  - ch11-prov.strata
  - README.md
- - README.md
  - train_gnn.py
- - README.md
- asp.strata
- comparison.strata
- edges.tsv
- example.strata
- forbid.strata
- grad.strata
- prob.strata
- prov.strata
- tc.strata
- tc_tsv.strata
- terms.strata
- total_on.strata
- high-ir.schema.json
- verdict.schema.json
.gitattributes
.gitignore
ARCHITECTURE.md
Cargo.lock
Cargo.toml
CONTRIBUTING.md
LICENSE-APACHE
LICENSE-MIT
README.md
rust-toolchain.toml
rustfmt.toml

# Use via CDN

jsDelivr

jsDelivr serves any public GitHub repository as a CDN with zero setup. Pick a version and a file to get a ready-to-paste link and snippet.

Version

File

Link

Example

# Project Badges

CI Visit
License: MIT OR Apache-2.0 Visit

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

A stratified, semiring-parameterized Datalog and its execution engine — the
symbolic core of a neuro-symbolic logic system. This repository is the CPU
reference stack: frontend, IR, checker, interpreter, and the probabilistic
(режим B) and answer-set layers. The **stable surface** is the deductive and
probabilistic facade — Bool/Trop, `?prob`/`?grad`, `Prov`/`Prov_k`, `@terms`,
loaders, the CLI and the `strata-k`/Python facades. The answer-set (`@asp`)
island, the GPU engine, knowledge compilation, and incremental provenance
exist beside it as **explicitly experimental** surfaces (see the
[Stability section](docs/language.md#stability) and
[ARCHITECTURE.md](ARCHITECTURE.md)).

> **Status.** The executable core runs end-to-end: `text → parse → check →
> Core-IR → interpret → result`. Positive Datalog, stratified negation, and
> aggregates over the **Bool** and **Trop** (tropical, min-plus) semirings;
> exact **probabilistic** queries (`?prob`, distribution semantics) with
> **gradients** (`?grad`, reverse-mode over the режим-B chain); **neural**
> predicates (model-sourced soft facts, differentiated back through `?grad`);
> **structural terms** (`@terms`, constructor terms via hash-consing, with a
> depth bound and a sound-but-incomplete status); **provenance annotations**
> (`Prov`/`Prov_k` — every derived fact carries its pedigree, compiled to a
> circuit for exact or declared-lower-bound marginals); and an **answer-set**
> (stable model) solver for `@asp` modules. Cross-checked against
> [Soufflé](https://souffle-lang.github.io/) (200 random programs per CI run;
> a 10k sweep is one env var away, see Correctness below) and fuzzed
> naive-vs-semi-naive over 10k random programs. **Every shipped surface
> construct either executes with defined semantics or refuses with a stable
> documented diagnostic — nothing parses into a silent no-op**;
> the GPU backend runs beside this stack, validated bit-for-bit against it on
> CUDA hardware (`--features cuda`; hosted CI runs the CPU stub — see
> [Beyond the CPU pipeline](ARCHITECTURE.md#beyond-the-cpu-pipeline)).

## Quick start

```sh
cargo build
cargo run -p strata-cli -- run examples/tc.strata
```

Install the `strata` binary onto your PATH, or embed the engine as a library:

```sh
cargo install --path crates/strata-cli    # the `strata` binary
```

```toml
# Cargo.toml — the library facade (parse → check → run, queries, provenance,
# ASP, in-process neural models); see crates/strata-k/README.md
strata-k = { git = "https://github.com/vsov/strata-k" }
```

Or use it from Python — the bridge exposes the same pipeline (`compile`,
`eval`, `prob_query`/`grad_query`, provenance DNFs, ASP models, Python
callables as neural models); see [crates/strata-py](crates/strata-py/README.md):

```sh
pip install maturin && pip install ./crates/strata-py
python -c 'import strata_k; print(strata_k.compile("pred p(int): Bool.\np(1).").eval())'
```

(The crates are not on crates.io/PyPI yet; the git dependency, `cargo install
--path`, and `pip install ./crates/strata-py` are the supported channels.)

`examples/tc.strata` computes a transitive closure:

```
% transitive closure
domain node.
pred edge(node, node): Bool.
pred path(node, node): Bool.

path(X, Y) :- edge(X, Y).
path(X, Z) :- edge(X, Y), path(Y, Z).

edge(a, b).
edge(b, c).
edge(c, d).
```

```
$ strata run examples/tc.strata
edge(a, b)
edge(b, c)
edge(c, d)
path(a, b)
path(a, c)
path(a, d)
path(b, c)
path(b, d)
path(c, d)
```

Past the syntax examples, [examples/workloads/](examples/workloads/README.md)
holds data-driven end-to-end programs — an AML ownership screen (soft model
flags, `Prov_k` pedigrees, gradients, negation over soft evidence) and
all-pairs cheapest-cost routing (Trop) — with every quoted number pinned in CI
(`crates/strata-cli/tests/workloads.rs`). A third recipe,
[examples/python/](examples/python/README.md), trains a GNN *through* the logic
layer: the engine's exact gradient flows back into the model's weights.

## The language

Grammar priority: **optimized for LLMs to write**, human readability second.
Familiar Datalog `:-`, Prolog lexical convention (variables `Uppercase`,
constants `lowercase`), and **mandatory predicate signatures** so a typo becomes
a compile error, not a silently empty relation.

```
pred edge(node, node): Bool.          % a predicate signature: types + semiring
5 :: edge(a, b).                       % a tropical (weighted) fact
reach(X, Z) :- edge(X, Y), reach(Y, Z). % a recursive rule
unreach(X) :- node(X), not reach(X).    % stratified negation
outdeg(X, count<Y>) :- edge(X, Y).      % an aggregate
input edge from "edges.tsv".            % load facts from a Soufflé-compatible TSV
```

| Feature | Notes |
|---|---|
| Semirings | `Bool` (boolean Datalog), `Trop` (min-plus: shortest paths, Viterbi) |
| Weights | `Trop` weights are `i64` with a distinct `+∞` — comparisons are bit-exact |
| Negation | `not p(..)` — stratified in the deductive core; unstratified under `@asp` |
| Aggregates | `min`/`max`/`sum`/`count` (`prob_or` reserved); non-recursive |
| Probabilistic | `0.87 :: fact.` + `?prob q(..)` → exact marginals (distribution semantics) |
| Queries | plain `?q(a, _)` filters the run's output to matching tuples; `?prob`/`?grad` compute |
| Answer sets | `@asp.` module → stable models via a reference solver |
| EDB | inline facts, or `input p from "file.tsv"` — typed columns, atomic once-only load |

```
$ strata run examples/prob.strata          # ?prob path(a, c)
0.625 :: path(a, c)

$ strata run examples/asp.strata           # @asp in/out choice over {x, y}
Answer 1: {in(x), in(y), node(x), node(y)}
Answer 2: {in(x), node(x), node(y), out(y)}
Answer 3: {in(y), node(x), node(y), out(x)}
Answer 4: {node(x), node(y), out(x), out(y)}
```

The full language is described in [docs/language.md](docs/language.md); the
formal grammar is in [docs/grammar.ebnf](docs/grammar.ebnf).

## CLI

```
strata check <file.strata> [--error-format=text|json]   # parse + type-check, no run
strata run   <file.strata> [--semi-naive]               # evaluate and print relations
strata fmt   <file.strata> [--check]                    # canonical formatter
strata ir    <file>        --to json|surface            # convert surface <-> JSON IR
strata grammar gbnf                                     # constrained-decoding grammar (sampler mask)
```

Diagnostics carry a stable code (`E0xxx` front-end, `E1xxx` checker), a source
span, and (where possible) a machine-applicable fix:

```
$ strata check bad.strata
error[E1001]: predicate `edge` is used but never declared
  --> 2:1
   | path(X, X) :- edge(X, X).
   | ^^^^^^^^^^^^^^^^^^^^^^^^^
```

Exit codes: `0` ok · `1` diagnostics · `2` usage · `4` runtime fault.

## Two representations

The **High-IR JSON** document is the source of truth; the surface syntax is a
canonical projection of it (`strata ir` converts both ways, and `fmt` is
`parse → print`). An LLM can author either. The JSON Schema is published at
[`schema/high-ir.schema.json`](schema/high-ir.schema.json); the encoding
convention is in [`docs/ir-encoding.md`](docs/ir-encoding.md).

## Architecture

A Cargo workspace of eleven crates, layered so the base has no sibling
dependencies:

```
strata-ir      IR data model (High-IR + Core-IR), symbol dictionary, diagnostics,
               JSON schema, tropical weight, hash-cons term table — the shared base
strata-front   lexer, parser (surface → High-IR), canonical printer, fmt, E0xxx diagnostics
strata-check   dependency graph, stratification, type/semiring checks (table 2.4),
               normalization High-IR → Core-IR, E1xxx diagnostics
strata-eval    the reference interpreter over Core-IR — naive T_P, semi-naive,
               exact probabilistic marginals + gradients (режим B), DRed; the oracle
strata-asp     the answer-set stack — reference solver, normalization, aspif,
               clasp embedding, unfounded-set verification
strata-gpu     the GPU execution engine (cuda-feature-gated; CPU stub without) —
               device-resident fixpoints, WCOJ, query planner, ASP grounding
strata-terms   structural-term machinery — interning, magic sets, points-to
strata-prob    provenance circuits — SDD-class WMC, gradients, top-k, MNIST-sum
strata-k       the library facade — embed the engine; Model trait (in-process neural)
strata-cli     the `strata` binary
strata-py      the Python bridge (pyo3) — `import strata_k`; built by maturin
```

`strata-front` and `strata-check` are siblings that both depend only on
`strata-ir`; the engine crates (`strata-gpu`, `strata-terms`, `strata-prob`)
sit beside `strata-eval` and are validated bit-for-bit against the reference
stack — for `strata-gpu` that validation needs CUDA hardware
(`cargo test -p strata-gpu --features cuda`; hosted CI runs the CPU stub, so
the badge does not cover the GPU differentials). See
[ARCHITECTURE.md](ARCHITECTURE.md) for the full picture and
[CONTRIBUTING.md](CONTRIBUTING.md) to build and test.

## Correctness

The reference interpreter is the oracle. It ships **two** engines — the
obviously-correct naive `T_P` fixpoint and a semi-naive delta engine — that are
cross-checked against each other, and against Soufflé for the Bool fragment:

```sh
cargo test                                     # unit + integration + corpus diffs
cargo test -p strata-eval --test fuzz          # naive == semi-naive over 10k random programs
cargo test -p strata-cli  --test souffle_diff  # our engine vs Soufflé (needs `souffle`)
STRATA_SOUFFLE_FUZZ_N=10000 cargo test -p strata-cli --test souffle_diff fuzz_bool_vs_souffle
```

Trop is validated against an independent shortest-path oracle rather than
Soufflé. If `souffle` is not installed, the differential tests skip cleanly.
Probabilistic queries are computed by exact possible-world enumeration (the
obviously-correct режим-B reference); answer sets by the Gelfond–Lifschitz
reduct — both the slow, exact oracles a compiled/GPU method must later match.
The provenance circuit has an *external* differential too: the Python test
suite compiles the same proof DNFs with PySDD (the UCLA SDD package) and the
two weighted counts must agree (`crates/strata-py/tests/`, mandatory in CI).

## The book

`book/` holds *Programs That Know Why* — a short book on logic programming in the
age of LLMs and the design of Strata/K, built with [mdBook](https://rust-lang.github.io/mdBook/).
📖 **Read it online: <https://vsov.github.io/strata-k/>**
**Work in progress.** Every runnable listing lives in `examples/book/` and runs
under the current `strata` CLI (CI-checked — see `crates/strata-cli/tests/book_listings.rs`). Text is licensed CC BY-SA 4.0; example code is
MIT/Apache like the rest of the repo.

```sh
mdbook serve book   # if you have mdBook installed
```

## Documentation

- [docs/language.md](docs/language.md) — the language reference (syntax + semantics)
- [crates/strata-py/README.md](crates/strata-py/README.md) — the Python bridge (`import strata_k`)
- [ARCHITECTURE.md](ARCHITECTURE.md) — crate graph, two-level IR, evaluation engines
- [CONTRIBUTING.md](CONTRIBUTING.md) — build, test, and the differential-testing story
- [docs/grammar.ebnf](docs/grammar.ebnf) — the formal grammar
- [docs/strata.gbnf](docs/strata.gbnf) — its GBNF projection for constrained decoding (`strata grammar gbnf`), parser-differentially tested
- [docs/ir-encoding.md](docs/ir-encoding.md) — the JSON IR encoding convention

## License

Licensed under either of

- Apache License, Version 2.0 ([LICENSE-APACHE](LICENSE-APACHE))
- MIT license ([LICENSE-MIT](LICENSE-MIT))

at your option. The book text under `book/` is licensed
[CC BY-SA 4.0](https://creativecommons.org/licenses/by-sa/4.0/); its example code
follows the repo's MIT/Apache dual license.

Unless you explicitly state otherwise, any contribution intentionally submitted
for inclusion in the work by you, as defined in the Apache-2.0 license, shall be
dual licensed as above, without any additional terms or conditions.