Originator of the representation and lead for its implementation and evaluation.
Correspondence Matrices / implementation
Correspondence Matrices in code.
Working code, independent checks and measured decisions.
I developed Correspondence Matrices and built exact Boolean workflows around the representation. The public implementation and audit show where the evaluator is promising, where complete calls cost more, and when another method is the better engineering choice.
Public implementation · Reproducible results · Independent checks
Interested in the original representation? Explore CM theory and the paper →
Watch the films: Film 1: CM Overview Video · Film 2: CM Benchmarking Video
Film 2 · 5:12
CM Benchmarking Video
An engineering account of exact-computation improvements across Correspondence Matrices, common-subexpression elimination, BitSet and related methods.
Click the picture to play. Full screen and volume are available in the controls.
Open the video file ↗2n canonical truth assignments5 documented comparison paths123 default reproducible seedPython implementation & reports
Python compilers, benchmark tooling, generated reports and independent truth-table checks.
An original structural representation became runnable, comparable and independently checkable.
A public repository, published audit and independently checked examples.
01 / The decision
When does a new representation earn its place?
A new algorithmic idea becomes useful only when it produces the required answer correctly and its full workflow holds up against alternatives. The work here turns a mathematical representation into runnable compilers and evaluators, then compares their behavior under stated workloads.
The evaluation keeps construction, computation and checking visible so that a fast inner operation is not mistaken for a fast complete call. The companion theory page explains how the representation works.
02 / From representation to implementation
01Expression AST
One shared symbolic representation
→02Align & combine
Broadcast sub-expressions by variable
→03Materialize
Construct the canonical matrix once
→04Validate
Compare with independent truth-table evaluation
The lazy path aligns sub-expressions through size-one axes and broadcasting, then materializes the canonical matrix at the end. Eager construction remains available as a fallback.
03 / The computational boundary
Make the scale visible.
Keep the claim narrow.
The full truth space grows exponentially with the number of variables. The benchmark driver therefore records compilation and evaluation work by operation and backend, and documents when particular validation paths are capped or skipped.
State-space scale
Truth assignments grow as 2n.
Reproducible comparison
The driver generates Boolean expressions and compares the CM path with SymPy logic simplification, an in-repository ROBDD, optional dd.autoref, Espresso and a canonical BDD-to-SOP baseline. Seeded runs write per-trial CSVs and summaries, collected through the published results and audit site.
Correctness outside the clock
Backend results are checked against explicit vectorized truth-table evaluation outside the timing windows. This separates “did it compute the same function?” from “how long did this specific implementation take?”
Implementation evidence
The check and the measurement boundary.
A worked expression shows independent agreement; the audit separates evaluator measurements from complete-call behavior.
A worked example shows the matrix compiler and an independent truth-table check arriving at the same result.
Open full-size view ↗
The audit shows where the current computation is promising—and where wrapper overhead still needs improvement.
Open full-size view ↗Scope & limitations
What this work
does not claim.
The published measurements compare particular implementations, operations and problem sizes. They are not evidence of a general performance advantage over symbolic simplifiers or decision diagrams.
Correctness checks support the implemented cases; they are not a formal proof of every possible implementation or use.
Inspect the evidence
Read it. Run it.
Check the boundary.
Useful when
Your team needs to turn an unconventional algorithmic claim into runnable software, reproducible comparisons and explicit correctness checks.
Explore technical validation →