May 1992 - Categories - categories.org.au

modified realizability and intensional type theory
by Thomas Streicher 26 May '92

26 May '92

TRULY INTENSIONAL MODELS OF TYPE THEORY ARISING FROM MODIFIED REALIZABILITY The definition of what is a model structure for intensional Martin-Loef Type Theory has been given by John Cartmell in his Thesis (Oxford 1978). Essentially it is like semantics for extensional type theory with the only exception that one drops uniqueness constraints and replaces them by the constraint that Eliminators are preserved by substitution. There has been described quite a lot of models for extensional type theory mainly based on the idea of Kleene realizability. The most important structure in this context is the category of so called realizability sets which we will refer to by r-Set and the full reflective internally complete subcategory PER. It seems to be impossible to find truly intensional models for type theory in this setting as extensionality is built in almost by definition. (Extensionality for me means that the terminal object is a generator). But instead of considering a category of Kleene realizability sets one can also build a category based on KreiselBs Modified Realizability. Whereas in Kleene realizability propositions are considered as arbitrary sets of natural numbers the key idea of modified realizability is to endow any such set A of natural numbers with a subset B . The set A has to be thought of as the collection of potential realizers and the subset B as the collection of ACTUAL REALIZERS. This intuitive idea can be lifted to realizability sets. Based on the category r-Set of realizability sets we construct a category mr-Set of so called "modified realizability sets". Description of mr-Set : objects : triples ( X , d(X) , r(X) ) such that (1) X is a set (2) d(X) is a subset of X (objects in d(X) will be called "defined") (3) ( X , r(X) ) is an r-set , i.e. r(X) is a relation between natural numbers and X such that for any x in X there is a natural number n with n r(X) x morphisms : a morphism from ( X , d(X) , r(X) ) to ( Y , d(Y) , r(Y) ) is a set-theoretic function f : X -> Y such that (1) f (x) is in d(Y) provided that x is in d(X) (i.e. f preserves actual realizers !) (2) f is a morphism from ( X , r(X) ) to ( Y , r(Y) ) in r-Set ( i.e. there is a natural number n such that for all x in X and m with m r(X) x : {n}(m) is defined and {n}(m) r(Y) f(x) ) . More abstractly the category mr-Set can be described as the result of the Grothendieck construction applied to the fibration of REGULAR MONOs in r-Set over r-Set . The category r-Set is a full reflective subcategory of mr-Set by the embedding sending ( X , r(X) ) to ( X , X , r(X) ) . THEOREM Just as r-Set is locally cartesian closed so is mr-Set. The category mr-Set is not extensional. Proof : Obviously, mr-Set has finite limits. The Pi-s are computed as in r-Set , BUT elements are defined iff they preserve definedness. The underlying r-set of the terminal object in mr-Set is the terminal object in r-Set and all elements are defined. Of course, there exist two different parallel morphisms in mr-Set which coincide on defined elements and such morphisms cannot be separated by global elements, i.e. morphism whose source is the terminal object. As mr-Set is left exact it constitutes a model of extensional type theory. Nevertheless we can interpret intensional identity typs in a way such that they do not fulfill the laes of extensional identity types. For this purpose we consider mr-Set as a model of the ambient logical framework. For what Martin-Loef calls "constructive set theory" we have to identify a certain full subcategory of mr-Set. DEFINITION A small set is an object ( X , d(X) , r(X) ) in mr-Set such that (1) n r(X) x1 and n r(X) x2 implies x1 = x2 (2) for some object x in X we have 0 r(X) x . In the sequel we shall need two distinguished small sets : Succeed = ( {e , r} , {r} , { ( 0 , e ) , (1 , r ) }) and Fail = ( {e} , {} , { (0,e) } ) . Now we shall interpret Martin-Loefs identity types in mr-Set in such a way that they do not satisfy the laws of extensional identity types. If A is a small set and a1 , a2 are objects of the underlying set of A then Id A a1 a2 = Fail if a1 and a2 are different Id A a a = Succeed . For any small set A and a in A (not necessarily defined!) r A a = r . Finally we give the definition of the elimination operator J . Given A : Set and a family C : {a1 , a2 : A} {c : Id A a1 a2} Set and a function d : {a : A} C a a (r A a) the function J A C d : {a1 , a2 : A} {c : Id A a1 a2} C a1 a2 c is defined as follows J A C d a a r = d a J A C d a1 a2 e = the unique object in C a1 a2 e realized by 0 . Obviously, J is realizable as one simply performs a decidable case analysis on the realizer for the lasr argument. THEOREM The following sequents are NOT valid in this model : (1) A : Set , x : A , y : A , z : Id A x y |- x = y : A [ but, of course, theer is a term t such that A : Set , x : A , y : A , z : Id A x y |- t : Id Ax y : A ] (2) A : Set , C : A -> Set , x : A , y : A , z : Id A x y |- C x = C y [ put for A a small set with at least two different objects a and b where a is assumed to be defined and for C the family [x:A] Id A a x ; then we have Id A a a = Succeed but Id A a b = Fail although e : Id A a b ] . (3) The socalled Equality Reflection Lemma (terminology of LuoBs Thesis) holds If |- p : Id A t s is valid in the model then |- t = s : A is valid in the model, too. (The restriction to the empty context is important, see (1) ! The interpretation of the empty context contains one defined and no undefined object ! ). THEOREM In the model defined above the principle of extensionality {A,B : Set} {f,g : A->B} ({x:A} Id B (f x) (g x)) -> Id (A->B) f g is NOT realized !! Proof : by a continuity argument !! //** In General Leibniz Equality is different from Martin-Loef Idenity Types **// Interpret Prop as small sets and interpret Type(0) as those mr-sets where the underlying r-set is a per. Then both Prop and Type(0) are closed under arbitrary internal products. In Type(0) we can interpret (even extensional) Martin-Loef identity types as we have mr-sets whose underlying r-set is empty. On the other hand we can define Leibniz equality employing Prop . Now let A be a type containing ar least two different defined elements a1 and a2 . Then LE A a1 a2 is in Prop containing no defined element BUT surely a nondefined element realized by 0 . Id A a1 a2 contains not even an undefined element. Therefore there cannot exist a morphism from LE A a1 a2 to Id A a1 a2 !! Thomas Streicher

