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

[Johannes Waldmann]

Daryoush Mehrtash <dmehrtash <at> gmail.com> 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.