Wim Feijen's excercise
73 views
Skip to first unread message
alexk
Nov 29, 2021, 2:23:08 PM11/29/21
to Calculational Mathematics
Hi. I hope everyone is doing well in these strange times.
I am new here, but i was lurking around for some time and one problem posed by Wim Feijen caught my attention. Namely (letter from 21.09.2018):
> Dear Jeremy,
>
> With regard to WF175 the following. It ends where it ends, with a sad remark. The point is that at that time we had no satisfactory treatment of what had to follow the dagger and star story, and that is why it ends where it ends. I thought that, nevertheless, the foregoing 11 pages were nice enough to be recorded and that is why they are recorded.
>
> Many years later we ran into a theorem that should have been applicable in completing WF175 in a satisfactory way. It is recorded in my very last written essay with Netty: AvG183/WF270 . I gladly leave it to our younger calculationists to see whether the findings in this essay can help in completing WF175. I hope this message is a little helpful. Greetings,
>
> Wim.
Recently i was able to compose some calculaiton, that can tackle the problem. I think it is technicaly correct, but I am not quite sure how satisfactory, crisp or nice it is. So i wonder if esteemed members of the group could provide some guidance there?
Thanks in advance.
//////////////////////////////////
Goal of the excercise is:
- to finish WF175, i.e. to establish relation between symmetric and skewed equations for 'star' and 'dagger'
- to see if AvG183/WF270 can help with this
AvG183/WF270 relates two skewed equations for 'star' in three steps:
- spells out equations
- establishes the proof obligation
- discharges it using Galois connections theory
We will follow the pattern.
Here are our equations for 'star', symmetric and skewed:
X: [J v R v X;X => X] and
X: [J v R;X => X]
We assume that their respective strongest solutions P and Q exist, i.e. - spelled out -
(0a) [J => X] ^ [R => X] ^ [X;X => X] => [P => X] for all X
(0b) [J => P]
(0c) [R => P]
(0d) [P;P => P]
(1a) [J => X] ^ [R;X => X] => [Q => X] for all X
(1b) [J => Q]
(1c) [R;Q => Q]
We want to establish that [P == Q].
Let's discover our proof obligation. By mutual implication:
[Q => P]
<= { (1a) }
[J => P] ^ [R;P => P]
<= { predicate calculus }
[J => P] ^ [R => P] ^ [R;P => P]
<= { weakening antecedent on right conjunct }
[J => P] ^ [R => P] ^ [P;P => P]
= { (0b), (0c), (0d) }
true
[P => Q]
<= { (0a) }
[J => Q] ^ [R => Q] ^ [Q;Q => Q]
= { J is identity of compotision on middle conjunct }
[J => Q] ^ [R;J => Q] ^ [Q;Q => Q]
<= { weakening antecedent on middle conjunct}
[J => Q] ^ [R;Q => Q] ^ [Q;Q => Q]
= { (1b), (1c) }
[Q;Q => Q]
One can notice, that the proof obligation is not very differerent from that of AvG183/WF270 ([Q;R => Q])
It is our opportunity to explore something more general:
[Q;T => X]
(we leave Q on the left side, because we want to appeal to (1a))
We define function f by
[f.X == X;T]
And, qouting AvG183/WF27:
Since it is universally disjunctive, it has
an upper Galois adjoint, to be called g.
So we have
(2) [f.X => Y] == [X => g.Y] for all X and Y
The corresponding cancellation rules are
(3a) [X => g.(f.X)] for all X
(3b) [f.(g.Y) => Y] for all X
(End of quote)
[Q;T => X]
= { definition of f }
[f.Q => X]
= { Galois connection (2) }
[Q => g.X)
<= { (1a) with X := g.Q}
[J => g.X] ^ [R;g.X => g.X]
= { Galois connection (2) on both conjuncts }
[f.J => X] ^ [f.(R;g.X) => X]
= { definition of f on both conjuncts }
[J;T => X] ^ [(R;g.X);T => X]
= { J is identity of composition on the left conjunct;
associativity of semi on the second conjunct }
[T => X] ^ [R;(g.X;T) => X]
= { definition of f }
[T => X] ^ [R;f.(g.X) => X]
<= { cancellation rule (3b) with Y := X }
[T => X] ^ [R;X => X]
or
(4) [T v R;X => X] => [Q;T => X]
which nicely incapsulate all conserns about factoring/universal junctivity. One may even call it 'a theorem of utmost importance'.
Now we only have one last step left:
[Q;Q => Q]
<= { (4) with T, X := Q, Q }
[Q => Q] ^ [R;Q => Q]
= { ; (1c) on second conjunct }
true
The alternative is to start from the 'dagger' eqations:
X: [R v X;X => X] and
X: [R v R;X => X]
where dual of (4) for 'dagger' is:
[R;T v R;X => X] => [R+;T => X]
I am new here, but i was lurking around for some time and one problem posed by Wim Feijen caught my attention. Namely (letter from 21.09.2018):
> Dear Jeremy,
>
> With regard to WF175 the following. It ends where it ends, with a sad remark. The point is that at that time we had no satisfactory treatment of what had to follow the dagger and star story, and that is why it ends where it ends. I thought that, nevertheless, the foregoing 11 pages were nice enough to be recorded and that is why they are recorded.
>
> Many years later we ran into a theorem that should have been applicable in completing WF175 in a satisfactory way. It is recorded in my very last written essay with Netty: AvG183/WF270 . I gladly leave it to our younger calculationists to see whether the findings in this essay can help in completing WF175. I hope this message is a little helpful. Greetings,
>
> Wim.
Recently i was able to compose some calculaiton, that can tackle the problem. I think it is technicaly correct, but I am not quite sure how satisfactory, crisp or nice it is. So i wonder if esteemed members of the group could provide some guidance there?
Thanks in advance.
//////////////////////////////////
Goal of the excercise is:
- to finish WF175, i.e. to establish relation between symmetric and skewed equations for 'star' and 'dagger'
- to see if AvG183/WF270 can help with this
AvG183/WF270 relates two skewed equations for 'star' in three steps:
- spells out equations
- establishes the proof obligation
- discharges it using Galois connections theory
We will follow the pattern.
Here are our equations for 'star', symmetric and skewed:
X: [J v R v X;X => X] and
X: [J v R;X => X]
We assume that their respective strongest solutions P and Q exist, i.e. - spelled out -
(0a) [J => X] ^ [R => X] ^ [X;X => X] => [P => X] for all X
(0b) [J => P]
(0c) [R => P]
(0d) [P;P => P]
(1a) [J => X] ^ [R;X => X] => [Q => X] for all X
(1b) [J => Q]
(1c) [R;Q => Q]
We want to establish that [P == Q].
Let's discover our proof obligation. By mutual implication:
[Q => P]
<= { (1a) }
[J => P] ^ [R;P => P]
<= { predicate calculus }
[J => P] ^ [R => P] ^ [R;P => P]
<= { weakening antecedent on right conjunct }
[J => P] ^ [R => P] ^ [P;P => P]
= { (0b), (0c), (0d) }
true
[P => Q]
<= { (0a) }
[J => Q] ^ [R => Q] ^ [Q;Q => Q]
= { J is identity of compotision on middle conjunct }
[J => Q] ^ [R;J => Q] ^ [Q;Q => Q]
<= { weakening antecedent on middle conjunct}
[J => Q] ^ [R;Q => Q] ^ [Q;Q => Q]
= { (1b), (1c) }
[Q;Q => Q]
One can notice, that the proof obligation is not very differerent from that of AvG183/WF270 ([Q;R => Q])
It is our opportunity to explore something more general:
[Q;T => X]
(we leave Q on the left side, because we want to appeal to (1a))
We define function f by
[f.X == X;T]
And, qouting AvG183/WF27:
Since it is universally disjunctive, it has
an upper Galois adjoint, to be called g.
So we have
(2) [f.X => Y] == [X => g.Y] for all X and Y
The corresponding cancellation rules are
(3a) [X => g.(f.X)] for all X
(3b) [f.(g.Y) => Y] for all X
(End of quote)
[Q;T => X]
= { definition of f }
[f.Q => X]
= { Galois connection (2) }
[Q => g.X)
<= { (1a) with X := g.Q}
[J => g.X] ^ [R;g.X => g.X]
= { Galois connection (2) on both conjuncts }
[f.J => X] ^ [f.(R;g.X) => X]
= { definition of f on both conjuncts }
[J;T => X] ^ [(R;g.X);T => X]
= { J is identity of composition on the left conjunct;
associativity of semi on the second conjunct }
[T => X] ^ [R;(g.X;T) => X]
= { definition of f }
[T => X] ^ [R;f.(g.X) => X]
<= { cancellation rule (3b) with Y := X }
[T => X] ^ [R;X => X]
or
(4) [T v R;X => X] => [Q;T => X]
which nicely incapsulate all conserns about factoring/universal junctivity. One may even call it 'a theorem of utmost importance'.
Now we only have one last step left:
[Q;Q => Q]
<= { (4) with T, X := Q, Q }
[Q => Q] ^ [R;Q => Q]
= { ; (1c) on second conjunct }
true
The alternative is to start from the 'dagger' eqations:
X: [R v X;X => X] and
X: [R v R;X => X]
where dual of (4) for 'dagger' is:
[R;T v R;X => X] => [R+;T => X]
Jeremy Weissmann
Nov 29, 2021, 2:59:53 PM11/29/21
to mathmeth
Dear Alex (?),
I confess it has been many years since I have been familiar with the relational calculus — you seem to have some mastery of it! Would you be willing to do a little online presentation of the background of the problem and your proof here for me and anyone else who is interested?
Best,
+j
--
You received this message because you are subscribed the mathmeth.com mailing list.
To unsubscribe from this group, send email to Calculational-Math...@googlegroups.com
For more options, visit this group at http://groups.google.com/group/Calculational-Mathematics?hl=en
---
You received this message because you are subscribed to the Google Groups "Calculational Mathematics" group.
To unsubscribe from this group and stop receiving emails from it, send an email to calculational-math...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/28647480-98d0-466f-9bc4-66d54c193a47n%40googlegroups.com.
alexk
Nov 29, 2021, 6:34:01 PM11/29/21
to Calculational Mathematics
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
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 }
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:
Jeremy Weissmann
Nov 29, 2021, 6:46:24 PM11/29/21
to calculationa...@googlegroups.com
I have no doubts about your work — I simply don’t have enough familiarity with the relational calculus at present to evaluate it. That’s why I asked if you’d be willing to present your work “live”, say on a Zoom call.
On Nov 29, 2021, at 18:34, alexk <krae...@gmail.com> wrote:
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/f59616f6-77f3-4a9a-a31e-38f383e9b4c6n%40googlegroups.com.
Алексей Краевский
Nov 29, 2021, 7:07:10 PM11/29/21
to calculationa...@googlegroups.com
Well... Willingness is one thing, ability to speak English is (sadly) another. :( We can try but I don't know how tolerable it would be.
You received this message because you are subscribed to a topic in the Google Groups "Calculational Mathematics" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/calculational-mathematics/mn6Fy-h7fhs/unsubscribe.
To unsubscribe from this group and all its topics, send an email to calculational-math...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/B5D6561F-83C5-4E31-9A8E-91834D36004B%40gmail.com.
Jeremy Weissmann
Nov 30, 2021, 9:35:50 AM11/30/21
to mathmeth
We can go slow — you write English very well!
To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/CAL3M6kMVOh16RG1FG6T-HS3qoN5NJCKFcjabF4gBKi0vDjjNmA%40mail.gmail.com.
Reply all
Reply to author
Forward
0 new messages