4 Jan 17:05 1993

### notation decision


After much agitation and Christmas pudding I have decided on
the following notation for systems that assign types to terms:

A TYPE-ASSIGNMENT is an expression of form
M:tau  (M a term, tau a type).

A TYPE-ENVIRONMENT (E) is a set of type-assignments
{x-1:tau-1,..., x-n:tau-n}
where x-1,...,x-n are distinct variables.

A TA-FORMULA is
E |-> M:tau       (E any type-environment).

To say
E |- M:tau
means that there exists a subset E' of E such that the
formula  E' |-> M:tau  is provable from the system's rules.

The notation "Environment" has seemed marginally preferable
over "context" because it has marginally fewer other meanings
in current use.

What we really need is a new notation and "Typothesis" fills this
need superbly, but I lack the courage to use it! Perhaps a
younger man...?

Happy New Year from Roger Hindley!

P.S. Thanks very much indeed to everyone who commented


5 Jan 23:57 1993

### Paper available by ftp


I just completed the following paper to appear in the
"Cahiers du Centre de Logique" of the Universite' Catholique
de Louvain.

On the Correspondence Between Proofs and lambda-Terms''

Abstract. The correspondence between natural deduction proofs
and \lambda-terms is presented and discussed.  A variant of the
reducibility method is presented, and a general theorem for
establishing properties of typed (first-order) \lambda-terms is
proved.  As a corollary, we obtain a simple proof of the Church-Rosser
property, and of the strong normalization property, for the typed
\lambda-calculus associated with the system of (intuitionistic)
first-order natural deduction, including all the connectors
\rightarrow, \times, +, \forall, \exists, and \false
(falsity) (with or without \eta-like rules).

-- Jean

-------------------------------------------------------------
The above paper can be retrieved by anonymous ftp using the
instructions below. The file name is:

cahiers2.dvi.Z

% ftp ftp.cis.upenn.edu
Name: anonymous
ftp> cd pub/papers/gallier


8 Jan 10:02 1993

### A uniqueness question


Here is a uniqueness question on type-assignment. Any info
especially literature references would be very gratefully
-------------------------------------------------------
In type-assignment (only arrow-types, type-variables, &
pure lambda-terms but RESTRICTED TO \I-TERMS),
is the whole deduction of an assignment
M:tau
determined completely by M?
-------------------------------------------------------

(The rules are the usual arrow-intro and elim:

(->E)  P:A->B  Q:A
___________
PQ:B        (A,B are arbitrary types)

(->I)   [x:A]
:
M:B
__________
(\x.M):(A->B)  (discharge x:A).)

If the M in the question is not restricted to \I-terms
then the answer is "Certainly not". For example in the
following deduction where M is (\xy.y)(\z.z) the type B can
be arbitrary without affecting the conclusion.

[y:A]


5 Jan 13:48 1993

### Constant-Only LL is undecidable


We prove that propositional Linear Logic containing
either only one literal or only one constant \bottom
is of the extreme expressive power.
As a corollary, both one-literal Linear Logic
and constant-only Linear Logic turned out to be undecidable.

P.Lincoln, J.Mitchell, A.Scedrov, and N.Shankar (1990)
proved the undecidability of full propositional Linear Logic

