Re: [isabelle] Fixed Points and Denotational Semantics

Many Thanks Brian and Andreas!

I have already downloaded Brian´s PhD thesis and it seems
highly readable!

All The Best!

On Tue, Oct 8, 2013 at 1:59 PM, Brian Huffman <huffman.brian.c at>wrote:

> On Tue, Oct 8, 2013 at 7:32 AM, Andreas Lochbihler
> <andreas.lochbihler at> wrote:
> > Hi Alfio,
> >
> > Have you already looked at HOLCF? It formalises domain theory and
> > denotational semantics. If not, that's where you should go first. Brian
> > Huffman's PhD thesis describes what is in there and how to use it.
> [...]
> > If you only have a chain-complete partial order with a least element, you
> > cannot use lfp, but instead fixp from the theory Complete_Partial_Order,
> but
> > you have to deal with admissibility yourself. This is where HOLCF greatly
> > helps you.
> Hi Alfio,
> I should point out a few differences between the HOLCF and
> Complete_Partial_Order formalizations of fixpoints:
> Class ccpo from Complete_Partial_Order uses a slightly stronger
> completeness condition than HOLCF uses; ccpo requires lubs of
> arbitrary chains, while HOLCF requires lubs only for countable chains.
> On the other hand, class ccpo has fixpoints for all monotone
> functions, whereas HOLCF additionally requires functions to be
> continuous.
> The other major consideration is that HOLCF uses a continuous function
> space type "'a -> 'b" almost everywhere, rather than using ordinary
> functions "'a => 'b" with a continuity predicate. One consequence is
> that you are locked in to using type classes for cpos (type 'a -> 'b
> is only defined for cpo types); Complete_Partial_Order is a bit more
> flexible in this regard.
> That said, if you are willing to commit to using type classes and the
> continuous function space type, HOLCF provides highly tuned automation
> for proving continuity and admissibility.
> Whichever library you decide to use, I'd welcome any questions,
> comments, or suggestions for improvements to either library.
> - Brian

Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil

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