Introduction

Quoting in natural language

The password is long.

The password is “long”.

Church’s Thesis

“Every function is computable.”

• Which notion of computable?
• Which functions?

Church’s Thesis

“For every function ℕ → ℕ there is a Kleene-index computing the function”

Church’s Thesis

“For every function ℕ → ℕ there is a term in λ-calculus computing the function”

• Which encoding?
• What quantifiers?

Church’s Thesis

• Λ’(⊥ + ⊤) is the type of terms of the λ’-calculus with one free variable.
• Square brackets are substitution of λ’-terms.
• r : ℕ → Λ’⊥ encodes the numerals as closed λ’-terms.
• _↝_ : Λ’ X → Λ’ X → Set denotes reduction relation on λ’-terms.

The setting of this talk

We will consider “type theory” in this talk to mean dependent type theory with

• Π-types
• And a limited collections of inductive types: Σ,+,⊥,⊤,Id,ℕ,Fin,Λ,Λ’,↝
• No η-rules, but we have the ξ-rule (conversion under λ-abstractions)
• No unverses (yet).

Representing (untyped) binding operations in type theory

Binding operations

Ways to express variables and substitution:

• Strings
• De Bruijn indices
• Explicit substitutions
• Combinators

The following representation is due to Bird and Paterson.

Type based de Bruijn indices

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

Examples:

• л (var (right ∗))
• л (var (left ∗))
• л (л (var (left (right ∗))))

The translation to de Bruijn indices is simply that right ∗ corresponds to the index 0 and left x is x + 1.

Type based de Bruijn indices

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

Using this representation it is easy to:

• see that Λ is a monad, with substitution as the Kleisli composition.
• define the reduction relation _↝_ : Λ X → Λ X → Set.

λ’-calculus

λ’ calculus

λ’-calculus extends λ-calculus with a new binder:

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

Examples

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

Examples

• [x]’x, or 1 ’ (var (right ∗))
• []’x, or 0 ’ (var (left ∗))
• λx.[]’x, or л (0 ’ (var (left (right ∗))))
• []’(λx.x), or 0 ’ (л (var (right ∗)))
• [x y]’(x y), or 2 ’ (app (var (right ∗)) ())

Quoting terms in λ-calculus

Detour: Church numerals

• ZERO ≔ λfx.x
• SUCC ≔ λn.λfx.f(nx)

This can be used to build a function c : ℕ → Λ ⊥ in type theory.

Detour: Alternative representation of ℕ in λ-calculus

From Martin-Löf type theory: 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

This inspires the following:

• ZERO ≔ λc₀c₁. c₀
• SUCC ≔ λn.λc₀c₁. c₁ n (n c₀ c₁)

Which gets the computation rules by β-reduction:

• ZERO c₀ c₁ ↝ c₀
• (SUCC n) c₀ c₁ ↝ c₁ n (n c₀ c₁)

This way of encoding extends to many inductive types.

Representing λ-calculus in λ-calculus

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

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

VAR = λx.  v l a. v x
LAM = λt.  v l a. l t (t v l a)
APP = λt u.v l a. a t u (t v l a) (u v l a)

Representing λ’-calculus in λ(’)-calculus

The definition we had of terms in Λ’ gives a similar representation

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

VAR   ≔ λx.    v l a q. v x
LAM   ≔ λt.    v l a q. l t (t v l a q)
APP   ≔ λt u.  v l a q. a t u (t v l a q) (u v l a q)
QUOTE ≔ λ n t. v l a q. q n t (t v l a q)

Notice: No quotes are used to represent terms.

The reduction relation in λ’-calculus: variable-quoting

A quote will only be encoding variables which it has bound:

n ’ (var (right x)) ↝ VAR (r x)

Example: We have [x]’x ↝ VAR ZERO but []’x does not reduce.

The reduction relation in λ’-calculus: λ-quoting

Informally, we want, whenever x does not occur in v:

v ’ (λx.t) ↝ LAM (x·v ’ t)

Formally, we need to do some variable yoga:

associate : Λ ((X + Fin n) + ⊤) → Λ (X + Fin (succ n))

And we get:

 n ’ (л t) ↝ app LAM ((succ n) ’ associate f)

Example

[]’(λx.x) ↝ LAM ([x] ’ x)
          ↝ LAM (VAR ZERO)

The reduction relation in λ’-calculus: app-quoting

A trap!

It would be tempting to have:

v ’ (t u) ↝ APP (v’t) (v’u)

[y]’((λx.x)y) ↝ APP (LAM (VAR ZERO)) (VAR ZERO)

[y]’((λx.x)y) ↝ [y]’y ↝ VAR ZERO

The reduction relation in λ’-calculus: app-quoting

However, this is safe, whenever the head of t is a variable in v:

v ’ (t u) ↝ APP (v’t) (v’u)

n ’ (app t u) ↝ APP (n’t) (n’u)

The reduction relation in λ’-calculus: ’-quoting

Finally, we must also be careful when quoting quotes:

Properties of the λ’-calculus

1. Confluence: Rules were carefully chosen for this.
2. Canonicity: For any normal term t : Λ(⊥+Fin(n)) the closed term n ’ t : Λ ⊥ reduces to a normal (quote-free) λ-term.

Example

Some quoted terms do not normalise:

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

Z ↝ (APP (VAR ZERO) Z).

Quoting as an extension of type theory

Representing terms of type theory in λ-calculus

• For ℕ we got an encoding in λ-calculus by looking at ℕ-elimination.
• Similarly, we can encode our other inductive types:
  • PAIR = λa b.λp. p a b for Σ-types.
  • REFL = λx.λp.p x for Id-types etc
• λ-abstraction will represented by λ-abstraction.

Consistency of type theory

Consistency of type theory can be proven from:

• Canonicity: If ⊢ a : A then 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 do we extend type theory with it?

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

Extending type theory with new constants

How much does type theory know about the new constant f?

  x:ℕ,y:ℕ , p : x ≤ y ⊢ monf x y p : f(x) ≤ f(y)

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

We first extend our type theory with the rule:

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

Examples

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

Computation rules

Now, using the representation we discussed, we add rules to compute Q-abstractions:

This is straight forward for canonical terms:

Q(Δ)(zero) ≡ zero
Q(Δ)(succ n) ≡ app SUCC (Q(Δ) n)
Q(Δ)(λ(x:A)t) ≡ л (Q(Δ,x:A)t)
(⋯)

Computation rules

But for eliminators we must make sure that the head of the principle argument is a variable bound by the quote:

Q(Δ)(elim-ℕ P n c₀ c₁)
    ≡ app (Q(Δ)n) (Q(Δ)c₀) (Q(Δ,x:ℕ,p:P(x))c₁)

is only added when the head of n is a variable in Δ.

Church’s Thesis

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
(Q(Δ,x:A)t(x)) [Q(Δ)a] ↝ Q(Δ)t(a)

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 q [r n] ↝ r (f n):

q [r n] = q [Q()n]
        ≡ 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.