Erratum in

“Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory” and “Irrelevance in Type Theory with a Heterogeneous Equality Judgement”

Andreas Abel

22 September 2011

The Kripke model for completeness presented in Section 5 of the article [ACD08] has problems. The relation Ⓢ cannot be shown transitive, at least not directly, thus Lemma 1 breaks.

The definition is:

Δ ⊢ f : Fun XF Ⓢ Δ′ ⊢ f′ : Fun X′F′

⟺ for all Δ̂ ≤ Δ, Δ̂′ ≤ Δ′, d, d′, Δ̂ ⊢ d : X Ⓢ Δ̂′ ⊢ d′ : X′
implies Δ̂ ⊢ f · d : F · d Ⓢ Δ̂′ ⊢ f′ · d′ : F′ · d′

To show transitivity, assume Δ_{1} ⊢ f_{1} : Fun X_{1} F_{1} Ⓢ Δ_{2} ⊢ f_{2} : Fun X_{2} F_{2} and Δ_{2} ⊢ f_{2} : Fun X_{2} F_{2} Ⓢ Δ_{3} ⊢ f_{3} : Fun X_{3} F_{3} and show Δ_{1} ⊢ f_{1} : Fun X_{1} F_{1} Ⓢ Δ_{3} ⊢ f_{3} : Fun X_{3} F_{3}. That is, assume arbitrary Δ̂_{1} ≤ Δ_{1} and Δ̂_{3} ≤ Δ_{3} and Δ̂_{1} ⊢ d_{1} : X_{1} Ⓢ Δ̂_{3} ⊢ d_{3} : X_{3} and show Δ̂_{1} ⊢ f_{1} · d_{1} : F_{1} · d_{1} Ⓢ Δ̂_{3} ⊢ f_{3} · d_{3} : F_{3} · d_{3}. We would like to proceed by induction hypothesis, i.e., transitivity, on Δ̂_{1} ⊢ f_{1} · d_{1} : F_{1} · d_{1} Ⓢ Δ̂_{3} ⊢ f_{2} · d_{3} : F_{2} · d_{3} and Δ̂_{3} ⊢ f_{2} · d_{3} : F_{2} · d_{3} Ⓢ Δ̂_{3} ⊢ f_{3} · d_{3} : F_{3} · d_{3}. However, this requires us to show Δ̂_{3} ≤ Δ_{2}, which does not hold.

While a homogeneous Kripke logical relation Δ ⊢ dⓈd′ : X over a transitive base relation Δ ⊢ d®d′ : X is always transitive, this breaks down for a heterogeneous Kripke logical relation Δ ⊢ d : X Ⓢ Δ′ ⊢ d′ : X′, even if the base relation is transitive. This is what I overlooked.

The article [Abe11] has inherited this problem; the relation presented in Section 4.2 is not transitive.

A newer article [AS11] shows how to get the meta-theory right.

References

[Abe11] Andreas Abel. Irrelevance in type theory with a heterogeneous equality judgement. In Martin Hofmann, editor, Foundations of Software Science and Computational Structures, 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26 - April 3, 2011. Proceedings, volume 6604 of Lecture Notes in Computer Science, pages 57–71. Springer-Verlag, 2011.

[ACD08] Andreas Abel, Thierry Coquand, and Peter Dybjer. Verifying a semantic βη-conversion test for Martin-Löf type theory. In Philippe Audebaud and Christine Paulin-Mohring, editors, Mathematics of Program Construction, 9th International Conference, MPC 2008, Marseille, France, July 15-18, 2008. Proceedings, volume 5133 of Lecture Notes in Computer Science, pages 29–56. Springer-Verlag, 2008.

[AS11] Andreas Abel and Gabriel Scherer. On irrelevance and algorithmic equality in predicative type theory. TYPES’10 post proceedings, 2011. Submitted.