Portability | non-portable (GHC Extensions) |
---|---|

Stability | experimental |

Maintainer | Patrick Bahr <paba@diku.dk> |

This module defines term rewriting systems (TRSs) using compositional data types.

- type RPS f g = Hom f g
- type Var = Int
- type Rule f g v = (Context f v, Context g v)
- type TRS f g v = [Rule f g v]
- type Step t = t -> Maybe t
- type BStep t = t -> (t, Bool)
- matchRule :: (Ord v, EqF f, Eq a, Functor f, Foldable f) => Rule f g v -> Cxt h f a -> Maybe (Context g v, Map v (Cxt h f a))
- matchRules :: (Ord v, EqF f, Eq a, Functor f, Foldable f) => TRS f g v -> Cxt h f a -> Maybe (Context g v, Map v (Cxt h f a))
- appRule :: (Ord v, EqF f, Eq a, Functor f, Foldable f) => Rule f f v -> Step (Cxt h f a)
- appTRS :: (Ord v, EqF f, Eq a, Functor f, Foldable f) => TRS f f v -> Step (Cxt h f a)
- bStep :: Step t -> BStep t
- parTopStep :: (Ord v, EqF f, Eq a, Foldable f, Functor f) => TRS f f v -> Step (Cxt h f a)
- parallelStep :: (Ord v, EqF f, Eq a, Foldable f, Functor f) => TRS f f v -> Step (Cxt h f a)
- reduce :: Step t -> t -> t

# Documentation

type Rule f g v = (Context f v, Context g v)Source

This type represents term rewrite rules from signature `f`

to
signature `g`

over variables of type `v`

type TRS f g v = [Rule f g v]Source

This type represents term rewriting systems (TRSs) from signature
`f`

to signature `g`

over variables of type `v`

.

type Step t = t -> Maybe tSource

This type represents a potential single step reduction from any input.

type BStep t = t -> (t, Bool)Source

This type represents a potential single step reduction from any
input. If there is no single step then the return value is the
input together with `False`

. Otherwise, the successor is returned
together with `True`

.

matchRule :: (Ord v, EqF f, Eq a, Functor f, Foldable f) => Rule f g v -> Cxt h f a -> Maybe (Context g v, Map v (Cxt h f a))Source

This function tries to match the given rule against the given term (resp. context in general) at the root. If successful, the function returns the right hand side of the rule and the matching substitution.

matchRules :: (Ord v, EqF f, Eq a, Functor f, Foldable f) => TRS f g v -> Cxt h f a -> Maybe (Context g v, Map v (Cxt h f a))Source

This function tries to match the rules of the given TRS against the given term (resp. context in general) at the root. The first rule in the TRS that matches is then used and the corresponding right-hand side as well the matching substitution is returned.

appRule :: (Ord v, EqF f, Eq a, Functor f, Foldable f) => Rule f f v -> Step (Cxt h f a)Source

This function tries to apply the given rule at the root of the
given term (resp. context in general). If successful, the function
returns the result term of the rewrite step; otherwise `Nothing`

.

appTRS :: (Ord v, EqF f, Eq a, Functor f, Foldable f) => TRS f f v -> Step (Cxt h f a)Source

This function tries to apply one of the rules in the given TRS at
the root of the given term (resp. context in general) by trying each
rule one by one using `appRule`

until one rule is applicable. If no
rule is applicable `Nothing`

is returned.

bStep :: Step t -> BStep tSource

This is an auxiliary function that turns function `f`

of type
`(t -> Maybe t)`

into functions `f'`

of type `t -> (t,Bool)`

. `f' x`

evaluates to `(y,True)`

if `f x`

evaluates to `Just y`

, and to
`(x,False)`

if `f x`

evaluates to `Nothing`

. This function is useful
to change the output of functions that apply rules such as `appTRS`

.

parTopStep :: (Ord v, EqF f, Eq a, Foldable f, Functor f) => TRS f f v -> Step (Cxt h f a)Source

This function performs a parallel reduction step by trying to
apply rules of the given system to all outermost redexes. If the given
term contains no redexes, `Nothing`

is returned.

parallelStep :: (Ord v, EqF f, Eq a, Foldable f, Functor f) => TRS f f v -> Step (Cxt h f a)Source

This function performs a parallel reduction step by trying to
apply rules of the given system to all outermost redexes and then
recursively in the variable positions of the redexes. If the given
term does not contain any redexes, `Nothing`

is returned.