$\lambda$-calculus with reflection

Question

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.

Answer 1

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.

Answer 2

Doing so is very difficult, if not imposible, without giving up confluence. Which is to say, I suspect you are right about a hairy meta-theory. On the other hand, it is possible to design a combinator calculus that can express all turing computable functions, and that has full ability to inspect its terms: see Jay and Give-Wilson .

I believe that having this ability does some bad things to your equational theory, however. In particular you will tend to only be able to prove two values are equal if the the are equal up to alpha equivalences.

I have not yet read the Krivine paper cody linked to, but I should note that in Classical logic you essentially have only two things: true, and false. Everything is equivalent to one of those. That is, you tend to have a collapsed equational theory anyways.

Answer 3

In the theory of programming languages the feature you speak about is usually referred to as "quote". For instance, John Longley wrote about it in some of his work, see this paper.

If you are just after theoretical considerations (as opposed to an actualy useful implementation) then you can simplify things by stating that quote (or reflect as you call it) maps into the type of integers nat by returning a Gödel code of its argument. You can then decompose the number just as you would an abstract syntax tree. Furthermore, you do not need eval because that can be implemented in the language – it is essentially an interpreter for the language.

For a concrete model which has these features you can consider Kleene's first combinatory algebra: interpret everything as a number (think of them as Gödel codes) and define Kleene application $n \star m$ to mean $\varphi_n(m)$ where $\varphi_n$ is the $n$-th partial function. This will give you a model of $\lambda$-calculus (with partial maps) in which quote is simply the identity function. No further features need to be added to the language.

If you tell me what you're after, I may be able to give you more specific references.

By the way, here is an open problem:

Enrich $\lambda$-calculus (typed or untyped) with quote which is a congruence in such a way that you preserve the $\xi$-rule.

The $\xi$-rule $$\frac{e_1 \equiv e_2}{\lambda x \,.\, e_1 \equiv \lambda x \,.\, e_2}$$ says that $\lambda$-abstraction is a congruence. It allows us to reduce under $\lambda$ so to speak. In combination with quote this becomes problematic, since quote is supposed to be a congruence as well, $$\frac{e_1 \equiv e_2}{\mathtt{quote}\,e_1 \equiv \mathtt{quote}\,e_2},$$ so for instance we see that it must be the case that $$\mathtt{quote}\,((\lambda x \,.\,x) y) \equiv \mathtt{quote}\, y.$$ So somehow this quote is supposed to calculate "very canonical" Gödel codes – but even assuming we have a typed $\lambda$-calculus without recursion this seems to be hard to do.

Answer 4

Here is an alternative answer, instead of using my nominal approach which is still experimental there is some more established approach that goes back to the paper:

LEAP: A language with eval and polymorphism
Frank Pfenning and Peter Lee
https://www.cs.cmu.edu/~fp/papers/tapsoft89.pdf

The paper starts with:

This then led us to the question, first posed by Reynolds, of whether strongly typed languages admit metacircular interpreters. Conventional wisdom seemed to indicate that the answer was "No". Our answer is "Almost".

Please note that LEAP is much stronger than what the OP wants. First of all it is typed. And second it asks for metacircularity, which means for example that eval can execute its own definition. In Prolog you get metacircularity for solve/1:

solve(true).
solve((A,B)) :- solve(A), solve(B).
solve(H) :- clause(H,B), solve(B).

If you add the following clause to solve/1:

solve(clause(H,B)) :- clause(H,B).

And if you see to it that clause/2 also returns the clauses of solve/1. You can then call solve(solve(...)) and see how solve executes itself.

Questions of self representatio still spurr some research, see for example:

Self representation in Girards System U
Matt Brown, Jens Palsberg
http://compilers.cs.ucla.edu/popl15/popl15-full.pdf

Answer 5

The problem is identified in vincinity of proof assistants such as Coq and Isabelle/HOL. It goes under the acronym HOAS. There are some claims around λ-Prolog that through the new ∇ quantifier such things can be done. But I couldn't get a grip yet of this claim. I guess the main insight I got so far is that there is no definite approach, there are a couple of possible approaches.

My own take, not yet finished, is inspired by a recent paper by Paulson on proving Gödels incompletness. I would use the object-level binders in connection with some data structure that has the meta-level names. Basically a similar yet distinct data structure as the one from the OP, and with Church coding since I am interested in dependent types:

datatype Expr = var Name                 /* written as n */
              | app Expr Expr            /* written as s t */
              | abs Name Expr Expr       /* written as λn:s.t */

The meta level expressions can be distinguished from the object level expressions in that we use the variable names n, m, .. etc.. to denote names. Whereas we use the variable names x, y, .. etc.. on the object level. The interpretation of a meta term in the object logic would then work as follows. Lets write [t]σ for the interpretation of the nominal term t in the nominal context σ, which should give an object term. We would then have:

 [n]σ = lookup σ n
 [s t]σ = [s]σ [t]σ
 [λn:s.t]σ = λx:[s]σ.[t]σ,n:x

The above would define what the OP calls an EVAL function. Small difference to Paulson, σ is only a finite list and not a functional. In my opinion it would be only possible to introduce an EVAL function and not a REFLECT function. Since on the object level you might have some equality so that different lambda expressions are the same. What you have to do would be to use eval to reason possibly also about reflection if you feel the need.

You would need to go to extremes like Prolog where nothing is expanded, if you want to tear down the wall between nominal and non-nominal. But as the λ-Prolog system example shows, in the higher-order case there are luring additional problems which can for example only be overcome in logical way by introducing new means such as a ∇ quantifier!