ICMS 2020 in Braunschweig / Online

**Jesper Cockx**, Nicolas Tabareau, and Théo Winterhalter

15 July 2020

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

- Strict positivity
- Coverage of pattern matching
- Structural recursion

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

What if this is not enough?

- Option 1: use
`postulate`

- Option 2: hack the language
- Option 3: use a language with
*rewrite rules*

-- 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 #-}

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 #-}

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 #-}

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

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.

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.

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*

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

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

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

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

The `--confluence-check`

flag in Agda:

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

- Agda documentation:

agda.readthedocs.io - Paper on rewriting in Agda:

jesper.sikanda.be/publications.html - Formalization in MetaCoq (work in progress):

https://github.com/TheoWinterhalter/template-coq/