Re: [isabelle] Fixed Points and Denotational Semantics



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, 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




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