Language Reference

Release context: Current released language surface Language coverage: Core language, the language-completeness contract, the epistemic solver surface, epistemic executor completion (EIR-derived candidate enumeration, value-level modal membership, per-tuple-key FAEEL foundedness, ground epistemic constraints, safe split, and joint multi-epistemic solving), and semantic completion (mixed global+per-row modal gates compose conjunctively; finite nested modal chains normalize by parity/duality; same-name multi-arity disambiguates by arity-qualified tuple sources; recursive execution covers determined stratification, positive Gelfond 1991 compatibility recursion, stratified negated modals, and cyclic negated modals through the xlog-gpu GPU-backed WFS plan without the old xlog_prob host-WFS solver; only genuinely unbounded, unsafe, or unfounded modal cycles remain fail-closed)

This document provides a comprehensive reference for the XLOG language, covering all syntax, semantics, and features of XLOG as a GPU-native logic programming language. The language-completeness additions define the contract for finite terms, lists, safe meta-predicates, deterministic negation, magic sets, probabilistic aggregates, approximate inference, and CLI inspectability. The epistemic source surface adds know, possible, not know, not possible, and #pragma epistemic_mode = faeel|g91. Accepted epistemic programs route through the high-level EIR and GPU epistemic runtime; unsupported forms must fail with typed diagnostics rather than silently falling back to CPU evaluation.

Overview
Basic Syntax
Data Types
Language Completeness Contract
Predicates and Declarations
Facts
Rules
Queries
Constraints
Variables and Wildcards
Comparisons
Arithmetic Expressions
Negation
Aggregations
Lists
Safe Meta-Predicates
Magic Sets
User-Defined Functions
Modules
Symbols
Probabilistic Logic
Epistemic Logic
Approximate Inference
Neural Predicates
Learnable Rules
Term Embeddings
GPU ILP Configuration
Pragmas and Directives
CLI Developer Experience
Float Predicates and IEEE 754 Semantics
Comments
Complete Grammar Reference

Overview

XLOG is a GPU-native logic programming language that compiles typed, modular logic programs into backend-specific GPU execution paths. It supports:

Datalog fundamentals: Facts, rules, recursive queries, and stratified negation
Arithmetic operations: Comparisons, computed values via is, and built-in functions
Aggregations: count, sum, min, max, and logsumexp
Probabilistic reasoning: Probabilistic facts, annotated disjunctions, evidence, and queries
Epistemic reasoning: know/possible modal body literals, FAEEL default semantics, and Gelfond 1991 compatibility mode through explicit EIR/GPU execution paths
Language-completeness contract: Finite lists, safe meta-predicates, explicit negation contracts, magic-set planning, probabilistic aggregate semantics, approximate inference configuration, incremental parsing, and CLI inspectability
GPU execution: All core operations (joins, sorts, aggregations) run on the GPU

Hello World Example

// Declare predicates with types
pred edge(u32, u32).
pred reach(u32, u32).

// Facts: a directed graph
edge(1, 2).
edge(2, 3).
edge(3, 4).

// Rules: transitive closure (reachability)
reach(X, Y) :- edge(X, Y).
reach(X, Z) :- reach(X, Y), edge(Y, Z).

// Query: what nodes can 1 reach?
?- reach(1, N).

Running this program:

xlog run program.xlog

Output:

reach(1, N):
| N |
|---|
| 2 |
| 3 |
| 4 |

Basic Syntax

Program Structure

An XLOG program consists of a sequence of statements. Each statement ends with a period (.).

// Comments start with //
pred node(u32).        // Predicate declaration
node(1).               // Fact
node(2).
reach(X, Y) :- edge(X, Y).   // Rule
?- reach(1, N).        // Query
:- cycle(X).           // Constraint

Statement Types

Statement	Syntax	Description
Predicate declaration	`pred name(types).`	Declares a predicate with typed columns
Fact	`name(values).`	Asserts a ground tuple
Rule	`head :- body.`	Derives new facts from existing ones
Query	`?- atom.`	Specifies output relations
Constraint	`:- body.`	Asserts that body must have no solutions
Function	`func name(params) = expr.`	Defines a user function
Use	`use module.`	Imports predicates from a module
Domain	`domain name: type.`	Declares a domain type
Pragma	`#pragma key = value`	Sets compiler/runtime options

Identifiers

Predicates and atoms: Start with a lowercase letter, followed by alphanumerics or underscores (edge, reach_from, node2)
Variables: Start with an uppercase letter, followed by alphanumerics or underscores (X, Node, Value1)
Anonymous variable: A single underscore (_) matches any value without binding

Data Types

XLOG supports the following scalar types:

Type	Description	Range
`u32`	Unsigned 32-bit integer	0 to 4,294,967,295
`u64`	Unsigned 64-bit integer	0 to 18,446,744,073,709,551,615
`i32`	Signed 32-bit integer	-2,147,483,648 to 2,147,483,647
`i64`	Signed 64-bit integer	-9,223,372,036,854,775,808 to 9,223,372,036,854,775,807
`f32`	32-bit floating point	IEEE 754 single precision
`f64`	64-bit floating point	IEEE 754 double precision
`bool`	Boolean	`true` or `false`
`symbol`	Interned string	Reversible `u32` ID with string table

Literals

// Integers (defaults to i64 in expressions)
42
-17
0

// Floating point (defaults to f64)
3.14
-0.5
1.0

// Boolean
true
false

// String literals (for symbol type)
"hello"
"user_name"

Type Inference

Types are inferred from predicate declarations. All uses of a predicate must be consistent with its declared types.

pred temperature(u32, f64).   // sensor_id: u32, temp: f64

temperature(1, 22.5).         // Correct: u32, f64
temperature(1, 22).           // Error: 22 inferred as i64, not f64
temperature(1, cast(22, f64)). // Correct: explicit cast

Language-Completeness Type Forms

The language-completeness contract extends the type model with finite language-level terms that must lower to typed relation layouts before execution:

Type form	Meaning	Execution status
`domain name: type`	Named alias for an existing scalar type	Existing source form; the contract requires alias preservation in diagnostics and schema metadata
`column: type`	Named predicate column	Named predicate columns are accepted and preserved in schema metadata
`list<T>`	Finite homogeneous list of `T`	Accepted lists lower to helper relations, not CPU term heaps
`term`	Finite ground term value	Only finite, typed terms are accepted
`compound`	Finite compound term with functor and arity	Unsupported recursive or open compounds are rejected
`predref`	Static predicate reference for `maplist` and related meta use	Runtime-variable predicate names are rejected

Unsupported type forms must fail during parsing or semantic analysis before runtime execution starts.

Language Completeness Contract

The language-completeness contract is a language-surface expansion over the core runtime. New syntax is accepted only when it can be normalized into the existing typed AST, RIR, probabilistic IR, optimizer, runtime, WCOJ, and CLI paths.

Execution Responsibilities

Layer	Allowed work
Parser and AST	Recognize source syntax, preserve spans, and represent finite high-level terms
Semantic analysis	Type check, safety check, reject unbounded or dynamic forms, and desugar high-level constructs
Optimizer and planner	Rewrite programs, including magic sets, while preserving output semantics
Runtime, epistemic, and probability engines	Execute accepted relational, epistemic, aggregate, exact, and MC work through production GPU-capable paths
CLI	Orchestrate commands, format diagnostics, and transfer only requested final results

Accepted language-completeness and epistemic features must not execute by constructing an arbitrary CPU Prolog term heap, running dynamic CPU predicate calls, or using a hidden CPU-only fallback for a GPU-claimed path.

Feature Coverage Matrix

