Module Rewriting.Narrowing

Library for representation and computation of narrowings on first-order terms and representation of narrowing strategies.

Author: Jan-Hendrik Matthes

Version: November 2016

Summary of exported operations:

 ```defaultNOptions :: Eq a => NOptions a```    The default narrowing options. ```showNarrowing :: (a -> String) -> Narrowing a -> String```    Transforms a narrowing into a string representation. ```stdNStrategy :: Eq a => [(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]```    The standard narrowing strategy. ```imNStrategy :: Eq a => [(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]```    The innermost narrowing strategy. ```omNStrategy :: Eq a => [(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]```    The outermost narrowing strategy. ```loNStrategy :: Eq a => [(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]```    The leftmost outermost narrowing strategy. ```lazyNStrategy :: Eq a => [(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]```    The lazy narrowing strategy. ```wnNStrategy :: Eq a => [(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]```    The weakly needed narrowing strategy. ```narrowBy :: ([(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]) -> [(Term a,Term a)] -> Int -> Term a -> [(FM Int (Term a),Term a)]```    Narrows a term with the given strategy and term rewriting system by the given number of steps. ```narrowByL :: ([(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]) -> [[(Term a,Term a)]] -> Int -> Term a -> [(FM Int (Term a),Term a)]```    Narrows a term with the given strategy and list of term rewriting systems by the given number of steps. ```narrowingBy :: ([(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]) -> [(Term a,Term a)] -> Int -> Term a -> [Narrowing a]```    Returns a list of narrowings for a term with the given strategy, the given term rewriting system and the given number of steps. ```narrowingByL :: ([(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]) -> [[(Term a,Term a)]] -> Int -> Term a -> [Narrowing a]```    Returns a list of narrowings for a term with the given strategy, the given list of term rewriting systems and the given number of steps. ```narrowingTreeBy :: ([(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]) -> [(Term a,Term a)] -> Int -> Term a -> NarrowingTree a```    Returns a narrowing tree for a term with the given strategy, the given term rewriting system and the given number of steps. ```narrowingTreeByL :: ([(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]) -> [[(Term a,Term a)]] -> Int -> Term a -> NarrowingTree a```    Returns a narrowing tree for a term with the given strategy, the given list of term rewriting systems and the given number of steps. ```solveEq :: Eq a => NOptions a -> ([(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]) -> [(Term a,Term a)] -> Term a -> [FM Int (Term a)]```    Solves a term equation with the given strategy, the given term rewriting system and the given options. ```solveEqL :: Eq a => NOptions a -> ([(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]) -> [[(Term a,Term a)]] -> Term a -> [FM Int (Term a)]```    Solves a term equation with the given strategy, the given list of term rewriting systems and the given options. ```dotifyNarrowingTree :: (a -> String) -> NarrowingTree a -> String```    Transforms a narrowing tree into a graphical representation by using the DOT graph description language. ```writeNarrowingTree :: (a -> String) -> NarrowingTree a -> String -> IO ()```    Writes the graphical representation of a narrowing tree with the DOT graph description language to a file with the given filename.

Exported datatypes:

NStrategy

A narrowing strategy represented as a function that takes a term rewriting system and a term and returns a list of triples consisting of a position, a rule and a substitution, parameterized over the kind of function symbols, e.g., strings.

Type synonym: `NStrategy a = TRS a -> Term a -> [(Pos,Rule a,Subst a)]`

Narrowing

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

Constructors:

• ```NTerm :: (Term a) -> Narrowing a``` : The narrowed term `t`.
• ```NStep :: (Term a) -> Pos -> (Subst a) -> (Narrowing a) -> Narrowing a``` : The narrowing of term `t` at position `p` with substitution `sub` to narrowing `n`.

NarrowingTree

Representation of a narrowing tree for first-order terms, parameterized over the kind of function symbols, e.g., strings.

Constructors:

