The Expressiveness of Simple and Second-Order Type Structures

Abstract

Typed lambda ([formula omitted]-) calculi provtde convement mathematical settings in which to investigate the effects of type structure on the function definmon mechamsm m programming languages. Lambda expressaons mtmic programs that do not use while loops or carcular function definitions. Two typed [formula omitted]-calculi are investigated, the sunply typed [formula omitted]-calculus, whose types are similar to Pascal types, and the second-order typed [formula omitted]-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 is 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 discussed are the lmphcataons of the present [formula omitted]-calculus results for the programming languages PASCAL, ALPHARD, RUSSELL, and MODEL. © 1983, ACM. All rights reserved.