The Expressiveness of Simple and Second-Order Type Structures
Steven Fortune, Daniel M. Leivant, Michael P. O'Donnell · Journal of the ACM · 1983
Typed lambda (?`-) calculi provtde convement mathematical settings in which to investigate the effects of type structure on the function definmon mechamsm m programming languages.Lambda expressaons mtm~c programs that do not use while loops or carcular function definitions.Two typed ?`-calculi are investigated, the sunply typed ?`-calculus, whose types are similar to Pascal types, and the second-order typed ?,-calculus, which has a type abstractaon mechamsm simdar to that of modern data abstraction languages such as ALPHARD.Two related questions are considered for each calculus: (1) What functaons are definable m the calculus?and (2) How difficult is the proof that all expressions in the calculus are normahzable 0.e., that all computaUons termmate)* The simply typed calculus only defines elementary functtons.Normahzation for this calculus ~s provable using commonplace forms of reasoning formalazable m Peano arithmetic The second-order calculus defines a huge hierarchy of funcuons going far beyond Ackermann's function These funcuons are so rapidly increasing that Peano arithmetic cannot prove that they are total In fact, normalizataon for the second-order calculus cannot be proved even m second-order Peano artthmetic, nor m Peano anthmettc augmented by all true statements Also d~scussed are the lmphcataons of the present ?`-calculusresults for the programming languages PASCAL, ALPHARD, RUSSELL, and MODEL.