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  Deterministic 
Transforms a reduction into a string representation.
redexes :: Eq a => [(Term a,Term a)] -> Term a -> [[Int]]  Deterministic 
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]]  Deterministic 
Returns a sequential reduction strategy according to the given ordering function.
parRStrategy :: Eq a => ([Int] -> [Int] -> Ordering) -> [(Term a,Term a)] -> Term a -> [[Int]]  Deterministic 
Returns a parallel reduction strategy according to the given ordering function.
liRStrategy :: Eq a => [(Term a,Term a)] -> Term a -> [[Int]]  Deterministic 
The leftmost innermost reduction strategy.
loRStrategy :: Eq a => [(Term a,Term a)] -> Term a -> [[Int]]  Deterministic 
The leftmost outermost reduction strategy.
riRStrategy :: Eq a => [(Term a,Term a)] -> Term a -> [[Int]]  Deterministic 
The rightmost innermost reduction strategy.
roRStrategy :: Eq a => [(Term a,Term a)] -> Term a -> [[Int]]  Deterministic 
The rightmost outermost reduction strategy.
piRStrategy :: Eq a => [(Term a,Term a)] -> Term a -> [[Int]]  Deterministic 
The parallel innermost reduction strategy.
poRStrategy :: Eq a => [(Term a,Term a)] -> Term a -> [[Int]]  Deterministic 
The parallel outermost reduction strategy.
reduce :: Eq a => ([(Term a,Term a)] -> Term a -> [[Int]]) -> [(Term a,Term a)] -> Term a -> Term a  Deterministic 
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  Deterministic 
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  Deterministic 
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  Deterministic 
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  Deterministic 
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  Deterministic 
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  Deterministic 
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  Deterministic 
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  Deterministic 
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  Deterministic 
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  Deterministic 

Transforms a reduction into a string representation.

redexes :: Eq a => [(Term a,Term a)] -> Term a -> [[Int]]  Deterministic 

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]]  Deterministic 

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

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

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

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

The leftmost innermost reduction strategy.

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

The leftmost outermost reduction strategy.

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

The rightmost innermost reduction strategy.

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

The rightmost outermost reduction strategy.

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

The parallel innermost reduction strategy.

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

The parallel outermost reduction strategy.

reduce :: Eq a => ([(Term a,Term a)] -> Term a -> [[Int]]) -> [(Term a,Term a)] -> Term a -> Term a  Deterministic 

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  Deterministic 

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  Deterministic 

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  Deterministic 

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  Deterministic 

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  Deterministic 

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  Deterministic 

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  Deterministic 

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  Deterministic 

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  Deterministic 

Returns the reduction of a term with the given strategy, the given list of term rewriting systems and the given number of steps.