zbMATH — the first resource for mathematics

Normal forms in the typed \(\lambda\)-calculus with tuple types. (English) Zbl 0594.03005
The author studies a typed lambda calculus that includes tuples of terms with, as types, cartesian products of types, as well as a projection function. The theory does not have intersections and disjoint unions, included in some other modern systems. A generalized form of reduction is defined which is shown to be both strongly normalizing and Church-Rosser.
Reviewer: M.W.Bunder
03B40 Combinatory logic and lambda calculus
Full Text: EuDML
[1] H. P. Barendregt: The Lambda Calculus. Its syntax and semantics. (Studies in Logic and the Foundations of Mathematics 103.), North-Holland, Amsterdam 1981. · Zbl 0467.03010
[2] A. Church: A formulation of the simple theory of types. J. Symb. Logic 5 (1948), 1, 56-68. · Zbl 0023.28901
[3] A. Church: The Calculi of \(\lambda\)-conversion. (Annals of Mathematics Studies No. 6.), Princeton University Press, Princeton 1941 (1951). · Zbl 0026.24205
[4] R. O. Gandy: An early proof of normalization by A. M. Turing. To H. B. Curry: Essays on Combinatory Logic, Lambda-calculus and Formalism (J. R. Hindley, J. P. Seldin, Academic Press, London 1980, pp. 453 - 456.
[5] R. O. Gandy: Proofs of strong normalization. [4], pp. 457-477.
[6] M. H. A. Newman: On theories with a combinatorial definition of ”equivalence”. Ann. of Math. (2), 43 (1942), 223-243. · Zbl 0060.12501
[7] D. S. Scott: Lectures on a Mathematical Theory of Computation. Oxford University Computing Laboratory, Technical Monograph PRG-19, 1981.
[8] D. S. Scott: Relating theories of the \(\lambda\)-calculus. [4], pp. 403 - 450.
[9] A. S. Troelstra (ed.): Metamathematical Investigations of Intuitionistic Arithmetic and Analysis. (Lecture Notes in Mathematics 344). Springer-Verlag, Berlin 1973. · Zbl 0275.02025
[10] J. Zlatuška: HIT data model. Data bases from the functional point of view. Proc. 11th VLDB (A. Pirotte, Y. Vassiliou, Stockholm 1985, pp. 470-477.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.