On 04/26/2013 11:58 AM, Ramana Kumar wrote:
On Fri, Apr 26, 2013 at 4:50 PM, Vincent Aravantinos
<vincent.aravanti...@gmail.com <mailto:vincent.aravanti...@gmail.com>>
wrote:
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).
Where would these environments live in the implementation of the logic?
Are they attached to terms?
Then something like:
let x = mk_var("P",bool) in
let P = mk_var("P",`:bool->bool`) in
mk_comb(P,x)
would have to either fail or automatically rename a variable.
This could be annoying in writing automation when the variables come
from elsewhere (not just calls to mk_var).
No idea. Intuitively, I would rather pair terms with an environment
instead of considering a general environment.
--
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
