$\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

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.

StackExchange Computer Science Q#2707, answer score: 16