Test.Speculate.Reason.Order

This module is part o Speculate.

Orders for term rewriting and completion.

Documentation

(|>|) :: Expr -> Expr -> Bool infix 4

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

Strict order between expressions loosely as defined in TRAAT p124 (KBO)

Reversed K >| for Knuth, sorry Bendix.

(|>) :: Expr -> Expr -> Bool infix 4

kboBy :: (Expr -> Int) -> (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool

dwoBy :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool

Dershowitz reduction order as defined in TRAAT

|> a D for Dershowitz

weight :: Expr -> Int

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 >|.

weightExcept :: Expr -> Expr -> Int

Weight function for kboBy:

• Variables weigh 1
• Nullary functions weigh 1 (a.k.a. constants)
• N-ary functions weigh 0
• Unary functions weigh 1 except for the one given as argument

gtExcept :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Expr -> Bool

To be used alongside weightExcept