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
                  :: [(Term a,Term a)] -> Term a -> [[Int]]

Returns the redex positions of a term according to the given term rewriting system.

seqRStrategy
                  :: ([Int] -> [Int] -> Ordering) -> [(Term a,Term a)] -> Term a -> [[Int]]

Returns a sequential reduction strategy according to the given ordering function.

parRStrategy
                  :: ([Int] -> [Int] -> Ordering) -> [(Term a,Term a)] -> Term a -> [[Int]]

Returns a parallel reduction strategy according to the given ordering function.

liRStrategy
                  :: [(Term a,Term a)] -> Term a -> [[Int]]

The leftmost innermost reduction strategy.

loRStrategy
                  :: [(Term a,Term a)] -> Term a -> [[Int]]

The leftmost outermost reduction strategy.

riRStrategy
                  :: [(Term a,Term a)] -> Term a -> [[Int]]

The rightmost innermost reduction strategy.

roRStrategy
                  :: [(Term a,Term a)] -> Term a -> [[Int]]

The rightmost outermost reduction strategy.

piRStrategy
                  :: [(Term a,Term a)] -> Term a -> [[Int]]

The parallel innermost reduction strategy.

poRStrategy
                  :: [(Term a,Term a)] -> Term a -> [[Int]]

The parallel outermost reduction strategy.

reduce
                  :: ([(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
                  :: ([(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
                  :: ([(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
                  :: ([(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
                  :: [(Term a,Term a)] -> [Int] -> Term a -> Term a

Reduces a term with the given term rewriting system at the given redex position.

reduceAtL
                  :: [(Term a,Term a)] -> [[Int]] -> Term a -> Term a

Reduces a term with the given term rewriting system at the given redex positions.

reduction
                  :: ([(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
                  :: ([(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
                  :: ([(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
                  :: ([(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 :: [(Term a,Term a)] -> Term a -> [[Int]]

Returns the redex positions of a term according to the given term rewriting system.

seqRStrategy :: ([Int] -> [Int] -> Ordering) -> [(Term a,Term a)] -> Term a -> [[Int]]

Returns a sequential reduction strategy according to the given ordering function.

parRStrategy :: ([Int] -> [Int] -> Ordering) -> [(Term a,Term a)] -> Term a -> [[Int]]

Returns a parallel reduction strategy according to the given ordering function.

liRStrategy :: [(Term a,Term a)] -> Term a -> [[Int]]

The leftmost innermost reduction strategy.

loRStrategy :: [(Term a,Term a)] -> Term a -> [[Int]]

The leftmost outermost reduction strategy.

riRStrategy :: [(Term a,Term a)] -> Term a -> [[Int]]

The rightmost innermost reduction strategy.

roRStrategy :: [(Term a,Term a)] -> Term a -> [[Int]]

The rightmost outermost reduction strategy.

piRStrategy :: [(Term a,Term a)] -> Term a -> [[Int]]

The parallel innermost reduction strategy.

poRStrategy :: [(Term a,Term a)] -> Term a -> [[Int]]

The parallel outermost reduction strategy.

reduce :: ([(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 :: ([(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 :: ([(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 :: ([(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 :: [(Term a,Term a)] -> [Int] -> Term a -> Term a

Reduces a term with the given term rewriting system at the given redex position.

reduceAtL :: [(Term a,Term a)] -> [[Int]] -> Term a -> Term a

Reduces a term with the given term rewriting system at the given redex positions.

reduction :: ([(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 :: ([(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 :: ([(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 :: ([(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.