Feature	Syntax	Semantics	Example	Unsupported forms	Execution path
Incremental parsing	Statement-level `.xlog` source units with stable spans	Reuse unchanged statement parses and invalidate changed statements plus dependent module state	Editing one rule in a REPL/watch session preserves parse cache for unchanged facts	Cache reuse across changed module dependencies without invalidation	Parser/session cache only; no runtime execution
List syntax and built-ins	`[]`, `[A, B]`, `[H\|T]`, `list<T>`	Finite, typed lists normalize to helper relations	`has_member(X) :- member(X, [1,2,3]).`	Open-ended generators, cyclic lists, heterogeneous lists without a declared finite term type	AST/desugar to typed helper relations and normal runtime joins/aggregates
Safe meta-predicates	`ground`, `var`, `nonvar`, `functor`, `=..`, `findall`, `maplist`	Static inspection and finite collection only	`xs(L) :- findall(X, edge(1, X), L).`	Unrestricted `call/N`, dynamic database mutation, runtime-variable predicate names	Compile-time/static expansion plus typed relational lowering
Deterministic NAF	`not atom(...)`	Closed-world stratified negation over deterministic relations; named variables in the negated atom must be bound by a prior source-order binder	`leaf(X) :- node(X), not edge(X, _).`	Unbound variables in negated atoms, unstratified deterministic cycles	Existing stratification and runtime anti-join paths
Magic sets	`#pragma magic_sets = on\|off\|auto` and compiler configuration override	Bound deterministic recursive queries may be rewritten with adornments and magic predicates	`?- reach(1, Y).` specializes recursive reachability	Unsafe interaction with negation, aggregates, meta/list helpers, mutual recursion, or SIPS cases if equivalence cannot be proven	Source/RIR rewrite before optimizer and WCOJ planning
Probabilistic aggregates	Aggregate heads and aggregate outputs in `query`/`evidence`	Finite aggregate outcomes in exact and MC inference	`query(out_degree(1, 2)).` over probabilistic `edge` facts	Exact aggregate domains over cap, unsupported numeric operator/domain pairs	Exact provenance/PIR or MC sampling plus deterministic aggregate execution
Aggregate lifting	Finite-domain aggregate metadata and caps	Use lifted compact-domain computation when identical to finite exact enumeration	Small count/sum domains avoid naive enumeration	Domain cap exceeded, non-finite domains, unsupported floating tolerance	Probabilistic aggregate planner and exact/MC engines
Approximate inference	`#pragma prob_engine = mc`, samples, seed, confidence, method	MC estimates are reproducible under fixed seed and report uncertainty	`#pragma prob_samples = 10000` with `query(rain).`	Invalid confidence ranges, unsupported methods, hidden default override ambiguity	Existing MC engine with documented source/CLI precedence
Epistemic literals	`know atom(...)`, `possible atom(...)`, `not know atom(...)`, `not possible atom(...)`, finite nested modal chains, `#pragma epistemic_mode = faeel\|g91`	Modal literals are preserved in EIR; the epistemic executor derives candidate worlds from EIR, checks value-level tuple-key membership, normalizes finite nested chains by parity/duality, solves same-name multi-arity by arity-qualified tuple sources, supports determined-head stratification, positive Gelfond 1991 compatibility recursion, stratified negated-modal recursion, and cyclic negated-modal recursion through the `xlog-gpu` GPU-backed WFS plan without the old `xlog_prob` host-WFS solver. This is not a device-resident/no-host-interaction WFS residency claim; host orchestration and metadata convergence reads may still occur.	`accepted() :- know fact().`	Direct raw RIR lowering, genuinely unbounded/untyped modal tuple keys, unsafe unbound negated epistemic variables, CPU-only world-view scans, and genuine modal cycles without a founded order	Parser/AST -> EIR -> epistemic GPU executable plans, reduced ordinary plans, or GPU-backed WFS alternating-fixpoint plans through high-level `xlog run` dispatch
CLI explain	`xlog explain --format text\|json\|dot file.xlog`	Show parse, strata, RIR, optimized RIR, magic-set, WCOJ, and probability sections when applicable	`xlog explain --format json reach.xlog`	Unknown output formats or unavailable sections without a typed reason	CLI orchestration plus compiler/explain APIs
CLI REPL	`xlog repl`	Interactive multiline fact/rule/query session using parser cache	Add facts, then query relation state	GPU execution before a command requests it, unsupported mutation semantics	CLI session cache plus normal compile/run on submitted programs
CLI watch	`xlog watch file.xlog`	Rerun or re-explain changed files with debounce and typed diagnostics	Edit a rule and see updated diagnostics/output	Silent stale cache reuse after file/module change	CLI file watcher plus parser/session cache and normal commands

Diagnostic Contract

Unsupported language-completeness and epistemic forms must report:

the feature area, such as list, meta, naf, magic_sets, prob_aggregate, or epistemic;
the source span when available;
the reason the form is unsafe, unbounded, or not GPU-lowerable;
a remediation, such as adding a positive binder, a finite cap, or a static predicate reference.

Diagnostic examples:

list error at program.xlog:12: unbounded append/3 generation is unsupported; bind at least two list arguments or add a finite split mode.
meta error at program.xlog:8: maplist predicate argument must be a static predref; replace runtime variable P with a named predicate.
negation safety error: unbound variable Y in negated atom edge/2; bind it before not with a positive atom or deterministic is expression, or use '_' for existential positions.
magic_sets declined at program.xlog:21: recursive query crosses an aggregate boundary; run with #pragma magic_sets = off or isolate the aggregate.
prob_aggregate error at program.xlog:17: exact aggregate domain exceeds cap 1024; add a finite cap or use prob_engine = mc.
epistemic error at program.xlog:9: unbounded modal tuple key [H|T] has no finite GPU key-column set; use a fixed-arity typed list or bind the tail to a finite relation.

Source-Audit Status

The historic documentation-reference checkpoint is retained by the language-completeness rows above. Current source accepts the epistemic literals and epistemic_mode pragma listed here and routes accepted epistemic examples through xlog run. The epistemic executor adds EIR-derived candidate enumeration, value-level modal membership, per-tuple-key FAEEL foundedness, ground and variable-keyed epistemic integrity constraints, safe split equivalence, same-name multi-arity disambiguation, finite nested-chain normalization, determined-head stratification, positive Gelfond 1991 compatibility recursion, stratified negated-modal recursion, and cyclic negated-modal recursion through the xlog-gpu GPU-backed WFS plan without the old xlog_prob host-WFS solver. The remaining unsupported epistemic boundaries are direct raw RIR lowering, genuinely unbounded/untyped modal tuple keys, unsafe unbound negated epistemic variables, CPU-only world-view scans, unimplemented cyclic WFS shapes outside the xlog-gpu GPU-backed negated-modal WFS plan, and modal cycles without a founded order.

Predicates and Declarations

Predicate Declarations

Predicate declarations specify the name and column types:

pred edge(u32, u32).           // Two u32 columns
pred weight(u32, u32, f64).    // Three columns: u32, u32, f64
pred label(u32, symbol).       // Node with a string label
pred active(u32).              // Single-column predicate

Visibility

By default, predicates are public and can be imported by other modules. Use private to hide internal predicates:

private pred helper(u32).      // Not visible outside this module
pred public_api(u32).          // Visible to other modules

helper(X) :- internal(X).
public_api(X) :- helper(X).

Domain Declarations

Domain declarations provide semantic naming for types:

domain user_id: u32.
domain temperature: f64.

Facts

Facts are ground atoms (no variables) that assert tuples exist in a relation:

pred parent(symbol, symbol).

parent(alice, bob).
parent(bob, charlie).
parent(charlie, dave).

Facts can also be written on a single line:

edge(1, 2). edge(2, 3). edge(3, 4).

Numeric Facts

pred point(u32, f64, f64).    // id, x, y

point(1, 0.0, 0.0).
point(2, 3.0, 4.0).
point(3, -1.5, 2.7).

Rules

Rules derive new facts from existing ones. A rule has a head (the derived fact) and a body (the conditions).

head(X, Y) :- body_atom1(X, Z), body_atom2(Z, Y).

Simple Rules

// Direct edge implies reachability
reach(X, Y) :- edge(X, Y).

// Grandparent relationship
grandparent(X, Z) :- parent(X, Y), parent(Y, Z).

Recursive Rules

Recursive rules derive facts that depend on themselves:

// Transitive closure
reach(X, Y) :- edge(X, Y).
reach(X, Z) :- reach(X, Y), edge(Y, Z).

// Ancestor relationship
ancestor(X, Y) :- parent(X, Y).
ancestor(X, Z) :- parent(X, Y), ancestor(Y, Z).

XLOG uses semi-naive evaluation for efficient recursive computation, processing only new (delta) tuples in each iteration.

Multi-Atom Bodies

Rules can have multiple atoms in the body, which are implicitly joined:

// Find triangles in a graph
triangle(A, B, C) :- edge(A, B), edge(B, C), edge(C, A), A < B, B < C.

// Star-schema join
sales_by_category(Cat, sum(Amt)) :-
    sale(_, Customer, Product, Amt),
    customer(Customer, Segment),
    product(Product, Cat).

Variable Binding

Variables are bound by appearing in positive atoms. The same variable name in different atoms creates a join condition:

// X appears in both atoms, creating a join on that column
connected(X, Z) :- edge(X, Y), edge(Y, Z).

Queries

Queries specify which relations to output. Use ?- followed by an atom pattern:

// Output all edges
?- edge(X, Y).

// Output reachable nodes from node 1
?- reach(1, N).

// Output all triangles
?- triangle(A, B, C).

Queries can include constants to filter results:

// Only nodes reachable from node 1
?- reach(1, X).

