# Rewriting Type Theory

ICMS 2020 in Braunschweig / Online

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:

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