Browse Prior Art Database

Power Set Models of A-Calculus: Theories, Expansions, Isomorphisms

IP.com Disclosure Number: IPCOM000149090D
Original Publication Date: 1899-Dec-30
Included in the Prior Art Database: 2007-Apr-12
Document File: 72 page(s) / 2M

Publishing Venue

Software Patent Institute

Related People

Longo, Giuseppe: AUTHOR [+2]

Abstract

Polrer Set Models of A-Galeulus: Theories, Expansions, I[sa~raaorphisms (1) I.S.I., Corso Btalia 40, 56100 Pisa, Italy. Pairtially supported by a grant of the Italian C.N.R. to work at the Laboratory for Computer Science, Massachusetts T~~stitute of 'kchnology, Cam bridge, MA, U.S.A, This work was supported in pal% by the National Scietice Foundation, Grant No. MCS 8010707, and by a grant to the M.I.T. Laboratory for Compeiter Science by the IBM Corporation, C-Introduction and summary: n i s paper mainly deals with the models fsr type ficc A-calcu%tasdefined by Plotkin (Plo [1972]) and Engeler (Eng [1979]), For every nmon empty set A, the model DA is built up In a very natural set theopetic way and provides a code free generalization of early ideas sf Scott, Scott [j1976jv Namely, the notion of application (interpreting forma% applieadon of A-terns) generalizes the classical Payhill-Shepherdson-Rogers definition of application in Pa, introduced to define Enlamesation Operaters (see Ro [9667!,

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

Page 1 of 72

 Polrer Set Models of A-Galeulus: Theories, Expansions, I[sa~raaorphisms

(1) I.S.I., Corso Btalia 40, 56100 Pisa, Italy. Pairtially supported by a grant of the Italian C.N.R. to work at the Laboratory for Computer Science, Massachusetts T~~stitute of

'kchnology, Cam bridge, MA, U.S.A,

  This work was supported in pal% by the National Scietice Foundation, Grant No. MCS 8010707, and by a grant to the M.I.T. Laboratory for Compeiter Science by the IBM Corporation,

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

Page 2 of 72

  C-Introduction and summary: n i s paper mainly deals with the models fsr type ficc A-calcu%tas
defined by Plotkin (Plo [1972]) and Engeler (Eng [1979]),

  For every nmon empty set A, the model DA is built up In a very natural set theopetic way and provides a code free generalization of early ideas sf Scott, Scott [j1976jv Namely, the notion of application (interpreting forma% applieadon of A-terns) generalizes the classical Payhill-Shepherdson-Rogers definition of application in Pa, introduced to define Enlamesation Operaters (see Ro [9667!,


p.1431, Abstraction is defined accordingly,

  An interesting fact is that these definitions do not depend on codings of pairs or of finite sets, wS:iZe tae elassica', ones do. Tiis doesn't affect the Rec~lssisn Theory one should be able :3 i;?mrc QU; on It, but does affect the model theory 0% A-C~ICMIUS

                                         (see BB [1979]). NI~scever, fbr vz.,rict,s Teasons which should become clear in the next sections, Plotkin- Engeier3s structt~res are '%handy ppa~-tiic~da.sly
in Engeler9s version: it is easy to grasp Ide ,:l'cuEtnerrs or which d'ie definitions and abstraction rely and to modify them for the p~rp3se
aof he model theory of A-CBPGU~US
we aim at,

  Scctisn 5 (pa2 1) ii"~troduces A-eems and CL-terns (terns of A-calculus, hg3, and sf Combinatory Lcgjc, @E) ohvarious orders, corresponding to levels sf f~~nctionality or

number of A-abstsactis-ns, Part JBI discusses the consequences in Combinatmy Algebras of an e~rly remark 3f SNadsworth (and Scott) on how to interpret the vvloss of jnf~flnation" which is ixpiQisrt in perhming eornb4watary reductions, as in any effective pmcess.

  Section 2, ;oflowing Barendregt9s teminolsgy (Bar [1981]), deals with the local analysis of E~rgeler's models, i.e. sy nlacticnlly characterizes the true equalities in these models, Aetei,n,!!y the partid oder on these structures (i.e. set theoretic incIusion) matches perfectly weil *,he very n2t~11-d
syntactical partial order over A-terns, given by inelusion of Bsehm- trees +(the proofs are in Appendix W). This provides an algebraic characterization sf h-

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

Page 3 of 72

  Section 3 gives a ssernantical c'har~cterization of A-terms of my 'inrite (and infinite) order, Le., for nEw, l~haracterizes the class of terms such as d\xl...x,.N according to...