Some implementation choices behind the design of HOL Light are discussed in this paper:
John Harrison "HOL Done Right" http://www.cl.cam.ac.uk/~jrh13/papers/holright.html See e.g. section 7 where it is discussed in details the definition of the existential quantification. Marco Quoting Mark <[email protected]>: > I think you ask an interesting question, and I would also like to know > the answer. It seems that these definitions have been handed down, > but > it's difficult to find the original reasons why they were done the way > they were. Or maybe there's some crucial document I don't know > about.. > > Interestingly, HOL Light deviates from the other HOL systems for the > definitions for some constants (e.g. conjunction, implication and > existential quantification), enabling a smaller logical core. In HOL > Zero, I just stuck with the conventional definitions of HOL88, HOL90, > ProofPower HOL, HOL4, etc. I did, however, attempt to give informal > English explanations of the logical core's definitions and axioms in > source code comments, but this didn't stretch to falsity and logical > negation (but I would like it to!). > > Mark. > > On Wed, 23 Feb 2011 13:40:54 +0000, Russell Wallace > <[email protected]> wrote: >> Hi all, >> >> I'm looking at some of the Light source code, and curious about some >> of the design decisions. >> >> For example, this seems straightforward enough, given F: >> >> let NOT_DEF = new_basic_definition >> `(~) = \p. p ==> F`;; >> >> ... but on the face of it, it would seem even simpler to have done >> >> let NOT_DEF = new_basic_definition >> `(~) = \p. p <=> F`;; >> >> Is there a reason implication was chosen over equality for this >> definition? >> >> And this one I'm also not clear about: >> >> let F_DEF = new_basic_definition >> `F = !p:bool. p`;; >> >> falsehood is defined as "all propositions are true"... which is >> certainly false, though on the face of it would seem a little >> roundabout... does it have some particular felicitous properties, or >> is it just a case of it being the simplest way to define false given >> lambda and equals as primitives? >> >> Is there any documentation anywhere on the reasoning behind these >> decisions? >> >> >> ------------------------------------------------------------------------------ >> Free Software Download: Index, Search & Analyze Logs and other IT >> data in >> Real-Time with Splunk. Collect, index and harness all the fast moving >> IT data >> generated by your applications, servers and devices whether physical, >> virtual >> or in the cloud. Deliver compliance at lower cost and gain new >> business >> insights. http://p.sf.net/sfu/splunk-dev2dev >> _______________________________________________ >> hol-info mailing list >> [email protected] >> https://lists.sourceforge.net/lists/listinfo/hol-info > > > ------------------------------------------------------------------------------ > Free Software Download: Index, Search & Analyze Logs and other IT > data in > Real-Time with Splunk. Collect, index and harness all the fast > moving IT data > generated by your applications, servers and devices whether > physical, virtual > or in the cloud. Deliver compliance at lower cost and gain new > business > insights. http://p.sf.net/sfu/splunk-dev2dev > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info > ------------------------------------------------------------------------------ Free Software Download: Index, Search & Analyze Logs and other IT data in Real-Time with Splunk. Collect, index and harness all the fast moving IT data generated by your applications, servers and devices whether physical, virtual or in the cloud. Deliver compliance at lower cost and gain new business insights. http://p.sf.net/sfu/splunk-dev2dev _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
