Gradient Optimization Circuit Search Jacobians Stream Calculus Rewriting Multi-Dim Streams Coupled SDEs JAX & JIT Engineering Examples

Rewriting System

Define symbolic transformation rules and apply them to equations and circuits.

Concepts

The rewriting system has three layers:

  1. Rewrite rules — individual pattern => result transformations
  2. Rule groups — bundles of rules sharing a grammar and evaluator
  3. Strategies — orchestrate which groups to apply and in what order

Defining Rules

A rule specifies a source pattern, a target pattern, and an optional condition:

from gimle.asgard.core.rewriting.rewrite_rule import RewriteRule

rule = RewriteRule(
    "INTEGRAL_DISTRIBUTION",
    "int([X] + [Y], [Z]) => int([X], [Z]) + int([Y], [Z])",
)

Placeholders like [X], [Y], [Z] match and capture any subtree. Both sides of => must be valid expressions in their respective grammars.

Conditions

Conditions filter matches based on properties of captured subtrees:

RewriteRule(
    "ADDITIVE_IDENTITY",
    "[X] + [Y] => [Y]",
    "is_zero([X])",
)

Available predicates for equations:

Predicate Description
is_zero([X]) True if [X] is numeric zero.
is_one([X]) True if [X] is numeric one.
is_number([X]) True if [X] is a numeric literal.
is_variable([X]) True if [X] is an identifier.
is_dimension([X]) True if [X] is a dimension (x, y, z, t).
is_equal([X], [Y]) True if [X] and [Y] match structurally.

Combine with && (and), || (or), ! (not), and comparisons (=, !=, <, >):

RewriteRule(
    "DIFF_INDEPENDENT",
    "diff([X], [Y]) => 0",
    "([X] != [Y]) && is_dimension([X])",
)

Rule Groups

A rule group bundles related rules with their grammar and evaluator:

from gimle.asgard.core.rewriting.rewrite_rule_group import RewriteRuleGroup
from gimle.asgard.equation.equation_grammar import (
    EQUATIONAL_GRAMMAR,
    EQUATIONAL_CONDITIONAL_GRAMMAR,
)
from gimle.asgard.equation.equation_rewrite_rules import (
    ConditionalEvaluator,
    ArithmeticEvaluator,
)

my_rules = RewriteRuleGroup(
    name="my_physics_rules",
    source_rule_grammar=EQUATIONAL_GRAMMAR,
    target_rule_grammar=EQUATIONAL_GRAMMAR,
    conditional_grammar=EQUATIONAL_CONDITIONAL_GRAMMAR,
    rules=[
        RewriteRule("RULE_A", "[X] + 0 => [X]"),
        RewriteRule("RULE_B", "0 + [X] => [X]"),
    ],
    rewrite_term_identifier="REWRITE_TERM",
    conditional_evalutor=ConditionalEvaluator,
    term_evaluator=ArithmeticEvaluator,
)

Register the group to make it available by name:

from gimle.asgard.core.rewriting.rewrite_rule_registry import RewriteRuleRegistry

RewriteRuleRegistry.register(my_rules)

Built-in Groups

Equation rules:

Group Description
eq_integration_rules Integration and differentiation laws.
eq_elimination_rules Derivative/integral cancellation.
eq_ring_rules Algebraic ring properties.
eq_full All equation rules combined.

Circuit rules:

Group Description
circuit_category_rules Composition associativity, identity.
circuit_monoidal_rules Tensor product laws.
circuit_atomic_rules Add/multiply commutativity, identity elements.
circuit_trace_rules Trace naturality, cyclic properties.
circuit_compose_rules Power series composition identity and associativity.
circuit_sde_rules Constant drift/diffusion specializations.
circuit_full All circuit rules combined (excludes circuit_sde_rules).

Cross-grammar rules:

Group Description
equation_to_circuit Compile equation to circuit.
circuit_to_equation Decompile circuit to equation.

Applying Rules

Via the High-Level API

from gimle.asgard.api import GimleEquation

eq = GimleEquation.from_string("diff(int(f, x), x)")

# Apply a specific group (repeats until no more rules match)
simplified, rules_applied = eq.rewrite("eq_elimination_rules")
# Result: f

# Apply all equation rules
simplified, rules_applied = eq.rewrite("eq_full")

Single Step vs Repeated

from gimle.asgard.equation.equation import Equation

eq = Equation.from_string("(f + 0) + (g * 1) = h")

# Single step: applies one round of rewriting
new_eq, applied = eq.step_rewrite("eq_ring_rules")

# Full rewrite: repeats until fixed point
final_eq, all_applied = eq.full_rewrite("eq_ring_rules")
# Result: f + g = h

Rule Application Order

Deduction Engine

For multi-step transformations (e.g. equation-to-circuit compilation), the deduction engine orchestrates tactics via strategies.

Architecture

Strategy
  └── decides which Tactic to apply next
        └── Tactic produces a DeductionStep
              └── Step is recorded in a DeductionTrace

Built-in Tactics

Tactic Description
term_rewrite_equational_rules Apply all equation rewrite rules (eq_full).
term_rewrite_equational_integration_rules Apply integration/differentiation rules.
term_rewrite_equational_ring_rules Apply ring simplification.
term_rewrite_equational_elimination_rules Apply elimination rules.
isolate_variables Solve for variables in equations.
translate_to_circuit Compile equation to circuit (with trace wiring).
translate_to_circuit_no_trace Compile equation to circuit (without trace).

Using a Strategy

from gimle.asgard.core.deduction.trace import DeductionTrace
from gimle.asgard.core.deduction.strategy import DeductionStrategyRegistry
from gimle.asgard.equation.equation import Equation

eq = Equation.from_string("int(f, x) = g")
trace = DeductionTrace(eq, name="compilation")
strategy = DeductionStrategyRegistry.get("equation_to_network")

while strategy.next_step(trace):
    step = trace.steps[-1]
    print(f"Applied: {step.tactic.name}")

circuit = trace.current_tree()

Debugging

Check Which Rules Match

from gimle.asgard.core.rewriting.rewrite_term import rewrite_term
from gimle.asgard.core.rewriting.rewrite_rule_registry import RewriteRuleRegistry

eq = Equation.from_string("diff(int(f, x), y) = g")
rule_group = RewriteRuleRegistry.get("eq_elimination_rules")

rewritten, applied = rewrite_term(eq.trees[0], rule_group)
if applied:
    print(f"Matched: {applied}")
else:
    print("No rules matched")

Inspect Applied Rules

eq = Equation.from_string("(a + 0) * 1 = b")
final, all_iterations = eq.full_rewrite("eq_ring_rules")

for i, rules in enumerate(all_iterations):
    print(f"Iteration {i}: {rules}")

Common Pitfalls