Rewriting Type Theory

ICMS 2020 in Braunschweig / Online

Jesper Cockx, Nicolas Tabareau, and Théo Winterhalter

15 July 2020

Introduction

Extending Martin-Löf Type Theory

Formation rules: \(\quad\) Bool : Type . . .
Introduction rules: \(\quad\) true false : Bool . . .
Elimination rules:
if pt : P true and pf : P false
then if b then pt else pf : P b . . .
Computation rules:
if true then pt else pf ↝ pt

Restrictions imposed by proof assistants

Strict positivity
Coverage of pattern matching
Structural recursion

Required to ensure soundness, type preservation, and effective typechecking!

Drawing outside the lines

What if this is not enough?

Option 1: use postulate
Option 2: hack the language
Option 3: use a language with rewrite rules

Rewrite rules in Agda

Using rewrite rules in three simple steps

-- 1. Enable rewriting and import primitives:
{-# OPTIONS --rewriting #-}
open import Agda.Primitive renaming (Set to Type)
open import Agda.Builtin.Equality renaming (_≡_ to _==_)
open import Agda.Builtin.Equality.Rewrite

-- 2. Postulate some things:
postulate
  id : {A : Set} → A → A
  id-comp : ∀ {A} {x : A} → id x == x

-- 3. Register the rewrite rule:
{-# REWRITE id-comp #-}

HITs that compute

postulate
  S¹   : Type
  base : S¹
  loop : base == base

module _ (P : S¹ -> Set)
         (pbase : P base)
         (ploop : pbase == pbase [ P ↓ loop ]) where

  postulate
    elim-S¹ : (x : S¹) -> P x
    elim-S¹-base : elim-S¹ base == pbase
  {-# REWRITE elim-S¹-base #-}

  postulate
    elim-S¹-loop : apd elim-S¹ loop == ploop
  {-# REWRITE elim-S¹-loop #-}

Neutral terms that compute

data Nat : Type where
  zero : Nat
  suc  : Nat → Nat

_+_ : Nat → Nat → Nat
zero    + l = l
(suc k) + l = suc (k + l)

plus-0 : ∀ k → k + zero == k
plus-0 = ⋯
{-# REWRITE plus-0 #-}

plus-suc : ∀ k l → k + suc l == suc (k + l)
plus-suc = ⋯
{-# REWRITE plus-suc #-}

Taming your rewrite rules

Rewrite rules are great! But what about…

… logical soundness?
… decidable typechecking?
… type preservation?

Logical soundness

A rewrite rule 0 ↝ 1 breaks soundness!

… but that’s no different from using postulate.

Theorem. If all rewrite rules are provable, then soundness is preserved.

Proof. By translation to extensional type theory.

Termination

A rewrite rule loop ↝ loop breaks termination!

… but termination is not a critical property.

Theorem. When the usual conversion algorithm terminates, its answer is still correct.

Proof. Computing the weak-head normal form preserves definitional equality.

Type preservation

A rewrite rule true ↝ 42 breaks subject reduction…

and this is actually a serious problem!

Three requirements to ensure subject reduction:

Rewrite rules should preserve typing
No rewriting of type constructors
Rewrite rules + β-reduction should be confluent

Checking confluence

Two problems:

Checking local confluence is not enough
Checking termination first is not possible

⇒ standard criterion on critical pairs fails!

We need a stronger property: the triangle property of parallel reduction as used by Tait and Martin-Löf

The triangle property

Parallel reduction \(⇛\) reduces all redexes in one step:

\[↝ \ ⊆\ ⇛\ ⊆\ ↝^*\]

Triangle property: each \(t\) has a best reduct \(ρ(t)\)

Checking confluence with the triangle property

The --confluence-check flag in Agda:

2.6.1: local confluence using critical pairs
2.6.2: global confluence using triangle property