HTML
|
HTML |
There have been individual notions of reflection in different branches of logic and computer science. Apart from an intuitive connection between these notions about a ``meta'' level, there is little understanding of relationships between them. In this paper, we present a preliminary report of an exploration of a deeper understanding of these relationships. The three notions we are going to explore are: logical, computational and monadic. Based on the logical notion, we setup a framework of desirable properties with which to evaluate the other forms of reflection. Computational reflection does not satisfy some these properties, while monadic reflection does. Computational reflection is, however, of greater utility, since it allows finer control over program implementation. Based on some of this understanding, we show how this utility of computational reflection can be achieved in the framework of monadic reflection by separating base-code from meta-code, and restricting them in certain ways. This allows us to use the reasoning mechanisms provided by the lambda calculus for reflective programming.
