Jeremy, your message echoes my personal doubt about the presented solution. The proof follows closely that of Wim Feijen and Netty van Gasteren, who are indeed the real masters, but their presentation was initially not very transparent for me. In fact I completely failed to understand what AvG183/WF270 is all about until i had solved problem myself.
So it is kind of a part of the question, how to make the proof and its presentation sufficiently clear.
I can provide my personal solution and discuss some difficulties, but I am not sure how much it will help.
//////////////////////////////////////////////////////////////////////////////
We have two equations:
(0) [s v x;x => x] - symmetric equation
and
(1) [s v s;x => x] - skewed equation
We assume they have the strongest solutions p and q respectively.
Can we prove that (0) and (1) have something in common?
We observe:
[s v x;x => x]
= {predicate calculus}
[s => x] ^ [x;x => x]
=> {weakening antecedent in second conjunct, ';' is monotonic }
[s => x] ^ [s;x => x]
= {predicate calculus}
[s v s;x => x]
or (0) => (1). Because one expression is formally weaker than the other, all solutions of (0) are solutions of (1),
and strongest solution of (1) implies all solutions of (0), including the strongest:
(2) [q => p]
Can we prove (1) => (0)? It is not obvious how can we undo weakening. But we can settle for weaker:
(3) [p => q]
My first solution was something like this:
[s v s;q => q]
= {predicate calculus}
[s => q] ^ [s;q => q]
= { magically assume [q;q => q] } (*)
[s => q] ^ [s;q => q] ^ [q;q => q]
=> { cancellation }
[s => q] ^ [q;q => q]
= {predicate calculus}
[s v q;q => q]
which has obvious problem, how to justify the (*)? I was completely unable to address it. Luckily AvG183/WF270 shows the right way.
we can prove it by exploit the fact that q is the strongest solution of (1), or:
(4.0) [s v p;p => p] or 'p is a solution of (0)'
(4.1) [s v x;x => x] => [p => x] or 'p is an extreme of (0)'
(5.0) [s v s;q => q] or 'q is a solution of (1)'
(5.1) [s v s;x => x] => [q => x] or 'q is an extreme of (1)'
so
[p => q]
<= {(4.1)}
[s v q;q => q]
= {predicate calculus}
[s => q] ^ [q;q => q]
= { (5.0) }
[q;q => q]
Indeed [q;q => q] is our proof obligation. Luckily this proof is very straightforward:
[q;q => q]
= { factoring }
[q => q/q]
<= { (5.1) }
[s v s;(q/q) => q/q]
= { factoring }
[s;q v s;(q/q);q => q]
<= { cancellation }
[s;q v s;q => q]
= { (5.0) }
true
Where 'factoring' is [x;y => z] == [x => z/y] and 'cancellation' is [(x/y);y => x]
So by ping pong argument we established [p == q] or that the equations (0) and (1) have the same strongest solution (s+).
Some additional steps are required to show an equivalence of 'star' equations:
[J v s v x;x => x] and
[J v s;x => x]
:
[J v s v x;x => x]
= { predicate calculus }
[J => x]^[s => x]^[x;x => x]
=> { weakening antecedent in third conjunct } (*)
[J => x]^[s => x]^[s;x => x]
=> { cancellation } (**)
[J => x]^[s;x => x]
= { predicate calculus }
[J v s;x => x]
We already know how 'undo' the weakening in (*) to undo (**) we have to show:
[J => x]^[s;x => x]
= { '^' is idempotent }
[J => x]^[s;x => x]^[s;x => x]
=> { weakening antecedent in second conjunct }
[J => x]^[s;J => x]^[s;x => x]
= {J is identity of composition }
[J => x]^[s => x]^[s;x => x]
and that is all.
/////////////////////////////////////////////////////////////
Some random observations:
- all in all the problem is not very difficult, it is very strange that it haven't been solved for almost 20 years
- in particular it is unclear why AvG183/WF270 discuss two skewed solution instead of skewed and symmetric
- connection of 'dagger' equations is much more obvious than between 'star' equations (when we weaken 'star' equation [J => x]^[s => x]^[x;x => x] => [J => x]^[s;x => x] we have to restore two terms [x;x => x] and [s => x])
- discussion in AvG183/WF270 revolves around importance of universal junctivity, which is somewhat strange and divert us form the real goal: in relational calculus existence of factors is an axiom, but universal junctivity of composition (';') is a theorem
понедельник, 29 ноября 2021 г. в 22:59:53 UTC+3, Jeremy Weissmann: