# Module Rewriting.Strategy

Library for representation and computation of reductions on first-order terms and representation of reduction strategies.

Author: Jan-Hendrik Matthes

Version: February 2020

## Summary of exported operations:

 ```showReduction :: (a -> String) -> Reduction a -> String```    Transforms a reduction into a string representation. ```redexes :: Eq a => [(Term a,Term a)] -> Term a -> [[Int]]```    Returns the redex positions of a term according to the given term rewriting system. ```seqRStrategy :: Eq a => ([Int] -> [Int] -> Ordering) -> [(Term a,Term a)] -> Term a -> [[Int]]```    Returns a sequential reduction strategy according to the given ordering function. ```parRStrategy :: Eq a => ([Int] -> [Int] -> Ordering) -> [(Term a,Term a)] -> Term a -> [[Int]]```    Returns a parallel reduction strategy according to the given ordering function. ```liRStrategy :: Eq a => [(Term a,Term a)] -> Term a -> [[Int]]```    The leftmost innermost reduction strategy. ```loRStrategy :: Eq a => [(Term a,Term a)] -> Term a -> [[Int]]```    The leftmost outermost reduction strategy. ```riRStrategy :: Eq a => [(Term a,Term a)] -> Term a -> [[Int]]```    The rightmost innermost reduction strategy. ```roRStrategy :: Eq a => [(Term a,Term a)] -> Term a -> [[Int]]```    The rightmost outermost reduction strategy. ```piRStrategy :: Eq a => [(Term a,Term a)] -> Term a -> [[Int]]```    The parallel innermost reduction strategy. ```poRStrategy :: Eq a => [(Term a,Term a)] -> Term a -> [[Int]]```    The parallel outermost reduction strategy. ```reduce :: Eq a => ([(Term a,Term a)] -> Term a -> [[Int]]) -> [(Term a,Term a)] -> Term a -> Term a```    Reduces a term with the given strategy and term rewriting system. ```reduceL :: Eq a => ([(Term a,Term a)] -> Term a -> [[Int]]) -> [[(Term a,Term a)]] -> Term a -> Term a```    Reduces a term with the given strategy and list of term rewriting systems. ```reduceBy :: Eq a => ([(Term a,Term a)] -> Term a -> [[Int]]) -> [(Term a,Term a)] -> Int -> Term a -> Term a```    Reduces a term with the given strategy and term rewriting system by the given number of steps. ```reduceByL :: Eq a => ([(Term a,Term a)] -> Term a -> [[Int]]) -> [[(Term a,Term a)]] -> Int -> Term a -> Term a```    Reduces a term with the given strategy and list of term rewriting systems by the given number of steps. ```reduceAt :: Eq a => [(Term a,Term a)] -> [Int] -> Term a -> Term a```    Reduces a term with the given term rewriting system at the given redex position. ```reduceAtL :: Eq a => [(Term a,Term a)] -> [[Int]] -> Term a -> Term a```    Reduces a term with the given term rewriting system at the given redex positions. ```reduction :: Eq a => ([(Term a,Term a)] -> Term a -> [[Int]]) -> [(Term a,Term a)] -> Term a -> Reduction a```    Returns the reduction of a term with the given strategy and term rewriting system. ```reductionL :: Eq a => ([(Term a,Term a)] -> Term a -> [[Int]]) -> [[(Term a,Term a)]] -> Term a -> Reduction a```    Returns the reduction of a term with the given strategy and list of term rewriting systems. ```reductionBy :: Eq a => ([(Term a,Term a)] -> Term a -> [[Int]]) -> [(Term a,Term a)] -> Int -> Term a -> Reduction a```    Returns the reduction of a term with the given strategy, the given term rewriting system and the given number of steps. ```reductionByL :: Eq a => ([(Term a,Term a)] -> Term a -> [[Int]]) -> [[(Term a,Term a)]] -> Int -> Term a -> Reduction a```    Returns the reduction of a term with the given strategy, the given list of term rewriting systems and the given number of steps.

## Exported datatypes:

RStrategy

A reduction strategy represented as a function that takes a term rewriting system and a term and returns the redex positions where the term should be reduced, parameterized over the kind of function symbols, e.g., strings.

Type synonym: `RStrategy a = TRS a -> Term a -> [Pos]`

