Rob, I think Michael's IMAGE idea may show that I was wrong about your semantic
embedding idea. I said that I was happy with the HOL Light parser's definition
of the set comprension
{f x | R x} = {a | ∃x. a = f x ∧ R x}
and I didn't think that it made sense to talk about the semantic value of f x
and R x here. But maybe I was wrong, because this set comprension is an image,
the image of the function f on the set of x such that R x, and this set is in
fact equal to R. Let's look at HOL's IMAGE:
IMAGE;;
val it : thm = |- !s f. IMAGE f s = {y | ?x. x IN s /\ y = f x}
type_of `IMAGE`;;
Warning: inventing type variables
val it : hol_type = `:(?86076->?86077)->(?86076->bool)->?86077->bool`
So IMAGE has polymorphic type
(A->B)->(A->bool)->B->bool
Now I'm sorry I haven't pursued this myself. But I think your
HOL4/semantic-embedding ideas give a way to define IMAGE independently of {...}
which need to be parsed. Is that what you did, or something that you can do?
--
Best,
Bill
------------------------------------------------------------------------------
CenturyLink Cloud: The Leader in Enterprise Cloud Services.
Learn Why More Businesses Are Choosing CenturyLink Cloud For
Critical Workloads, Development Environments & Everything In Between.
Get a Quote or Start a Free Trial Today.
http://pubads.g.doubleclick.net/gampad/clk?id=119420431&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
