Possible forms of evaluation or reduction in Martin-Löf type theory (Q1087865)

In his Report ''Constructive mathematics and computer programming'' [Report No.11, Dep. Math. Univ. Stockholm (1979; Zbl 0443.68039)] \textit{P. Martin- Löf} considers two forms of expression. A ''canonical'' expression is one which ''has itself as value'', a ''noncanonical'' expression is one ''for which it is laid down in some other way how an expression of such a form is evaluated''. As basic statements of his theory Martin-Löf has four basic ''judgements'' which are given meanings in terms of the evaluation of the noncanonical expressions that appear in them. Formally, however, the basic judgements are specified by means of twelve ''general rules'' which refer in no way to any evaluation or reduction procedure. In this paper the four judgements are defined in terms of two new primitives and some simple properties of the primitives are identified which ensure that the general rules hold. In particular reduction in \(\lambda\)-calculus and simplification of set theoretic or arithmetical expressions satisfy these properties and hence the Martin-Löf general rules.