The Expressiveness of Simple and Second Order Type Structures
Original Publication Date: 1980-Oct-31
Included in the Prior Art Database: 2007-Mar-30
Software Patent Institute
Fortune, Steven: AUTHOR [+4]
RC 8542 (ij37221) 10/31/80 Computer Science 73 pages The Exprcssivcricss of Sirnplc and Sccorid Order Type StructuresStcven Fortune?
RC 8542 (ij37221) 10/31/80 Computer Science 73 pages
The Exprcssivcricss of Sirnplc and Sccorid Order Type Structures
IBM Thomas J. Watson Rcscnscli Ccntcr Yorkto\vn Ilcights. Ncw York 10598
Daniel I.c.i~ant Cor~iell University Ithaca, New York 14853
West I-afayette, Indiana 47907
Typed by Itlichclle A. Cofer
Formatted Using the Yorktown Fornlattitig Li~ngiiage Printed on the APS-5
Typcd lambda calculi proviclc convcnicnt n~ntIicrii;i(icril wttiiigs in \vliich to irivcstigatc the effects of type structure on the function dcfi~iitiorl mcchnnism in programming Innguagcs. Lambda cxprcssions ~iiirnic prograins that do not use \Yt~ilc-loops or circular function dcfini- [ions. We investigate two typed lambda calculi: the siniply typed la~~ibda
cnlculus, whose typcs are similar to Pascal types, and the sccond order typed lambda calculus, which has a type abstraction mcchanisni similar to that of modern dala abstractio~l languages such us .\lph;lrd. We consider two problcn~s for each calculus: characterizing the functions rlcfinable in tlie calculus and cl~aracterizing the difficulty of proving normalization of cxyressions in the calculus. The si~ilply typed calculus only defincs eletnentary functions (each such furictioll is
bounded by z2'. for soiile fixed number of 2s). Normalization for this calculus is protrable using conimonplace for~lls of reasoning formalizable in Pcano1s Aritlinietic. The sccotid order
calculus drfiilcs a li~~gt:
liicrarclly of fu~lctioils going far bcyo~id Ackcr1iia1111's fu~iction. Tllcse
fur~ctions are so big that Pcnno's Aritli~~ictic
psovc that they are total. Tn fact,
norn~alization for the second order calculus caririot bc pro\cd ; ~ c n in sccoi~d ordcr Pcano's
Arithmetic, nor in Peano's Arithmetic augmcl~tcd by all truc 21, stntcrncnts. We also discuss the implications of o w lambda cnlculus results for [lie pro;s:i~ilrning Innguagcs Pnscal, Alphard, Russcil and Model.
7 Part of the research reported in this paper was done ~ h i l e
the author was a grliiiu;lte
studcnt at Cornell University and while the author \\-as supported in port by Officc of Saval Research Grant NO001 4-76-C-00 18.
f; The research of the author was supported in part by Sational Science Foundatiotĝrillit
XICS-780 18 12.
1.1 Type Structure in Programming Languages
Many recent programming language designs have used a classification of the objects of
.. computation into different types to express strong restrictions on how different objects may be combined. A primary motivation for the imposition of type structure on a programming language is that many errors that would otherwise be found by hand searching may be detected by...