// Only edges starting from node 5
?- edge(5, Y).

Constraints

Constraints assert that a condition must have no solutions. If any tuples satisfy the constraint body, execution fails:

// No self-loops allowed
:- edge(X, X).

// Graph must be acyclic (no node reaches itself)
:- reach(X, X).

// No negative values
:- temperature(_, T), T < 0.0.

Constraints are checked after all derivations complete. If violated, XLOG reports an error.

Variables and Wildcards

Named Variables

Variables start with an uppercase letter and are bound to values when matched:

// X, Y, Z are variables
path(X, Z) :- edge(X, Y), edge(Y, Z).

Anonymous Wildcard

The underscore (_) matches any value without binding. Multiple underscores in a rule are independent:

// Check if a node has any outgoing edge
has_edge(X) :- edge(X, _).

// Check if any path exists (don't care about endpoints)
path_exists() :- path(_, _).

// Multiple wildcards are independent
connected() :- edge(_, X), edge(X, _).

Comparisons

XLOG supports comparison operators in rule bodies:

Operator	Meaning
`=`	Equal
`==`	Equal (alternative syntax)
`!=`	Not equal
`<`	Less than
`<=`	Less than or equal
`>`	Greater than
`>=`	Greater than or equal

Examples

// Filter by value
adult(X) :- person(X, Age), Age >= 18.

// Inequality for self-join
different_pair(X, Y) :- node(X), node(Y), X != Y.

// Ordering for canonical representation
triangle(A, B, C) :- edge(A, B), edge(B, C), edge(C, A), A < B, B < C.

// Equality between variables
same_score(X, Y) :- score(X, S), score(Y, S), X != Y.

Explicit Equality

Use = to explicitly compare variables (in addition to implicit join):

// Explicit equality
equal_pair(X) :- pair(X, Y), X = Y.

// Range filter
in_range(Id) :- value(Id, V), V >= 50, V <= 100.

Arithmetic Expressions

XLOG uses the is keyword for arithmetic computations. The left-hand side must be a fresh (unbound) variable.

Basic Syntax

Result is Expression

Operators

Category	Operators
Binary	`+`, `-`, `*`, `/`, `%` (modulo)
Precedence	`*`, `/`, `%` bind tighter than `+`, `-`
Parentheses	Override precedence with `(...)`

Built-in Functions

Function	Description	Return Type
`abs(X)`	Absolute value	Same as input
`min(X, Y)`	Minimum of two values	Same as inputs
`max(X, Y)`	Maximum of two values	Same as inputs
`pow(X, Y)`	X raised to power Y	`f64`
`cast(X, type)`	Type conversion	Specified type

Examples

pred input(u32, u32).
pred doubled(u32, u32).
pred distance(u32, f64).

input(1, 10).
input(2, 20).

// Double each value
doubled(X, Y) :- input(X, V), Y is V * cast(2, u32).

// Compute distance from origin
distance(Id, D) :-
    point(Id, X, Y),
    D is pow(X * X + Y * Y, 0.5).

// Complex expression with precedence
metrics(X, Result) :-
    value(X, V),
    Result is (V * 3 + 1) / 2.

// Using multiple is expressions
normalized(Id, N) :-
    raw(Id, V),
    AbsV is abs(V),
    Clamped is min(max(AbsV, 0), 100),
    N is cast(Clamped, f64) / 100.0.

Type Casting

Type casting is explicit in XLOG. Use cast(expr, type):

// Cast integer to float for division
ratio(X, R) :-
    count(X, N),
    total(T),
    R is cast(N, f64) / cast(T, f64).

// Cast for type compatibility
doubled(X, Y) :- input(X, V), Y is V * cast(2, u32).

Division and Error Handling

Condition	Integer Behavior	Float Behavior
Division by zero	Returns `INT64_MAX`	Returns `NaN` or `Inf`
Overflow	Wraps (standard semantics)	IEEE 754 behavior

To avoid division by zero errors, filter explicitly:

safe_ratio(X, Y, R) :-
    numerator(X), denominator(Y),
    Y != 0,
    R is X / Y.

Negation

XLOG supports deterministic negation as failure using the not keyword. In deterministic programs, not atom(...) is closed-world, stratified negation. This is distinct from probabilistic nonmonotone negation, where exact inference may use Well-Founded Semantics (WFS) for accepted probabilistic programs.

Syntax

not atom(args)

Examples

// Nodes with no outgoing edges
leaf(X) :- node(X), not edge(X, _).

// Nodes with no incoming edges
root(X) :- node(X), not edge(_, X).

// Isolated nodes (no edges at all)
isolated(X) :- node(X), not edge(X, _), not edge(_, X).

// Childless people
childless(X) :- person(X), not parent(X, _).

// Unreachable nodes
unreachable(X) :- node(X), not reach(start, X).

Stratification Requirements

Negation must be stratifiable: there cannot be a cycle where a predicate depends on its own negation. Valid (stratifiable):

has_child(X) :- parent(X, _).
childless(X) :- person(X), not has_child(X).

Invalid (unstratifiable):

// ERROR: p depends on not p
p(X) :- q(X), not p(X).

XLOG detects unstratifiable deterministic programs at compile time and reports a negation safety error. Low-level stratification analysis still reports the underlying dependency cycle for callers that use it directly.

Domain Safety

Named variables in negated atoms must be bound by a prior source-order binder in the same rule body. Positive atoms bind their named variables, and a deterministic is expression binds its target after the expression appears. Source order matters: a later positive atom does not make an earlier negated atom safe. Use _ for existential positions inside negated atoms.

// Valid: X is bound by node(X) before used in not edge(X, _)
leaf(X) :- node(X), not edge(X, _).

// Invalid: Y is not bound by a prior source-order binder
// bad(X) :- node(X), not edge(X, Y).  // ERROR

// Invalid: X is bound too late
// bad(X) :- not edge(X, _), node(X).  // ERROR

Aggregations

Aggregations compute summary values over groups of tuples.

Supported Aggregates

Aggregate	Description	Input Types	Output Type
`count(X)`	Count of values	Any	`u64`
`sum(X)`	Sum of values	`u32`	`u64`
`min(X)`	Minimum value	`u32`	`u32`
`max(X)`	Maximum value	`u32`	`u32`
`logsumexp(X)`	Log-sum-exp (numerically stable)	`f64`	`f64`

Syntax

Aggregates appear in the rule head. Variables not in the aggregate form the grouping key:

head(GroupKeys, aggregate(AggVar)) :- body(GroupKeys, AggVar, ...).

Examples

pred edge(u32, u32).
pred out_degree(u32, u32).

edge(1, 2). edge(1, 3). edge(2, 4).

// Count outgoing edges per node
out_degree(X, count(Y)) :- edge(X, Y).

// Result: out_degree(1, 2), out_degree(2, 1)

Multi-Key Aggregation

pred txn(u32, u32, u32).    // user, day, amount
pred daily_total(u32, u32, u64).

txn(1, 1, 10). txn(1, 1, 5). txn(1, 2, 7). txn(2, 1, 3).

// Sum amount per (user, day)
daily_total(User, Day, sum(Amount)) :- txn(User, Day, Amount).

// Result: daily_total(1, 1, 15), daily_total(1, 2, 7), daily_total(2, 1, 3)

Multiple Aggregates

pred latency(u32, u32).     // service_id, latency_ms
pred stats(u32, u32, u32).  // service_id, min_latency, max_latency

latency(1, 100). latency(1, 250). latency(1, 150).
latency(2, 7). latency(2, 3). latency(2, 5).

// Min and max per service
stats(Service, min(L), max(L)) :- latency(Service, L).

// Result: stats(1, 100, 250), stats(2, 3, 7)

Computing Averages

XLOG does not have a built-in avg aggregate. Compute it using sum and count:

pred txn(u32, u32).         // user_id, amount
pred total(u32, u64).
pred cnt(u32, u32).
pred avg(u32, f64).

txn(1, 10). txn(1, 5). txn(1, 7).
txn(2, 3). txn(2, 9).

total(User, sum(Amount)) :- txn(User, Amount).
cnt(User, count(Amount)) :- txn(User, Amount).

avg(User, A) :-
    total(User, Total),
    cnt(User, N),
    A is cast(Total, f64) / cast(N, f64).

Log-Sum-Exp Aggregation

For probabilistic and numerical applications, logsumexp computes log(sum(exp(values))) in a numerically stable way:

pred obs(u32, f64).         // group_id, log_value
pred score(u32, f64).

obs(1, 0.0). obs(1, 1.0). obs(1, 2.0).
obs(2, 0.0). obs(2, 0.0).

score(X, logsumexp(Y)) :- obs(X, Y).

