<div dir="ltr"><div>Hi, Jacques.<br></div><div><br></div><div>The CeTA certified termination checker can also certify confluence by producing Isabelle proofs:</div><div><br></div><div><a href="http://cl-informatik.uibk.ac.at/software/ceta/">http://cl-informatik.uibk.ac.at/software/ceta/</a></div>
<div><br></div><div>The logic is different, of course, but probably one could get many ideas from looking at their formalization, though be careful: it is over 100kloc of Isabelle!</div><div><br></div><div>Aaron</div></div>
<div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Oct 22, 2013 at 11:22 AM, Jacques Carette <span dir="ltr"><<a href="mailto:carette@mcmaster.ca" target="_blank">carette@mcmaster.ca</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Thank you, this was exactly the kind of example I was looking for. Is your complete example available somewhere? Or would you mind sharing it?<span class="HOEnZb"><font color="#888888"><br>
<br>
Jacques</font></span><div class="HOEnZb"><div class="h5"><br>
<br>
On 2013-10-22 11:13 AM, Twan van Laarhoven wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
As a somewhat related data point, a while ago I proved confluence of beta reduction for untyped lambda calculus (as I am sure many others have as well). To encode the rewrite rules I used a data type to represent the reduction relation. Here is single step beta reduction<br>
<br>
data _-B->_ {V} : Term V → Term V → Set where<br>
beta : ∀ {x y} → (ap (lam x) y) -B-> (subst y x)<br>
under-ap₁ : ∀ {x y x'} → (x -B-> x') → (ap x y -B-> ap x' y)<br>
under-ap₂ : ∀ {x y y'} → (y -B-> y') → (ap x y -B-> ap x y')<br>
under-lam : ∀ {x x'} → (x -B-> x') → (lam x -B-> lam x')<br>
<br>
And here is the parallel beta reduction:<br>
<br>
data _-PB->_ {V} : Term V → Term V → Set where<br>
var : ∀ {v} → var v -PB-> var v -- no reduction in leaf<br>
beta : ∀ {x y x' y'} → (x -PB-> x') → (y -PB-> y')<br>
→ (ap (lam x) y) -PB-> (subst y x)<br>
under-ap : ∀ {x y x' y'} → (x -PB-> x') → (y -PB-> y')<br>
→ (ap x y -PB-> ap x' y')<br>
under-lam : ∀ {x x'} → (x -PB-> x') → (lam x -PB-> lam x')<br>
<br>
In the generic case you might try to split the `under` constructors into another data type.<br>
<br>
For confluence it turned out to be useful to define a datatype:<br>
<br>
data CommonReduct {a r s} {A : Set a} (R : Rel A r) (S : Rel A s)<br>
(x y : A) : Set (a ⊔ r ⊔ s) where<br>
_||_ : {z : A} → R x z → S y z → CommonReduct R S x y<br>
<br>
then confluence can be expressed as<br>
<br>
Confluent : ∀ {a r A} → (R : Rel A r) → Set (a ⊔ r)<br>
Confluent R = ∀ {x y z} → R x y → R x z → CommonReduct R R y z<br>
<br>
And using Data.Star you can prove lemma's like strong normalization & local confluence imply global confluence.<br>
<br>
<br>
Twan<br>
<br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</blockquote>
<br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>