Michael, that's extremely helpful, I need to read the part about [p 17] The meaning of HOL terms in such a model will now be described.
and terms means constants as well as abstractions. I should be able to decode your simple picture from the general description there. Page 19 more formidable. BTW I'm familiar with the notation [[...]] from Denotational Semantic (DS) for Scheme e.g. Do you see any connection between HOL semantics and DS? What's bugging me a good deal more the ZFC connection, how do we pick up all the sets we need from such a small number of type operators and constants? I only know of bool, ind & ->, and I can throw in point now. I know that your universe U is, very crudely, a ZFC model, your semantic function M take type stuff to operators on U, and as you're telling me, to actual elements of U. I'm sure I'm missing something really obvious. My theory would be that the problem is that MESON is bad at equational reasoning. All you need to do (easy for me to say, of course) is to occasionally use rewriting as well as MESON. Thanks, and I think that's what John meant by "using a logical equivalence |- !x. P[x] <=> Q[x] to "rewrite" P to Q inside another formula". I'm over 100,000 in MESON calculations routinely, and I'm not sure I want to add REWRITE_TAC to every offending line. I suppose there are more sophisticated rewriting tactics as well... -- Best, Bill ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
