DRMacIver's Notebook
Notation for test-case reducers
Notation for test-case reducers
A thing I’ve been noticing recently is that it’s really useful to have compact notation for describing things. Usually this is equivalent to primivitives + some combinators.
One thing that I think it would be useful to have such a notation for is (greedy) test-case reduction passes. They combine pretty well, and it makes it useful to discuss various things.
For example, if you have reducers \(A\), \(B\), you can define the reducer \(AB\) which runs \(A\), then runs \(B\) on its result. You can also define the reducer \(A^+\) which runs \(A\) to a fixed point.
Another interesting combinator is \(/\). \(A / B\) runs \(A\), then runs \(B\) if \(A\) didn’t do anything..
There are a bunch of really basic algebraic relations that hold, like composition and \(/\) are associative, and \((A^+)^+ = A^+\), but not a huge amount beyond that.
A bunch of interesting questions about test-case reduction can be compactly expressed in this notation though. For example, suppose you want to reduce to something that is a fixed point of both \(A\) and \(B\). You could do \((AB)^+\), but you could also do \((A^+B^+)^+\), and it’s quite natural to do this in some contexts. My suspicion, which I’ve yet to verify, is that it’s almost never the right thing to do.
You can kinda regard the quadratic mode failure of greedy search as an instance of this problem: If \(\delta_i\) is the operation that deletes the element at position \(i\), the correct pass to run for greedy deletion is \((\delta_0^+ \ldots \delta_n^+)^+\), but if you start again at the beginning every time you succeed you are running \((\delta_0 / \ldots / \delta_n)^+\).