zbMATH — the first resource for mathematics

Terminating general recursion. (English) Zbl 0659.68020
In Martin-Löf’s type theory, general recursion is not available. The only iterating constructs are primitive recursion over natural numbers and other inductive sets. The paper describes a way to allow a general recursion operator in type theory (extended with propositions). A proof rule for the new operator is presented. The addition of the new operator will not distroy the property that all well-typed programs terminate. An advantage of the new program construct is that it is possible to separate the termination proof of the program from the proof of other properties.
Reviewer: B.Nordström

68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science
03B15 Higher-order logic; type theory (MSC2010)
68N01 General topics in the theory of software
Full Text: DOI
[1] Peter Aczel. An introduction to inductive definitions. In J. Barwise, editor,Handbook of Mathematical Logic, pages 739-, North-Holland Publishing Company, 1977.
[2] R. L. Constable and et. al.Implementing Mathematics with the NuPRL Proof Development System. Prentice-Hall, Englewood Cliffs, NJ, 1986.
[3] Per Martin-Löf. Constructive mathematics and computer programming. InLogic, Methodology and Philosophy of Science, VI, 1979, pages 153–175, North-Holland, 1982. · Zbl 0443.68039
[4] Per Martin-Löf.Intuitionistic Type Theory. Bibliopolis, Napoli, 1984.
[5] Bengt Nordström and Kent Petersson.The Semantics of Module Specifications in Martin-Löf’s Type Theory. PMG Report 36, Chalmers University of Technology, S-412 96 Göteborg, 1987. · Zbl 0744.03029
[6] Bengt Nordström and Kent Petersson. Types and specifications. In R. E. A. Mason, editor,Proceedings of IFIP 83, pages 915–920, Elsevier Science Publishers, Amsterdam, October 1983.
[7] Bengt Nordström and Jan Smith. Propositions, types and specifications in Martin-Löf’s type theory.BIT, 24(3):288–301, October 1984. · Zbl 0551.68027 · doi:10.1007/BF02136027
[8] Lawrence C. Paulson. Constructing recursion operators in intuitionistic type theory.Journal of Symbolic Computation, (2):325–355, 1986. · Zbl 0631.03045
[9] Lawrence C. Paulson.Natural Deduction Proof as Higher-Order Resolution. Technical report 82, University of Cambridge Computer Laboratory, Cambridge, 1985. · Zbl 0576.68070
[10] Kent Petersson.A Programming System for Type Theory. PMG report 9, Chalmers University of Technology, S-412 96 Göteborg, 1982, 1984.
[11] E. Saaman and G. Malcolm.Well-founded Recursion in Type theory. Technical Report, Subfaculteit Wiskunde en Informatica, Rijksuniversiteit Groningen, Netherlands, 1987.
[12] Jan M. Smith. The identification of propositions and types in Martin-Löf’s type theory. InFoundations of Computation Theory, Proceedings of the Conference, pages 445–456, 1983.
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.