// score(1) = log(exp(0) + exp(1) + exp(2)) = log(1 + e + e^2) ≈ 2.407
// score(2) = log(exp(0) + exp(0)) = log(2) ≈ 0.693

Lists

The language-completeness contract defines finite list syntax and list built-ins. Lists are accepted only when they are finite and typed; accepted programs lower to relation layouts and normal GPU-capable execution paths. Current finite-list implementation status: scalar, symbol, nested finite list, and finite meta term IDs are normalized to u64 list identifiers plus __xlog_list_* helper relations. list<T> predicate columns lower to scalar list-id columns while helper relations carry length, item, cons, append, sort, msort, and set facts. The current implementation accepts finite literals, declared list<T> columns, safe [Head | Tail] patterns in declared list columns, and the built-ins below when their list argument has a finite literal or a known list<T> type.

Syntax

[]                 // empty list
[A, B, C]          // finite list literal
[Head | Tail]      // finite cons pattern when Tail is bound to a finite list
list<u32>          // homogeneous finite list type

Built-Ins

Built-in	Contract
`is_list(X)`	Succeeds when `X` is a finite list value
`member(X, L)`	Enumerates or checks finite membership
`memberchk(X, L)`	Deterministic membership check
`length(L, N)`	Computes the finite list length
`nth(N, L, X)`	Binds/checks zero-based element `N`
`append(A, B, C)`	Concatenates finite lists when at least two sides are bound enough to avoid generation
`sort(L, S)`	Sorts finite list values with duplicate removal
`msort(L, S)`	Sorts finite list values preserving duplicates
`list_to_set(L, S)`	Removes duplicates while producing a finite normalized list

Pair helpers may be added as typed helpers when they lower to finite relation columns. Unsupported helpers must be rejected with a typed diagnostic rather than simulated by a CPU term evaluator. Current implementation limits:

append(A, B, C) accepts finite first and second list literals in this node; split generation such as append(A, B, [1,2,3]) is rejected as unbounded;
sort, msort, and list_to_set require a finite input literal in this node;
term, compound, and predref list elements lower to finite u64 meta term IDs when they appear in declared list<term>, list<compound>, or list<predref> contexts.

Examples

pred seed(u32).
pred selected(u32).

selected(X) :- seed(_), member(X, [1, 2, 3]).

pred path(symbol, list<symbol>).
pred path_len(symbol, u32).

path_len(Name, N) :- path(Name, Steps), length(Steps, N).

Unsupported Forms

The following forms are outside the finite-list contract:

unbounded list generation, such as asking append(A, B, [1,2,3]) to enumerate every split unless a finite split mode is explicitly implemented;
cyclic lists;
heterogeneous lists unless represented through a declared finite term domain;
list evaluation that requires an arbitrary CPU Prolog term heap.

Safe Meta-Predicates

Safe meta-predicates provide finite term inspection and static predicate mapping. They do not introduce an unrestricted Prolog dynamic database or unrestricted call/N. Current safe-meta implementation status: accepted safe meta forms normalize before stratification and lowering into ordinary helper relations such as __xlog_meta_functor, __xlog_meta_univ, __xlog_meta_findall_*, and __xlog_meta_maplist_*. Finite term, compound, and predref predicate columns lower to u64 term IDs; compound metadata and univ parts are stored in typed helper relations. findall and maplist currently accept finite source facts and finite list literals only; derived-goal collection and non-literal maplist inputs are explicitly rejected until an aggregate-backed collection path lands.

Supported Meta-Predicates

Predicate	Contract
`ground(Term)`	True when the term is fully ground after static analysis or finite binding
`var(Term)`	True only at the supported static/runtime boundary for unbound variables
`nonvar(Term)`	True when `Term` is known not to be a variable
`functor(Term, Name, Arity)`	Inspects or checks a finite compound term’s functor and arity
`Term =.. Parts`	Converts between finite compound terms and a finite `[Functor, Args...]` list
`findall(Template, Goal, List)`	Collects finite goal results into a normalized list relation; empty result succeeds with `[]`
`maplist(PredRef, List)`	Statically expands a unary predicate reference over a finite list
`maplist(PredRef, ListA, ListB)`	Statically expands a binary predicate reference over aligned finite lists

Examples

pred edge(u32, u32).
pred fanout(u32, list<u32>).

fanout(Ys) :- findall(Y, edge(1, Y), Ys).

pred positive(u32).
pred all_positive(list<u32>).

all_positive(1) :- maplist(positive, [1, 2, 3]).

Unsupported Forms

runtime-variable predicate names in maplist or any future call-like form;
assert, retract, dynamic database mutation, or IO predicates;
findall over derived goals or goals with variables that are neither bound before findall nor collected by the template;
non-literal maplist inputs in the current safe-meta subset;
constructing recursive or open compound terms with =..;
higher-arity maplist unless explicitly implemented and tested.

Magic Sets

Magic-set rewriting specializes bound deterministic recursive queries by adding derived magic predicates and adorned rules before optimization. The accepted accepted magic-set subset is a source-level rewrite over positive recursive rules that can be proven query-equivalent under the supported left-to-right SIPS.

Configuration

#pragma magic_sets = auto
#pragma magic_sets = on
#pragma magic_sets = off

auto lets the compiler apply the rewrite only when it can prove that the transformed program preserves query output. on requests the rewrite and fails with a typed magic_sets error if the compiler cannot safely apply it. off disables the rewrite.

Example

pred edge(u32, u32).
pred reach(u32, u32).

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

?- reach(1, Y).

The bound query argument 1 may seed a magic predicate so recursive evaluation does not materialize unreachable source components. xlog explain must show the adornment, generated magic predicates, and any declined-rewrite reason. The compiler currently emits helper predicates such as __xlog_magic_reach_bf, where b marks a bound argument and f marks a free argument. Accepted rules continue through the normal AST, stratification, lowering, optimizer, WCOJ, and runtime paths.

Supported Subset

deterministic programs with ?- queries over recursive predicates;
at least one scalar constant in the queried recursive atom;
positive recursive rules over the same head predicate;
source-order binding propagation through prior positive body atoms;
auto, on, and off source pragmas.

Declined Forms

auto leaves the program unchanged and records a decline reason. on fails with a typed diagnostic for:

unbound recursive calls under the supported SIPS;
rules with negation, aggregation, comparison, is, or unnormalized univ in the recursive target;
recursive rules that cross language-completeness list/meta helper predicates;
mutual-recursive SCCs in the current subset;
probabilistic profiles, which remain governed by the probabilistic engine.

Unsupported Forms

Magic-set rewriting must decline or fail before execution when negation, aggregates, list/meta constructs, or probabilistic rules would make equivalence uncertain. It must not create a runtime side engine.

User-Defined Functions

XLOG supports user-defined functions for reusable calculations.

Basic Functions

func double(X) = X * 2.
func add(X, Y) = X + Y.
func square(X) = X * X.

Conditional Functions

Use if-then-else for conditional logic:

func abs(X) = if X < 0 then 0 - X else X.

func clamp(X, Lo, Hi) =
    if X < Lo then Lo
    else if X > Hi then Hi
    else X.

func sign(X) =
    if X < 0 then -1
    else if X > 0 then 1
    else 0.

Recursive Functions

Functions can be recursive but must have a base case:

func factorial(N) = if N <= 1 then 1 else N * factorial(N - 1).

func fib(N) = if N <= 1 then N else fib(N - 1) + fib(N - 2).

func gcd(A, B) = if B = 0 then A else gcd(B, A % B).

Using Functions in Rules

Functions can be called in rule bodies using the is expression or direct call syntax:

// Using 'is' expression
pred doubled_value(u32, u32).
doubled_value(X, Y) :- input(X, V), Y is double(V).

// Direct call syntax (function result assigned to variable)
pred result(u32, u32).
result(X, Y) :- input(X, V), double(V) = Y.

Type Annotations

Optional type annotations for documentation and checking:

func add(X: f64, Y: f64) -> f64 = X + Y.
func celsius_to_fahrenheit(C: f64) -> f64 = C * 1.8 + 32.0.

Private Functions

Functions can be marked private:

private func helper(X) = X * X + 1.
func public_calc(X) = helper(X) * 2.

Modules

XLOG supports organizing code into modules for reusability and encapsulation.

Creating Modules

A module is a .xlog file. The filename (without extension) becomes the module name:

// File: graph.xlog
pred edge(u32, u32).
edge(1, 2).
edge(2, 3).

pred reach(u32, u32).
reach(A, B) :- edge(A, B).
reach(A, C) :- edge(A, B), reach(B, C).

Importing Modules

Use the use statement to import predicates from modules:

// Import all public predicates
use graph.

