headers
Benjamin Pierce | 4 Aug 1992 15:03
Picon
Picon

Coherence and polymorphic instantiation

Date: Mon, 03 Aug 92 14:26:36 +0100

In the course of experimenting with adding some polymorphic constants
to the second-order polymorphic lambda-calculus with subtyping (Fsub),
we were led to wonder what kind of equational properties should be
imposed to express compatibility between polymorphic instantiation and
subtyping.

To see the issue, consider the polymorphic type

    T = All(A) F(A) -> G(A)

where both F and G are monotone type operators.  If we have f:T,
X<X', and x:F(X), then f can be applied to x in two ways:

    f [X] x

    f [X'] x

We can now ask whether these two terms are equal elements of G(X') --
or more explicitly, whether

      [G(X) < G(X')] (f [X] x) 
    = f [X'] ([F(X) < F(X')] x) 
    : G(X')

where [S<T] denotes the coercion from S to T.

This equation holds trivially in untyped models and also, it seems,
for definable polymorphic terms.  It becomes interesting in typed
(Continue reading)

Permalink | Reply | 0 comments |
headers
Djordje Cubric | 4 Aug 1992 15:10
Picon

Embedding free CCC into SET

Date: Mon, 3 Aug 92 14:02:00 EDT

I would like to announce that a draft of a paper "On Free CCC" (by me)
is available from ftp triples.math.mcgill.ca. The paper contains a
proof of the following:

Theorem: Let C be a free cartesian closed category. Then there exists a
faithful structure preserving functor F:C->Set.

Isn't it just the H. Friedman's completeness result for the typed
lambda calculus? NO. One has also to show that in the free cartesian
closed category  all the  arrows into the terminal object are epi. 

We prove the result using Mints' reductions (but with the repaired proof). 
Along the way we conclude also that:

Mints reductions are weakly normalizing, the strategy being: first do
all eta-like expansions (with the restrictions) and
then beta-like reductions.  

To get the file (if you can read ps files) do:
ftp triples.math.mcgill.ca
Name: anonymous
Password: "your e-mail address"
>cd pub/cubric
>binary
>get frccc.ps
>quit

If you can't read ps files there are also frccc.dvi and frccc.tex (which needs
(Continue reading)

Permalink | Reply | 0 comments |
headers
Andre Scedrov | 4 Aug 1992 18:13

Coherence and polymorphic instantiation

Date: Tue, 4 Aug 92 11:12:24 EDT
To: bcp@...
Cc: types@...

Some of the issues raised in the recent message by M. Hofmann and 
B. Pierce are discussed in the paper: 

Cardelli, L, J.C. Mitchell, A. Scedrov, and S. Martini,  An Extension 
of System F with Subtyping. Extended abstract in: "Theoretical Aspects 
of Computer Software", T.Ito and A.R. Meyer (Eds.), Springer LNCS 526, 
1991, pp. 750--770. Full paper to appear in Information and Computation.  

  - Andre Scedrov
Permalink | Reply | 0 comments |
headers
Alan Jeffrey | 5 Aug 1992 16:34
Picon

Regular subobjects in CCCPO

Date: Wed, 5 Aug 92 14:30:01 +0100

This is a short note giving a characterization of the regular
subobjects in the category CCCPO (3CPO) which has:

   objects: consistently complete cpos.
   morphisms: functions preserving bottom and consistent join.

Note that the morphisms are NOT arbitrary continuous functions, 
but strict ones which in addition preserve the consistent join. 

Proposition. e : A --> B is a regular monic in CCCPO iff:
1. A is a subset of B (up to isomorphism).
2. bottom is in A.
3. if X is a subset of A and is consistent in B then \/X is in A.

Proof.

=> Let f, g: B -> C form an equalizer for e : A -> B.  Then:

   1. A is isomorphic to { b in B | f(b) = g(b) }.
   2. f bottom = bottom = g bottom, so bottom is in A.
   3. Since X is a subset of A, f[X] = g[X], so
      f(\/X) = \/f[X] = \/g[X] = g(\/X), so \/X is in A.

<= Define:

      a(b) = \/{ a in A | a <= b }
      f(b) = (b,b)
      g(b) = (b,a(b))
(Continue reading)

Permalink | Reply | 0 comments |
headers
Martin Abadi | 5 Aug 1992 16:36
Picon

Re: Coherence and polymorphic instantiation

Date: Tue,  4 Aug 92 13:32:53 PDT

This issue can be considered in Fsub, as Andre points out, but it 
already arises in F.  John Mitchell studied the theories where 
any two terms with the same type and the same erasure are equated; 
he proved that any such theory corresponds to some PER model.  (See 
p. 208 in "Logical Foundations of Functional Programming", ed. Huet.)

Martin Abadi
Permalink | Reply | 0 comments |
headers
Eugene Stark | 6 Aug 1992 19:31
Picon

Regular subobjects in CCCPO

Date: Thu, 6 Aug 92 08:39:30 -0400

(Alan Jeffrey and Edmund Robinson give a characterization of regular subobjects
in the category of consistently complete cpos and strict, join-preserving maps,
and ask whether this result or similar ones are known in the community.)

In my papers:

``Compositional Relational Semantics for Indeterminate Dataflow Networks,''
Proceedings of Summer Conference on Category Theory and Computer Science,
Manchester, U.K., September, 1989, Springer LNCS 389, pp. 52-74.

``Connections Between a Concrete and an Abstract Model of Concurrent Systems,''
Proceedings of Fifth Conference on Mathematical Foundations of Program
Semantics, New Orleans, LA, Springer LNCS 442, pp. 53-79, March, 1989.

I showed the completeness of the subcategory of your CCCPO that
consists of the ``conflict event domains,'' which are finitary, algebraic,
consistently complete cpos that have some additional properties pertaining
to prime (covering) intervals.  The morphisms are strict,
consistent-join-preserving maps that in addition preserve finite joins of
prime intervals.  From the construction for equalizers given there, it is
clear that regular subobjects have the properties you state.  Moreover,
a subobject satisfying these properties has a right adjoint with identity unit,
hence every regular subobject is a split coreflexive.  (I get the impression
>from your posting that this is part of what is of interest to you.)

This is the first time I have heard of anyone else being interested in
categories of strict, consistent-join-preserving maps, and I am eager to hear
about anything else you find out.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Guoqiang Zhang | 6 Aug 1992 22:19
Picon
Favicon

Stark's reply re regular subobjects in CCCPO

Date: Thu, 6 Aug 92 16:15:40 -0400

(Gene Stark, when responding to Alan Jeffrey and Edmond Robinson's
question on  Regular subobjects in CCCPO, writes:

>This is the first time I have heard of anyone else being interested in
>categories of strict, consistent-join-preserving maps, and I am eager to hear
>about anything else you find out.  )

Many such categories have been considered by  people for
domain theoretic models of linear logic
(symmetric monoidal closed categories):

* Of course Girard's coherent spaces uses these kind of maps,
  which are linear, stable functions under Berry order.

* Vaughan Pratt's work on Event Spaces and Their Linear Logic, 
  uses certain join preserving functions as morphisms (under the
  extensional order).

* My MFPS paper (LNCS 598, pp426-435) gives a monoidal closed category
  of stable event structures with linear maps. These corresponds to
  the category of dI-domains and linear, stable functions, under the
  Berry order.

* The journal version (to appear in MSCS) of the above paper
  contains a description of the linear category of prime algebraic
  lattices with linear functions under the extensional order.

* The category of prime algebraic lattices with linear functions
(Continue reading)

Permalink | Reply | 0 comments |
headers
John C. Mitchell | 13 Aug 1992 20:53
Picon

OOP Tutorial

Date: Thu, 13 Aug 92 11:38:22 -0700

I recently gave a 4-hour tutorial on "foundations of object-oriented
programming" at the TOOLS (Techniques of OO Languages and Systems) Conference.
The slides from this presentation are available by anon ftp from
theory.stanford.edu, files pub/jcm/tools-tutorial.{dvi,ps}

John Mitchell
Permalink | Reply | 0 comments |
headers
Amadio Roberto | 14 Aug 1992 15:17
Picon
Favicon

unification in CCC

Date: Fri, 14 Aug 92 10:58:32 +0200

Dear Moderator,

I would like to submit the following question to the attention
of the subscribers of the types list.

yours truly,

Roberto Amadio

=========================================================================

I know of at least two surveys on unification which mention the
problem of unification in the free theory of a cartesian
closed category but do not give any substantial reference.

One of these surveys goes a little bit further and states that
unification in a ccc `corresponds' to higher order unification
(say unification in the simply typed lambda beta eta calculus,
as described in G. Huet [1975] `A unification algorithm for 
typed lambda calculus', TCS ).

I am a bit sceptic about this statement and I would appreciate
receiving references to papers where this point is actually worked out.

Roberto Amadio (amadio@...)

P.S. Here is a sketch of how, I guess, a typical problem could be formalized.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Gavin Bierman | 17 Aug 1992 21:26
Picon
Picon
Favicon

Term Assignment for ILL

To: linear@...
Date: Thu, 13 Aug 92 17:43:43 +0100

The following paper is now available by anonymous ftp.

               TERM ASSIGNMENT FOR INTUITIONISTIC LINEAR LOGIC

         Nick Benton, Gavin Bierman, Valeria de Paiva & Martin Hyland
                           University of Cambridge

We consider the problem of deriving a term assignment system for 
intuitionistic linear logic (actually only the multiplicative fragment 
for the moment). Our system differs from previous calculi (e.g. that of 
Abramsky) and has two important properties which they lack. These are the 
*substitution property* (the set of valid deductions is closed under 
substitution) and *subject reduction* (reduction on terms is well-typed). 
We have approached the derivation of a term assignment system in two ways

    1. By considering a *linear* natural deduction system. We can then 
    consider the connectives and their correct formulation. We use the 
    Curry-Howard correspondence to form a term assignment system.

    2. By taking the sequent calculus formulation, as given by Girard. 
    We have considered the rules using our categorical model (details below). 
    By considering the naturality properties of each rule, we can derive 
    a term assignment system.

We show that these two approaches provide equivalent logics and term 
assignment systems. (We give a procedure for mapping proofs from one system 
to the other).
(Continue reading)

Permalink | Reply | 0 comments |

Gmane