Browse Prior Art Database

The Expressiveness of Simple and Second Order Type Structures Disclosure Number: IPCOM000148529D
Original Publication Date: 1980-Oct-31
Included in the Prior Art Database: 2007-Mar-30
Document File: 74 page(s) / 3M

Publishing Venue

Software Patent Institute

Related People

Fortune, Steven: AUTHOR [+4]


RC 8542 (ij37221) 10/31/80 Computer Science 73 pages The Exprcssivcricss of Sirnplc and Sccorid Order Type StructuresStcven Fortune?

This text was extracted from a PDF file.
At least one non-text object (such as an image or picture) has been suppressed.
This is the abbreviated version, containing approximately 4% of the total text.

Page 1 of 74

RC 8542 (ij37221) 10/31/80 Computer Science 73 pages

The Exprcssivcricss of Sirnplc and Sccorid Order Type Structures
Stcven Fortune?

IBM Thomas J. Watson Rcscnscli Ccntcr Yorkto\vn Ilcights. Ncw York 10598

Daniel I.c.i~ant Cor~iell University Ithaca, New York 14853

Purdue University
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

[This page contains 1 picture or other non-text object]

Page 2 of 74

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.

[This page contains 1 picture or other non-text object]

Page 3 of 74

1. Introduction
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...