[Agda] Modelling term-rewriting systems in Agda
Jacques Carette
carette at mcmaster.ca
Tue Oct 22 17:22:10 CEST 2013
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
More information about the Agda
mailing list