# Quoting operations as extensions of λ-calculus and type theory

Tuesday February 26, 10:15–12:00

## Abstract

Going back to Gödel, we know that many formal languages have the ability to represent its own syntax. The operation which turns an expression into its internal representation is called quoting. For programming languages, one can also ask if they can internally represent their own evaluation function. Work by Brown and Palsberg show that this is even possible to some extent for strongly normalising languages.

Quoting usually a meta-theoretical operation. However, some programming languages, such as LISP or Scheme, have this as internal operation in the language. In this talk I will present extensions of λ-calculus and type theory with internal quoting operations. They differ from the LIPS or Scheme equivalents by being confluent while allowing reductions under the quote.

# Quoting in Scheme

## Quoting in Scheme: Example 0

`````` > (' (lambda (x) x))
(lambda (x) x)``````

## Quoting in Scheme: Example 0

`````` > (' (lambda (x) x))
(list 'lambda (list 'x) 'x)``````

## Quoting in Scheme: Example 1

Reductions cannot be de done under the quote:

``````> (' ((lambda (x) x) 'z)
(list ('lambda (list 'x) 'x) 3)``````

which is very different from the quote of `3`, (which is the number 3 itself).

## Quoting in Scheme: Example 2

The following expression gives an error:

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

but the following β-equivalent expression returns a value:

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

# Representing λ-calculus in λ-calculus

## Church numerals

The church numeral `c[n]`, represents the natural number `n`, by a term in λ-calculus:

• `c[z] = λf x. x`
• `c[s n] = λf x. f c[n]`

This could be typed as: `c[n] : Π x → (x → x) → (x → x)`.

Moral: Applying a Church numeral, corresponds to a kind of recursor.

## Alternative representation of ℕ in λ-calculus

From MLTT: Induction principle for ℕ:

``````x:ℕ        ⊢ P x type
⊢ c₀ : P z
x:ℕ,y:P(x) ⊢ c₁ : P (s n)
──────────────────────────── ℕ-ELIM
x : ℕ ⊢ elim-ℕ P x c₀ c₁ : P x``````

Computation rules:

`````` ⊢ elim-ℕ P z     c₀ c₁ ≡ c₀
⊢ elim-ℕ P (s n) c₀ c₁ ≡ c₁ n (elim-ℕ P n c₀ c₁)``````

## Alternative representation of ℕ in λ-calculus

Given a natural number `n` we can define an alternative representation `r[n]`, inspired by the elimination rule for ℕ:

• `r[z] = λ c₀ c₁. c₀`
• `r[s n] = λ c₀ c₁. c₁ (r[n]) (r[n] c₀ c₁)`

## Representing λ-calculus in type theory

``````data Λ (X : Set) : Set where
var : X → Λ X
л : Λ (X + 1) → Λ X
app : Λ X → Λ X → Λ X``````

Which inspires the following the representation of λ-calculus in λ-calculus:

``````var = λx   cv cl ca. cv x
л   = λt   cv cl ca. cl t (t cv cl ca)
app = λt u cv cl ca. ca t u (t cv cl ca) (u cv cl ca)``````

# Extending λ-calculus with a quote operator

## Quoting as a binder

Extend the syntax of λ-calculus with a new binder:

``````t term   X list of distinct variables
─────────────────────────────────────
X’t term

FV (X’t) = FV t \ X``````

## Examples

• `[x]’x`
• `[]’x`
• `λx.[]’x`
• `[]’(λx.x)`
• `[x]’(x y)`
• `[y]’(x y)`

## Representing λ’-calculus in type theory

``````data Λ (X : Set) : Set where
var : X → Λ X
л : Λ (X + 1) → Λ X
app : Λ X → Λ X → Λ X
_’_ : (n : ℕ) → Λ (X + Fin n) → Λ X``````

Using this representation, we can for instance implement a substitution operation `subst : Λ(X+1) → Λ(X) → Λ(X)`

## Rewriting under quotes

We want to be able to rewrite under the quote – i.e.:

``t ↝ u   ⇒   X’t ↝ X’u ``

# Computation rules for the quote

## Computation rules for the quote: λ

The case for λ-abstraction:

`` X’(λy.t) ↝ (л (X.y ’ t))``

…assuming `x` is not in `X`.

## Computation rules for the quote: variables

`` X’(Xi) ↝ (var (r[i]))``

Example: `[x,y]’y ↝ var (r[s z])`.

## Computation rules for the quote: Application

It would be tempting to have:

``X’(t u) ↝ (app (X’t) (X’u))``

But, that would break confluence when rewriting under quotes.

## Computation rules for the quote: Application

However, this is safe:

``X’(x u) ↝ (app (X’x) (X’u))``

when `x ≡ X i` for some `i`.

## Computation rules for the quote: Application

In fact, we can have

``X’(t u) ↝ (app (X’t) (X’u))``

whenever the head of `t` is a variable in `X`.

## Computation rules for the quote: Quote

Finally, we need rules for quoting quotes: needing first a representation of the quote constructor in λ-calculus:

``````var = λx   cv cl ca cq. cv x
л   = λt   cv cl ca cq. cl t (t cv cl ca cq)
app = λt u cv cl ca cq. ca t u (t cv cl ca cq) (u cv cl ca cq)
quote = λ n t cv cl ca cq. cq n t (t cv cl ca cq)``````

## Computation rules for the quote: Quote

Again, we cannot always have:

``X’(Y’u) ↝ quote (r[∥Y∥]) (X.Y’u)``

But must require that the head of `u` is a variable in X, and X and Y must be disjoint.

## Example computations

• `[x]’x ↝ (var (r))`
• `[]’x` is normal (`x` is free).
• `λx.[]’x` is normal.
• `[]’(λx.x) ↝ (л (var (r)))`
• `[x]’(x y) ↝ (app (var (r)) y)`
• `[y]’(x y)` is normal.

## Observation

If `t` is normal and `FV(t)` are all in `X`, then `X’t` reduces to a `’`-free term.

Proof-sketch: By induction on `t`: we have given rules reducing `X’t` for each head normal form `t` could have. Each computation rule applies `’` only to subterms of `t`.

## Example

Some quoted terms do not normalise:

`Z = [f]’((λx. f (x x)) (λx. f (x x)))` has the property that

`Z ↝ (app (var (r)) Z)`.

# Quoting as an extension of MLTT

## Consistency of type theory

Consistency of MLTT can be proven from:

• Canonicity: Every normal `⊢ a : A` is canonical.
• Normalisation: Every term can be reduced to a normal form.

## Extending type theory with new constants

Given a function `φ : ℕ → ℕ` in the meta-theory, how can we extend type theory with it?

## Extending type theory with new constants

Adding a constant `⊢ cφ : ℕ → ℕ` breaks canonicity.

But adding a constant `x : ℕ ⊢ cφ(x) : ℕ` does not…

if we also add (for each `n : ℕ` in the meta theory) a computation rule:

``cφ(N[n]) ≡ N[φ n]``

where `N[n]=sⁿz` is the numeral representation of `n` in type theory.

## Extending type theory with new constants

How much does type theory know about the new constant `cφ`?

• Not very much: If φ is, say, monotone, type theory does not know it.

``  x:ℕ,y:ℕ , p : x ≤ y ⊢ monφ p : cφ(x) ≤ cφ(y)``

And computation rules, which computes `monφ (Nn)(Nm)`.

## Choices

Quoting could be done in several ways:

1. Quoting into an internal representation of type theory syntax (with quoting extensions).
2. Quoting into λ’-calculus

This approach falls into 2.

## The typed quoting binder

``````  Γ·Δ ⊢ a : A
─────────────── QUOTE
Γ ⊢ Q(Δ)a : Λ(Fin ∥Δ∥)``````

## Examples

• `⊢ Q(x:ℕ)x : Λ (0+1)`
• `x:ℕ ⊢ Q()x : Λ 0`
• `⊢ (λ(x:A) → Q()x) : A → Λ 0`

## Computation rules

We add computation rules for `Q` similar to those we had in the λ’-calculus. As an example, here are the computations rules for quoting natural numbers:

``````Q(Δ)z ≡ л л v₊
Q(Δ)(s t)
≡ л л (app (app v (Q(Δ)t) (app (app (Q(Δ)t) v) v₊))
Q(Δ)(elim-ℕ P u c₀ c₁)
≡ app (app (Q(Δ)u) (Q(Δ)c₀)) (Q(Δ,x:ℕ,y:P(x))c₁)``````

The quote rule for the eliminator applies only whenever the head of `u` is in Δ.

Here `v` and `v₊` are deBruĳn-indices.

## Church’s thesis in type theory

Given an internal definition of `r[-] : ℕ → Λ 0`, we propose the following alternative internalisation of church thesis.

``````∏(f : ℕ → ℕ) ∑(q : Λ (0+1)) ∏ (n:ℕ)
(subst q (r[n])) ↝ r[f n]``````

(Where `subst : Λ(X+1) → Λ(X) → Λ(X)` is the internally defined substitution of λ’-terms)

The quote operation provides a candidate `q`, given `f : ℕ → ℕ` namely `Q(x:ℕ)(f x)`.

• Further extensions needed to show the rest of the statement.

## Substitution rule

Here is such a further substitution rule:

``````Δ,x:A ⊢ t(x) : B(x)  Δ ⊢ a:A
────────────────────────────────────── Q-SUBST
subst (Q(Δ,x:A)t(x)) (Q(Δ)a) ↝ Q(Δ)t(a)``````

Where `t(a)` denotes the substitution of `x` with `a` on the type theory level, and `subst` is the internally defined

## Church thesis from Q-SUBST (proof sketch)

By induction one can show that `r[n] = Q()n`.

So given `f : ℕ → ℕ`, we let `q ≔ Q(x:ℕ)(f x)`, and must prove `(subst q (r[n])) ↝ r[f n]`:

``````subst q (r[n]) = subst q (Q()n)
≡ subst (Q(x:ℕ)(f x)) (Q()n)
↝ Q()(f n)
= r[f n]``````

The reduction step uses `Q-SUBST`.

## Current status

• Definition of λ’-calculus and substitution formalised in Agda.
• Still many proofs to formalise (confluence, normalisation)
• An interpreter implemented in Haskell (and a small programming language based on the calculus).
• Ongoing: Giving the computation rules for `Q-SUBST` and proving normalisation and canonicity for these.

Expecting a comment section? Feel free to e-mail me your comments, or otherwise contact me to discuss the content of this site. See my contact info. You can also write your opinion on your own website, and link back here! ☺