1 0

informations
by momathie＠mathp7.jussieu.fr 23 May '92

23 May '92

Journees de travail "ESQUISSES ET TYPES DE STRUCTURE" organisees les 2 , 3 et 4Juillet 1992 a l'Universite Paris7 et a l'Ecole Centrale de Paris sur le theme : SYSTEMES, STRUCTURES, BASES DE DONNEES: modelisations diagrammatiques et applications (calcul formel,optimisation, theorie de la demonstration, ....) CONTACTER : L. Coppey ou M. Mathieu UNIVERSITE PARIS 7 U.F.R. de Mathematiques Tours 45-55, 5eme etage 2 place JUSSIEU 75251 PARIS CEDEX 05 FRANCE e-mail: coppey(a)mathp7.jussieu.fr ou : momathie(a)mathp7.jussieu.fr ==================================================================

1 0

A new book by Carl Gunter
by barr＠triples.Math.McGill.CA 20 May '92

20 May '92

This just came from my account at Penn and I thought it was of interest. >From gunter(a)saul.cis.upenn.edu Mon May 18 17:41:36 1992

1 0

Draft 5 of book
by gunter＠saul.cis.upenn.edu 19 May '92

19 May '92

Draft 5 of my forthcoming book for MIT press is now (finally) complete. I'm having a copy made to put in the theory lab if you'd like to have a look. After writing the index, incorporating more corrections, and adding a few more exercises, the final version will be delivered to the press in mid-June. The books themselves are expected to be in bookstores by September. I need some help with technical review of Chapters 9 and 11---the new chapters on polymorphism. If you have an interest in polymorphism and a keen eye for detail, then I would very much appreciate your assistance on proof-reading. Send me email if you are willing to lend a hand. Here is a copy of the table of contents: SEMANTICS OF PROGRAMMING LANGUAGES Structures and Techniques List of Tables List of Figures Series Foreword Preface 1. Introduction 1 1.1 Semantics 1.2 Semantics of Programming Languages 1.3 Notes 2. The Simply-Typed Lambda-Calculus 31 2.1 Syntax of Lambda-Terms 2.2 Rules 2.3 Models 2.4 Notes 3. Categorical Models of Simple Types 63 3.1 Products and Cartesian Closure 3.2 Lambda-Calculus with Constants and Products 3.3 The Use of Category Theory 3.4 Notes 4. Recursive Definitions of Functions 95 4.1 A Programming Language for Computable Functions 4.2 Fixed Points in Complete Partial Orders 4.3 Fixed-Point Semantics of PCF 4.4 Bounded Recursion 4.5 Notes 5. Two Theories of Finite Approximation 141 5.1 Bc-domains 5.2 Stable functions and dI-domains 5.3 Equivalences between categories. 5.4 Notes 6. Relating Interpretations 169 6.1 Full Abstraction 6.2 Extensions of Adequacy Results 6.3 Products and Sums 6.4 Notes 7. Types and Evaluation 207 7.1 Expressiveness 7.2 Security 7.3 Reference types 7.4 Recursive Types 7.5 ML Polymorphism and Type Inference 7.6 Notes 8. Universal Domains 245 8.1 Untyped lambda-Calculus 8.2 Domain Equations 8.3 Notes 9. Subtype Polymorphism 273 9.1 Subtypes as Subsets 9.2 Subsumption as Implicit Coercion 9.3 Notes 10. Domain Theory 303 10.1 Fixed Points of Functors 10.2 Bifinite domains 10.3 Adjunctions and Powerdomains 10.5 Notes 11. Parametric Polymorphism 343 11.1 Calculi for Expressing Parametric Polymorphism 11.2 Indexed Families of Domains 11.3 Notes List of Notations 377 Bibliography 381 Subject Index 391

1 0

Some abstracts from Barwise
by barr＠triples.Math.McGill.CA 19 May '92

19 May '92

