Crate tensorlogic_ir

Expand description

§TensorLogic IR

Engine-agnostic Abstract Syntax Tree & Intermediate Representation for TensorLogic

Version: 0.1.0-beta.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
Parametric types with type constructors (List<T>, Option<T>, Tuple<A,B>, etc.)
Type unification using Robinson’s algorithm
Generalization and instantiation for polymorphic types
Effect system for tracking computational effects (purity, differentiability, stochasticity)
Effect polymorphism and inference
Dependent types with value-dependent types (e.g., Vec<n, T> where n is a runtime value)
Linear types for resource management and safe in-place operations
Refinement types for constraint-based type checking (e.g., {x: Int | x > 0})
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
Profile-guided optimization (PGO) for runtime-informed optimization decisions

§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
07_parametric_types: Parametric types, unification, and polymorphic signatures
08_effect_system: Effect tracking, polymorphism, and annotations
09_dependent_types: Dependent types with value-dependent dimensions
10_linear_types: Linear types for resource management
11_refinement_types: Refinement types with predicates
12_profile_guided_optimization: Profile-guided optimization with runtime profiling
13_sequent_calculus: Sequent calculus and proof search
14_constraint_logic_programming: Constraint satisfaction problems
15_advanced_graph_algorithms: Graph analysis (SCC, cycles, critical paths)
16_resolution_theorem_proving: Resolution-based automated theorem proving

§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
parametric_types: Parametric types, type constructors, and unification
effect_system: Effect tracking, polymorphism, and annotations
dependent: Dependent types with value-dependent dimensions
linear: Linear types for resource management and multiplicity tracking
refinement: Refinement types with logical predicates
metadata: Provenance and source tracking
serialization: Versioned JSON/binary formats
util: Pretty printing and statistics
diff: Expression and graph comparison
graph::pgo: Profile-guided optimization with runtime profiling
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 dependent::DependentType;
pub use dependent::DependentTypeContext;
pub use dependent::DimConstraint;
pub use dependent::IndexExpr;
pub use diff::diff_exprs;
pub use diff::diff_graphs;
pub use diff::ExprDiff;
pub use diff::GraphDiff;
pub use diff::NodeDiff;
pub use effect_system::infer_operation_effects;
pub use effect_system::ComputationalEffect;
pub use effect_system::Effect;
pub use effect_system::EffectAnnotation;
pub use effect_system::EffectScheme;
pub use effect_system::EffectSet;
pub use effect_system::EffectSubstitution;
pub use effect_system::EffectVar;
pub use effect_system::MemoryEffect;
pub use effect_system::ProbabilisticEffect;
pub use linear::Capability;
pub use linear::LinearContext;
pub use linear::LinearResource;
pub use linear::LinearType;
pub use linear::LinearityChecker;
pub use linear::Multiplicity;
pub use linear::Usage;
pub use parametric_types::compose_substitutions;
pub use parametric_types::generalize;
pub use parametric_types::instantiate;
pub use parametric_types::unify;
pub use parametric_types::Kind;
pub use parametric_types::ParametricType;
pub use parametric_types::TypeConstructor;
pub use parametric_types::TypeSubstitution;
pub use refinement::LiquidTypeInference;
pub use refinement::Refinement;
pub use refinement::RefinementContext;
pub use refinement::RefinementType;
pub use resolution::Clause;
pub use resolution::Literal;
pub use resolution::ProofResult;
pub use resolution::ProverStats;
pub use resolution::ResolutionProver;
pub use resolution::ResolutionStep;
pub use resolution::ResolutionStrategy;
pub use sequent::CutElimination;
pub use sequent::InferenceRule;
pub use sequent::ProofSearchEngine;
pub use sequent::ProofSearchStats;
pub use sequent::ProofSearchStrategy;
pub use sequent::ProofTree;
pub use sequent::Sequent;
pub use serialization::VersionedExpr;
pub use serialization::VersionedGraph;
pub use serialization::FORMAT_VERSION;
pub use unification::anti_unify_terms;
pub use unification::are_unifiable;
pub use unification::lgg_terms;
pub use unification::rename_vars;
pub use unification::unify_term_list;
pub use unification::unify_terms;
pub use unification::Substitution;
pub use util::pretty_print_expr;
pub use util::pretty_print_graph;
pub use util::ExprStats;
pub use util::GraphStats;

Modules§