// Import specific predicates
use graph::{edge, reach}.

// Import from nested module path
use utils/math::{abs, clamp}.
use data/graph/algorithms::{shortest_path}.

Module Paths

Module paths use / as the separator:

project/
  main.xlog
  graph.xlog
  utils/
    math.xlog
    string.xlog

// In main.xl
use graph.
use utils/math.

Visibility and Encapsulation

Predicates and functions are public by default. Use private to hide implementation details:

// File: graph.xlog

// Public API
pred edge(u32, u32).
pred reach(u32, u32).

// Private helper (not visible outside this module)
private pred internal_cache(u32, u32).

reach(A, B) :- edge(A, B).
reach(A, C) :- internal_cache(A, C).  // Uses private helper
internal_cache(A, C) :- edge(A, B), reach(B, C).

Private predicates cannot be imported by other modules:

// ERROR: internal_cache is private
use graph::{internal_cache}.

Symbols

Symbols are interned strings, represented internally as integers for efficient comparison and storage.

Declaring Symbol Types

pred color(symbol).
pred person(symbol, u32).   // name: symbol, age: u32

color(red).
color(green).
color(blue).

person(alice, 30).
person(bob, 25).

Symbol Literals

Symbol literals are written as identifiers (lowercase) or as string literals:

// As identifiers
color(red).
color(green).

// As string literals (for names with special characters)
city("New York").
city("Los Angeles").

Querying Symbols

Symbols are displayed as their original string values in query output:

pred status(symbol).
status(active).
status(pending).
status(completed).

?- status(S).

Output:

status(S):
| S         |
|-----------|
| active    |
| pending   |
| completed |

Symbol Comparison

Symbols can be compared for equality:

same_status(X, Y) :- item(X, S), item(Y, S), X != Y.

Reversible Symbols

Symbols are reversible: the original string value is preserved and displayed in query output. Symbols are stored internally as u32 IDs with a bidirectional mapping to strings.

pred task(symbol, symbol).
task(project_alpha, alice).
task(project_beta, bob).

?- task(Project, Owner).

Output displays original string values:

| Project       | Owner |
|---------------|-------|
| project_alpha | alice |
| project_beta  | bob   |

Probabilistic Logic

XLOG supports probabilistic Datalog for reasoning under uncertainty.

Probabilistic Facts

Probabilistic facts are Bernoulli random variables with a specified probability:

3::rain.           // P(rain) = 0.3
7::sprinkler.      // P(sprinkler) = 0.7
5::edge(1, 2).     // P(edge(1,2)) = 0.5

Annotated Disjunctions

Annotated disjunctions represent categorical distributions (mutually exclusive outcomes):

// Coin flip: heads (60%) or tails (40%)
0.6::coin(heads); 0.4::coin(tails).

// Die roll
0.167::die(1); 0.167::die(2); 0.167::die(3);
0.167::die(4); 0.167::die(5); 0.166::die(6).

If probabilities sum to less than 1, the remaining mass represents an implicit “none” outcome.

Deterministic Rules with Probabilistic Facts

Rules can derive facts from probabilistic facts:

0.3::rain.
0.2::sprinkler.

// Deterministic derivation from probabilistic facts
wet :- rain.
wet :- sprinkler.

Evidence

Evidence constrains the probabilistic model to worlds consistent with observations:

evidence(wet, true).      // Condition on wet being true
evidence(sprinkler, false). // Condition on sprinkler being false

Probabilistic Queries

Use query to compute the probability of an atom:

query(rain).        // Compute P(rain | evidence)
query(wet).         // Compute P(wet | evidence)

Complete Probabilistic Example

// Probabilistic facts
0.7::rain.
0.2::sprinkler.

// Deterministic rules
wet :- rain.
wet :- sprinkler.

// Evidence: we observed that wet is true
evidence(wet, true).

// Queries: compute posterior probabilities
query(rain).
query(sprinkler).

Running with exact inference:

xlog prob weather.xlog --prob-engine exact_ddnnf

Output:

query(rain):      P = 0.875
query(sprinkler): P = 0.25

Inference Engines

XLOG supports two inference engines:

Engine	Flag	Description
Exact	`--prob-engine exact_ddnnf`	Knowledge compilation via Decision-DNNF; exact probabilities
Monte Carlo	`--prob-engine mc`	Sampling-based; approximate with confidence intervals

Exact inference supports:

Stratified deterministic negation: Automatic layer detection and two-valued evaluation for deterministic not atom programs
Probabilistic non-monotone negation: Well-Founded Semantics (WFS) for accepted cyclic probabilistic programs
Finite probabilistic aggregates: count, sum, min, max, and logsumexp aggregate outputs compiled through provenance/PIR when the exact finite domain cap is respected
Gradients: Correct gradient flow through negated literals

Probabilistic aggregates in the language-completeness contract: finite count, sum, min, max, and logsumexp aggregate programs are supported for exact and MC inference in the finite probabilistic-aggregate subset. Exact mode enumerates finite aggregate outcomes into provenance/PIR formulas, so query and evidence may reference aggregate output tuples. Exact enumeration is capped at 16 uncertain contributing rows per group; cap excess fails with a typed prob_aggregate error that recommends MC or reducing the finite domain. Monte Carlo supports probabilistic rules and non-monotone recursion. The production MC path is the GPU-resident megakernel engine, which rejects negation, aggregates, and other unbounded constructs with a typed ResidentRejection. Programs in that fragment (including non-monotone recursion and language-completeness probabilistic aggregates under MC) require an explicit opt-in to the labeled CPU oracle — --allow-cpu-oracle on the CLI, allow_cpu_oracle=True in Python, McEvalConfig::allow_cpu_oracle_fallback in Rust — and their results carry mc_engine = "cpu-oracle". Without the opt-in, such programs fail closed with the typed rejection (corrected 2026-06-10; previously this fallback was silent and unlabeled):

xlog prob program.xlog --prob-engine mc --samples 10000 --seed 42
# resident-rejected fragment (negation / aggregates) needs the explicit oracle:
xlog prob program.xlog --prob-engine mc --samples 10000 --allow-cpu-oracle

Probabilistic Aggregates

Finite probabilistic aggregate programs may query or condition on aggregate outputs:

0.5::edge(1, 2).
0.5::edge(1, 3).

out_degree(X, count(Y)) :- edge(X, Y).
query(out_degree(1, 2)).

Exact mode compiles each supported finite aggregate outcome into a Boolean PIR formula over contributing row-presence formulas. Empty probabilistic groups do not materialize count(..., 0) tuples. MC mode samples worlds on the GPU and executes the shared deterministic aggregate path for each accepted sample batch.

Aggregate Lifting

Small-domain aggregate lifting is permitted only when the lifted computation is semantically identical to finite exact enumeration. Explain output must report the detected finite domain, cap, operator, and whether lifting fired, declined, or fell back to supported exact enumeration. In the aggregate-lifting subset, finite probabilistic count aggregate heads use exact cardinality dynamic programming when every aggregate expression in the head is count(...). The lift constructs formulas for exactly k contributing rows over the same row-presence formulas used by finite enumeration, so it does not change exact semantics. The count lift accepts up to 64 uncertain rows per group; larger count domains fail closed with a typed agg_lift error. sum, min, max, and logsumexp remain on exact finite outcome enumeration in this subset. Their explain entries report fallback_exact_enumeration with a per-operator rationale and continue to use the 16-uncertain-row exact aggregate cap. xlog explain --format json emits an aggregate_lifting array containing the predicate, group key, operator, finite-domain source, domain size, cap, status, reason, naive outcome count, and dynamic-programming state count.

Monte Carlo Sampling Methods

The Monte Carlo engine supports two sampling methods:

Method	Description
`Rejection`	Sample from the prior and discard worlds where evidence is not satisfied.
`EvidenceClamping`	Force evidence variables directly in the CUDA sampler when the evidence is forceable at the probabilistic-fact / positive-AD level.

Evidence clamping avoids wasted samples when rejection acceptance rates are low. If evidence is derived, deterministic, or otherwise not directly forceable, XLOG falls back to rejection sampling.

Negation in Probabilistic Programs

Probabilistic exact inference supports both stratified probabilistic negation and accepted non-monotone WFS profiles:

// Stratified negation (layered evaluation)
0.3::rain.
dry :- not rain.
query(dry).  // P(dry) = 0.7

// Non-monotone negation (WFS)
0.5::bias.
p :- bias, not q.
q :- not p.
query(p).  // WFS: atoms in cycle may be undefined

Probabilistic Recursion

Probabilistic facts can be used with recursive rules:

0.5::edge(1, 2).
0.5::edge(2, 3).

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

