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[0] 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 natural language

Quoting in natural language

The password is long.

The password is “long”.

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

> ((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[0]))
• []’x is normal (x is free).
• λx.[]’x is normal.
• []’(λx.x) ↝ (л (var (r[0])))
• [x]’(x y) ↝ (app (var (r[0])) 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[0])) 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.

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

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.

But we can add:

  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 deBruijn-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)

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.