$\lambda$-calculus with reflection 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 to
syntactic 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 or
not?

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 different
expression. 

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.
Jean Louis Krivine introduced an abstract calculus which extends the "Krivine Machine" in a very non-trivial way (note that the Krivine machine already supports the call/cc instruction from lisp):

He introduces a "quote" operator in this article defined in the following manner: if $\phi$ is a $\lambda$-term, note $n_\phi$ the image of $\phi$ by some bijection $\pi: \Lambda \rightarrow \mathbb{N}$ from lambda terms to natural numbers. Note $\overline{n}$ the church numeral which corresponds to $n\in\mathbb{N}$. Krivine defines the operator $\chi$ by the evaluation rule:
$$ \chi\ \phi \rightarrow \phi\ \overline{n_\phi}$$
I believe Kleene wizardry will show that this is sufficient to do what you wish: i.e. define a quote and eval operators, if $\pi$ is computable.

Note that Krivine is notoriously challenging to read (please don't get mad if you read this, Jean-Louis!), and some researchers have done the charitable act of trying to extract the technical content in a more readable manner. You might try to take a look at these notes by Christophe Raffali.

Hope this helps!



It occurs to me that there is another reference that may be relevant to your interests: the Pure Pattern Calculus by Jay and Kesner formalizes a variant of the $\lambda$-calculus which extends simple abstraction over a variable to an abstraction over a pattern representing a pattern calculus itself. This is phenomenally expressive and in particular allows one to deconstruct an application itself: if I am not mistaken, the term:

$$ (\lambda (x\ y). x)((\lambda x.x\ x)\ (\lambda y.y)) $$

reduces to $\lambda x.x\ x$. Again, I belive that this is more than enough to implement the quote and eval operators.