2013/4/26 Bill Richter <rich...@math.northwestern.edu>
> Thanks, Vince! That's great we're in agreement about the same symbol
> being given two different types. How hard would it be to change HOL Light
> so that it behaves like Coq:
>
> Note that having an environment (i.e., a mapping from variable
> names to types) is what is done in Coq for instance.
>
Yeah, I think I wrote this too fast. It's been a while I've not been using
Coq, and I was definitely not an expert of it at that time.
The only thing I actually remember is that, in the assumptions of a goal,
in addition to having assumptions, you also have "variable declarations",
so the environment appears in the goal itself. (note that there is a good
theoretical reason for having this environment appear in the goal, which is
due to the logic used by Coq; I don't go into details though).
It's a simple question I'm asking here:
>
> 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.
>
> How does HOL Light manage to see the earlier variable with name "v" and
> type "real^2"? I would think it would be because of an environment, but
> you tell me that's not true.
>
Maybe I don't get your question here, because it looks more complex than I
thought.
Where would these environments live in the implementation of the
> logic?
>
> Ramana, all I know is that
>
> 1) retypecheck takes an environment as its first argument, and the
> environment has type
> (string * pretype) list
>
> 2) Freek's miz3.ml and John's mizar.ml are the only places in the HOL
> Light sources where retypecheck is given a non-empty environment as an
> argument. I figure it can't be that hard to understand what they did,
> especially if we use strings, as I posted here recently, instead of
> preterms.
>
I still don't understand why you want to avoid preterms.
>
> --
> Best,
> Bill
>
--
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
Verification Group
http://users.encs.concordia.ca/~vincent/
2013/4/26 Bill Richter <rich...@math.northwestern.edu>
> Thanks, Vince! That's great we're in agreement about the same symbol
> being given two different types. How hard would it be to change HOL Light
> so that it behaves like Coq:
>
> Note that having an environment (i.e., a mapping from variable
> names to types) is what is done in Coq for instance.
>
> It's a simple question I'm asking here:
>
> 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.
>
> How does HOL Light manage to see the earlier variable with name "v" and
> type "real^2"? I would think it would be because of an environment, but
> you tell me that's not true.
>
> Where would these environments live in the implementation of the
> logic?
>
> Ramana, all I know is that
>
> 1) retypecheck takes an environment as its first argument, and the
> environment has type
> (string * pretype) list
>
> 2) Freek's miz3.ml and John's mizar.ml are the only places in the HOL
> Light sources where retypecheck is given a non-empty environment as an
> argument. I figure it can't be that hard to understand what they did,
> especially if we use strings, as I posted here recently, instead of
> preterms.
>
> --
> Best,
> Bill
>
--
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
