Re: [isabelle] HOLCF Finite Sets



Hi,

Am Freitag, den 09.11.2012, 09:44 +0000 schrieb Simon Foster:
> I'm trying to devise a HOLCF cpo for finite sets.

just checking: What will your order relation be? Because if it is just
going to be subset, then you will not be able to construct a cpo, as the
limit of a chain of finite sets can be infinite (unless the type of the
elements is finite, of course).

I have a theory of finite maps with the HOLCF setup done
(http://darcs.nomeata.de/isa-launchbury/FMap-HOLCF.thy), but depending
on the order relation that you need, this is not going to help you.

Greetings,
Joachim

-- 
Joachim "nomeata" Breitner
  mail at joachim-breitner.de  |  nomeata at debian.org  |  GPG: 0x4743206C
  xmpp: nomeata at joachim-breitner.de | http://www.joachim-breitner.de/

Attachment: signature.asc
Description: This is a digitally signed message part



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