Enum Term 

pub enum Term {
    Var(String),
    Const(String),
    Typed {
        value: Box<Term>,
        type_annotation: TypeAnnotation,
    },
}

Variants

Var(String)

Const(String)

Typed

Typed term with explicit type annotation

Fields

value: Box<Term>

type_annotation: TypeAnnotation

Implementations

impl Term

pub fn var(name: impl Into<String>) -> Term

Examples found in repository

examples/00_minimal_rule/main.rs (line 11)

fn main() {
    println!("=== Tensorlogic Example: Minimal Rule ===\n");

    // Define a simple implication rule:
    // Parent(a, b) → Ancestor(a, b)
    // "If a is a parent of b, then a is an ancestor of b"

    let parent = TLExpr::pred("Parent", vec![Term::var("a"), Term::var("b")]);

    let ancestor = TLExpr::pred("Ancestor", vec![Term::var("a"), Term::var("b")]);

    let rule = TLExpr::imply(parent, ancestor);

    println!("Rule: Parent(a, b) → Ancestor(a, b)");
    println!("Compiling logic rule to tensor graph...\n");

    match compile_to_einsum(&rule) {
        Ok(plan) => {
            println!("Compilation successful!");
            println!("  Tensors: {}", plan.tensors.len());
            println!("  Nodes: {}", plan.nodes.len());
            println!("\nGenerated tensors:");
            for (i, tensor) in plan.tensors.iter().enumerate() {
                println!("  {}: {}", i, tensor);
            }
            println!("\nGenerated nodes:");
            for (i, node) in plan.nodes.iter().enumerate() {
                println!("  {}: {:?} (inputs: {:?})", i, node.op, node.inputs);
            }
        }
        Err(e) => {
            eprintln!("Compilation error: {}", e);
        }
    }

    println!("\n=== Compilation Complete ===");
}

examples/04_compilation_strategies/main.rs (line 27)

fn main() {
    let sep = "=".repeat(70);
    println!("{}", sep);
    println!("TensorLogic - Compilation Strategies Comparison");
    println!("{}", sep);
    println!();

    // Create a simple logical expression: P(x) AND Q(x)
    let p = TLExpr::pred("P", vec![Term::var("x")]);
    let q = TLExpr::pred("Q", vec![Term::var("x")]);
    let and_expr = TLExpr::and(p.clone(), q.clone());

    // Test data: 5 different cases
    // P values: [0.0, 0.2, 0.5, 0.8, 1.0]
    // Q values: [1.0, 0.8, 0.5, 0.2, 0.0]
    let p_data =
        Scirs2Exec::from_vec(vec![0.0, 0.2, 0.5, 0.8, 1.0], vec![5]).expect("valid tensor data");
    let q_data =
        Scirs2Exec::from_vec(vec![1.0, 0.8, 0.5, 0.2, 0.0], vec![5]).expect("valid tensor data");

    println!("Test Data:");
    println!("  P(x): {:?}", p_data.as_slice().unwrap_or(&[]));
    println!("  Q(x): {:?}", q_data.as_slice().unwrap_or(&[]));
    println!();

    // Test each compilation strategy
    test_strategy(
        "Soft Differentiable",
        &and_expr,
        &p_data,
        &q_data,
        CompilationConfig::soft_differentiable(),
    );

    test_strategy(
        "Hard Boolean",
        &and_expr,
        &p_data,
        &q_data,
        CompilationConfig::hard_boolean(),
    );

    test_strategy(
        "Fuzzy Gödel",
        &and_expr,
        &p_data,
        &q_data,
        CompilationConfig::fuzzy_godel(),
    );

    test_strategy(
        "Fuzzy Product",
        &and_expr,
        &p_data,
        &q_data,
        CompilationConfig::fuzzy_product(),
    );

    test_strategy(
        "Fuzzy Łukasiewicz",
        &and_expr,
        &p_data,
        &q_data,
        CompilationConfig::fuzzy_lukasiewicz(),
    );

    test_strategy(
        "Probabilistic",
        &and_expr,
        &p_data,
        &q_data,
        CompilationConfig::probabilistic(),
    );

    println!();
    let sep = "=".repeat(70);
    println!("{}", sep);
    println!("Analysis:");
    println!("{}", sep);
    println!();
    println!("1. Soft Differentiable (Product):");
    println!("   - Smooth, differentiable everywhere");
    println!("   - Good for gradient-based optimization");
    println!("   - Penalizes low values more");
    println!();
    println!("2. Hard Boolean (Min):");
    println!("   - Exact Boolean semantics");
    println!("   - Not differentiable at certain points");
    println!("   - Returns minimum of inputs");
    println!();
    println!("3. Fuzzy Gödel (Min):");
    println!("   - Same as Hard Boolean for AND");
    println!("   - Part of Gödel fuzzy logic system");
    println!();
    println!("4. Fuzzy Product (Product):");
    println!("   - Similar to Soft Differentiable");
    println!("   - Standard product t-norm");
    println!();
    println!("5. Fuzzy Łukasiewicz (max(0, a+b-1)):");
    println!("   - Different from other strategies");
    println!("   - More conservative (lower values)");
    println!("   - Good for certain applications");
    println!();
    println!("6. Probabilistic (Product, assumes independence):");
    println!("   - Treats values as probabilities");
    println!("   - P(A AND B) = P(A) * P(B) if independent");
    println!();
    let sep = "=".repeat(70);
    println!("{}", sep);
    println!();
    println!("Note: This example demonstrates how different compilation strategies");
    println!("affect the semantics of logical operations. Each strategy compiles");
    println!("the same logical expression to different tensor operations.");
    println!();
    let sep = "=".repeat(70);
    println!("{}", sep);
    println!("Example Complete!");
    println!("{}", sep);
}

