[Agda] Modelling term-rewriting systems in Agda
Twan van Laarhoven
twanvl at gmail.com
Tue Oct 22 17:13:40 CEST 2013
On 22/10/13 15:33, Jacques Carette wrote:
> On 2013-10-22 10:24 AM, Sergei Meshveliani wrote:
>> Do you mean
>> to formulate in Agda
>> 1) a notion of what is a set of _rewriting rules_
>> (or `equations'),
>> 2) a notion of a rule (equation) set being confluent,
>> and so on
>> ?
>
> Yes. And to be able to effectively work with these notions. Just encoding is
> easy enough.
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
More information about the Agda
mailing list