Hi David, > On 26 Sep 2018, at 19:47, David Fetter <da...@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
