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

This is not a simplification order on funny Exprs.

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

funny :: Expr -> Bool

Returns True when an Expression has either a functional type or functional variables.

funny xx        =  False
funny one       =  False
funny idE       =  True
funny (ff one)  =  True

serious :: Expr -> Bool

Returns True when an Expression has no functional return type and no functional variables.

serious xx        =  True
serious one       =  True
serious idE       =  False
serious (ff one)  =  False