Rewriting Systems / Canonical Forms Engineer (Delay Calculus Normal Forms)

About the Role

Our platform relies on a custom delay calculus: we compose delay bricks into delay polynomials/operators, evaluate them on windows, and use them to align/cancel shared components. In practice, the same mathematical object can appear in many syntactic forms—different compositions, factorizations, or rewrite sequences.

If we can’t canonicalize these expressions, we get duplicated work, exploding search spaces, inconsistent results across implementations, brittle diagnostics, and proofs/specs that can’t pin down semantics cleanly.

This role owns the rewrite engine and canonical forms that make the delay calculus stable, comparable, and testable.

What You’ll Own

• A rewrite system for the delay calculus: implementable rewrite rules that preserve semantics (not just on paper).
• Canonical forms / normal forms: deterministic representations up to the equivalences we care about (associativity/identities, commutation conditions, window-conditional rewrites).
• Practical confluence/termination strategy: what can be made confluent/terminating, what can’t, and bounded strategies with fallbacks.
• Equivalence checking: fast “are these two expressions the same (under our rules)?” with optional traces/certificates.
• Rewrite-aware QA tooling: property tests, counterexample generators, and CI gates that prevent simplifier drift.

What You’ll Do

• Define expression syntax + semantics: ASTs for delay bricks/polynomials and the semantics they denote (time-domain and/or spectral).
• Design rewrite rules: identities, simplifications, factoring/expansion policies, and domain-specific rules tied to window assumptions (with explicit “only valid if…” guards).
• Build a canonicalizer: deterministic normal-form pipeline (parse → normalize → order → simplify → canonical print/hash).
• Handle conditional rewrites safely: record when a rule was used under assumption A; allow abstain/annotation when A is not guaranteed.
• Prove or test correctness: where full proofs aren’t feasible, use semantic equivalence testing at scale (randomized windows, adversarial cases).
• Integrate with proof/spec and validation teams: align rules with Rocq/TLA+ targets and golden tests.

Concrete Deliverables

• A Delay Expression IR (AST + printer) with stable formatting and hashing.
• A rewrite rule library with metadata: rule name, preconditions, priority/cost, unconditional vs window-conditional.
• A canonical form definition (doc + implementation): “two expressions are equivalent iff their canonical forms match (under assumptions X).”
• An equivalence checker with optional rewrite traces for debugging/audits.
• A regression shield: property-based tests + a golden corpus ensuring canonicalization stability across releases.

Required Qualifications

• Strong experience with term rewriting systems, symbolic algebra, compiler-like transformations, or theorem-prover-adjacent engineering.
• Ability to reason about equivalence relations, normal forms, invariants, and practical limits of confluence/termination.
• Solid implementation skills in at least one systems-friendly language (Rust/C++/OCaml/Haskell) or Python with disciplined architecture.
• Comfort building deterministic tooling: stable ordering, reproducible outputs, careful semantic testing strategies.

Preferred Qualifications

• Experience with Knuth–Bendix, critical pair analysis, or practical confluence tooling.
• Familiarity with e-graphs/egg, SMT rewriting, or CAS internals.
• Experience collaborating with formal methods teams (extracting rewrite lemmas, producing certificates).
• Signal processing context familiarity (delay operators, frequency-domain evaluation) helpful but not required.

How You’ll Be Measured (First 60–90 Days)

• You ship a working canonicalizer for a meaningful subset of the delay calculus that is deterministic and adopted by the team.
• Deduplication improves measurably (fewer duplicates, smaller search spaces, more stable results).
• CI catches at least one real regression related to simplifier/canonicalization drift.
• The rule set and assumptions are documented clearly enough that engineers stop arguing about “which form is right.”

Working Style

• You treat “simplify” as a specification problem, not a convenience function.
• You prefer deterministic, explainable transforms over clever but opaque heuristics.
• You build engines that can say: “I rewrote this under assumption A; if A fails, don’t trust this equivalence.”

Title & Level

Rewriting Systems / Canonical Forms Engineer (Delay Calculus Normal Forms) (senior IC; can scale to Staff/Principal if owning IR + equivalence infrastructure), partnering with applied math/DSP, proof/spec, and validation teams.