Hi Reza, | John Harrison wrote (1995) that reflection hasn't proven very useful in | practice and it has workarounds in higher order logic: | http://www.cl.cam.ac.uk/~jrh13/papers/reflect.ps.gz | | But in 2005 he said that "[...] Still some more impressive applications | of reflection are starting to appear": | http://www.cl.cam.ac.uk/~jrh13/slides/wg23-07jun05/slides.pdf | | What are these more impressive applications?
There are now some good examples in Isabelle/HOL, such as the arithmetic decision procedures by Amine Chaieb and Tobias Nipkow, and an enumeration program for tame graphs, also by Tobias Nipkow. These programs are proved correct inside the system itself and then can be turned into code, run, and the results imported back. In Coq there are even more impressive examples of "reflective" decision procedures, so much so that it seems invidious to pick out any in particular. However, in the terminology of my 1995 paper, Coq's usual "reflection" would not be called reflection, being closer to the "workarounds in higher order logic" you mentioned. The point is that Coq reflection relies neither on new inference rules nor on extending the implementation with new code. Rather, the existing resources of the logic are used to define an internal syntactic "world" and the mappings to and from the semantic objects, and the core transformations are executed on the internal syntax inside the logic. In a HOL context, this is just what my 1995 paper was advocating, as you noted. In Coq, however, the rewards are much greater because this lets you use the high-performance reduction engine that is part of the logic, and avoid proof generation as well. In HOL, there is not much difference between evaluation on the internal syntax and proof in the ordinary way, so the approach only pays when you can prove strong general results about the restricted syntactic world. The following presentation I gave in Nijmegen a few years ago might be useful in elaborating this point: http://www.cl.cam.ac.uk/~jrh13/slides/nijmegen-20aug03/slides.pdf Of course, as the Coq internal reduction engine gets more highly optimized and more like an OCaml virtual machine, you might argue that the distinction between execution inside the logic and as code is artificial. However, to me there is something attractive about always staying inside a single, fixed, logical system, albeit a rather complicated one. So when I suggest that Coq's reflection is not really reflection, it's not meant pejoratively, but rather the reverse. John. ------------------------------------------------------------------------------ Come build with us! The BlackBerry(R) Developer Conference in SF, CA is the only developer event you need to attend this year. Jumpstart your developing skills, take BlackBerry mobile applications to market and stay ahead of the curve. Join us from November 9 - 12, 2009. Register now! http://p.sf.net/sfu/devconference _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