examples/01_exists_reduce/main.rs (line 22)

fn main() {
    println!("=== Tensorlogic Example: Exists Quantifier with Reduction ===\n");

    // Define domains
    let mut ctx = CompilerContext::new();
    ctx.add_domain("Person", 10);
    ctx.add_domain("City", 5);

    println!("Domains defined:");
    println!("  Person: cardinality = 10");
    println!("  City: cardinality = 5\n");

    // Example 1: Basic exists quantifier
    // ∃z ∈ Person. Friend(x, z)
    // "There exists a person z who is a friend of x"
    println!("Example 1: ∃z ∈ Person. Friend(x, z)");
    println!("  'For each person x, check if there exists a friend z'");

    let friend_pred = TLExpr::pred("Friend", vec![Term::var("x"), Term::var("z")]);
    let exists_friend = TLExpr::exists("z", "Person", friend_pred);

    match compile_to_einsum_with_context(&exists_friend, &mut ctx.clone()) {
        Ok(graph) => {
            println!("  Compiled successfully!");
            println!("  Tensors: {}", graph.tensors.len());
            println!("  Nodes: {}", graph.nodes.len());
            println!("  Graph tensors: {:?}\n", graph.tensors);
        }
        Err(e) => println!("  Compilation error: {}\n", e),
    }

    // Example 2: Exists with conjunction
    // ∃z ∈ Person. (Friend(x, z) ∧ LivesIn(z, "Tokyo"))
    // "There exists a person z who is a friend of x AND lives in Tokyo"
    println!("Example 2: ∃z ∈ Person. (Friend(x, z) ∧ LivesIn(z, Tokyo))");
    println!("  'For each person x, check if they have a friend in Tokyo'");

    let friend_pred2 = TLExpr::pred("Friend", vec![Term::var("x"), Term::var("z")]);
    let lives_in_tokyo = TLExpr::pred("LivesIn", vec![Term::var("z"), Term::constant("Tokyo")]);
    let and_expr = TLExpr::and(friend_pred2, lives_in_tokyo);
    let exists_friend_tokyo = TLExpr::exists("z", "Person", and_expr);

    match compile_to_einsum_with_context(&exists_friend_tokyo, &mut ctx.clone()) {
        Ok(graph) => {
            println!("  Compiled successfully!");
            println!("  Tensors: {}", graph.tensors.len());
            println!("  Nodes: {}", graph.nodes.len());
            for (i, tensor) in graph.tensors.iter().enumerate() {
                println!("    Tensor {}: {}", i, tensor);
            }
            println!();
        }
        Err(e) => println!("  Compilation error: {}\n", e),
    }

    // Example 3: Nested quantifiers
    // ∃y ∈ City. ∃z ∈ Person. (LivesIn(z, y) ∧ Friend(x, z))
    // "There exists a city y and a person z such that z lives in y and is a friend of x"
    println!("Example 3: ∃y ∈ City. ∃z ∈ Person. (LivesIn(z, y) ∧ Friend(x, z))");
    println!("  'For each person x, check if they have a friend living somewhere'");

    let lives_in = TLExpr::pred("LivesIn", vec![Term::var("z"), Term::var("y")]);
    let friend = TLExpr::pred("Friend", vec![Term::var("x"), Term::var("z")]);
    let inner_and = TLExpr::and(lives_in, friend);
    let exists_z = TLExpr::exists("z", "Person", inner_and);
    let exists_y_z = TLExpr::exists("y", "City", exists_z);

    match compile_to_einsum_with_context(&exists_y_z, &mut ctx.clone()) {
        Ok(graph) => {
            println!("  Compiled successfully!");
            println!("  Tensors: {}", graph.tensors.len());
            println!("  Nodes: {}", graph.nodes.len());
            println!("  This demonstrates reduction over multiple axes:");
            for (i, node) in graph.nodes.iter().enumerate() {
                println!("    Node {}: op = {:?}", i, node.op);
            }
            println!();
        }
        Err(e) => println!("  Compilation error: {}\n", e),
    }

    println!("=== Compilation Complete ===");
    println!("\nNote: These examples demonstrate how existential quantifiers");
    println!("compile to tensor reductions. The actual tensor execution would");
    println!("happen with a backend like SciRS2.");
}

