Re: [isabelle] Well-foundedness of Relational Composition



Hi Tjark / Christian,

I'm confused by the notation here.
Firstly, R O S:
doesn't this mean, that where (a, b) in S and (b, c) in R, then (a, c) in R 0 S ?
Secondly, wf R - doesn't this mean that there is no infinite chain
 ..... an ... a1 a0
such that each (a_{n+1}, a_n) in R ?

So using this notation,
let R = (n, n+1) for all n (naturals)
let S = (n+1, n) for all n
Then R O S = {(n, n) | n >= 1}
S O R = {(n, n) | n >= 0}

Anyhow, in
http://users.cecs.anu.edu.au/~jeremy/isabelle/2005/gen/WfUn.{thy,ML}
I have proofs of
 "(s O r <= r O s^*) --> wf r --> wf (r O s^*)"
and  "(s O r <= r O s^*) --> wf r --> wf (s^* O r)"
(they're called
wf_movl_comp and wf_movl_comp2)
(obviously, wf (r O s) = wf (s O r))
(proofs are in Isabelle2005)

I now see in that file I have a note:

(* note - can't get result
  "(r O s <= s^* O r) ==> wf r ==> wf (s^* O r)", eg
  E = {(x, y) | x >= 0, 0 <= y <= x}
  (x, y) >_r (x, y+1) - so r is wf
  (x, y) >_s (x+1, y) - so r O s, s O r not wf
  In r O s, (x, y) > (x+1, y+1) but only if y < x
  In s O r, (x, y) > (x+1, y+1) always
  So (r O s <= s O r) *)

As for the paper proof below - what does it mean? It seems to correspond to the theorem stated if
RS RS ...
means x0 >R x1 >S x2 >R x3 >S x4 ...
in which case wf R means R R R R ... is not possible, but then
haven't you actually applied SR <= RS, not RS <= SR?

Even if I've got conused somewhere above I can't see how you and I could have both proved results, in Isabelle, one of which seems to be wrong. Has the definition of wf or of O changed since 2005?

Cheers,

Jeremy


On 27/04/15 19:58, Christian Sternagel wrote:
Dear Tjark and Tobias,

This is my first impression: I've definitely seen this fact applied
(although implicitly) and think it counts as, as they say, "folklore".

Especially so, since the paper "proof" is trivial ;):

Assume: RS RS RS RS RS RS ...
Rearrange into: R SR SR SR SR SR ...
Apply "RS <= SR": R RS RS RS RS RS ...
Repeat this process to obtain: R R R R R R ...
Contradiction.

I checked IsaFoR by hypersearch but didn't find anything that looks
alike immediately. That is, I'm not aware of any formalized proof.


After investigating a little further, I found some relevant literature.
Commutation has been investigated by Rosen [3], but as far as I can tell
on a short glance only w.r.t. confluence. Bachmair and Dershowitz [2]
pronounce "RS <= SR" as "R *commutes over* S" (whereas "commutation"
without "over" would result in a "diamond" diagram). And Geser [1]
(which was the reference I started from) at least comments about
something similar to your lemma on page 38:

   If R is Noetherian, it is more convenient to check for strict
   local commutation than for quasi-commutation: They are
   equivalent, and checking for strict local commutation is
   less complex ...

But also here I did not find a proof by skimming through. Maybe a closer
look would reveal something.

[1] Alfons Geser. Relative Termination. PhD-Thesis. 1990.
[2] Leo Bachmair, Nachum Dershowitz. Commutation, Transformation, and
Termination. CADE. 1986. http://dx.doi.org/10.1007/3-540-16780-3_76
[3] Barry K. Rosen. Tree-Manipulating Systems and Church-Rosser
Theorems. J. ACM (JACM) 20(1):160-187 (1973).
http://doi.acm.org/10.1145/321738.321750

cheers

chris

On 04/26/2015 03:51 PM, Tjark Weber wrote:
Tobias,

On Sun, 2015-04-26 at 09:24 +0200, Tobias Nipkow wrote:
I'll be happy to include it in HOL/Wellfounded.thy if you do me the
favour of
getting rid of metis - it is not available at that theory yet.

Certainly. A proof that uses only simp and blast is attached.

Maybe somebody can also think of a more telling name suffix than
"_compatible".

This was inspired by the existing lemma wf_union_compatible. Of course,
it is a terrible name.

Best,
Tjark

===== 8< =====

lemma wf_relcomp_compatible:
   assumes "wf R" and "R O S \<subseteq> S O R"
   shows "wf (S O R)"
proof (rule wfI_pf)
   fix A assume A: "A \<subseteq> (S O R) `` A"
   {
     fix n have "(S ^^ n) `` A \<subseteq> R `` (S ^^ Suc n) `` A"
     proof (induction n)
       case 0 show ?case
         using A by (simp add: relcomp_Image)
     next
       case (Suc n)
       then have "S `` (S ^^ n) `` A \<subseteq> S `` R `` (S ^^ Suc n)
`` A"
         by (simp add: Image_mono)
       also have "\<dots> \<subseteq> R `` S `` (S ^^ Suc n) `` A"
         using assms(2) by (simp add: Image_mono O_assoc
relcomp_Image[symmetric] relcomp_mono)
       finally show ?case
         by (simp add: relcomp_Image)
     qed
   }
   then have "(\<Union>n. (S ^^ n) `` A) \<subseteq> R `` (\<Union>n. (S
^^ n) `` A)"
     by blast
   then have "(\<Union>n. (S ^^ n) `` A) = {}"
     using assms(1) by (simp only: wfE_pf)
   then show "A = {}"
     using relpow.simps(1) by blast
qed








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.