Dependently typed system ensures strong normalization despite circularity

A sound pure type system with ranks as sorts and Type-in-Type

Logic in Computer Science

Summary

The paper addresses a technical challenge in designing logical systems that can define their own types without causing contradictions. The authors created a system where types can reference themselves in a circular way but still guarantee that computations will always finish (strong normalization). They avoid known paradoxes by carefully restricting how functions are typed according to a notion called rank. Their system behaves similarly to simpler typed languages in terms of complexity, supports complex mathematical functions, and can be modeled within established mathematical theories. The proof of these properties is straightforward and fully verified in a standard proof assistant without extra assumptions.

What this means in practice

A theory result. No direct application yet.

Authors

Pavel Sokolov, Alexander Kuklev

Abstract

We present a dependently typed pure type system that contains a circular axiom $s : s$ for a certain sort $s$ and is nonetheless strongly normalizing. Girard's paradox is avoided because our sorts are not closed under a $Π$-former: function types are placed in sorts according to their rank. Turns out that this system has a unique set of characteristics: it has similar normalization behaviour as STLC (so complexity of normalization is TOWER-complete) while at the same time allowing non-uniform representation of arbitrary elementary recursive functions; furthermore, it has a nontrivial set-theoretical model in ZF+GCH and allows to carry out nontrivial proof developments. Base normalization proof is surprisingly simple (modulo general metatheoretical properties of pure type systems) and has been fully formalized in vanilla Rocq (formerly Coq) without additional axioms.
View PDFOpen arXiv