Abstract
Suppose that Λ is a model for untyped λ-calculus and that T is some typed λ-calculus (transfinite, second order or whatever). One standard procedure for obtaining a model for T is to regard all terms in T as untyped terms, interpret each type as a subset of Λ and then prove that each typed term is interpreted into the interpretation of the type.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
The system F of variable types fifteen years later; Preprint.
Kleene spaces, Informal manuscript
Kleene spaces, To appear in the proceedings from Logic Colloquium ‘88, Padova 1988.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1990 Plenum Press, New York
About this chapter
Cite this chapter
Normann, D. (1990). Formalizing the Notion of Total Information. In: Petkov, P.P. (eds) Mathematical Logic. Springer, Boston, MA. https://doi.org/10.1007/978-1-4613-0609-2_7
Download citation
DOI: https://doi.org/10.1007/978-1-4613-0609-2_7
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4612-7890-0
Online ISBN: 978-1-4613-0609-2
eBook Packages: Springer Book Archive