On 4 Jan 2014, at 6:17 pm, Bill Richter <[email protected]> wrote:
> To see this, think of a mathematical function f: X ---> Y between sets and a
> subset A of X. Then we speak of the image f(A), which is a subset of Y,
> defined by
>
> f(A) = {f(a) | a ∈ A}.
>
> But what does that mean? I claim it's just a short-hand for
>
> {b | ∃a ∈ A. b = f(a)}.
>
> Or back to HOL, we of course know that sets are just a way of talking about
> abstractions of type alpha->bool. So I say before finding the semantic
> value, we must first turn
> {f x y z | R x y z}
> into an abstraction, and that means
> λa. ∃x y z. a = f x y z ∧ R x y z
> where a must not be free in f x y z or R x y z.
It is easy to see the connection between HOL4_GSPEC and image. The former has
type
:(A -> bool # B) -> (B -> bool)
we know that functions into a product (the first argument above) are in
bijection with a pair of functions so that the type above is in bijection with
the type
:(A -> bool) # (A -> B) -> (B -> bool)
If you curry this type and reorder, then you get
:(A -> B) -> (A -> bool) -> (B -> bool)
which is exactly the type you'd expect to see for image.
In other words, you might argue that given IMAGE (as it is called in HOL4),
GSPEC is actually redundant. However, forcing users to give up on the nice
syntax that we/they expect to be able to use is usually a bad idea. The exact
encoding used underneath the covers of that syntax is less important.
Incidentally, GSPEC in HOL4 predates my involvement in the system. If forced
to guess, I’d hazard that it’s due to Tom Melham, who did a lot of the early
work on that part of the system. He defined cardinality for example; comments
still in the sources suggesting this happened in early 1991.
Happy New Year.
Michael
________________________________
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
------------------------------------------------------------------------------
Rapidly troubleshoot problems before they affect your business. Most IT
organizations don't have a clear picture of how application performance
affects their revenue. With AppDynamics, you get 100% visibility into your
Java,.NET, & PHP application. Start your 15-day FREE TRIAL of AppDynamics Pro!
http://pubads.g.doubleclick.net/gampad/clk?id=84349831&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
