Re: [Haskell-cafe] What does it mean to derive "equations of restricted from" in Haskell?

Daryoush Mehrtash writes:

What does "restricted form" mean?

non-restricted: e.g., f (f x y) z = f x (f y z)) restricted: the shape of function declarations in Haskell (where lhs is a pattern)

"definitions are terminating ...

non-termination: an equation like "f x y = f y x" when you orient it as a rule "f x y -> f y x", there are infinite derivations

and exhaustive"

non-exhaustive: you have an equation "f (x : ys) = ..." but you don't have an equation for "f [] = ..." (all the above is is standard stuff in algebraic specification, equational reasoning, etc.) - J.W.