Daryoush Mehrtash | 16 Jul 10:19 2013

What does it mean to derive "equations of restricted from" in Haskell?

In John Hughes's "The Design of Pretty printing  library" paper,  he says:

"The implementations which we are trying to derive consist of equations of a restricted form. We will derive implementations by proving their constituent equations from the specification. By itself this is no guarantee that the implemented functions satisfy the specification because we might not have proved enough equation But if we also check that the derived definitions are terminating and exhaustive then this property is guaranteed"

What does "restricted form" mean?

What is the meaning and significance of "definitions are terminating and exhaustive"?


Weblog:  http://onfp.blogspot.com/
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
Johannes Waldmann | 16 Jul 14:01 2013

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

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.