clp: Constraint Logic Programming (CLP) Module
dependent: Dependent type system for value-dependent types in TensorLogic.
diff: IR diff tool for comparing graphs and expressions.
effect_system: Effect system for tracking computational effects in TensorLogic expressions.
fuzzing: Fuzzing and stress testing infrastructure for the IR.
linear: Linear type system for resource management in TensorLogic.
parametric_types: Parametric type system with type constructors and unification.
refinement: Refinement types for constraint-based type checking.
resolution: Resolution-Based Theorem Proving
sequent: Sequent Calculus for Proof-Theoretic Foundations
serialization: Enhanced serialization support for TensorLogic IR.
unification: First-Order Unification
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.
ConstantInfo: Information about a constant tensor.
ConstantPropagationResult: Result of constant propagation 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.
CriticalPath: Critical path analysis result.
Cycle: A cycle in the computation graph.
DomainInfo: Represents a domain constraint for a variable.
DomainRegistry: Registry for managing domain information.
DotExportOptions: Options for DOT export customization.
EinsumGraph
EinsumNode
ExecutionProfile: Execution profile for entire graph.
ExecutionSchedule: A schedule for executing graph operations
ExpressionProfile: Characteristics of an expression used for strategy selection.
FoldingStats: Statistics from constant folding transformation.
FusionStats: Statistics about fusion optimizations applied
FuzzySet: Represents a fuzzy membership function over a continuous domain.
GraphCostModel: Cost model for an entire graph.
GraphRewriteRule: A rewrite rule that transforms matched patterns
GraphScheduler: Advanced scheduler for computation graphs
GraphValidationStats: Statistics about the validated graph.
LayoutOptimizationResult: Result of layout optimization.
MemoryAnalysis: Memory optimization analysis result
Metadata: Metadata container that can be attached to IR nodes
Multiset: Multiset for AC matching.
NodeStats: Runtime execution statistics for a single node.
OnnxExportOptions: Export options for ONNX format.
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.
OptimizationStats
ParallelGroup: A group of nodes that can execute in parallel
ParallelizationAnalysis: Analysis result containing parallel execution opportunities
PatternAnalysis: Pattern detection results.
PatternMatch: Result of a successful pattern match
PatternMatcher: Pattern matcher for graphs
PatternRewriteStats: Statistics about pattern matching and rewriting
PipelineConfig: Configuration for the optimization pipeline.
PredicateSignature: Signature for a predicate: defines expected argument types
ProbabilityInterval: Probability interval representing imprecise probabilities.
ProfileGuidedOptimizer: Profile-guided optimizer.
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.
StridePattern: Stride pattern for a tensor.
StronglyConnectedComponent: A strongly connected component (SCC) in the computation graph.
TemporalComplexity: Temporal logic complexity metrics.
TensorLayout: Layout configuration for a tensor.
TensorMemory: Memory footprint estimate for a tensor
TensorStats: Tensor usage statistics.
TileConfig: Tiling configuration for a specific axis.
TilingResult: Result of applying tiling transformations.
TilingStrategy: Multi-dimensional tiling strategy.
TorchScriptExportOptions: Export options for TorchScript format.
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.
GraphPattern: A pattern that can match against graph structures
IrError
IsomorphismResult: Graph isomorphism result.
LayoutStrategy: Memory layout strategy for tensors.
ModalSystem: Modal logic axiom systems.
OpType: Operation types supported in the tensor graph
OptimizationHint: Optimization hint derived from profiling.
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.
SchedulingObjective: Scheduling objective to optimize for
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
analyze_constants: Analyze constant propagation opportunities in a graph.
analyze_inplace_opportunities: Estimate memory savings from in-place operations
analyze_memory: Analyze memory usage patterns in a computation graph
analyze_parallelization: Analyze graph for parallel execution opportunities
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_constant_folding: Apply constant folding transformations to a graph.
apply_distributive_laws: Apply distributive laws to an expression.
apply_layouts: Apply the recommended layouts to a graph.
apply_modal_equivalences: Apply modal logic equivalences to simplify an expression.
apply_multilevel_tiling: Apply multi-level tiling (L1, L2, L3 cache hierarchy).
apply_register_tiling: Apply register-level tiling for maximum register reuse.
apply_temporal_equivalences: Apply temporal logic equivalences to simplify an expression.
apply_tiling: Apply loop tiling to einsum operations in the graph.
are_graphs_equivalent: Check if two graphs are canonically equivalent.
are_isomorphic: Check if two graphs are isomorphic.
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
critical_path_analysis: Find the critical path in the computation graph.
decompose_safety_liveness: Convert temporal formula to safety-progress decomposition.
defuzzify: Defuzzify a fuzzy set using the specified method.
eliminate_common_subexpressions: Common Subexpression Elimination (CSE) - detects and deduplicates identical subgraphs
eliminate_dead_code: Dead Code Elimination (DCE) - removes unused tensors and nodes
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.
export_to_onnx_text: Export EinsumGraph to ONNX text representation.
export_to_onnx_text_with_options: Export EinsumGraph to ONNX text representation with custom options.
export_to_torchscript_text: Export EinsumGraph to TorchScript text representation.
export_to_torchscript_text_with_options: Export EinsumGraph to TorchScript text representation 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.
find_all_paths: Find all paths between two tensors.
find_cycles: Find all cycles in the computation graph.
find_layout_fusion_opportunities: Find opportunities for layout fusion (avoiding layout conversions).
flatten_ac: Flatten an AC expression into a list of operands.
fold_constants_aggressive: Perform aggressive constant folding with all available optimizations.
fuse_all: Apply all fusion optimizations to a graph
fuse_einsum_operations: Fuse einsum operations when possible
fuse_elementwise_operations: Fuse element-wise operations that operate on the same tensors
fuse_map_reduce: Fuse reduction operations with their producers when possible
graph_diameter: Compute graph diameter (longest shortest path).
identify_constant_subgraphs: Identify constant subgraphs that can be pre-computed.
identify_temporal_pattern: Identify temporal pattern in a formula.
is_cnf: Check if an expression is in Conjunctive Normal Form (CNF).
is_dag: Check if a graph is a directed acyclic graph (DAG).
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
optimize_graph: Apply all optimization passes to the graph
optimize_layouts: Optimize tensor layouts for a graph.
partition_independent_subgraphs: Partition graph into independent subgraphs for parallel execution
propagate_constants
propagate_probabilities: Propagate probability intervals through a logical expression.
recommend_tiling_strategy: Analyze a graph and recommend optimal tiling strategies.
simplify_identity_operations: Simplify identity operations (operations that don’t transform their input)
smallest_of_maximum: Smallest of Maximum defuzzification.
strongly_connected_components: Find all strongly connected components using Tarjan’s algorithm.
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).
topological_sort: Perform topological sort on the computation graph.
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.