The attached abstracts, especially the last two, seem very interesting. Michael >From chris(a)central.cis.upenn.edu Mon May 18 15:44:45 1992

1 0

Talks by John Barwise, May 19, 20, 21, 1992
by Chris Sandy 19 May '92

19 May '92

Institute for Research in Cognitive Science University of Pennsylvania 401C seminar room 3401 Walnut St., suite 400C May 19, 1992 Talk No. 1: Channels 1:00 pm A central debate in cognitive science and modern philosophy is whether or not it is possible to give a naturalistic account of intentionality. How can we understand this ability of people and other cognitive agents as part of the natural order, populating a physical world governed by natural law? Or must we understand the physical world as a mental, linguistic, or social construct? In this talk I want to propose a mathematical model for the notion of a law-like regularity, which I will call a {\em channel}, into two parts: a relationship between particular events (called a {\em signaling relation}) and a relationship between types of events (called an {\it indicating relation}). The latter is a {\em regularity} by virtue of reflecting properties of the former. The two-level analysis allows us to explain how regularities can be reliable but also admit of exceptions, and allows us to unify a great many apprarently divergent approaches to information and knowledge within a single framework. The talk will be informal with the mathematics kept to a minimum. Only at the very end will I point in the direction of connections with the work of Freyd and Scedrov on the notion of an allegory. Part of this work is joint with Jerry Seligman. May 20, 1992 Talk No. 2: Logic and Diagrams 1:00 pm When one looks at logic in practice, whether it be in science, engineering, or everyday life, the extent to which various forms of diagrammatic representation are used in design, reasoning, and problem solving is more than striking; it is staggering. Think about the diagrams used in physics, chemistry, biology, hardware design, and architecture, let alone geometry and topology. But diagrams have been largely ignored by logicians. Aside from a few obvious counter-examples (Euler, Venn, Frege, Peirce, e.g.), most logicians have closed their eyes, and those of their students, to the diagrammatic aspects of reasoning. In this talk I will suggest that logicians should study valid reasoning in systems of representation that make use of such graphical devices as first-class representations, and that they should teach principles of diagrammatic reasoning to their students. I will go on to discuss some steps that have been undertaken in that direction. This talk is based on joint work with John Etchemendy and a number of other people who will be identified and blamed during the talk. May 21, '92 Talk No.3: After the Revolution: Information and Academia 1pm The function and structure of the research university (RU), as we have come to know and love it, is based on certain assumptions. I want to examine some of these assumptions, suggesting that they are being called into serious question by the information revolution. If my analysis is correct, the RU is in jeopardy and could go the way of the the dinosaur, the ship-building industry in the 19th century, and the Soviet Union. I then want to propose some short-term measures which should be taken to help RUs adapt, rather than succumb, to the revolution. This is not an area in which I am an expert, but it is one where I have had many painful experiences, ones which give rise to the reflections in the talk. ==================================================================

1 0

Oktoberfest
by barr＠triples.Math.McGill.CA 12 May '92

12 May '92

Fox has asked me to announce that there will be a Montreal meeting in October on the Thanksgiving/Columbus Day weekend. I believe the dates are Oct. 10 and 11. More details will be forthcoming, but it will be just like previous meetings. Michael ==================================================================

1 0

generalizations of monads and comonads
by Thomas Streicher 12 May '92

12 May '92

During a discussion at the Durham meeting last year on monads versus comonads in semantics of programming languages Bill Lawvere made a remark on some recent work where a concept has been developed which generalizes both monads and comonads. It should be the Thesis by a person called Thiebaud or Thibault or so ... I would be very grateful for any reference on this work ! Thomas Streicher ==================================================================

1 0

Second Announcement
by jfunk＠kean.ucs.mun.ca 02 May '92

02 May '92

Atlantic Canada Algebra Conference Sir Wilfred Grenfell College Memorial University of Newfoundland Corner Brook, Newfoundland Friday, Saturday and Sunday, May 22, 23, 24, 1992 The Mathematics Department of Grenfell College is pleased to announce its first algebra and category theory conference. The conference will coincide with an interdisciplinary conference on Myth and Knowledge. John Casti, author of "Paradigms Lost", will be speaking Saturday morning at 9:00. There will be four sessions of talks on the mornings and afternoons of Saturday and Sunday with the possibility for more talks on Monday. On Friday evening, May 22, there will be a reception at the college. Accommodations can be obtained from the following: 1. The Glynmill Inn Telephone: 1-800-563-4400 (Atlantic Provinces) (709) 634-5181 (Other) 2. College Residence Telephone: (709) 637-6321 Room with shared bath: $29.40 (Cdn.) tax included. If you would like to give a talk at the conference, or would just like to attend, please notify one of the organizers as soon as possible. Organizers: Jonathon Funk (709) 637-6284 (office) 634-1934 (home) Richard Macleod (709) 637-6284 (office) 634-0545 (home) Richard Squire (709) 637-6290 (office) 639-1263 (home) _________________________________________________________________ Dept. of Mathematics and Statistics Sir Wilfred Grenfell College Corner Brook, Newfoundland Fax: (709) 639-8125 (General Office) ==================================================================

1 0