[Agda] Modelling term-rewriting systems in Agda

[Aaron Stump]

Hi, Jacques.

The CeTA certified termination checker can also certify confluence by
producing Isabelle proofs:

http://cl-informatik.uibk.ac.at/software/ceta/

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!

Aaron


On Tue, Oct 22, 2013 at 11:22 AM, Jacques Carette <carette at mcmaster.ca>wrote:

> 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?
>
> Jacques
>
>
> On 2013-10-22 11:13 AM, Twan van Laarhoven wrote:
>
>>
>> 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
>>
>>   data _-B->_ {V} : Term V → Term V → Set where
>>     beta      : ∀ {x y} → (ap (lam x) y) -B-> (subst y x)
>>     under-ap₁ : ∀ {x y x'} → (x -B-> x') → (ap x y -B-> ap x' y)
>>     under-ap₂ : ∀ {x y y'} → (y -B-> y') → (ap x y -B-> ap x y')
>>     under-lam : ∀ {x x'} → (x -B-> x') → (lam x -B-> lam x')
>>
>> And here is the parallel beta reduction:
>>
>>   data _-PB->_ {V} : Term V → Term V → Set where
>>     var       : ∀ {v} → var v -PB-> var v -- no reduction in leaf
>>     beta      : ∀ {x y x' y'} → (x -PB-> x') → (y -PB-> y')
>>                                 → (ap (lam x) y) -PB-> (subst y x)
>>     under-ap  : ∀ {x y x' y'} → (x -PB-> x') → (y -PB-> y')
>>                                 → (ap x y -PB-> ap x' y')
>>     under-lam : ∀ {x x'} → (x -PB-> x') → (lam x -PB-> lam x')
>>
>> In the generic case you might try to split the `under` constructors into
>> another data type.
>>
>> For confluence it turned out to be useful to define a datatype:
>>
>>    data CommonReduct {a r s} {A : Set a} (R : Rel A r) (S : Rel A s)
>>                        (x y : A) : Set (a ⊔ r ⊔ s) where
>>       _||_ : {z : A} → R x z → S y z → CommonReduct R S x y
>>
>> then confluence can be expressed as
>>
>>     Confluent : ∀ {a r A} → (R : Rel A r) → Set (a ⊔ r)
>>     Confluent R = ∀ {x y z} → R x y → R x z → CommonReduct R R y z
>>
>> And using Data.Star you can prove lemma's like strong normalization &
>> local confluence imply global confluence.
>>
>>
>> Twan
>>
>> ______________________________**_________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>>
>
> ______________________________**_________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131022/e794052c/attachment.html