Hi David,
> On 26 Sep 2018, at 19:47, David Fetter <david@fetter.org> wrote:
>
>> Invalidating operations are "INSERT(t) and UPDATE(t.b, t.n)".
>
> So would DELETE(t), assuming n can be negative.
Oops, right you are. Bug in my implementation :-)
> Is there some interesting and fairly easily documented subset of
> ASSERTIONs that wouldn't have the "can't prove" property?
We can certainly know at the time the ASSERTION is created if we
can use the transition table optimisation, as that relies upon
the expression being written in such a way that a key can be
derived for each expression.
We could warn or disallow the creation on that basis. Ceri & Widom
mention this actually in their papers, and their view is that most
real-world use cases do indeed allow themselves to be optimised
using the transition tables.
-Joe