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 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
⊢ 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
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))
x is not in
X’(Xi) ↝ (var (r[i]))
[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))
x ≡ X i for some
In fact, we can have
X’(t u) ↝ (app (X’t) (X’u))
whenever the head of
t is a variable in
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))
’xis normal (
’(λx.x) ↝ (л (var (r)))
[x]’(x y) ↝ (app (var (r)) y)
[y]’(x y)is normal.
t is normal and
FV(t) are all in
X’t reduces to a
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
Some quoted terms do not normalise:
Z = [f]’((λx. f (x x)) (λx. f (x x))) has the property that
Z ↝ (app (var (r)) Z).
Consistency of MLTT can be proven from:
⊢ a : Ais canonical.
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]
N[n]=sⁿz is the numeral representation of
n in type theory.
How much does type theory know about the new constant
But we can add:
x:ℕ,y:ℕ , p : x ≤ y ⊢ monφ p : cφ(x) ≤ cφ(y)
And computation rules, which computes
Quoting could be done in several ways:
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 Δ.
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]
subst : Λ(X+1) → Λ(X) → Λ(X) is the internally defined substitution of λ’-terms)
The quote operation provides a candidate
f : ℕ → ℕ namely
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)
t(a) denotes the substitution of
a on the type theory level, and
subst is the internally defined
By induction one can show that
r[n] = Q()n.
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-SUBSTand proving normalisation and canonicity for these.