Abstract
We present a concrete example of how one can extract constructive content from a non-constructive proof. The proof investigated is a termination proof of the string-rewriting system 1100 → 000111. This rewriting system is self-embedding, so the standard termination techniques which rely on Kruskal's Tree Theorem cannot be applied directly. Dershowitz and Hoot [3] have given a classical termination proof using a minimal bad sequence argument. We analyse their proof and give a constructive interpretation of it, which enables us to extract a first proof in Type Theory that uses generalised inductive definitions. By simplifying this constructive proof we obtain a second proof in a theory conservative over primitive recursive arithmetic. This proof is generalised to a theorem about string rewriting systems.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
P. Aczel. An Introduction to Inductive Definitions. In J. Barwise, editor, Handbook of Mathematical Logic, pages 739–782. North-Holland Publishing Company, 1977.
Th. Coquand. Constructive topology and combinatorics. In proceeding of the conference Constructivity in Computer Science, San Antonio, LNCS 613, pages 28–32, 1992.
N. Dershowitz and C. Hoot. Topics in termination. In proceeding of the 5th Conf. Rewriting Techniques and Applications, Montreal, LNCS 690, pages 198–212, 1993.
N. Dershowitz and C. Hoot. Natural termination. Theoret. Comput. Sci., 142(2):179–207, 1995. Selected papers of the Fifth International Conference on Rewriting Techniques and Applications (Montreal, PQ, 1993).
H. Lombardi. Relecture constructive de la theorie d'Artin-Schrier. Prepublication, March 1994.
C. Murthy. Extracting Constructive Content from Classical Proofs. PhD thesis, Cornell University, 1990.
C. Nash-Williams. On well-quasi-ordering finite trees. Proceedings of the Cambridge Philosophical Society, 59:833–835, 1963.
B. Nordström, K. Petersson, and J. M. Smith. Programming in Martin-Löf's Type Theory. An Introduction. Oxford University Press, 1990.
C. Parsons. On a number theoretic choice schema and its relation to induction. In Intuitionism and Proof Theory (Proc. Conf., Buffalo, N. Y., 1968), pages 459–473. North-Holland, Amsterdam, 1970.
J. Peterson and K. Hammond. The Haskell 1.3 Report. Technical Report YALEU/DCS/RR-1106, Yale University, 1996.
J-C. Raoult. Proving open properties by induction. Information processing letters, 29:19–23, 1988.
S. G. Simpson. Partial realizations of Hilbert's Program. J. Symbolic Logic, 53(2):349–363, 1988.
E. Tahhan-Bittar. Non-erasing, right-linear orthogonal term rewrite systems, application to Zantema's problem. Technical Report RR2202, INRIA, France, 1994.
W. Pohlers W. Sieg W. Buchholz, S. Feferman. Iterated inductive definitions and subsystems of analysis, volume Recent Proof-Theoretical Studies of Lecture Notes in Mathematics 897 Springer-Verlag, 1981.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Coquand, T., Persson, H. (1998). A proof-theoretical investigation of Zantema's problem. In: Nielsen, M., Thomas, W. (eds) Computer Science Logic. CSL 1997. Lecture Notes in Computer Science, vol 1414. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028014
Download citation
DOI: https://doi.org/10.1007/BFb0028014
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64570-2
Online ISBN: 978-3-540-69353-6
eBook Packages: Springer Book Archive