Data.Comp.TermRewriting

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

Documentation

type RPS f g = Hom f g

This type represents recursive program schemes.

type Var = Int

This type represents variables.

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

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]

This type represents term rewriting systems (TRSs) from signature f to signature g over variables of type v.

type Step t = t -> Maybe t

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

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

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))

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))

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)

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)

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 t

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)

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)

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.

reduce :: Step t -> t -> t

This function applies the given reduction step repeatedly until a normal form is reached.