goguen | 11 Nov 00:39 1987

Re: Type : Type

Dear Uday,

Thanks for your question.  What is common to "TYPE : TYPE" and "TRIV :: TRIV"
is (one of) the intuitions that they both capture.  I have assumed that it is
of interest, at least for programming languages, to capture the intuition that
that "T : TYPE" means "T defines some structure", using an approach that does
*not* require making sense of anything like things being members of
themselves, but that still allows (its version of) "TYPE : TYPE" to mean that
"TYPE defines some structure".  

Part of what makes our approach workable is that models also appear as types
(i.e., as theories).  Thus,


technically means that the _theory of natural numbers_ *satisfies* TRIV, *not*
that some particular model of NAT, say omega, is a *member* of TRIV, though of
course its intuition is that omega is a member of (the *denotation* of) TRIV.

A nice fringe benefit of this approach is that *abstractness* is automatic:
the denotation of NAT is actually the _abstract data type_ for the natural
numbers, i.e., the (category of) algebras that satisfy NAT, which is the
category of algebras *isomorphic* to omega; in fact, omega plays no privileged
role here at all.  (Data constraints provide the underlying machinery giving
theories that impose initiality on models.)

Going a little further down this route, the denotation of the theory
interpretation TRIV -> NAT (which is the actual content of "NAT :: TRIV") is
the forgetful functor which gives the underlying sets of these algebras.

(Continue reading)

Daniel.Leivant | 14 Nov 16:27 1987

CMU meeting on metadeduction

Below is the schedule of a meeting that has taken place at 
Carnegie Mellon University, on


Please address requests for abstracts of talks
to jfm@... (ARPAnet).

Friday, November 13

 9:00 Using a Higher-Order Logic Programming Language to Implement 
	Program Transformations
      Dale Miller, University of Pennsylvania

 9:45 Building Proof Systems in an Extended Logic Programming Language
      Amy Felty, University of Pennsylvania

10:45 The Categorical Abstract Machine, State of the Art
      Pierre-Louis Curien, Ecole Normale Superieure, Paris VII

 1:15 A Very Brief Look at NuPRL
      Joseph Bates, Carnegie Mellon University

 1:45 Reasoning about Programs that Construct Proofs
      Robert Constable, Cornell University

 2:30 Theorem Proving via Partial Reflection
      Douglas Howe, Cornell University

 3:15 MetaPrl: A Framework for Knowledge Based Media
(Continue reading)

Albert R. Meyer | 14 Nov 22:22 1987


From: mcvax!doc.ic.ac.uk!sa@...
Date: Mon, 9 Nov 87 15:10:26 GMT
To: meyer@...
Subject: Re:  [meyer: TYPE:TYPE]

I was interested in the discussion about computational adequacy, because
it seems to relate quite strongly to some work I have been doing recently
(and also work of my student Luke Ong).

