[Agda] Modelling term-rewriting systems in Agda

[Christian Sternagel]

Dear Jacques (and thanks Aaron for pointing to IsaFoR/CeTA!),

Indeed, IsaFoR is an Isabelle/HOL formalization of many facts on 
first-order term rewritng (more concretely, almost all termination 
methods that are used in termination tools like AProVE, CiME, Jambox, 
Matchbox, Muterm, TPA, TTT2, ... nowadays; and most theorems of the 
first 7 Chapters of the book "Term Rewriting and All That" by Baader and 
Nipkow), and constantly growing. This also includes the cirtical pair 
lemma and Knuth-Bendix completion.

In total there are 3 projects on formalizing rewriting (initially mostly 
on termination) I know of:

   - A3PAT: http://a3pat.ensiie.fr/
   - CoLoR: http://color.inria.fr/
   - IsaFoR: http://cl-informatik.uibk.ac.at/software/ceta/

the first two using Coq and the latter Isabelle/HOL.

I'm sure that all of them include many ideas that can be reused in Agda.

cheers

chris

On 10/23/2013 01:08 AM, Aaron Stump wrote:
> 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
> <mailto: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 <mailto: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 <mailto: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
>