query(reach(1, 2)).
query(reach(1, 3)).

Pragma for Engine Selection

The inference engine can be specified in the source file:

// Non-monotone negation works with exact inference (uses WFS)
#pragma prob_engine = exact_ddnnf

0.5::flip.
p :- flip.
q :- not p.
p :- not q.

query(p).  // WFS: p is undefined in worlds where bias is false

For approximate inference with confidence intervals:

#pragma prob_engine = mc
#pragma prob_samples = 10000

0.5::flip.
p :- flip.
q :- not p.

query(p).  // P(p) ≈ 0.5 ± CI

Epistemic Logic

Epistemic logic is part of the accepted source surface. Epistemic logic adds modal body literals for bounded knowledge and possibility reasoning. Modal literals are valid in rule bodies and use the same atom syntax as ordinary predicates.

Form	Meaning
`know atom(...)`	The atom must hold in every accepted world/model.
`possible atom(...)`	The atom must hold in at least one accepted world/model.
`not know atom(...)`	The atom is not known in every accepted world/model.
`not possible atom(...)`	The atom is absent from every accepted world/model.

Finite nested modal chains such as know possible fact(), not know possible fact(), and know not possible fact() are accepted program forms. The parser normalizes them to a single epistemic literal by the semantic parity/duality rules: the operator adjacent to the atom determines the modal operator, while leading/interior/atom-adjacent not tokens dualize or negate the resulting literal according to their position.

Epistemic Mode Pragma

#pragma epistemic_mode = faeel
#pragma epistemic_mode = g91

faeel is the default epistemic mode when no pragma is present. g91 is an explicit compatibility mode for programs that need Gelfond 1991 possibility behavior.

Runtime Boundary

Accepted epistemic programs enter EIR through xlog_logic::build_eir and run through the high-level xlog run / xlog_gpu::LogicProgram dispatch path. That path lowers accepted programs into epistemic GPU executable plans. Direct ordinary RIR lowering of raw epistemic body literals remains a rejection boundary and must report UnsupportedEpistemicConstruct.

Examples

FAEEL default knowledge:

pred fact().
pred accepted().

fact().

accepted() :- know fact().

Gelfond 1991 compatibility:

#pragma epistemic_mode = g91

pred fact().
pred accepted().

fact().

accepted() :- possible fact().

Independent split components:

pred left_fact().
pred right_fact().
pred left().
pred right().

left_fact().
right_fact().

left() :- know left_fact().
right() :- possible right_fact().

Run the shipped pilots:

xlog run examples/epistemic/03-faeel-default.xlog
xlog run examples/epistemic/02-g91-compatibility.xlog
xlog run examples/epistemic/05-splitting.xlog

Approximate Inference

Approximate inference is the source and CLI contract for Monte Carlo probabilistic reasoning. It must be reproducible under a fixed seed and must report uncertainty, sample counts, evidence handling, and sampling method.

Source Pragmas

#pragma prob_engine = mc
#pragma prob_samples = 10000
#pragma prob_seed = 42
#pragma prob_confidence = 0.95
#pragma prob_method = evidence_clamping

Pragma	Meaning
`prob_samples`	Number of MC samples
`prob_seed`	Fixed random seed; identical input plus seed must replay identical counts
`prob_confidence`	Confidence level for reported intervals
`prob_method`	Sampling method, such as `rejection` or `evidence_clamping`
`prob_max_nonmonotone_iterations`	Bound for nonmonotone WFS/MC iteration where applicable

CLI flags override source pragmas when both are provided; the effective configuration must be visible in CLI output and explain JSON. In the approximate-inference subset, xlog prob uses source #pragma prob_engine = mc when --prob-engine is not supplied. CLI flags override source pragmas field-by-field: --samples, --seed, --confidence, --prob-method, and --prob-max-nonmonotone-iterations replace only their matching source values. --output json emits a machine-readable MC report with the same probability, standard-error, confidence-interval, sample-count, evidence-count, seed, confidence, and sampling-method fields as the pretty/csv batch output.

Output Contract

Approximate output formats must include:

probability estimate;
standard error;
confidence interval low/high;
sample count;
evidence count or acceptance/clamping count;
seed and method.

Invalid confidence ranges, unsupported methods, or ambiguous precedence must fail before sampling begins.

Neural Predicates

Neural predicate declarations embed a neural network directly into an XLOG program as a first-class predicate.

Declaration Forms

Classification (nn/4):

nn(network_name, [InputVar1, InputVar2, ...], OutputVar, [label1, label2, ...]) :: atom.

Embedding mode (nn/3):

nn(network_name, [InputVar], OutputVar) :: atom.

Arguments

Position	Meaning
`network_name`	Python-side registration name
`[InputVar, ...]`	Input variables passed to the forward pass
`OutputVar`	Predicted label or dense embedding output
`[label1, ...]`	Label set for `nn/4` declarations
`atom`	Predicate template instantiated by the declaration

Lowering

For nn/4, the network output is treated as a label distribution and lowered to probabilistic facts that enter the inference pipeline. For nn/3, the network output is a dense tensor bound into the program and used through the embedding APIs.

Example: MNIST Classification

nn(mnist_net, [X], Y, [0,1,2,3,4,5,6,7,8,9]) :: digit(X, Y).
addition(X, Y, Z) :- digit(X, LeftDigit), digit(Y, RightDigit), Z is LeftDigit + RightDigit.

Python side:

program = pyxlog.Program.compile(source)
net = MnistClassifier().cuda()
optimizer = torch.optim.Adam(net.parameters(), lr=1e-3)
program.register_network("mnist_net", net, optimizer)

Example: Embedding Mode

nn(entity_embed, [X], E) :: embed(X, E).

Python side:

embedding = torch.nn.Embedding(100, 64).cuda()
program.register_embedding("entity_embed", embedding, trainable=True)

Cross-Registration Validation

Classification declarations (nn/4) require register_network(). Embedding declarations (nn/3) require register_embedding(). Reusing the same name across both forms is rejected.

Learnable Rules

Learnable rules are the source-level surface for differentiable ILP. A rule is gated by a named mask tensor:

learnable(W_reach) :: reach(X, Y) :- bL(X, Z), bR(Z, Y).

During training, candidate rules are softly weighted; at convergence, argmax selects the winning rule and the learned artifact serializes the concrete program.

Training API

from pyxlog.ilp import train_only, train_and_promote, TrainConfig

result = train_only(source, "W_reach", positive_examples, negative_examples, TrainConfig(...))
promotion = train_and_promote(source, "W_reach", positive_examples, negative_examples, TrainConfig(...))

Multiple Learnable Rules

learnable(W_gp)  :: grandparent(X, Y) :- bL(X, Z), bR(Z, Y).
learnable(W_col) :: colleague(X, Y)   :- bL(X, Z), bR(Y, Z).

Cross-References

Term Embeddings

Term embeddings associate dense vectors with discrete logic terms.

`register_embedding()`

program = pyxlog.Program.compile(source)
embedding = torch.nn.Embedding(100, 64).cuda()
program.register_embedding("entity_embed", embedding, trainable=True)

weights = torch.randn(100, 64).cuda()
program.register_embedding("pretrained_emb", weights, trainable=False)

`forward_embedding()`

vectors = program.forward_embedding("entity_embed", [0, 5, 12])

The returned tensor stays on the same device as the registered embedding. For a trainable nn.Embedding, gradients remain attached; for frozen tensors they do not. Current scope: explicit training-side embedding registration and batched lookup are supported. Rule-level embedding inference remains deferred.

GPU ILP Configuration

The GPU-resident ILP path exposes runtime configuration and telemetry through Python.

`coo_chunk_budget`

Controls the per-chunk temporary allocation ceiling used during sparse COO construction on GPU:

trainer.set_coo_chunk_budget(256 * 1024 * 1024)

The older coo_memory_cap naming is deprecated.

`host_transfer_stats()`

Training APIs expose transfer telemetry so strict zero device-to-host workflows can verify that the hot path stayed device-resident:

stats = trainer.host_transfer_stats()
trainer.reset_host_transfer_stats()

Pragmas and Directives

Pragmas configure compiler and runtime behavior. The current source grammar accepts prob_engine, prob_cache, epistemic_mode, max_recursion_depth, magic_sets, and the MC configuration pragmas below. The language-completeness rows remain contract-backed where they depend on finite-list, safe-meta, magic-set, probability, and CLI nodes; the epistemic mode pragma is accepted for the epistemic solver surface.

Syntax

#pragma key = value

Available Pragmas

