6 Oct 11:17 1993

### non-commutative tensor

```During the summer there was a discussion on calculi
involving both commutative and non-commutative connectives.
I mentionned the work I did on this topic,
but there was nothing available by ftp.

I partly fixed this trouble by putting the
english introduction of my thesis
called:                    intro.dvi
on the ftp site:           cma.cma.fr
under the directory:       pub/papers/retore

The paper on this ordered calculus will soon be available
on the same ftp directory, with the name pomset.dvi

```
5 Oct 15:05 1993

### paper available

```
The following report is available by anonymous ftp from the University
of Cambridge.
Larry Paulson

Set Theory for Verification: II. Induction and Recursion

A theory of recursive definitions has been mechanized in Isabelle's
Zermelo-Fraenkel (ZF) set theory.  The objective is to support the
formalization of particular recursive definitions for use in
verification, semantics proofs and other computational reasoning.

Inductively defined sets are expressed as least fixedpoints,
applying the Knaster-Tarski Theorem over a suitable set.  Recursive
functions are defined by well-founded recursion and its derivatives,
such as transfinite recursion.  Recursive data structures are
expressed by applying the Knaster-Tarski Theorem to a set that
is closed under Cartesian product and disjoint sum.

Worked examples include the transitive closure of a relation, lists,
variable-branching trees and mutually recursive trees and forests.
The Schr\"oder-Bernstein Theorem and the soundness of
propositional logic are proved in Isabelle sessions.

FTP Instructions:

* Connect to host ftp.cl.cam.ac.uk [128.232.0.56]
* put ftp in BINARY MODE ("binary")
* go to directory reports (by typing "cd reports")
```

12 Oct 19:45 1993

### subtyping variants

```
What is the current state of art in (sub)typing variants?
For example consider the following data type declaration:

data I1 = Xcoord | Ycoord | Mv(Real,Real)

I would like to write something like

data I2 = Color | I1

data I3 = Color | Coerce(I1)

If one considers only non-recursive (polymorphic) data type
declarations then:

1) Are type reconstruction algorithms awailable to compute
the principal type of functions defined by using the
constructors of I2?

2) Is there any functional of the form:

I2-w :: x -> (I1 -> x) -> I2 -> x

I2-w (a)(f)(x) = case x of
Color     => a
otherwise => f x

corresponding to the functional obtained for I3:
```

13 Oct 14:07 1993

### proof terms for classical logic in natural deduction formulation

```
PROOF TERM ASSIGNMENT for CLASSICAL LOGIC in NATURAL DEDUCTION
FORMULATION

In this note we will define a proof term calculus for First Order
Classical Logic (CL) in a Natural Deduction Formulation (as can be
found in several recent papers of Michel Parigot). But instead of
using Parigot's mu-calculus we stick to a more traditional language
for proof terms, namely a fragment of Martin-Loef's Type Theory.
Actually it is a rather poor fragment. Besides \-calculus we simply
use the pairing function <_,_> (which is a constructor) and
Martin-Loef's eliminator pattern-matching. It is just the operator
defined by the semantics :

p => <a,b>  e[a,b/x,y] => c
-----------------------------
E(p , (x,y) e) => c

In a more traditional (SML-style notation one could write

let  <x,y> = p  in  e    instead of  E(p , (x,y) e)  .

Our proof term assignment is inspired by the negative polarity
fragment of Girard's LC. This gives rise to the following improved
~~-translation :

G(A) := ~ A*

where  (_)*  is defined inductively as follows :

```

13 Oct 17:47 1993

### Chu is cofree

```
A paper on

THE CHU CONSTRUCTION AND
COFREE MODELS OF CLASSICAL LINEAR LOGIC
by Dusko Pavlovic

is available by anonymous FTP from triples.math.mcgill.ca. The files
chu-{A4,US}.{dvi,ps}.Z are the directory pub/pavlovic. Each of them
contains the whole paper, but in various formats.

Abstract

We describe a couniversal property of the Chu construction. It induces
a comonad on a category of autonomous categories. *-Autonomous
categories are exactly the coalgebras for this comonad.  The models of
full classical linear logic (with the exponentials) are then obtained
as the coalgebras on the models of intuitionistic linear logic ---
this time for a comonad derived from the Chu construction.  In view of
the computational interpretations of linear logic, these results
suggest an interesting connection of the functional and the concurrent
programming. For this reason, some effort has been spent to make all
the constructions effective.

```
11 Oct 19:32 1993

### erratum: Undecidabilty of System F

```
I am grateful to Henk Barendregt, Martin Hoffmann, and Pawel Urzyczyn
who have pointed out the problem with unjustified "extraction term
from termination proof" trick, which I used to construct the term
\$f_p\$ in the very end of my proof of undecidability of F published in
the "types" mailing list this summer. Therefore I withdraw my claim
till I find satisfactory reparation or another proof. I am awfully
sorry for creating confusion. I would like to thank Jean-Jacques Levy
and Roberto Amadio for useful discussions.

Sergei Vorobyov

----------------------------------------------------------------

Postscript: here are some explanations

> Henk Barendregt writes:
>
> You have a term f^ p Q x representing f_p x where Q is a proof of
> Inf(X_p). If X_p is infinite (provably so), then this gives a term
> for f_p. If X_p is not infinite we have nothing, it seems.

> Martin Hoffmann writes:
>
> The thing I don't understand is how you obtain a lambda term f_p in
> case p does not have a solution. The only thing which comes to mind
> would be to take the lambda term corresponding to \x . mu y>x .
> "enum(y) solves p" where we use some coding of the mu operator. Of
> course this term is not F typable in case p has no solution, but I
> don't see why it should have an F type in case there is such a
```

