jr hindley | 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
(Continue reading)

Jean Gallier | 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
Password:  <<your e-mail address>>
ftp> cd pub/papers/gallier
(Continue reading)

jr hindley | 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
received.
-------------------------------------------------------
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]
(Continue reading)

Lev D. Beklemishev | 5 Jan 13:48 1993
Picon

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
 (containing Multiplicatives, Additives, and Exponentials).

 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.
(Continue reading)

Lev D. Beklemishev | 10 Jan 15:13 1993
Picon

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)
(Continue reading)

Pascal van Hentenryck | 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
(Continue reading)

kgs | 11 Jan 21:34 1993
Picon

UPDATE: 3rd Kurt Goedel Colloquium


UPDATE:
Note list of invited speakers
Proceedings will be published by Springer

            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.

(Continue reading)

types | 19 Jan 20:05 1993
Picon
Picon

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
(Continue reading)

Wayne Snyder | 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
(Continue reading)

Robert A. G. Seely | 19 Jan 20:26 1993
Picon

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:
(Continue reading)


Gmane