Pragma	Values	Description
`prob_engine`	`exact_ddnnf`, `mc`	Select probabilistic inference engine
`prob_cache`	`on`, `off`	Enable/disable probability caching
`epistemic_mode`	`faeel`, `g91`	Select FAEEL default or Gelfond 1991 compatibility epistemic semantics
`max_recursion_depth`	integer	Maximum recursion iterations
`magic_sets`	`auto`, `on`, `off`	Control bound-recursive magic-set rewriting
`prob_samples`	integer	Monte Carlo sample count
`prob_seed`	integer	Monte Carlo random seed
`prob_confidence`	float in `(0, 1)`	Monte Carlo confidence level
`prob_method`	`rejection`, `evidence_clamping`	Monte Carlo sampling method
`prob_max_nonmonotone_iterations`	integer	Bound nonmonotone probabilistic iteration where applicable

Examples

// Use Monte Carlo inference
#pragma prob_engine = mc

// Disable probability caching
#pragma prob_cache = off

// Select epistemic compatibility semantics
#pragma epistemic_mode = g91

// Limit recursion depth
#pragma max_recursion_depth = 100

// Let the compiler specialize safe bound recursive queries
#pragma magic_sets = auto

// Configure approximate inference
#pragma prob_samples = 10000
#pragma prob_seed = 42
#pragma prob_confidence = 0.95
#pragma prob_method = evidence_clamping

CLI Developer Experience

Developer-experience commands make the language inspectable and interactive without changing the runtime execution contract.

`xlog explain`

xlog explain [--format text|json|dot] <FILE>

The CLI explain subset reports deterministic parse, AST, stratification, RIR, optimizer, WCOJ, magic-set, and probability sections without requiring GPU execution. JSON output is deterministic for fixed input. Full explain output must include deterministic sections when applicable:

parse and AST summary;
predicate declarations and schema metadata;
stratification and negation safety;
RIR and optimized RIR summaries;
magic-set adornments, generated predicates, and declined reasons;
WCOJ eligibility and selected execution path;
probabilistic engine, aggregate, and approximate-inference sections for probabilistic programs.

JSON output must be deterministic for fixed input. Unknown formats are rejected before compilation.

Incremental Parsing

xlog_logic::ParserSession is the shared parser cache for explain, REPL, and watch workflows. It splits .xlog source into statement units, records stable text hashes and byte/line spans, and reparses only changed statements through the production parser. Cache statistics report hits, misses, invalidations, module invalidations, statement count, and an estimated statement-unit speedup. Module invalidation removes the changed module and cached sources that import that module name. Incremental parse diagnostics include the original line/column and byte span before forwarding the underlying parser error.

`xlog repl`

xlog repl [--module-path DIR[:DIR...]]

The REPL accepts multiline facts, rules, declarations, pragmas, and queries. It shares the incremental parser/session cache and does not require GPU access until the user submits a command that needs execution. The CLI smoke implementation reads a multiline stdin session, preserves the accumulated parser state, and reports statement/rule/query counts.

`xlog watch`

xlog watch [--debounce-ms N] [--explain] <FILE>

Watch mode reruns compilation, execution, or explanation after file changes. It must debounce rapid writes, invalidate changed statements and dependent module state, and display typed diagnostics without reusing stale parse results. The CLI smoke implementation supports --once, --explain, and --debounce-ms, using the shared parser session before any execution path. Unsupported REPL/watch mutation semantics, such as dynamic assert or retract, remain outside the language.

Float Predicates and IEEE 754 Semantics

XLOG uses hybrid semantics for floating-point comparisons to handle special values (NaN, Infinity, signed zero) correctly.

Comparison Semantics

Operator	Semantics	NaN Behavior
`=`, `!=`	IEEE 754 equality	`NaN = NaN` is FALSE
`<`, `<=`, `>`, `>=`	Total ordering	NaN is comparable

Total Ordering

For ordering comparisons, XLOG uses a total ordering consistent with Rust’s f64::total_cmp:

-NaN < -Inf < ... < -0.0 < +0.0 < ... < +Inf < +NaN

This means:

NaN values are at the extremes (negative NaN is smallest, positive NaN is largest)
-0.0 and +0.0 are distinguishable in ordering (unlike IEEE equality)
All values are comparable (no undefined ordering)

Filtering NaN Values

Since NaN != NaN under IEEE 754, use equality to filter out NaN:

// V = V is true only for non-NaN values
valid(Id, V) :- data(Id, V), V = V.

Detecting Special Values

Use ordering to detect special values:

// NaN is greater than any finite value
is_nan(Id, V) :- data(Id, V), V > 1e308.

// Infinity detection
is_infinite(Id, V) :- data(Id, V), V > 1e300, V = V.

// Finite values only
is_finite(Id, V) :- data(Id, V), V > -1e308, V < 1e308.

Example: Data Cleaning Pipeline

pred raw(u32, f64).
pred valid(u32, f64).
pred anomaly(u32, f64).

raw(1, 22.5).
raw(2, 0.0).        // Will compute NaN from 0/0
raw(3, 28.3).

// Filter valid readings (not NaN)
valid(Id, V) :- raw(Id, V), V = V.

// Detect anomalies (NaN or extreme values)
anomaly(Id, V) :- raw(Id, V), V > 1000.0.
anomaly(Id, V) :- raw(Id, V), V < -1000.0.

Comments

XLOG supports single-line comments:

// This is a comment
pred edge(u32, u32).  // Inline comment

// Multi-line explanation
// spanning several lines
// before a complex rule
reach(X, Z) :- reach(X, Y), edge(Y, Z).

Block comments (/* ... */) are not supported.

Complete Grammar Reference

The following is a summary of the current XLOG grammar plus the language-completeness extensions and epistemic source surface in PEG-style notation.

Lexical Elements

WHITESPACE = _{ " " | "\t" | "\r" | "\n" }
COMMENT = _{ "//" ~ (!"\n" ~ ANY)* }

ident = @{ ASCII_ALPHA_LOWER ~ (ASCII_ALPHANUMERIC | "_")* }
variable = @{ ASCII_ALPHA_UPPER ~ (ASCII_ALPHANUMERIC | "_")* }
anonymous = @{ "_" }

integer = @{ "-"? ~ ASCII_DIGIT+ }
float_num = @{ "-"? ~ ASCII_DIGIT+ ~ "." ~ ASCII_DIGIT+ }
string_lit = @{ "\"" ~ (!"\"" ~ ANY)* ~ "\"" }
bool_lit = { "true" | "false" }

Types

type_spec = { "u32" | "u64" | "i32" | "i64" | "f32" | "f64" | "bool" | "symbol" }
type_list = { type_spec ~ ("," ~ type_spec)* }

Language-completeness contract:

type_spec = {
    scalar_type
    | domain_ref
    | list_type
    | "term"
    | "compound"
    | "predref"
}
scalar_type = { "u32" | "u64" | "i32" | "i64" | "f32" | "f64" | "bool" | "symbol" }
domain_ref = { ident }
list_type = { "list" ~ "<" ~ type_spec ~ ">" }
named_column = { ident ~ ":" ~ type_spec }
pred_column = { named_column | type_spec }
type_list = { pred_column ~ ("," ~ pred_column)* }

Terms and Atoms

term = { var_or_anon | float_num | integer | string_lit | ident }
term_list = { term ~ ("," ~ term)* }
atom = { ident ~ "(" ~ term_list? ~ ")" }

Language-completeness contract:

list_literal = { "[" ~ (term ~ ("," ~ term)*)? ~ "]" }
cons_pattern = { "[" ~ term ~ "|" ~ term ~ "]" }
compound_term = { ident ~ "(" ~ term_list? ~ ")" }
predref_term = { ident }
term = {
    var_or_anon
    | float_num
    | integer
    | string_lit
    | list_literal
    | cons_pattern
    | compound_term
    | predref_term
    | ident
}
term_list = { term ~ ("," ~ term)* }
atom = { ident ~ "(" ~ term_list? ~ ")" }

Expressions

cmp_op = { "==" | "!=" | "<=" | ">=" | "<" | ">" | "=" }
comparison = { term ~ cmp_op ~ term }

arith_op_mul = { "*" | "/" | "%" }
arith_op_add = { "+" | "-" }

builtin_fn = { "abs" | "min" | "max" | "pow" | "cast" }
func_call = { ident ~ "(" ~ (arith_expr ~ ("," ~ arith_expr)*)? ~ ")" }

arith_primary = {
    builtin_fn ~ "(" ~ arith_expr ~ ("," ~ (arith_expr | type_spec))* ~ ")" |
    func_call |
    "(" ~ arith_expr ~ ")" |
    variable |
    float_num |
    integer
}

arith_term = { arith_primary ~ (arith_op_mul ~ arith_primary)* }
arith_expr = { arith_term ~ (arith_op_add ~ arith_term)* }

