Crate tensorlogic_ir

Expand description

§TensorLogic IR

Engine-agnostic Abstract Syntax Tree & Intermediate Representation for TensorLogic

Version: 0.1.0-alpha.1 | Status: Production Ready

This crate provides the core data structures and operations for representing logic-as-tensor computations in the TensorLogic framework. It serves as the foundational layer that all other TensorLogic components build upon.

§Overview

TensorLogic IR enables the compilation of logical rules (predicates, quantifiers, implications) into tensor equations (einsum graphs) with a minimal DSL + IR. This approach allows for:

Neural, symbolic, and probabilistic models within a unified tensor computation framework
Engine-agnostic representation that can be executed on different backends
Static analysis and optimization of logical expressions before execution
Type-safe construction and validation of logical expressions

§Core Components

§Terms (`Term`)

Variables and constants that appear in logical expressions:

Variables: Free or bound variables (e.g., x, y, Person)
Constants: Concrete values (e.g., alice, bob, 42)
Typed terms: Terms with explicit type annotations

§Logical Expressions (`TLExpr`)

The DSL for expressing logical rules:

Predicates: Atomic propositions like Person(x) or knows(alice, bob)
Logical connectives: AND (∧), OR (∨), NOT (¬), Implication (→)
Quantifiers: Existential (∃) and Universal (∀) with domain constraints
Arithmetic: Addition, subtraction, multiplication, division
Comparisons: Equality, less than, greater than, etc.
Control flow: If-then-else conditionals

§Tensor Computation Graphs (`EinsumGraph`)

The compiled IR representing tensor operations:

Tensors: Named tensor values with indices
Nodes: Operations on tensors (einsum, element-wise, reductions)
Outputs: Designated output tensors
Validation: Comprehensive graph validation and error checking

§Features

§Type System

Static type checking with PredicateSignature and TypeAnnotation
Arity validation ensures consistent predicate usage
Type inference and compatibility checking

§Domain Constraints

Domain management via DomainRegistry and DomainInfo
Built-in domains: Bool, Int, Real, Nat, Probability
Custom finite and infinite domains
Domain validation for quantified variables

§Metadata & Provenance

Source location tracking with SourceLocation and SourceSpan
Provenance information via Provenance for rule tracking
Custom metadata support for nodes and expressions

§Serialization

Full serde support for JSON and binary formats
Versioned serialization with VersionedExpr and VersionedGraph
Backward compatibility checking

§Analysis & Utilities

Free variable analysis
Predicate extraction and counting
Graph statistics with GraphStats
Expression statistics with ExprStats
Pretty printing and DOT export for visualization
Expression and graph diffing with diff_exprs and diff_graphs

§Quick Start

§Creating Logical Expressions

use tensorlogic_ir::{TLExpr, Term};

// Simple predicate: Person(x)
let person = TLExpr::pred("Person", vec![Term::var("x")]);

// Logical rule: ∀x. Person(x) → Mortal(x)
let mortal = TLExpr::pred("Mortal", vec![Term::var("x")]);
let rule = TLExpr::forall("x", "Entity", TLExpr::imply(person, mortal));

// Verify no free variables (all bound by quantifier)
assert!(rule.free_vars().is_empty());

§Building Computation Graphs

use tensorlogic_ir::{EinsumGraph, EinsumNode};

let mut graph = EinsumGraph::new();

// Matrix multiplication: C = A @ B
let a = graph.add_tensor("A");
let b = graph.add_tensor("B");
let c = graph.add_tensor("C");

graph.add_node(EinsumNode::einsum("ik,kj->ij", vec![a, b], vec![c])).unwrap();
graph.add_output(c).unwrap();

// Validate the graph
assert!(graph.validate().is_ok());

§Domain Management

use tensorlogic_ir::{DomainRegistry, DomainInfo, TLExpr, Term};

// Create registry with built-in domains
let mut registry = DomainRegistry::with_builtins();

// Add custom domain
registry.register(DomainInfo::finite("Person", 100)).unwrap();

// Create and validate expression
let expr = TLExpr::exists("x", "Person", TLExpr::pred("P", vec![Term::var("x")]));
assert!(expr.validate_domains(&registry).is_ok());

§Examples

See the examples/ directory for comprehensive demonstrations:

00_basic_expressions: Simple predicates and logical connectives
01_quantifiers: Existential and universal quantifiers
02_arithmetic: Arithmetic and comparison operations
03_graph_construction: Building computation graphs
05_serialization: JSON and binary serialization
06_visualization: Pretty printing and DOT export

§Architecture

The crate is organized into focused modules:

term: Variables, constants, and type annotations
expr: Logical expressions and builders
graph: Tensor computation graphs and nodes
domain: Domain constraints and validation
signature: Type signatures for predicates
metadata: Provenance and source tracking
serialization: Versioned JSON/binary formats
util: Pretty printing and statistics
diff: Expression and graph comparison
error: Comprehensive error types

