On 04/26/2013 01:16 AM, Bill Richter wrote:
> Thanks, Vince! I didn't know this:
>
> Mathematically, a variable is the pair of a name and a type, so if
> two variables have the same name and the same type then they're
> just the same variable.
>
> But I should have known this, because there are 4 different kinds of terms,
> each having a type, and the simplest kind of term is a variable. So a
> variable is not just a symbol. Thanks.
>
> (note thus that if two variables have the same name but different
> types, then they are different; this is really counter intuitive)
>
> So what I want is a dialect of HOL Light where this seems not to be true, but
> instead:
> If x is a variable (which of course has a type, say alpha), then any other
> occurrence of the symbol x in the scope of the first x will then inherit the
> type alpha. So there will be no need to give the second x a type annotation,
> and it will be an error to give x a different type annotation than alpha.
> This is the way Freek's miz3.ml works.
> Do you like this idea?
Sure. I don't know what was the original reason for allowing two
variables of different types to have the same name but I always found
this extremely weird.
I guess maybe this makes the logic easier to express in some way,
because otherwise we need mappings from variable names to types (called
"environments").
But I'm not convinced myself by this argument since we need environments
in other contexts anyway (probably in the semantics).
Note that having an environment (i.e., a mapping from variable names to
types) is what is done in Coq for instance.
> Do you instead think that it's an important ability for the same symbol x to
> have different types at different places and so be different variables?
No.
> My plan to make this work is
> 1) to use strings as in my modification of quotexpander I posted here
> 2) understand tactics.ml.
> I don't think anything else is needed. I don't mind mining miz3.ml for good
> ideas, but I don't think it will be necessary to understand miz3.ml. My
> guess is that using strings will simplify matters that were difficult with
> Freek's preterms.
>
> > (`!u v w:real^2. ~collinear {vec 0,v,w} ==> ? s t. s % v + t % w =
> u`,
> > INTRO_TAC "!u v w; H1" [...]
> > So in the SUBGOAL_TAC expression, v and w need type annotations.
> > But then they received the value given by INTRO_TAC. That is, the
> > statement of the theorem is "for all u, v, w...", and INTRO_TAC then
> > fixes arbitrary real^2 vectors u, v, w,
>
> I'm not sure what you mean by "INTRO_TAC then *fixes* arbitrary".
> In this particular example, INTRO_TAC is just the same as GEN_TAC
> THEN GEN_TAC THEN GEN_TAC THEN DISCH_THEN (LABEL_TAC "H1").
>
> Sorry for my "set theory" terminology, which I see isn't the way HOL Light
> describes INTRO_TAC:
>
> # help "INTRO_TAC";;
>
> INTRO_TAC : string -> tactic
>
> Given a string s, INTRO_TAC s breaks down outer universal quantifiers
> and implications in the goal, fixing variables [...]
>
> I guess I don't know what "fix" means. I know what it looks like to me: The
> symbols u, v, w were already typed real^2 in the goal
> `!u v w:real^2. ~collinear {vec 0,v,w} ==> ? s t. s % v + t % w = u`
> so u, v, w are already variables. But these variables right now don't have
> any scope outside the goal. Evaluating
>
> INTRO_TAC "!u v w; H1"
>
> then gives scope to these variables u, v, w which extends at least as far as
> the next line:
>
> > THEN SUBGOAL_TAC "H1'" `~(v$1 * w$2 - (w:real^2)$1 * (v:real^2)$2 =
> &0)`
> > [HYP MESON_TAC "H1" [COLLINEAR_3_2Dzero; REAL_SUB_0]] THEN [...]);;
>
> So the v, w that occur in the term
> `~(v$1 * w$2 - (w:real^2)$1 * (v:real^2)$2 = &0)`
> must be equal to to the v, w above that has the scope, as long as the type of
> the new v, w is also real^2.
>
> What I don't understand is how HOL Light realizes that the new u, v is the
> same as the old u, v. Really I suppose I mean I don't understand how HOL
> Light still remembers about the old v, w. There should be an environment
> which keeps track of the fixed variables and their scope. How is that
> handled in HOL Light? Are you saying that Ocaml handles the environment?
HOL Light does a lot less than you think: it just sees a variable with
name "v" and type "real^2", now if it sees elsewhere a variables with
the same name and same type then they are equal. As simple as that.
--
Vincent Aravantinos
Postdoctoral Fellow, Concordia University, Hardware Verification Group
http://users.encs.concordia.ca/~vincent
------------------------------------------------------------------------------
Try New Relic Now & We'll Send You this Cool Shirt
New Relic is the only SaaS-based application performance monitoring service
that delivers powerful full stack analytics. Optimize and monitor your
browser, app, & servers with just a few lines of code. Try New Relic
and get this awesome Nerd Life shirt! http://p.sf.net/sfu/newrelic_d2d_apr
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
