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