We have been studying what I call the ``Lazy lambda-calculus'', where
one considers convergence to WEAK head normal form, i.e. to an
abstraction. This is in fact what all implementations of lazy functional
languages do (see e.g. Simon Peyton Jones' book on graph reduction).
Taking convergence to weak head normal form as the basic observable,
one can define a bisimulation-like preorder on terms (closed terms,
then extended to all terms via their closed instances). This gives
rise to a rather interesting--although of course non-sensible--
lambda theory, in which: Longo's POk terms   are grouped into an
ascending chain; this chain's lub (the PO infinity terms) are the
global top element (represented e.g. by YK); (beta) holds, and (eta) holds in
the conditional form:

  lambda x. Mx = M  (M converges, x not free in M)
where ``converges'' means of course ``head reduces to an abstraction''.

The bisimulation preorder IS equivalent to the one obtained from
convergence by closing under all contexts, but this is by no means
trivial to prove; in fact, my proof of this purely syntactic fact
goes via the denotational semantics, and specifically the ``Domain logic''
version of it, in the sense of my LICS paper.
(Continue reading)

Albert R. Meyer | 14 Nov 22:27 1987

[meyer: TYPE:TYPE]

Please send me your draft paper with Ong on ``lazy lambda calculus''.

I am unable to guess what ``a bisimulation-like preorder on terms'' might be.
Can you give me more of a hint?

Regards, A. 

Albert R. Meyer | 16 Nov 10:41 1987


Date: Sun, 15 Nov 87 13:02:46 EST
From: gunter@... (Carl Gunter)
Posted-Date: Sun, 15 Nov 87 13:02:46 EST
To: meyer@...
Subject: Re:  [mcvax!doc.ic.ac.uk!sa@...: Re:  [meyer: TYPE:TYPE]]

Albert, how many people know that mcva!doc.ic.ac.uk!sa@...
is Samson Abramsky?  It seems to me that people who are posting
on the bb should SOMEWHERE include their full name.  Perhaps you
could refer this request to the bb users at large.

				--- Thanks, Carl A. Gunter

Albert R. Meyer | 17 Nov 08:40 1987

LICS logo and theorynet subscription

I think I'm contributing to e-mail noise by forwarding messages from other
large subscription lists, so this is the last mail I will forward from
TheoryNet.  I suggest you subscribe directly if you're interested.

Regards, Albert
Moderator, types@...
Date:         16 Nov 1987 18:19:50-EST (Monday)
Reply-To:     TheoryNet List <THEORYNT%NDSUVM1.BITNET@...>
Sender: TheoryNet List <THEORYNT%NDSUVM1.BITNET@...>
Comments:     Warning -- original Sender: tag was THEORYNT <at> YKTVMX
From: "Ashok K. Chandra" <ASHOK@...>
Subject:      LICS competition
To: Local Distribution <THEORY@...>

                        LICS Cover and Logo Competition

          Submissions are  invited for the  design of a cover  for the
          LICS proceedings, and a logo  for the LICS symposium.  It is
          expected  that  one  of  the  submissions  will  become  the
          standard cover  for the LICS proceedings  (for examples, see
          the proceedings of  the FOCS symposium, or  the Structure in
          Complexity Theory symposium).  The  logo is intended for use
          in conference announcements.

          The cover  design should be 8"  x 10", black on  white, with
          space to print the conference name and credits.  The logo is
          intended  for use  in approximately  2" x  2", and  1" x  1"
          sizes, but submissions may be larger.

(Continue reading)

jcm%research.att.com | 18 Nov 15:47 1987

sub CCC's of Set

I have some preliminary ideas on how to describe the
cartesian closed subcategories of Set. Is there some
well-known characterization I might be rediscovering?
(I am interested in subcategories that are not "full,"
so, for example, Hom(1,a) might be smaller than the
set a.)

John Mitchell

Edmund Robinson | 26 Nov 20:47 1987

Churchian integers in PER

There seems to be enough demand for a proof that the Churchian integers
in the PER model of polymorphism are the natural numbers to post the
proof that Martin Hyland showed to Edmund and me some time ago.

Let e be in \Pi X.[[X -> X] -> [X -> X]]. 

Denote the partial function coded by the number f with the same symbol f.
For any natural number a let f^n(a) be f applied n times to a (possibly
indefined). If for all n the value f^n(a) exists, we'll say that a has
f-orbit, and write O(f,a) = { f^n(a) : n in N } for the orbit. When we write
f:O(f,a) -> O(f,a) we mean the endofunction induced by f on the diagonal
relation on O(f,a) in PER.

If O(f,a) exists, then e(f)(a) exists and is in O(f,a): we aim to show
that it is uniformly  a |---> f^r(a)   for some fixed r.

Note that e acts on any (index for a) partial recursive function g as 
g: { a : O(g,a) exists } ->  { a : O(g,a) exists }.

CLAIM. If O(f,a) is infinite, then there is a number k such that for any
partial recursive function g with O(g,a) infinite such that 
       <a,g(a),...,g^k(a)> = <a,f(a),...,f^k(a)>
one has e(f)(a) = e(g)(a).

Proof: First take an enumeration of suitable basis functions: for any sequence
without repetions u = <u_0, u_1, ..., u_k> let u~ be the partial function
such that 
            u~ (u_i) = u_{i+1}      for i < k
            u~ (u_k) = u_k
and notice that a code for u~ can be effectively computed from u.
(Continue reading)

Albert R. Meyer | 28 Nov 14:38 1987

[meyer: TYPE:TYPE]

   From: mcvax!doc.ic.ac.uk!sa@... <SAMSON ABRAMSKY>
   Date: Mon, 23 Nov 87 11:05:25 GMT
   To: meyer@...
   Subject: Re:  [meyer: TYPE:TYPE]

   I will send you the draft paper (which incidentally is by me; Luke Ong
   is writing his thesis on extensions to what I have done.  His thesis
   is shaping up as a very nice piece of work; he should have a draft
   version to circulate by the end of the year, and plans to submit next
   summer.  If you are interested, I will ask him to send you a copy of
   the draft.)

   Meanwhile, here is a hint. Say we are in the untyped pure lambda
   calculus, and we have defined a notion of convergence (e.g. to weak
   head normal form, i.e. an abstraction).  Then we define, for closed
   terms M, N:

    M preord N <-> M converges to lambda x. M' implies N converges to
		    lambda y.N', and for all P, M'[P/x] preord N'[P/x].

   This recursive definition unwinds into a maximal fixpoint; the closure
   ordinal is omega. The realtion can then be extended to all terms by
   ground instances.

   Because there is no non-determinism in this particular language, the
   relation would perhaps better be called simulation; however, the
   analogy with bisimulation in CCS etc. is clear.  Moreover, this notion
   can be extended to typed calculi such as Plotkin's meta-language; once
   powerdomains enter the picture, calling the relation a bisimulation
   becomes fully justified.
(Continue reading)