Tuesday February 26, 10:15–12:00

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.

The password is long.

The password is “long”.

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

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

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

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

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.

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

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

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

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

`[x]’x`

`[]’x`

`λx.[]’x`

`[]’(λx.x)`

`[x]’(x y)`

`[y]’(x y)`

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

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

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

The case for λ-abstraction:

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

…assuming `x`

is not in `X`

.

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

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

.

It would be tempting to have:

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

But, that would break confluence when rewriting under quotes.

However, this is safe:

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

when `x ≡ X i`

for some `i`

.

In fact, we can have

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

whenever the head of `t`

is a variable in `X`

.

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

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.

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

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`

.

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

.

Consistency of MLTT can be proven from:

- Canonicity: Every normal
`⊢ a : A`

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

Given a function `φ : ℕ → ℕ`

in the meta-theory, how can we extend type theory with it?

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.

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

.

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.

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

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

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

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

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.

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.

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

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`

.

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