Re: [isabelle] Lazy Lists

Absolutely and definitely true. HOLCF is explicitly a theory of computation; Coinductive is merely a theory of infinite objects. Such a pity if it doesn't yet support code generation.


On 25 Jun 2012, at 07:43, Andreas Lochbihler wrote:

> if you want to formalise functional programming, I recommend HOLCF over Coinductive, because domain theory is the semantics behind Haskell, not coinductive datatypes. HOLCF lists, for example, can distinguish between "definitely terminating", "definitely infinite", and "evaluated up to a certain point with unknown rest". Coinductive lists ('a llist) cannot express the last case. You can then also do induction over HOLCF lists, known as Scott induction.

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