examples/02_scirs2_execution/main.rs (line 19)

fn main() -> anyhow::Result<()> {
    println!("=== Tensorlogic + SciRS2: End-to-End Execution ===\n");

    // 1. Define logic rule: Parent(x, y) → Ancestor(x, y)
    let parent = TLExpr::pred("Parent", vec![Term::var("x"), Term::var("y")]);
    let ancestor = TLExpr::pred("Ancestor", vec![Term::var("x"), Term::var("y")]);
    let rule = TLExpr::imply(parent.clone(), ancestor.clone());

    println!("Logic Rule: Parent(x, y) → Ancestor(x, y)");
    println!("Interpretation: If Parent(x,y) holds, then Ancestor(x,y) should hold\n");

    // 2. Compile to einsum graph
    println!("Compiling to tensor graph...");
    let graph = compile_to_einsum(&rule)?;
    println!("  Tensors: {}", graph.tensors.len());
    println!("  Nodes: {}", graph.nodes.len());

    for (idx, tensor_name) in graph.tensors.iter().enumerate() {
        println!("  Tensor {}: {}", idx, tensor_name);
    }

    for (idx, node) in graph.nodes.iter().enumerate() {
        println!("  Node {}: {:?} (inputs: {:?})", idx, node.op, node.inputs);
    }
    println!();

    // 3. Create SciRS2 executor and input tensors
    println!("Creating SciRS2 executor...");
    let mut executor = Scirs2Exec::new();

    // Create a 3x3 Parent relation tensor (3 people, 3 people)
    // Parent[i,j] = 1.0 if person i is parent of person j
    let parent_data = vec![
        0.0, 1.0, 1.0, // Person 0 is parent of 1, 2
        0.0, 0.0, 0.0, // Person 1 has no children
        0.0, 0.0, 0.0, // Person 2 has no children
    ];

    let parent_tensor = Scirs2Exec::from_vec(parent_data, vec![3, 3])?;
    println!("Parent tensor shape: {:?}", parent_tensor.shape());
    println!("Parent tensor:\n{:?}\n", parent_tensor);

    // Create expected Ancestor tensor (also 3x3, same as Parent for this simple case)
    let ancestor_data = vec![
        0.0, 1.0, 1.0, // Person 0 is ancestor of 1, 2
        0.0, 0.0, 0.0, // Person 1 has no descendants
        0.0, 0.0, 0.0, // Person 2 has no descendants
    ];

    let ancestor_tensor = Scirs2Exec::from_vec(ancestor_data, vec![3, 3])?;
    println!(
        "Expected Ancestor tensor shape: {:?}",
        ancestor_tensor.shape()
    );
    println!("Expected Ancestor tensor:\n{:?}\n", ancestor_tensor);

    // Add tensors to executor storage using dynamic names from compiled graph
    executor.add_tensor(graph.tensors[0].clone(), parent_tensor);
    executor.add_tensor(graph.tensors[1].clone(), ancestor_tensor);

    // 4. Execute the graph
    println!("Executing forward pass...");
    let output = executor.forward(&graph)?;
    println!("Output tensor shape: {:?}", output.shape());
    println!("Output tensor (constraint violation):\n{:?}\n", output);

    // 5. Interpret results
    println!("=== Interpretation ===");
    println!("The output tensor represents constraint violations (via ReLU(Ancestor - Parent)).");
    println!("  - Values near 0: rule satisfied (Parent implies Ancestor)");
    println!("  - Positive values: violations (Parent holds but Ancestor doesn't)\n");

    // Example 2: Test element-wise operations
    println!("=== Testing SciRS2 Element-wise Operations ===\n");

    let test_data = vec![-2.0, -1.0, 0.0, 1.0, 2.0];
    let test_tensor = Scirs2Exec::from_vec(test_data, vec![5])?;

    println!("Input: {:?}", test_tensor);

    let relu_result = executor.elem_op(tensorlogic_infer::ElemOp::Relu, &test_tensor)?;
    println!("ReLU:  {:?}", relu_result);

    let sigmoid_result = executor.elem_op(tensorlogic_infer::ElemOp::Sigmoid, &test_tensor)?;
    println!("Sigmoid: {:?}", sigmoid_result);

    let one_minus_result = executor.elem_op(tensorlogic_infer::ElemOp::OneMinus, &test_tensor)?;
    println!("OneMinus: {:?}\n", one_minus_result);

    // Example 3: Test reduction operations
    println!("=== Testing SciRS2 Reduction Operations ===\n");

    let matrix_data = vec![1.0, 2.0, 3.0, 4.0, 5.0, 6.0];
    let matrix = Scirs2Exec::from_vec(matrix_data, vec![2, 3])?;

    println!("Input matrix (2x3):\n{:?}\n", matrix);

    let sum_axis0 = executor.reduce(tensorlogic_infer::ReduceOp::Sum, &matrix, &[0])?;
    println!("Sum over axis 0: {:?}", sum_axis0);

    let sum_axis1 = executor.reduce(tensorlogic_infer::ReduceOp::Sum, &matrix, &[1])?;
    println!("Sum over axis 1: {:?}", sum_axis1);

    let max_axis0 = executor.reduce(tensorlogic_infer::ReduceOp::Max, &matrix, &[0])?;
    println!("Max over axis 0: {:?}", max_axis0);

    let mean_axis1 = executor.reduce(tensorlogic_infer::ReduceOp::Mean, &matrix, &[1])?;
    println!("Mean over axis 1: {:?}\n", mean_axis1);

    println!("=== Execution Complete ===");
    println!("\nThis demonstrates the full pipeline:");
    println!("  Logic → IR → Einsum Graph → SciRS2 Execution → Results");

    Ok(())
}

