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
     : Type
  base : 
  loop : base == base

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

  postulate
    elim-S¹ : (x : ) -> 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:

  1. Rewrite rules should preserve typing
  2. No rewriting of type constructors
  3. 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

Conclusion

Further reading

Go forth and rewrite!