Quote operations

Abstract

This project explores confluent quoting operations in extensions of formal languages such as λ-calculus and type theories. The goals is to establish weather quoting is an acceptable constructive principle.

Documents

Introduction

Quoting is a fundamental linguistic operation. Its rôle is to turn expressions back into syntactic objects allowing us to discuss it from a syntactic point of view:

“read” has four letters.

The sentence ““read” has four letters.” has four words.

In some programming languages, such as LISP or Scheme, quoting is a fundamental operation as well. There the quoting operation takes an expression and turns it into its abstract syntax tree, which then can be manipulated and evaluated.

While quoting in LIPS or Scheme is practical and useful, there is a theoretical catch: one cannot rewrite under the quote (except for unquoted sub-expressions). The reason is that such a rewring would fail to be confluent. In Scheme, (quote ((lambda (x) x) 3) evaluates to a completely different expression than (quote 3), even though ((lambda (x) x) 3) evaluates to 3.

Further complications arise when evaluation is mixed in. While the following expression gives an error:

> (((lambda (y) (lambda (x) y)) (eval 'x)) 3)
Error: eval: unbound variable: x

the following β-equivalent expression returns a value:

> ((lambda (x) (eval 'x)) 3)
3

This is one of several ways Scheme does not behave confluently, but this way is particularly notable because quoting is not an inherently imperative or stateful operation. We may therefore wonder if there is some other way of handling quoting which would result in a more theoretically sound reduction calculus.

In order to study quoting, we introduce an extension of λ-calculus with a quoting operation. In order to deal with the issues sketched above, the quoting operation is a variable binding operation and we allow rewring expressions under quotes. In fact, we only compute quotes of expressions once they are reduced to weak head normal form.