§Logic-to-Tensor Mapping

Logic Operation	Tensor Equivalent	Notes
`AND(a, b)`	`a * b`	Hadamard product (element-wise)
`OR(a, b)`	`max(a, b)`	Or soft variant (configurable)
`NOT(a)`	`1 - a`	Complement operation
`∃x. P(x)`	`sum(P, axis=x)`	Or `max` for hard quantification
`∀x. P(x)`	`NOT(∃x. NOT(P(x)))`	Dual of existential
`a → b`	`ReLU(b - a)`	Soft implication

§Performance

Lazy validation: Operations are validated only when explicitly requested
Zero-copy indices: Graph operations use tensor indices instead of cloning
Incremental building: Graphs can be built step-by-step efficiently
Property tests: 30 randomized tests ensure correctness
Benchmarks: 40+ performance tests measure all operations

§See Also

tensorlogic-compiler: Compiles TLExpr → EinsumGraph
tensorlogic-infer: Execution and autodiff traits
tensorlogic-scirs-backend: SciRS2-powered runtime execution
tensorlogic-adapters: Symbol tables and axis metadata

Re-exports§

pub use diff::diff_exprs;
pub use diff::diff_graphs;
pub use diff::ExprDiff;
pub use diff::GraphDiff;
pub use diff::NodeDiff;
pub use serialization::VersionedExpr;
pub use serialization::VersionedGraph;
pub use serialization::FORMAT_VERSION;
pub use util::pretty_print_expr;
pub use util::pretty_print_graph;
pub use util::ExprStats;
pub use util::GraphStats;

Modules§

diff: IR diff tool for comparing graphs and expressions.
fuzzing: Fuzzing and stress testing infrastructure for the IR.
serialization: Enhanced serialization support for TensorLogic IR.
util: Utility functions for the IR.

Structs§

ACPattern: AC pattern matching with variable bindings.
AdvancedRewriteSystem: Advanced rewrite system with sophisticated control flow.
ComplexityMetrics: Complexity metrics for an expression.
ConditionalRule: A conditional rewrite rule with guards and priority.
ConfluenceChecker: Confluence checker for rewrite systems.
ConfluenceReport: Result of confluence analysis.
CostSummary: Summary of graph costs.
CredalSet: Credal set: convex set of probability distributions.
CriticalPair: A critical pair representing a potential conflict between two rules.
DomainInfo: Represents a domain constraint for a variable.
DomainRegistry: Registry for managing domain information.
DotExportOptions: Options for DOT export customization.
EinsumGraph
EinsumNode
ExpressionProfile: Characteristics of an expression used for strategy selection.
FuzzySet: Represents a fuzzy membership function over a continuous domain.
GraphCostModel: Cost model for an entire graph.
GraphValidationStats: Statistics about the validated graph.
Metadata: Metadata container that can be attached to IR nodes
Multiset: Multiset for AC matching.
OperationCost: Cost annotation for a single operation.
OperatorCounts: Detailed operator counts categorized by type.
OptimizationMetrics: Metrics collected during optimization.
OptimizationPipeline: Optimization pipeline that orchestrates multiple passes.
PatternAnalysis: Pattern detection results.
PipelineConfig: Configuration for the optimization pipeline.
PredicateSignature: Signature for a predicate: defines expected argument types
ProbabilityInterval: Probability interval representing imprecise probabilities.
Provenance: Provenance information tracking the origin of an IR node
RewriteConfig: Configuration for the advanced rewrite system.
RewriteRule: A rewrite rule that transforms expressions matching a pattern into a template.
RewriteStats: Statistics about a rewriting session.
RewriteSystem: A collection of rewrite rules that can be applied to expressions.
SignatureRegistry: Registry of predicate signatures
SingletonFuzzySet: Singleton fuzzy set for discrete inputs (common in fuzzy control).
SourceLocation: Source code location information
SourceSpan: Span information covering a range in source code
StrategySelector: Strategy selector that recommends optimization configurations.
TemporalComplexity: Temporal logic complexity metrics.
TypeAnnotation: Type annotation for a term.
ValidationError: Validation error with severity and context.
ValidationReport: Result of graph validation with detailed diagnostics.
ValidationWarning: Validation warning (non-fatal issue).

Enums§