is_expr = { variable ~ "is" ~ arith_expr }

Aggregates

agg_op = { "count" | "sum" | "min" | "max" | "logsumexp" }
aggregate = { agg_op ~ "(" ~ variable ~ ")" }

Rules and Facts

epistemic_op = { ("know" | "possible") ~ !ident_continue }
not_kw = @{ "not" ~ !ident_continue }
nested_modal_chain = { not_kw? ~ epistemic_op ~ (not_kw? ~ epistemic_op)+ ~ not_kw? ~ atom }
epistemic_atom = { epistemic_op ~ atom }
negated_epistemic_atom = { "not" ~ epistemic_atom }
negated_atom = { "not" ~ atom }
meta_goal = {
    ("ground" | "var" | "nonvar") ~ "(" ~ term ~ ")"
    | "functor" ~ "(" ~ term ~ "," ~ term ~ "," ~ term ~ ")"
    | term ~ "=.." ~ term
    | "findall" ~ "(" ~ term ~ "," ~ atom ~ "," ~ term ~ ")"
    | "maplist" ~ "(" ~ predref_term ~ "," ~ term ~ ("," ~ term)? ~ ")"
}
body_literal = {
    nested_modal_chain
    | negated_epistemic_atom
    | epistemic_atom
    | negated_atom
    | meta_goal
    | atom
    | comparison
    | is_expr
}
body = { body_literal ~ ("," ~ body_literal)* }

head = { ident ~ "(" ~ head_term_list? ~ ")" }
rule_def = { head ~ ":-" ~ body ~ "." }
fact = { atom ~ "." }
constraint = { ":-" ~ body ~ "." }
query = { "?-" ~ atom ~ "." }

Probabilistic Constructs

prob_num = @{ ASCII_DIGIT+ ~ ("." ~ ASCII_DIGIT+)? }
prob_choice = { prob_num ~ "::" ~ atom }
prob_fact = { prob_choice ~ "." }
annotated_disjunction = { prob_choice ~ (";" ~ prob_choice)+ ~ "." }

prob_query = { "query" ~ "(" ~ atom ~ ")" ~ "." }
evidence_stmt = { "evidence" ~ "(" ~ atom ~ "," ~ bool_lit ~ ")" ~ "." }

Declarations

pred_decl = { private_mod? ~ "pred" ~ ident ~ "(" ~ type_list? ~ ")" ~ "." }
domain_decl = { "domain" ~ ident ~ ":" ~ type_spec ~ "." }

func_param = { variable ~ type_annotation? }
func_params = { func_param ~ ("," ~ func_param)* }
return_type = { "->" ~ type_spec }
cond_expr = { "if" ~ cond_test ~ "then" ~ func_body ~ "else" ~ func_body }
func_body = { func_body_pred | func_body_arith }
func_def = {
    private_mod? ~ "func" ~ ident ~ "(" ~ func_params? ~ ")" ~ return_type?
    ~ "=" ~ func_body ~ "."
}

Modules

module_path = @{ ident ~ ("/" ~ ident)* }
import_list = { "{" ~ ident ~ ("," ~ ident)* ~ "}" }
use_stmt = { "use" ~ module_path ~ ("::" ~ import_list)? ~ "." }

Pragmas

prob_engine_value = { "exact_ddnnf" | "mc" }
prob_cache_value = { "on" | "off" }
epistemic_mode_value = { "g91" | "faeel" }
pragma_prob_engine = { "#pragma" ~ "prob_engine" ~ "=" ~ prob_engine_value }
pragma_prob_cache = { "#pragma" ~ "prob_cache" ~ "=" ~ prob_cache_value }
pragma_epistemic_mode = { "#pragma" ~ "epistemic_mode" ~ "=" ~ epistemic_mode_value }
pragma_max_recursion = { "#pragma" ~ "max_recursion_depth" ~ "=" ~ integer }
pragma_magic_sets = { "#pragma" ~ "magic_sets" ~ "=" ~ ("auto" | "on" | "off") }
pragma_prob_samples = { "#pragma" ~ "prob_samples" ~ "=" ~ integer }
pragma_prob_seed = { "#pragma" ~ "prob_seed" ~ "=" ~ integer }
pragma_prob_confidence = { "#pragma" ~ "prob_confidence" ~ "=" ~ float_num }
pragma_prob_method = { "#pragma" ~ "prob_method" ~ "=" ~ ("rejection" | "evidence_clamping") }
pragma_prob_max_nonmonotone_iterations = {
    "#pragma" ~ "prob_max_nonmonotone_iterations" ~ "=" ~ integer
}
pragma = {
    pragma_prob_engine
    | pragma_prob_cache
    | pragma_epistemic_mode
    | pragma_max_recursion
    | pragma_magic_sets
    | pragma_prob_samples
    | pragma_prob_seed
    | pragma_prob_confidence
    | pragma_prob_method
    | pragma_prob_max_nonmonotone_iterations
}

CLI Examples

xlog run program.xlog
xlog run examples/epistemic/03-faeel-default.xlog
xlog prob program.xlog --prob-engine exact_ddnnf
xlog prob program.xlog --prob-engine mc --samples 10000 --seed 42
xlog explain --format json program.xlog
xlog repl
xlog watch --debounce-ms 250 program.xlog

Program Structure

statement = {
    func_def
    | use_stmt
    | domain_decl
    | pred_decl
    | pragma
    | rule_def
    | prob_fact
    | annotated_disjunction
    | evidence_stmt
    | prob_query
    | fact
    | constraint
    | query
}

program = { SOI ~ statement* ~ EOI }

​Table of Contents

​Overview

​Hello World Example

​Basic Syntax

​Program Structure

​Statement Types

​Identifiers

​Data Types

​Literals

​Type Inference

​Language-Completeness Type Forms

​Language Completeness Contract

​Execution Responsibilities

​Feature Coverage Matrix

​Diagnostic Contract

​Source-Audit Status

​Predicates and Declarations

​Predicate Declarations

​Visibility

​Domain Declarations

​Facts

​Numeric Facts

​Rules

​Simple Rules

​Recursive Rules

​Multi-Atom Bodies

​Variable Binding

​Queries

​Constraints

​Variables and Wildcards

​Named Variables

​Anonymous Wildcard

​Comparisons

​Examples

​Explicit Equality

​Arithmetic Expressions

​Basic Syntax

​Operators

​Built-in Functions

​Examples

​Type Casting

​Division and Error Handling

​Negation

​Syntax

​Examples

​Stratification Requirements

​Domain Safety

​Aggregations

​Supported Aggregates

​Syntax

​Examples

​Multi-Key Aggregation

​Multiple Aggregates

​Computing Averages

​Log-Sum-Exp Aggregation

​Lists

​Syntax

​Built-Ins

​Examples

​Unsupported Forms

​Safe Meta-Predicates

​Supported Meta-Predicates

​Examples

​Unsupported Forms

​Magic Sets

​Configuration

​Example

​Supported Subset

​Declined Forms

​Unsupported Forms

​User-Defined Functions

​Basic Functions

​Conditional Functions

​Recursive Functions

​Using Functions in Rules

​Type Annotations

​Private Functions

​Modules

​Creating Modules

​Importing Modules

Table of Contents

Overview

Hello World Example

Basic Syntax

Program Structure

Statement Types

Identifiers

Data Types

Literals

Type Inference

Language-Completeness Type Forms

Language Completeness Contract

Execution Responsibilities

Feature Coverage Matrix

Diagnostic Contract

Source-Audit Status

Predicates and Declarations

Predicate Declarations

Visibility

Domain Declarations

Facts

Numeric Facts

Rules

Simple Rules

Recursive Rules

Multi-Atom Bodies

Variable Binding

Queries

Constraints

Variables and Wildcards

Named Variables

Anonymous Wildcard

Comparisons

Examples

Explicit Equality

Arithmetic Expressions

Basic Syntax

Operators

Built-in Functions

Examples

Type Casting

Division and Error Handling

Negation

Syntax

Examples

Stratification Requirements

Domain Safety

Aggregations

Supported Aggregates

Syntax

Examples

Multi-Key Aggregation

Multiple Aggregates

Computing Averages

Log-Sum-Exp Aggregation

Lists

Syntax

Built-Ins

Examples

Unsupported Forms

Safe Meta-Predicates

Supported Meta-Predicates

Examples

Unsupported Forms

Magic Sets

Configuration

Example

Supported Subset

Declined Forms

Unsupported Forms

User-Defined Functions

Basic Functions

Conditional Functions

Recursive Functions

Using Functions in Rules

Type Annotations

Private Functions

Modules

Creating Modules

Importing Modules