Defeq is algorithmic in HoTT

Stream: general

[Kevin Buzzard]

I'm currently browsing through the HoTT book and I notice in section 1.1 it claims that definitional equality is algorithmically decidable (in the para which defines definitional equality). My understanding is that Lean's definitional equality is not decidable. I realise I don't know the proof of this (so maybe I'm wrong), but what stops the proof from working in HoTT? Or have I misunderstood something?

[Floris van Doorn]

Lean's definitional equality is decidable if you decline to use a couple of its features (although I'm not actually sure if we proved this anywhere). These features that cause the undecidability do not exists in HoTT.
The example that causes undecidability of Lean's definitional equality that comes from Mario's master thesis involves inductive propositions, and relies on the fact that propositions are definitionally proof irrelevant (these do not exist in book-HoTT).

[Gabriel Ebner]

There's also this recent paper by Abel and Coquand, where they give an example for a (Lean) term where reduction does not terminate: https://arxiv.org/abs/1911.08174 (does not require inductive types afaict, except for maybe equality)

[Gabriel Ebner]

While searching for the Abel-Coquand paper, I also stumbled upon a new draft by Coquand:
Reduction Free Normalization for a proof-irrelevant type of propositions
https://arxiv.org/abs/2103.04287
Where he claims that defeq is decidable (for some system resembling Lean). I didn't read through it yet, so I don't know why it doesn't conflict with the other result.

[Kyle Miller]

Gabriel Ebner said:

There's also this recent paper by Abel and Coquand, where they give an example for a (Lean) term where reduction does not terminate: https://arxiv.org/abs/1911.08174 (does not require inductive types afaict, except for maybe equality)

For anyone that wants to experience the deterministic timeout themselves, here's the first example:

def False : Prop := ∀ (P : Prop), P
def True : Prop := False → False

lemma δ : True := λ z, z True z
lemma ω (h : ∀ (P Q : Prop), P = Q) : False := λ P, cast (h True P) δ
lemma Ω (h : ∀ (P Q : Prop), P = Q) : False := δ (ω h)

#reduce Ω

and the second:

def True : Prop := ∀ (P : Prop), P → P

lemma δ (z : True) : True := z (True → True) id z
lemma ω : True := λ P h, cast (propext (iff.intro (λ _, h) (λ _, id))) δ
lemma Ω : True := δ ω

#reduce Ω

[Mario Carneiro]

See also the original discussion about this paper: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Normalization.20fails.20in.20lean/near/181055359

[Ulrik Buchholtz]

Gabriel Ebner said:

Where he claims that defeq is decidable (for some system resembling Lean). I didn't read through it yet, so I don't know why it doesn't conflict with the other result.

There's no conflict, because the negative result concerns a reduction relation, while the positive result is a reduction free normalization algorithm (as it says in the title).

[Josh Chen]

From a brief skim the positive result also doesn't seem to consider propositional equality, which was central to the negative result. Is it straightforward to see that the counterexample given there doesn't transfer to the reduction-free setting?