Possible forms of evaluation or reduction in Martin-Löf type theory (Q1087865)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Possible forms of evaluation or reduction in Martin-Löf type theory |
scientific article |
Statements
Possible forms of evaluation or reduction in Martin-Löf type theory (English)
0 references
1985
0 references
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.
0 references
constructive mathematics
0 references
noncanonical expressions
0 references
judgements
0 references