Re: [isabelle] Fixed Points and Denotational Semantics
Many Thanks Brian and Andreas!
I have already downloaded Brian´s PhD thesis and it seems
All The Best!
On Tue, Oct 8, 2013 at 1:59 PM, Brian Huffman <huffman.brian.c at gmail.com>wrote:
> On Tue, Oct 8, 2013 at 7:32 AM, Andreas Lochbihler
> <andreas.lochbihler at inf.ethz.ch> 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,
> > 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
> 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