| Copyright | (c) 2016-2017 Rudy Matela |
|---|---|
| License | 3-Clause BSD (see the file LICENSE) |
| Maintainer | Rudy Matela <rudy@matela.com.br> |
| Safe Haskell | None |
| Language | Haskell2010 |
Test.Speculate.Reason.Order
Description
This module is part o Speculate.
Orders for term rewriting and completion.
Synopsis
- (|>|) :: Expr -> Expr -> Bool
- (>|) :: Expr -> Expr -> Bool
- (|>) :: Expr -> Expr -> Bool
- kboBy :: (Expr -> Int) -> (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool
- dwoBy :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool
- weight :: Expr -> Int
- weightExcept :: Expr -> Expr -> Int
- gtExcept :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Expr -> Bool
Documentation
(|>|) :: Expr -> Expr -> Bool infix 4 Source #
Strict order between expressions as defined in TRAAT p103.
s > t iff |s| > |t| and , for all x in V, |s|_x > |t|_x
This is perhaps the simplest order that can be used with KBC.
(>|) :: Expr -> Expr -> Bool infix 4 Source #
Strict order between expressions loosely as defined in TRAAT p124 (KBO)
Reversed K >| for Knuth, sorry Bendix.
dwoBy :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool Source #
Dershowitz reduction order as defined in TRAAT
|> a D for Dershowitz
weight :: Expr -> Int Source #
Weight function for kboBy:
- Variables weigh 1
- Nullary functions weigh 1 (a.k.a. constants)
- N-ary functions weigh 0
- Unary functions weigh 1
This is the weight when using >|.