Possible forms of evaluation or reduction in Martin-Löf type theory
type: Item
instance of: scholarly article
title: Possible forms of evaluation or reduction in Martin-Löf type theory
zbMATH Open document ID: 0612.03007
DOI: 10.1016/0304-3975(85)90065-9
published in: Theoretical Computer Science
publication date: 1985-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03B15
Mathematics Subject Classification ID: 03B70
zbMATH DE Number: 3989321
zbMATH Keywords: constructive mathematics
zbMATH Keywords: noncanonical expressions
zbMATH Keywords: judgements
author: Martin W. Bunder
MaRDI profile type: Publication
full work available at URL: 0304-3975(85)90065-9
OpenAlex ID: W2082341006
cites work: Constructive mathematics and computer programming
cites work: Q3918095
description: scientific article; zbMATH DE number 3989321