Stockholm 2019

# Introduction

## 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 Bruĳn indices
• Explicit substitutions
• Combinators

The following representation is due to Bird and Paterson.

## Type based de Bruĳn 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 Bruĳn indices is simply that `right ∗` corresponds to the index 0 and `left x` is `x + 1`.

## Type based de Bruĳn 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.

Observe:

• Every Church numeral can be typed: `(X → X) → (X → X)`
• In fact these are all such functions (assuming paramatricity).
• The function `iterate : ℕ → (X → X) → (X → X)` is an instance of the elimination principle for ℕ 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)``

But, that would break confluence when rewriting under quotes:

We would have both:

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

…and…

``[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)``

Formally: When `head t = right k` for some `k : Fin n`, we have

``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.

Proof-sketch of 2: 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 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?

• Adding a new constant `f`, and a rule giving `⊢ f : ℕ → ℕ` breaks canonicity.

But adding a new constant `x:ℕ ⊢ f(x) : ℕ` does not, if…

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

``cf(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 `f`?

• Not very much: If φ is, say, monotone, the new type theory does not deduce `x:ℕ,y:ℕ , p : x ≤ y ⊢ f(x) ≤ f(y)`.

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

And computation rules, which computes `monf N[n] N[m] p` to a witness for every n and m (from our meta-theory).

## 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 Δ.

Once we have added rules for each term former, it is straight-forward to show that if `⊢ a : A` and `a` is normal in the extended theory it reduces to a term of canonical form.

## 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.

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! ☺