On Sun, May 5, 2013 at 5:52 PM, Bill Richter
<rich...@math.northwestern.edu>wrote:
> Did I show this wasn't true in this theorem biz here, and did Ramana show
> it wasn't true in HOL4 with DB.fetch?
>
Not quite. Using a database that maps strings to values is a way to solve
the problem of looking up a theorem by its name. But the it doesn't solve
the problem of being able to represent and evaluate an OCaml expression
within OCaml. It just so happens that the only expressions you care about
are variable references, which are conveniently represented by strings.
Also, notice the painful duplication you needed to go through to create the
thmlist_tactics list ("Why do I have to list all of these both with quotes
and without?").
>
> RK> (Side note: some languages are their own meta-languages, like
> RK> Scheme, where a quoted expression is a value
>
> I didn't know to call it a meta-language, Ramana, but the lure of Scheme
> has been bugging me for a while, as a standard exercise in Scheme is to
> write a Scheme->Scheme interpreter using quotes. Would it be easy for HOL
> to get a similar quote feature?
>
The language I mentioned before, reFLect, has the quote feature. Look into
it. Also, ACL2 is another theorem prover which uses the same language for
both the logic and the implementation.
It would not at all be an easy extension to HOL4 or HOL Light.
>
> --
> Best,
> Bill
>
>
> ------------------------------------------------------------------------------
> Get 100% visibility into Java/.NET code with AppDynamics Lite
> It's a free troubleshooting tool designed for production
> Get down to code-level detail for bottlenecks, with <2% overhead.
> Download for free and get started troubleshooting in minutes.
> http://p.sf.net/sfu/appdyn_d2d_ap2
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
Introducing AppDynamics Lite, a free troubleshooting tool for Java/.NET
Get 100% visibility into your production application - at no cost.
Code-level diagnostics for performance bottlenecks with <2% overhead
Download for free and get started troubleshooting in minutes.
http://p.sf.net/sfu/appdyn_d2d_ap1
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
