Browse Prior Art Database

Impredicative Strong Existential Equivalent to Type:Type

IP.com Disclosure Number: IPCOM000148546D
Original Publication Date: 1986-Jun-30
Included in the Prior Art Database: 2007-Mar-30

Publishing Venue

Software Patent Institute

Related People

Hook, James G.: AUTHOR [+3]

Abstract

James G. Hook Douglas 3. Howe TR 8G760 June 1986 Department of Computer Science Cornell UniversityIthaca, NY 14853 Impredicative Strong Existential Equivalent to Type:Type James G. Hook Douglas J. Howe Cornell University June 12, 1986 The second-order existential quantifier provides a facility to express abstract data types in the typed A-calculus[l7]. When languages that allow "dependent" types are studied it seems natural to extend the interpretation of existential quantification to the full generality of Martin-Ef's C-types by allowing the carrier of an abstract type to be a legal type[13,12,10]. The languages KR and PEBBLE allow such a construction[7,1]. This paper shows that when the impredicative second-order A-calculus is extended in this way the type system becomes (logically) inconsistent; that is, terms can be constructed in every type, including those types that correspond to absurd proposit ions. The inconsistency is shown by translating a well-known inconsistent theory based on the axiom type : type into the theory with the strong existential. The most direct implication of the inconsistency is the failure of the strong normalization property-w hich insures that all computations on type correct terms terminate. Recent work by Cardelli suggests that these theories do have a weaker form of consistency[2]. He develops a domain theoretic account of a language with type : type and the strong existential and shows that the semantic soundness theorem (originally stated by Milner for ML[15]) holds.

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 15% of the total text.

Page 1 of 22

Impredicative Strong Existential Equivalent to Type:Type

James G. Hook Douglas 3. Howe

TR 8G760

June 1986

Department of Computer Science Cornell University
Ithaca, NY 14853

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

Page 2 of 22

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

Page 3 of 22

Impredicative Strong Existential Equivalent to Type:Type

 James G. Hook Douglas J. Howe * Cornell University

June 12, 1986

  The second-order existential quantifier provides a facility to express abstract data types in the typed A-calculus[l7]. When languages that allow "dependent" types are studied it seems natural to extend the interpretation of existential quantification to the full generality of Martin-Ef's C-types by allowing the carrier of an abstract type to be a legal type[13,12,10]. The languages KR and PEBBLE allow such a construction[7,1]. This paper shows that when the impredicative second-order A-calculus is extended in this way the type system becomes (logically) inconsistent; that is, terms can be constructed in every type, including those types that correspond to absurd proposit ions.

  The inconsistency is shown by translating a well-known inconsistent theory based on the axiom type : type into the theory with the strong existential. The most direct implication of the inconsistency is the failure of the strong normalization property-w hich insures that all computations on type correct terms terminate. Recent work by Cardelli suggests that these theories do have a weaker form of consistency[2]. He develops a domain theoretic account of a language with type : type and the strong existential and shows that the semantic soundness theorem (originally stated by Milner for ML[15]) holds.

*The work of this author was supported, in part, by NSF grant no. MCS-81-04018.

1

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

Page 4 of 22

1 The Strong Existential

To understand the meaning of quantification in a formal system one must first know the collection over which the quantified variables range. In first- order logic the domain is defined before the quantifiers are interpreted- making their interpretation straightforward. However, in second-order logic the domain of propositional variables must include the interpret at ions of all propositions. For example, the statement "for all propositions P, P implies Pn is a proposition; so it is itself within the range of the variable P and thus it stipulates, among other things, that "(for all propositions P, P implies P) implies (for all proposit ions P, P implies P)" . Such a definition, where the definition of the object refers to the entire collection to which it belongs, is said to be impredicative.

  The second major issue in comprehending a quantified formula is how it may be used in a logical argument. This has two parts: how can the truth of a quantifi...