• ```NTree :: (Term a) -> [(Pos,Subst a,NarrowingTree a)] -> NarrowingTree a``` : The narrowing of term `t` to a new term with a list of narrowing steps `ns`.

NOptions

Representation of narrowing options for solving term equations, parameterized over the kind of function symbols, e.g., strings.

Constructors:

• ```NOptions :: Bool -> (RStrategy a) -> NOptions a```

Fields:

• ```normalize :: Bool``` : Indicates whether a term should be normalized before computing further narrowing steps.
• ```rStrategy :: (RStrategy a)``` : The reduction strategy to normalize a term.

Exported operations:

 ```defaultNOptions :: Eq a => NOptions a```    The default narrowing options.
 ```showNarrowing :: (a -> String) -> Narrowing a -> String```    Transforms a narrowing into a string representation.
 ```stdNStrategy :: Eq a => [(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]```    The standard narrowing strategy.
 ```imNStrategy :: Eq a => [(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]```    The innermost narrowing strategy.
 ```omNStrategy :: Eq a => [(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]```    The outermost narrowing strategy.
 ```loNStrategy :: Eq a => [(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]```    The leftmost outermost narrowing strategy.
 ```lazyNStrategy :: Eq a => [(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]```    The lazy narrowing strategy.
 ```wnNStrategy :: Eq a => [(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]```    The weakly needed narrowing strategy.
 ```narrowBy :: ([(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]) -> [(Term a,Term a)] -> Int -> Term a -> [(FM Int (Term a),Term a)]```    Narrows a term with the given strategy and term rewriting system by the given number of steps.
 ```narrowByL :: ([(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]) -> [[(Term a,Term a)]] -> Int -> Term a -> [(FM Int (Term a),Term a)]```    Narrows a term with the given strategy and list of term rewriting systems by the given number of steps.
 ```narrowingBy :: ([(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]) -> [(Term a,Term a)] -> Int -> Term a -> [Narrowing a]```    Returns a list of narrowings for a term with the given strategy, the given term rewriting system and the given number of steps.
 ```narrowingByL :: ([(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]) -> [[(Term a,Term a)]] -> Int -> Term a -> [Narrowing a]```    Returns a list of narrowings for a term with the given strategy, the given list of term rewriting systems and the given number of steps.
 ```narrowingTreeBy :: ([(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]) -> [(Term a,Term a)] -> Int -> Term a -> NarrowingTree a```    Returns a narrowing tree for a term with the given strategy, the given term rewriting system and the given number of steps.
 ```narrowingTreeByL :: ([(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]) -> [[(Term a,Term a)]] -> Int -> Term a -> NarrowingTree a```    Returns a narrowing tree for a term with the given strategy, the given list of term rewriting systems and the given number of steps.
 ```solveEq :: Eq a => NOptions a -> ([(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]) -> [(Term a,Term a)] -> Term a -> [FM Int (Term a)]```    Solves a term equation with the given strategy, the given term rewriting system and the given options. The term has to be of the form `TermCons c [l, r]` with `c` being a constructor like `=`. The term `l` and the term `r` are the left-hand side and the right-hand side of the term equation.
 ```solveEqL :: Eq a => NOptions a -> ([(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]) -> [[(Term a,Term a)]] -> Term a -> [FM Int (Term a)]```    Solves a term equation with the given strategy, the given list of term rewriting systems and the given options. The term has to be of the form `TermCons c [l, r]` with `c` being a constructor like `=`. The term `l` and the term `r` are the left-hand side and the right-hand side of the term equation.
 ```dotifyNarrowingTree :: (a -> String) -> NarrowingTree a -> String```    Transforms a narrowing tree into a graphical representation by using the DOT graph description language.
 ```writeNarrowingTree :: (a -> String) -> NarrowingTree a -> String -> IO ()```    Writes the graphical representation of a narrowing tree with the DOT graph description language to a file with the given filename.