19 Oct 17:23 1993

### invitation

```
Days of Mathematical Logic at W\'egimont Castle,
december 6th,7th, and 8th  1993.

A three days meeting in Mathematical Logic are set up on december 6th,
7th and 8th december 1993 at W\'egimont Castle . This castle is situated
about fifteen kilometers near from Li\`ege (Belgium).

The programme consists in four basic courses (about 3 hours for each
course):
- F. Honsell (Udine) : Theory and applications of non-well-founded sets.
- R. Kaye (Oxford) : Quantifier complexity and applications to
arithmetic and set theory,
- A. Macintyre (Oxford) : Reals with exponentiation and their
applications (probable title),
- D. van Dalen (Utrecht) : Intuitionism and constructive mathematics.

A few contributed papers are planned, at the moment :

- O. Chapuis (Paris): D\'ecidabilit\'e et ind\'ecidabilit\'e des
th\'eories universelles des groupes r\'esolubles
libres,
- F. Koerner (Berlin) : Cofinal indiscernibles and applications to NF.

This meeting is organized by M. Boffa (U.M.H.) and A. P\'etry (I.S.I.L.)
thanks to the support of the Centre National de Recherches de Logique.

It will be possible to have meals and stay in W\'egimont castle.
However the number of rooms is limited.

```

25 Oct 20:19 1993

### Parametricity and Local Variables

```
The following paper is available by anonymous ftp from top.cis.syr.edu
in ohearn/plv.dvi

Parametricity and Local Variables
P. W. O'Hearn and R. D. Tennent

We propose that the phenomenon of local state may be understood
in terms of Strachey's concept of parametric (i.e., uniform)
polymorphism.  The intuitive basis for our proposal is the following
analogy: a non-local procedure is independent of locally-declared
variables in the same way that  a parametrically polymorphic function
is independent of types to which it is instantiated.

A connection between parametricity and representational abstraction
was first suggested by J.\,C.~Reynolds.  Reynolds used logical
relations to formalize this connection in languages with type
variables and user-defined types.  We use relational parametricity
to construct a model for an Algol-like language in which interactions
between local and non-local entities satisfy certain relational
criteria.  Reasoning about local variables essentially involves
proving properties of polymorphic functions. The new model supports
straightforward validations of all the test equivalences that have
been proposed in the literature for local-variable semantics,
and encompasses standard methods of reasoning about data
representations.  It is not known whether our techniques yield fully
abstract semantics.  A model based on partial equivalence relations
on the natural numbers is also briefly examined.

This is an expansion and elaboration of material from
```

31 Oct 13:25 1993

### complexity

```
Does anybody know the complexity of provability for non commutative
multiplicative linear logic with units but without atoms?

The formulae are built from Unit and Bottom using Times and Par.
The rules are:

|- GAMMA, A, GAMMA'    |- DELTA, B, DELTA'

-------         ------------------------------------------
|- Unit         |- DELTA, GAMMA, A Times B, DELTA', GAMMA'

|- GAMMA, GAMMA'              |- GAMMA, A, B, GAMMA'
------------------------         -------------------------
|- GAMMA, Bottom, GAMMA'         |- GAMMA, A Par B, GAMMA'

In the Times rule, GAMMA' or DELTA must be empty.

Yves Lafont <lafont@...>.

```
28 Oct 16:03 1993

### lambda - a program for solving lambda definability problems

```
An initial release of lambda, a program for solving lambda definability
problems of order at most two, is now available.

The lambda distribution consists of:

* The postscript source for the paper "Mechanizing Logical Relations",
by Allen Stoughton, which describes the theory on which lambda is
based and explains what the program does.  This paper will appear in
the proceedings of the Ninth International Conference on the
Mathematical Foundations of Programming Semantics, LNCS, vol. ?,
Springer-Verlag, 1994, pp. ?-?.  The paper's abstract is:

We give an algorithm for deciding whether there exists a definable
element of a finite model of an applied typed lambda calculus that
passes certain tests, in the special case when all the constants and
test arguments are of order at most one.  When there is such an
element, the algorithm outputs a term that passes the tests;
otherwise, the algorithm outputs a logical relation that demonstrates
the nonexistence of such an element.  Several example applications of
the C implementation of this algorithm are considered.

* A short manual page describing lambda.

* The implementation of lambda.  Lambda is written in ANSI C, with the
exception of its lexical analyzer and parser, which are written in lex
and yacc source, respectively.  It uses one UNIX System V system call
(also supported by SunOS Release 4.1).  The C programs that it
generates also conform to the ANSI standard; they use several UNIX
System V system calls (also supported by SunOS Release 4.1) in order
```