Library for representation and computation of reductions on first-order terms and representation of reduction strategies.
Author: Jan-Hendrik Matthes
Version: February 2020
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. |
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]
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
.
Transforms a reduction into a string representation. |
Returns the redex positions of a term according to the given term rewriting system. |
Returns a sequential reduction strategy according to the given ordering function. |
Returns a parallel reduction strategy according to the given ordering function. |
The leftmost innermost reduction strategy. |
The leftmost outermost reduction strategy. |
The rightmost innermost reduction strategy. |
The rightmost outermost reduction strategy. |
The parallel innermost reduction strategy. |
The parallel outermost reduction strategy. |
Reduces a term with the given strategy and term rewriting system. |
Reduces a term with the given strategy and list of term rewriting systems. |
Reduces a term with the given strategy and term rewriting system by the given number of steps. |
Reduces a term with the given strategy and list of term rewriting systems by the given number of steps. |
Reduces a term with the given term rewriting system at the given redex position. |
Reduces a term with the given term rewriting system at the given redex positions. |
Returns the reduction of a term with the given strategy and term rewriting system. |
Returns the reduction of a term with the given strategy and list of term rewriting systems. |