01_exists_reduce/
main.rs

1use tensorlogic_compiler::{compile_to_einsum_with_context, CompilerContext};
2use tensorlogic_ir::{TLExpr, Term};
3
4fn main() {
5    println!("=== Tensorlogic Example: Exists Quantifier with Reduction ===\n");
6
7    // Define domains
8    let mut ctx = CompilerContext::new();
9    ctx.add_domain("Person", 10);
10    ctx.add_domain("City", 5);
11
12    println!("Domains defined:");
13    println!("  Person: cardinality = 10");
14    println!("  City: cardinality = 5\n");
15
16    // Example 1: Basic exists quantifier
17    // ∃z ∈ Person. Friend(x, z)
18    // "There exists a person z who is a friend of x"
19    println!("Example 1: ∃z ∈ Person. Friend(x, z)");
20    println!("  'For each person x, check if there exists a friend z'");
21
22    let friend_pred = TLExpr::pred("Friend", vec![Term::var("x"), Term::var("z")]);
23    let exists_friend = TLExpr::exists("z", "Person", friend_pred);
24
25    match compile_to_einsum_with_context(&exists_friend, &mut ctx.clone()) {
26        Ok(graph) => {
27            println!("  Compiled successfully!");
28            println!("  Tensors: {}", graph.tensors.len());
29            println!("  Nodes: {}", graph.nodes.len());
30            println!("  Graph tensors: {:?}\n", graph.tensors);
31        }
32        Err(e) => println!("  Compilation error: {}\n", e),
33    }
34
35    // Example 2: Exists with conjunction
36    // ∃z ∈ Person. (Friend(x, z) ∧ LivesIn(z, "Tokyo"))
37    // "There exists a person z who is a friend of x AND lives in Tokyo"
38    println!("Example 2: ∃z ∈ Person. (Friend(x, z) ∧ LivesIn(z, Tokyo))");
39    println!("  'For each person x, check if they have a friend in Tokyo'");
40
41    let friend_pred2 = TLExpr::pred("Friend", vec![Term::var("x"), Term::var("z")]);
42    let lives_in_tokyo = TLExpr::pred("LivesIn", vec![Term::var("z"), Term::constant("Tokyo")]);
43    let and_expr = TLExpr::and(friend_pred2, lives_in_tokyo);
44    let exists_friend_tokyo = TLExpr::exists("z", "Person", and_expr);
45
46    match compile_to_einsum_with_context(&exists_friend_tokyo, &mut ctx.clone()) {
47        Ok(graph) => {
48            println!("  Compiled successfully!");
49            println!("  Tensors: {}", graph.tensors.len());
50            println!("  Nodes: {}", graph.nodes.len());
51            for (i, tensor) in graph.tensors.iter().enumerate() {
52                println!("    Tensor {}: {}", i, tensor);
53            }
54            println!();
55        }
56        Err(e) => println!("  Compilation error: {}\n", e),
57    }
58
59    // Example 3: Nested quantifiers
60    // ∃y ∈ City. ∃z ∈ Person. (LivesIn(z, y) ∧ Friend(x, z))
61    // "There exists a city y and a person z such that z lives in y and is a friend of x"
62    println!("Example 3: ∃y ∈ City. ∃z ∈ Person. (LivesIn(z, y) ∧ Friend(x, z))");
63    println!("  'For each person x, check if they have a friend living somewhere'");
64
65    let lives_in = TLExpr::pred("LivesIn", vec![Term::var("z"), Term::var("y")]);
66    let friend = TLExpr::pred("Friend", vec![Term::var("x"), Term::var("z")]);
67    let inner_and = TLExpr::and(lives_in, friend);
68    let exists_z = TLExpr::exists("z", "Person", inner_and);
69    let exists_y_z = TLExpr::exists("y", "City", exists_z);
70
71    match compile_to_einsum_with_context(&exists_y_z, &mut ctx.clone()) {
72        Ok(graph) => {
73            println!("  Compiled successfully!");
74            println!("  Tensors: {}", graph.tensors.len());
75            println!("  Nodes: {}", graph.nodes.len());
76            println!("  This demonstrates reduction over multiple axes:");
77            for (i, node) in graph.nodes.iter().enumerate() {
78                println!("    Node {}: op = {:?}", i, node.op);
79            }
80            println!();
81        }
82        Err(e) => println!("  Compilation error: {}\n", e),
83    }
84
85    println!("=== Compilation Complete ===");
86    println!("\nNote: These examples demonstrate how existential quantifiers");
87    println!("compile to tensor reductions. The actual tensor execution would");
88    println!("happen with a backend like SciRS2.");
89}
01_exists_reduce/main.rs

01_exists_reduce/
main.rs