pub fn constant(name: impl Into<String>) -> Term

Examples found in repository

examples/01_exists_reduce/main.rs (line 42)

fn main() {
    println!("=== Tensorlogic Example: Exists Quantifier with Reduction ===\n");

    // Define domains
    let mut ctx = CompilerContext::new();
    ctx.add_domain("Person", 10);
    ctx.add_domain("City", 5);

    println!("Domains defined:");
    println!("  Person: cardinality = 10");
    println!("  City: cardinality = 5\n");

    // Example 1: Basic exists quantifier
    // ∃z ∈ Person. Friend(x, z)
    // "There exists a person z who is a friend of x"
    println!("Example 1: ∃z ∈ Person. Friend(x, z)");
    println!("  'For each person x, check if there exists a friend z'");

    let friend_pred = TLExpr::pred("Friend", vec![Term::var("x"), Term::var("z")]);
    let exists_friend = TLExpr::exists("z", "Person", friend_pred);

    match compile_to_einsum_with_context(&exists_friend, &mut ctx.clone()) {
        Ok(graph) => {
            println!("  Compiled successfully!");
            println!("  Tensors: {}", graph.tensors.len());
            println!("  Nodes: {}", graph.nodes.len());
            println!("  Graph tensors: {:?}\n", graph.tensors);
        }
        Err(e) => println!("  Compilation error: {}\n", e),
    }

    // Example 2: Exists with conjunction
    // ∃z ∈ Person. (Friend(x, z) ∧ LivesIn(z, "Tokyo"))
    // "There exists a person z who is a friend of x AND lives in Tokyo"
    println!("Example 2: ∃z ∈ Person. (Friend(x, z) ∧ LivesIn(z, Tokyo))");
    println!("  'For each person x, check if they have a friend in Tokyo'");

    let friend_pred2 = TLExpr::pred("Friend", vec![Term::var("x"), Term::var("z")]);
    let lives_in_tokyo = TLExpr::pred("LivesIn", vec![Term::var("z"), Term::constant("Tokyo")]);
    let and_expr = TLExpr::and(friend_pred2, lives_in_tokyo);
    let exists_friend_tokyo = TLExpr::exists("z", "Person", and_expr);

    match compile_to_einsum_with_context(&exists_friend_tokyo, &mut ctx.clone()) {
        Ok(graph) => {
            println!("  Compiled successfully!");
            println!("  Tensors: {}", graph.tensors.len());
            println!("  Nodes: {}", graph.nodes.len());
            for (i, tensor) in graph.tensors.iter().enumerate() {
                println!("    Tensor {}: {}", i, tensor);
            }
            println!();
        }
        Err(e) => println!("  Compilation error: {}\n", e),
    }

    // Example 3: Nested quantifiers
    // ∃y ∈ City. ∃z ∈ Person. (LivesIn(z, y) ∧ Friend(x, z))
    // "There exists a city y and a person z such that z lives in y and is a friend of x"
    println!("Example 3: ∃y ∈ City. ∃z ∈ Person. (LivesIn(z, y) ∧ Friend(x, z))");
    println!("  'For each person x, check if they have a friend living somewhere'");

    let lives_in = TLExpr::pred("LivesIn", vec![Term::var("z"), Term::var("y")]);
    let friend = TLExpr::pred("Friend", vec![Term::var("x"), Term::var("z")]);
    let inner_and = TLExpr::and(lives_in, friend);
    let exists_z = TLExpr::exists("z", "Person", inner_and);
    let exists_y_z = TLExpr::exists("y", "City", exists_z);

    match compile_to_einsum_with_context(&exists_y_z, &mut ctx.clone()) {
        Ok(graph) => {
            println!("  Compiled successfully!");
            println!("  Tensors: {}", graph.tensors.len());
            println!("  Nodes: {}", graph.nodes.len());
            println!("  This demonstrates reduction over multiple axes:");
            for (i, node) in graph.nodes.iter().enumerate() {
                println!("    Node {}: op = {:?}", i, node.op);
            }
            println!();
        }
        Err(e) => println!("  Compilation error: {}\n", e),
    }

    println!("=== Compilation Complete ===");
    println!("\nNote: These examples demonstrate how existential quantifiers");
    println!("compile to tensor reductions. The actual tensor execution would");
    println!("happen with a backend like SciRS2.");
}

pub fn typed_var(name: impl Into<String>, type_name: impl Into<String>) -> Term

Create a typed variable

pub fn typed_const( name: impl Into<String>, type_name: impl Into<String>, ) -> Term

Create a typed constant

pub fn with_type(self, type_name: impl Into<String>) -> Term

Attach a type annotation to an existing term

pub fn is_var(&self) -> bool

pub fn is_const(&self) -> bool

pub fn name(&self) -> &str

pub fn get_type(&self) -> Option<&TypeAnnotation>

Get the type annotation if present

pub fn untyped(&self) -> &Term

Get the underlying untyped term

Trait Implementations

impl Clone for Term

fn clone(&self) -> Term

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Term

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for Term

fn deserialize<__D>( __deserializer: __D, ) -> Result<Term, <__D as Deserializer<'de>>::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Display for Term

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl Eq for Term

impl Hash for Term

fn hash<__H>(&self, state: &mut __H)

where __H: Hasher,

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for Term

fn eq(&self, other: &Term) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl Serialize for Term

fn serialize<__S>( &self, __serializer: __S, ) -> Result<<__S as Serializer>::Ok, <__S as Serializer>::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl StructuralPartialEq for Term