We proved the undecidability for a restricted fragment
of Linear Logic (the so-called generalized Horn fragment)
containing only four literals (LICS'92).

Here we prove that any standard Minsky machines can be
directly encoded in each of the two following fragments
of Linear Logic:
1. A one-literal fragment of LL.
It consists of sequents of the form
Gamma, !Delta |- p
where multisets Gamma and Delta contain
(a) the only positive literal p,
(b) no other literals,
(c) neither negative literals, nor constants, nor negations,
(d) two multiplicatives: tensor product and linear implication,
(e) one additive:  &   (or +),
(f) no exponentials
(! appears only outside of formulas from the multiset !Delta).
2. A constant-only fragment of LL.


10 Jan 15:13 1993

### Complexity of Constant-Only Fragments of LL


For ordinary logics (e.g. for classical or intuitionistic ones),
their one-literal and, especially, constant-only fragments
are essentially simpler than the corresponding full
logics (with unrestricted number of literals.)

The point is that the simulating of PSPACE-complete problems,
a priori, requires unrestricted number of variables.
For example, the proof of PSPACE-completeness of the implicative
fragment of intuitionistic logic as well as of quantified Boolean
formulas essentially uses unrestricted number of variables.

Contrary to what might be expected, we prove that
one-literal and even constant-only fragments of Linear
Logic are of the same expressive power as the corresponding
full parts of LL with infinite number of literals.

In abbreviations like
MLL,  MALL,  MELL,  MAELL
LL indicates Propositional Linear Logic,
M  indicates Multiplicatives: Tensor Product and Linear Implication,
A  indicates Additives:       & and \oplus,
E  indicates the storage operator !.

Let us recall that
1. MLL   is NP-complete (Kanovich, 1991).
2. MALL  is PSPACE-complete
(Lincoln, Mitchell, Scedrov, and Shankar, 1990)
3. MELL  can encode Petri Nets reachability.
4. MAELL is undecidable (Lincoln, Mitchell, Scedrov, and Shankar, 1990)


11 Jan 17:27 1993

### CFP: First Workshop on Principles and Practice of Constraint


PPCP93 --- Call For Papers
First Workshop on Principles and Practice of Constraint Programming
April 28--30, 1993
Newport, Rhode Island, U.S.A.
Sponsored by the Office of Naval Research

The First Workshop on the Principles and Practice of Constraint Programming
(April 28--30, 1993 in Newport, RI) will be an inter-disciplinary meeting
focusing on constraint programming as a general paradigm for computation.  The
workshop will be sponsored by the Office of Naval Research (ONR).

Conventional computing paradigms, such as functional, imperative, and
object-oriented programming, deal primarily with full information notions of
objects and data-types.  Constraint programming (CP) is based on the ability
to represent and manipulate partial information about objects, i.e.,
constraints such as equalities and inequalities.  CP augments conventional
notions of state, state-change, and control with notions of monotonic
accumulation of partial information about objects of interest, and with
operations involving constraints such as consistency and entailment.

Early studies, in the 60's and 70's, introduced and made use of CP in graphics
and in artificial intelligence. In the 80's, considerable progress was
achieved with the emergence of constraint logic programming and of concurrent
constraint programming. CP has been applied with some success to operations
research scheduling problems, hardware verification, user-interface design,
decision-support systems, and simulation and diagnosis in model-based
reasoning.  Currently, CP is contributing exciting new directions in research
areas such as: artificial intelligence, computational linguistics, concurrent
and distributed computing, database systems, graphical interfaces, operations


11 Jan 21:34 1993

### UPDATE: 3rd Kurt Goedel Colloquium


UPDATE:
Note list of invited speakers

3rd Kurt Goedel Colloquium KGC'93

Computational Logic and Proof Theory

August 24--27, 1993      Brno, Czech Republic

LAST CALL FOR PAPERS

The Kurt Goedel Society will hold its 3rd Kurt Goedel Colloquium
from Tuesday, August 24, to Friday, August 27, 1993 in Brno,
Czech Republic, the town where Kurt Goedel was born.

KGC'93 is the third in a series of biannual colloquia on logic,
theoretical computer science and philosophy of mathematics.
The first two colloquia took place in Salzburg (1989) and in
Kirchberg am Wechsel (1991).

Scope:  The colloquium is intended for logicians and computer
scientists interested in the proof-theoretic and algorithmic
aspects of logic. Topics include, but are not limited to:
proof theory, automated theorem proving, unification theory,
complexity theory, logics of programs, non-standard logics for
theoretical computer science and AI, recursion theory,
logic programming, lambda-calculus.



19 Jan 20:05 1993

### Types forum


Albert Meyer, the previous moderator of the Types Forum, had
a long-standing policy of not forwarding conference announcements
of a general nature, referring these to the Theory-A list instead.
After some experience, I've concluded that this is a good policy,
and modified the policy document accordingly.  Please see the
penultimate paragraph below.
-- Philip Wadler, Moderator, Types Forum

THE TYPES FORUM

TYPES is a moderated email forum focusing on Type Theory in Computer
Science, with a broad view of the subject encompassing semantical,
categorical, operational, and proof theoretical topics.  Typical topics
include:

Typed, untyped, polymorphic lambda calculus; type checking,
inference, and reconstruction; dependent types, calculus of
constructions, linear logic; adequate and fully abstract
models; Curry-Howard correspondence; recursive types; domain
theory; category and topos theory; term reduction: strong
normalization, confluence; abstract data types.

Comments and criticisms of results in the literature, open problems,
and research queries, are encouraged.  Announcements of meetings and
publications, and abstracts of papers, are also welcome.

Conference announcements of a general nature should not be sent to the
Types Forum.  A good place for these to appear is Theory-A, the
TheoryNet world-wide events list.  Send announcements or request to


16 Jan 21:32 1993

### workshop announcement


I would like to post the following announcement on the types
mailing list to attract the intrest of those working in
areas related to unification. The workshop has been timed to
make it easy for those coming to LICS to attend. Thanks
very much! -wayne snyder

UNIF93

Seventh International Workshop on Unification
Preliminary Annoucement and Call for Participation

Sunday, June 13 -- Monday, June 14
Boston University, Boston MA (USA)

This workshop is the seventh in a series of meetings on unification and
related topics, the previous ones having been in Val d'Ajol (France),
Lambrecht (Germany), Leeds (UK), Barbizon (France), and Dagstuhl (Germany).
As its predecessors, UNIF93 is meant to be an opportunity to meet
old and new colleagues, to present recent (even unfinished) work,
and to discuss new ideas and trends in unification and related fields.
It is also a good opportunity for young researchers and researchers
working in related areas to get an overview of the current state of
the art in unification theory.

The following is a (non-exclusive) list of possible topics:

* Narrowing				* Typed Unification
* General E-unification and Calculi	* Foundations


19 Jan 20:26 1993

### Coherence for weakly distributive categories


We wish to announce that the following paper may be obtained by
anonymous ftp (details below) or directly from the authors.

Natural deduction and coherence for weakly distributive categories
by
R.F. Blute, J.R.B. Cockett, R.A.G. Seely, T.H. Trimble

(The abstract follows, but first let us highlight some points for two
specific audiences:)

Some points that might interest categorists:

*  Proof of coherence for weakly distributive categories. (These are
a natural generalization of monoidal categories to include a second
"interwoven" tensor, the interweaving given by tensorial strength - the
"weak distributivities".)

*  New uses of logical techniques to prove coherence: proof nets and empires
(from linear logic).

*  Conservativity of the extension to *-autonomous categories.  (Here we
mean that the unit of the adjunction is fully faithful.)

Some points that might interest linear logicians: