Module Rewriting.Narrowing

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

Author: Jan-Hendrik Matthes

Version: February 2020

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.