Re: [isabelle] HOLCF Finite Sets


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
(, but depending
on the order relation that you need, this is not going to help you.


Joachim "nomeata" Breitner
  mail at  |  nomeata at  |  GPG: 0x4743206C
  xmpp: nomeata at |

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

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