I'm looking for a simple calculus that supports reasoning about reflection, namely, the introspection and manipulation of running programs.Is there an untyped $\lambda$-calculus extension that enables one to convert $\lambda$-terms into a form that can be syntactically manipulated and then subsequently evaluated?I imagine that the calculus has two main additional terms:$\mathtt{reflect}\ v$: takes $v$ and produces a representation of $v$ amendable tosyntactic manipulation.$\mathtt{eval}\ v$: takes a syntactic representation of a term and evaluates it.In order to support reflection, a syntactic representation of terms is required. It would look something like:$\lambda x.e$ would be represented as a term $(\mathsf{LAM}\ R(e))$, where$R(e)$ is the reflected version of $e$,$e\ e'$ would be represented as term $(\mathsf{APP}\ R(e)\ R(e'))$, and$x$ would be represented as $(\mathsf{VAR}\ x)$.With this representation, pattern matching could be used to manipulate terms.But we run into a problem. $\mathtt{reflect}$ and $\mathtt{eval}$ need to be encoded as terms, as does pattern matching. Dealing with this seems to be straightforward,adding $\mathsf{REFLECT}$, $\mathsf{EVAL}$ and $\mathsf{MATCH}$, but will I need to add other terms to support the manipulation of these?There are design choices that need to be made. What should the $R(-)$ function alluded to above do with the body of $\mathtt{reflect}$ and $\mathtt{eval}$? Should $R(-)$ transform the body ornot?As I am not so much interested in studying reflection itself -- the calculus would serve as a vehicle for other research -- I do not want to reinvent the wheel.Are there any existing calculi that match what I have just described?As far as I can tell, calculi such as MetaML, suggested in a comment, go a long way, but they do not include the ability to pattern match and deconstruct code fragments that have already been built.One thing I would like to be able to do is the following:$\mathtt{let}\ x=\lambda y.y\ \mathtt{in}\ \mathtt{reflect}\ x \to (\mathsf{LAM}\ (\mathsf{VAR}\ y)\ (\mathsf{VAR}\ y))$And then perform pattern matching on the result to build a completely differentexpression. This is certainly not a conservative extension to the $\lambda$-calculus and the meta-theory is likely to be ugly, but this is kind of the point for my application. I want to break $\lambda$-abstractions apart.
$\lambda$-calculus with reflection
logic;lambda calculus;semantics;reflection