Abstract
First we give a grammatical (or equational) description of the set {M normal form ¦ Γ ⊢ M: A} for a given basis Γ and a given type A in the simple type system, and give some applications of the description. Then we extend the idea to systems in λ-cube and more generally to normalizing pure type systems. The attempt resulted in derived (or ‘macro’) rules the totality of which is sound and complete for type assignments of normal terms. A feature of the derived rules is that they reflect the syntactic structure of legal terms in normal form, and thus they may give us more global view than the original definition of the 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
Y. Akama. Number of proofs and tree automaton. manuscript, 1991.
H Barendregt. Lambda calculi with types. In S. Abramsky, D.M. Gabbai, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume II. Oxford University Press, 1992.
S. Berardi. Personal communication, 1993.
C.-B. Ben-Yelles. Type-assignment in the Lambda-calculus. PhD thesis, University College, Swansea, 1979.
H. Geuvers. Conservativity between logics and typed λ calculi. In H. Geuvers, editor, Informal Proceedings of the 1993 Workshop on Types for Proofs and Programs, pages 131–156, 1993.
H. Geuvers and M.J. Nederhof. Modular proof of strong normalisation for the calculus of constructions. Journal of Functional Programming, 1(2):155–189, 1991.
J.R Hindley. The Simple Theory of Type Assignment. Forthcoming.
S. Hirokawa. The number of proofs for implicational formulas(abstract). In Proceedings of Logic Colloquium '92, volume 36. Janos Bolyai Mathematical Society, 1992.
J.E. Hopcroft and J.D. Ullman. Introduction to Automata Theory, Languages and Computation. Addison-Wesley, 1979.
M. Löb. Embedding first order predicate logic in fragments of intuitionistic logic. Journal of Symbolic Logic, 41(4):705–718, 1976.
D. Prawitz. Natural Deduction. Almqvist and Wiksell, 1965. Stockholm.
L.S. van Benthem Jutting. Typing in pure type systems. Information and Computation, 105:30–41, 1993.
M. Zaionc. Word operation definable in the typed λ-calculus. Theoretical computer science, 52:1–14, 1987.
M. Zaionc. λ-definability on free algebras. Annals of Pure and Applied Logic, 51:279–300, 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Takahashi, M., Akama, Y., Hirokawa, S. (1994). Normal proofs and their grammar. In: Hagiya, M., Mitchell, J.C. (eds) Theoretical Aspects of Computer Software. TACS 1994. Lecture Notes in Computer Science, vol 789. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57887-0_111
Download citation
DOI: https://doi.org/10.1007/3-540-57887-0_111
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57887-1
Online ISBN: 978-3-540-48383-0
eBook Packages: Springer Book Archive