scientific article; zbMATH DE number 1302058

The aim of this paper is to give a simple argument of normalization for a theory with ``real dependent types, i.e. a theory in which we can define types by recursion on the natural numbers (like \(N^n\)). For this we choose to study the simplest theory that has such types, namely the \(N\), \(\Pi\), \(U\)-fragment of Martin-Löf's polymorphic type theory [\textit{P. Martin-Löf}, ``An intuitionistic theory of types, same vol., 127-172 (1998; Zbl 0931.03070)] which contains the natural numbers, dependent functions and one universe. This theory has equality as conversion and is predicative. Martin-Löf gives in his paper a normalization proof based on a typed computability predicate. This paper illustrates the simplicity of \textit{W. W. Tait}'s untyped method [Lect. Notes Math. 453, 240-251 (1975; Zbl 0328.02014)]. One advantage of building an untyped realizability model is that we can separate the definition of the theory and the definition of the model. The problem when building a realizability model for theories with dependent types is that we can no longer define the realizability predicate by induction on the type. We will instead build a realizability model that captures the idea that types (formulas) and terms depend on each other. To do this, we give mutually dependent definitions of what expressions are to be realized and by what. For the entire collection see [Zbl 0899.00026].

Recommendations

Cited in

(19)

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4247302)