Re: [isabelle] HOLCF equality



On 07/09/2012 10:04 PM, Brian Huffman wrote:
On Mon, Jul 9, 2012 at 11:14 AM, Christian Sternagel
<c-sterna at jaist.ac.jp> wrote:
I am currently using

class eq =
   fixes eq :: "'a::pcpo → 'a → tr"
   assumes equals_strict [simp]:
     "eq⋅x⋅⊥ = ⊥" "eq⋅⊥⋅y = ⊥"
     and eq_iff [iff]:
     "eq⋅x⋅y = TT ⟷ x ≠ ⊥ ∧ y ≠ ⊥ ∧ x = y"
     "eq⋅x⋅y = FF ⟷ x ≠ ⊥ ∧ y ≠ ⊥ ∧ x ≠ y"
     "eq⋅x⋅y = ⊥ ⟷ x = ⊥ ∨ y = ⊥"

but did not think much about the details ;).
Btw, the above strictness rules came from observing how ghci handled equalities involving "undefined". For the case of (==) this is relatively simple.

On a related note, in the the ghc sources there are often several versions of a function (usually one due to the Haskell report and an optimized one). Furthermore there are rewrite rules that can be used by the compiler. In both cases the strictness-behaviour (I don't know the correct technical term) is sometimes different, i.e., optimized functions behave different (I think I experienced this with the two versions of "any", but am not a 100% sure) from report versions and sometimes rewrite rules have not been correct when considering strictness, e.g., consider the following excerpt from the sources:

{-# RULES
"filter" [~1] forall p xs. filter p xs = build (\c n -> foldr (filterFB c p) n xs)
"filterList" [1]  forall p.     foldr (filterFB (:) p) [] = filter p
"filterFB" forall c p q. filterFB (filterFB c p) q = filterFB c (\x -> q x && p x)
 #-}

-- Note the filterFB rule, which has p and q the "wrong way round" in the RHS.
--     filterFB (filterFB c p) q a b
--   = if q a then filterFB c p a b else b
--   = if q a then (if p a then c a b else b) else b
--   = if q a && p a then c a b else b
--   = filterFB c (\x -> q x && p x) a b
-- I originally wrote (\x -> p x && q x), which is wrong, and actually
-- gave rise to a live bug report.  SLPJ.

For verification this is of course important. It seems that HOLCF provides a nice way to verify such compiler rewrite rules in a reliable way.

chris


I think your eq_iff rules need to be weakened like this:

     "eq⋅x⋅y = TT ==> x = y"
     "eq⋅x⋅y = FF ==> x ≠ y"

Otherwise instances for lazy lists or other lazy datatypes are not
possible. (Your class "eq" is provably a subclass of "flat".)

Alternatively, a subclass "eq_flat" with the strong eq_iff rules might
be useful alongside a weakened "eq" class.

Maybe something like a theory for standard Haskell functions could be placed
where everybody can browse and contribute? (I am currently mainly defining
very basic list functions and proving basic properties about them.)

This sounds like a good idea. The question is where to put it. We
could add a theory file under HOLCF in the distribution, or we could
add an AFP entry for this purpose. (Maybe using the distribution is
better; as an "archive", the AFP seems not to be intended so much for
dynamic, growing works with open authorship.)

- Brian








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.