[Haskell-cafe] What does it mean to derive "equations of restricted from" in Haskell?
waldmann at imn.htwk-leipzig.de
Tue Jul 16 14:01:52 CEST 2013
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.)
More information about the Haskell-Cafe