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

[Daryoush Mehrtash]

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"?

-- 
Daryoush

Weblog:  http://onfp.blogspot.com/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130716/040173f7/attachment.htm>