Reduction

Representation of a reduction on first-order terms, parameterized over the kind of function symbols, e.g., strings.

Constructors:

• ```NormalForm :: (Term a) -> Reduction a``` : The normal form with term `t`.
• ```RStep :: (Term a) -> [Pos] -> (Reduction a) -> Reduction a``` : The reduction of term `t` at positions `ps` to reduction `r`.

## Exported operations:

 ```showReduction :: (a -> String) -> Reduction a -> String```    Transforms a reduction into a string representation.
 ```redexes :: Eq a => [(Term a,Term a)] -> Term a -> [[Int]]```    Returns the redex positions of a term according to the given term rewriting system.
 ```seqRStrategy :: Eq a => ([Int] -> [Int] -> Ordering) -> [(Term a,Term a)] -> Term a -> [[Int]]```    Returns a sequential reduction strategy according to the given ordering function.
 ```parRStrategy :: Eq a => ([Int] -> [Int] -> Ordering) -> [(Term a,Term a)] -> Term a -> [[Int]]```    Returns a parallel reduction strategy according to the given ordering function.
 ```liRStrategy :: Eq a => [(Term a,Term a)] -> Term a -> [[Int]]```    The leftmost innermost reduction strategy.
 ```loRStrategy :: Eq a => [(Term a,Term a)] -> Term a -> [[Int]]```    The leftmost outermost reduction strategy.
 ```riRStrategy :: Eq a => [(Term a,Term a)] -> Term a -> [[Int]]```    The rightmost innermost reduction strategy.
 ```roRStrategy :: Eq a => [(Term a,Term a)] -> Term a -> [[Int]]```    The rightmost outermost reduction strategy.
 ```piRStrategy :: Eq a => [(Term a,Term a)] -> Term a -> [[Int]]```    The parallel innermost reduction strategy.
 ```poRStrategy :: Eq a => [(Term a,Term a)] -> Term a -> [[Int]]```    The parallel outermost reduction strategy.
 ```reduce :: Eq a => ([(Term a,Term a)] -> Term a -> [[Int]]) -> [(Term a,Term a)] -> Term a -> Term a```    Reduces a term with the given strategy and term rewriting system.
 ```reduceL :: Eq a => ([(Term a,Term a)] -> Term a -> [[Int]]) -> [[(Term a,Term a)]] -> Term a -> Term a```    Reduces a term with the given strategy and list of term rewriting systems.
 ```reduceBy :: Eq a => ([(Term a,Term a)] -> Term a -> [[Int]]) -> [(Term a,Term a)] -> Int -> Term a -> Term a```    Reduces a term with the given strategy and term rewriting system by the given number of steps.
 ```reduceByL :: Eq a => ([(Term a,Term a)] -> Term a -> [[Int]]) -> [[(Term a,Term a)]] -> Int -> Term a -> Term a```    Reduces a term with the given strategy and list of term rewriting systems by the given number of steps.
 ```reduceAt :: Eq a => [(Term a,Term a)] -> [Int] -> Term a -> Term a```    Reduces a term with the given term rewriting system at the given redex position.
 ```reduceAtL :: Eq a => [(Term a,Term a)] -> [[Int]] -> Term a -> Term a```    Reduces a term with the given term rewriting system at the given redex positions.
 ```reduction :: Eq a => ([(Term a,Term a)] -> Term a -> [[Int]]) -> [(Term a,Term a)] -> Term a -> Reduction a```    Returns the reduction of a term with the given strategy and term rewriting system.
 ```reductionL :: Eq a => ([(Term a,Term a)] -> Term a -> [[Int]]) -> [[(Term a,Term a)]] -> Term a -> Reduction a```    Returns the reduction of a term with the given strategy and list of term rewriting systems.
 ```reductionBy :: Eq a => ([(Term a,Term a)] -> Term a -> [[Int]]) -> [(Term a,Term a)] -> Int -> Term a -> Reduction a```    Returns the reduction of a term with the given strategy, the given term rewriting system and the given number of steps.
 ```reductionByL :: Eq a => ([(Term a,Term a)] -> Term a -> [[Int]]) -> [[(Term a,Term a)]] -> Int -> Term a -> Reduction a```    Returns the reduction of a term with the given strategy, the given list of term rewriting systems and the given number of steps.