Stockholm 2019

The password is long.

The password is “long”.

“Every function is computable.”

- Which notion of computable?
- Which functions?

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

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

- Which encoding?
- What quantifiers?

*Λ*’(⊥ + ⊤) 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.

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

Ways to express variables and substitution:

- Strings
- De Bruĳn indices
- Explicit substitutions
- Combinators

The following representation is due to Bird and Paterson.

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

.

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

`[x]’x`

`[]’x`

`λx.[]’x`

`[]’(λx.x)`

`[x y]’(x y)`

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

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

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

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.

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

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.

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.

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

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

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`

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

Finally, we must also be careful when quoting quotes:

- Confluence: Rules were carefully chosen for this.
- 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`

.

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

.

- 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 can be proven from:

- Canonicity: If
`⊢ a : A`

then`a`

is canonical. - Normalisation: Every term can be reduced to a normal form.

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.

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

.

But we can add:

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

Quoting could be done in several ways:

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

This approach falls into 2.

We first extend our type theory with the rule:

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

`⊢ Q(x:ℕ)x : Λ (⊥+1)`

`x:ℕ ⊢ Q()x : Λ 0`

`⊢ (λ(x:A) → Q()x) : A → Λ ⊥`

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)
(⋯)
```

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.

The quote operation provides a candidate `q`

, given `f : ℕ → ℕ`

namely `Q(x:ℕ)(f x)`

.

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

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

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`

.

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