>>>>> "Fergus" == Fergus Henderson <[EMAIL PROTECTED]> writes:
Fergus> On 28-Sep-1999, Paul Hudak <[EMAIL PROTECTED]> wrote:
>> > Haskell's (&&) only models the logical AND when it is passed booleans.
>> > To say that _|_ is a Haskell Boolean, is to create another concept
>> > domain (Haskell Boolean), which shares many properties with Logic
>> > Boolean but is not identical with it.
>>
>> Right, but it is important to realize that when reasoning about programs
>> in most languages, the "logical" Boolean domain is not enough, since
>> most languages permit errors and non-termination; thus a richer domain
>> is needed.
Fergus> That depends on what you want to reason about.
For that you will start by defining your equivalence relation.
Fergus> If you just want to reason about whether the program produces
Fergus> wrong answers, then the "logical" Boolean domain works fine.
Here you use equality of the value produced. If you care for
termination you use the lifted domain, obtaining equivalence for equal
values *provided* they have similar termination properties.
Fergus> If you want to reason about performance, then Haskell's
Fergus> standard denotational semantics is not rich enough either.
Here the equivalence should only hold for equal values *provided* they
terminate within the same time/number of reductions.
See e.g. Andrew Moran and David Sands: Improvement in a Lazy Context:
An Operational Theory for Call-by-Need, available from Davids WWW
pages and possibly elsewhere.
Marko
--
Marko Schütz [EMAIL PROTECTED]
http://www.ki.informatik.uni-frankfurt.de/~marko/
