>> Does HOL4 have anything comparable to sets.ml? > Yes it will have, and it will probably be spread over many source code > files, but I'm afraid I don't know where this is in the HOL4 source. This > is a question for HOL4 community, Michael et al. I'm more of a HOL Light > and HOL Zero person.
The counterpart to sets.ml in HOL4 is in <holdir>/src/pred_set/src/pred_setScript.sml There is also a description of sets in HOL4 in the manual. Start at p. 102 of the HOL4 Description document: http://sourceforge.net/projects/hol/files/hol/kananaskis-7/kananaskis-7-description.pdf/download Konrad. On Mon, Aug 13, 2012 at 1:49 AM, "Mark" <m...@proof-technologies.com> wrote: > Hi Bill, > >> Isn't this supposed to be about sets? > > No, HOL is about types. Tom is informally explaining what the HOL logic is, > rather than explaining it in terms of some other formal notation (e.g. ZFC > set theory). > >> Can you explain how the set abstraction/enumerations of sets.ml are > lambdas? > > It's like I said - a set abstraction is (of course) a set, and so is a set > enumeration. Sets in HOL Light and HOL4 are functions to boolean (i.e. > "predicates"). A lambda is a function. So therefore one can understand > how, in HOL Light and HOL4, a set abstraction or enumeration might be a > lambda. Maybe I'm misunderstanding what your misunderstanding is... > > I think a problem for you here is that, in HOL Light, it's sometimes not > easy to see through the syntactic sugar. The parser will automatically > parse a set enumeration as ` { 1, 2, 3 }`, whereas it is actually internally > represented as `1 INSERT (2 INSERT (3 INSERT EMPTY))` (and parsing this > longhand will give precisely the same internal term). The pretty printer > will always print out this internal representation as `{ 1, 2, 3 }`. To get > around this in HOL Light and see the true internal representation, I think > you need to use the destructors 'dest_comb' and 'dest_abs'. Then, if you > want to know the definitions of the HOL constants used in the internal > representation, you can examine the ML state variable 'the_definitions', > which lists all constant definitions that have been made. > >> Does HOL4 have anything comparable to sets.ml? > > Yes it will have, and it will probably be spread over many source code > files, but I'm afraid I don't know where this is in the HOL4 source. This > is a question for HOL4 community, Michael et al. I'm more of a HOL Light > and HOL Zero person. > > Mark. > > > on 13/8/12 5:53 AM, Bill Richter <rich...@math.northwestern.edu> wrote: > >> Thanks, Mark! I looked at Tom Hales's Notices article, as you suggested >> www.ams.org/notices/200811/tx081101370p.pdf >> Now Tom is a great mathematician (he's the main reason I'm here), but Tom > is >> now an HOL Light expert, and I think mathematicians can't be expected to >> understand him. He starts out great: >> >> Much day-to-day mathematics is written at a level of abstraction >> that is indifferent to its exact representation as sets. >> >> This layer of abstraction is good news, because it allows us to >> shift from Zermelo-Fraenkel- Choice (ZFC) set theory to a different >> foundational system with equanimity and ease. >> >> HOL Light is a new axiomatic foundation with types, different from >> the usual ZFC. >> >> That sounds great, but here I want more details: >> >> The types are presented in the HOL Light System box. >> >> Terms are the basic mathematical objects of the HOL Light system. The >> syntax is based on Church’s lambda-calculus [to define functions] >> >> What is a type? Compared to a set, I think. What is a term? >> >> 1. Types: The collection of types is freely generated from type >> variables :A,:B,... and type constants :bool (boolean), :ind >> (infinite type), joined by arrows >> >> Isn't this supposed to be about sets? My code (largely written by John) >> doesn't obviously obey Tom's rule: >> new_type("point",0);; >> new_type_abbrev("point_set",`:point->bool`);; >> new_constant("Between",`:point->point->point->bool`);; >> new_constant("Line",`:point_set->bool`);; >> >> Maybe I need to read something by Church. >> >> 2. `{A,B}` is a set enumeration, not a set abstraction, so I'm not >> sure why you are pointing to the definition of "INSERT" (which is >> used in the representation of set enumerations) and then talking >> about set abstractions. >> >> Because it was about all that was explained about sets in the tutorial, > and >> because I was intrigued that INSERT was explicitly defined as a lambda in >> sets.ml. >> >> But anyway, any set enumeration or set abstraction is of course a >> set, and, in HOL Light, any set is a function (as explained by 1.), >> which is what a lambda is, so there should be no surprise that a >> set abstraction/enumeration can be expressed as a lambda in HOL >> Light. >> >> Can you explain how the set abstraction/enumerations of sets.ml are > lambdas? >> Does HOL4 have anything comparable to sets.ml? >> >> Sorry, I had two typos in my last post. I meant to say >> >> let I1 = new_axiom >> `! A B. ~(A = B) ==> ?! l. Line l /\ A IN l /\ B IN l`;; >> says there is a unique "line" containing any two DISTINCT "points". >> >> if A, B refer to "points" a & b, then open (A,B) refers to the >> subset of point consisting of all "points" between a and b. >> >> -- >> 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 >> hol-info@lists.sourceforge.net >> https://lists.sourceforge.net/lists/listinfo/hol-info >> >> >> > > ------------------------------------------------------------------------------ > 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 > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info ------------------------------------------------------------------------------ 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
