Module Rewriting.Strategy

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

Author: Jan-Hendrik Matthes

Version: November 2016

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.