ACOperator: Operators that are associative and commutative.
AggregateOp: Aggregation operation type.
DefuzzificationMethod: Defuzzification method selection.
DistributiveStrategy: Strategy for applying distributive laws.
DomainType: Type category of a domain.
FuzzyImplicationKind: Fuzzy implication operator kinds.
FuzzyNegationKind: Fuzzy negation kinds.
IrError
ModalSystem: Modal logic axiom systems.
OpType: Operation types supported in the tensor graph
OptimizationLevel: Optimization level controlling aggressiveness of optimizations.
OptimizationPass: A single optimization pass.
Pattern: A pattern that can match against expressions.
RewriteStrategy: Rewriting strategy controlling traversal order and application.
RulePriority: Priority level for rewrite rules.
TCoNormKind: T-conorm (triangular conorm) kinds for fuzzy OR operations. A t-conorm is the dual of a t-norm: S(a,b) = 1 - T(1-a, 1-b)
TLExpr
TNormKind: T-norm (triangular norm) kinds for fuzzy AND operations. A t-norm is a binary operation T: [0,1] × [0,1] → [0,1] that is:
TemporalClass: Classification of temporal formulas.
TemporalPattern: Temporal pattern types.
Term
ValidationErrorKind: Types of validation errors.
ValidationWarningKind: Types of validation warnings.

Functions§

ac_equivalent: Check if two expressions are AC-equivalent.
algebraic_simplify: Algebraic simplification: apply algebraic identities and simplification rules
apply_advanced_ltl_equivalences: Apply additional LTL equivalences beyond basic optimizations.
apply_axiom_k: Apply axiom K to simplify modal expressions.
apply_axiom_t: Apply axiom T to simplify modal expressions.
apply_distributive_laws: Apply distributive laws to an expression.
apply_modal_equivalences: Apply modal logic equivalences to simplify an expression.
apply_temporal_equivalences: Apply temporal logic equivalences to simplify an expression.
are_graphs_equivalent: Check if two graphs are canonically equivalent.
are_joinable: Check if two expressions can be joined under a rewrite system.
auto_annotate_costs: Auto-annotate a graph with estimated costs.
auto_optimize: Convenience function to automatically select and apply the best optimization strategy.
bisector: Bisector of Area defuzzification.
canonical_hash: Compute a hash of a graph in canonical form.
canonicalize_graph: Canonicalize a computation graph.
centroid: Centroid (Center of Area) defuzzification.
classify_temporal_formula: Classify a temporal formula.
compute_temporal_complexity: Compute temporal complexity metrics for a formula.
compute_tight_bounds: Compute tightest probability bounds for an expression using optimization.
constant_fold: Constant folding: evaluate constant expressions at compile time
decompose_safety_liveness: Convert temporal formula to safety-progress decomposition.
defuzzify: Defuzzify a fuzzy set using the specified method.
estimate_graph_cost: Estimate the total cost of a graph given per-node costs.
estimate_operation_cost: Estimate the cost of a graph operation.
export_to_dot: Export an EinsumGraph to DOT format.
export_to_dot_with_options: Export an EinsumGraph to DOT format with custom options.
extract_modal_subformulas: Extract all modal subformulas from an expression.
extract_probabilistic_semantics: Extract probabilistic semantics from weighted rules.
extract_state_predicates: Extract state predicates (non-temporal atomic propositions).
extract_temporal_subformulas: Extract all temporal subformulas from an expression.
flatten_ac: Flatten an AC expression into a list of operands.
identify_temporal_pattern: Identify temporal pattern in a formula.
is_cnf: Check if an expression is in Conjunctive Normal Form (CNF).
is_dnf: Check if an expression is in Disjunctive Normal Form (DNF).
is_modal_free: Check if an expression is modal-free (contains no modal operators).
is_temporal: Check if an expression contains temporal operators.
is_temporal_nnf: Check if formula is in negation normal form for temporal operators.
is_theorem_in_system: Verify that an expression is a theorem in a given modal system.
largest_of_maximum: Largest of Maximum defuzzification.
mean_of_maximum: Mean of Maximum defuzzification.
mln_probability: Compute probability of an expression under a Markov Logic Network (MLN) semantics.
modal_depth: Calculate the modal depth of an expression.
normalize: Compute normal form of an expression (if it exists).
normalize_ac: Normalize an AC expression by sorting operands.
normalize_s5: Normalize a modal expression according to S5 axioms.
optimize_expr: Apply multiple optimization passes in sequence
propagate_constants: Propagate constants through Let bindings
propagate_probabilities: Propagate probability intervals through a logical expression.
smallest_of_maximum: Smallest of Maximum defuzzification.
to_cnf: Convert an expression to Conjunctive Normal Form (CNF).
to_dnf: Convert an expression to Disjunctive Normal Form (DNF).
to_nnf: Convert an expression to Negation Normal Form (NNF).
validate_graph: Validate an EinsumGraph with comprehensive checks.
verify_axiom_4: Verify that an expression conforms to Axiom 4: □p → □□p
verify_axiom_5: Verify that an expression conforms to Axiom 5: ◇p → □◇p
verify_axiom_b: Verify that an expression conforms to Axiom B: p → □◇p
verify_axiom_d: Verify that an expression conforms to Axiom D: □p → ◇p
verify_axiom_k: Verify that an expression conforms to Axiom K: □(p → q) → (□p → □q)
verify_axiom_t: Verify that an expression conforms to Axiom T: □p → p
weighted_average: Weighted Average defuzzification for singleton fuzzy sets.