headers
Andre Scedrov | 1 Sep 1992 16:51

Paper available by ftp

Date: Mon, 31 Aug 92 16:38:50 EDT

        First Order Linear Logic Without Modalities is NEXPTIME-Hard 

                        P. Lincoln  and  A. Scedrov  

     ABSTRACT: In this paper the decision problem is studied for the 
     multiplicative-additive fragment of linear logic with first order 
     quantifiers. This fragment is shown to be NEXPTIME-hard. The hardness 
     proof combines Shapiro's logic programming simulation of nondeterministic
     Turing machines with the standard proof of the PSPACE-hardness of 
     quantified boolean formula validity, utilizing some of the surprisingly 
     powerful and expressive machinery of linear logic. In contrast to 
     previous work on linear logic proof search as a computational paradigm, 
     in which a computation proceeds ``upwards'' along a proof tree, here the 
     computation steps are applied ``horizontally across'' the leaves of a 
     proof tree.  

This paper can be retrieved by anonymous ftp using the instructions below.  
If you would like a copy but cannot use ftp to this site, please send me your 
postal address.   

% ftp ftp.cis.upenn.edu
Name: anonymous
Password:  <<your e-mail address>>
ftp> cd pub/papers/scedrov 
ftp> binary
ftp> get mall1.dvi  
ftp> quit
(Continue reading)

Permalink | Reply | 0 comments |
headers
Patrick Lincoln | 2 Sep 1992 17:49
Picon

paper available by FTP

Date: Tue, 1 Sep 92 10:14:03 -0700
To: linear@...

        Constant-Only Multiplicative Linear Logic is NP-Complete
                        P. Lincoln  and  T. Winkler

    This paper explores the decision problem for 
    multiplicative linear logic without propositions.  The
    fragment is shown to be NP-Complete.  Reduction from 
    3-Partition is used to demonstrate hardness, while 
    the obvious "guess and check entire proof" procedure
    shows that this decision problem is in NP.  This result
    lends evidence that the linear circuit evaluation problem
    (testing validity of expressions in AND, OR, TRUE, and FALSE
    in multiplicative linear logic) is intractable.  This paper
    is based on work by the authors and N. Shankar, as well as 
    earlier work by Girard and others.
	
% ftp ftp.csl.sri.com
Name: anonymous
Password:  <<your e-mail address>>
ftp> cd pub/lincoln
ftp> binary
ftp> get comult-npc.dvi  
ftp> quit
Permalink | Reply | 0 comments |
headers
David Rydeheard | 2 Sep 1992 17:58
Picon

Category Theory and Computer Science, Sep. 7-10, '93, Amsterdam

Date: Wed, 2 Sep 92 15:46:47 BST

                                 1993
              ********* Preliminary Announcement ***********
              *                                            * 
              *    CATEGORY THEORY AND COMPUTER SCIENCE    *
              *    ------------------------------------    *
              *                                            *  
              *          Fifth Biennial Meeting            * 
              *                                            *
              **********************************************

                                CTCS-5

                 Dates: 7th-10th September 1993.
                 Venue: CWI, Amsterdam, The Netherlands.

The fifth of the biennial conferences on category theory and computer science
is to be held in Amsterdam in 1993. 

The purpose of the conference series is the advancement of the foundations of
computing using the tools of category theory, algebra, geometry and logic.
Whilst the emphasis is upon applications of category theory, it is recognised
that the area is highly interdisciplinary and the organising committee welcomes
submissions in related areas. Topics central to the conference include:
        *   The semantics of computation
        *   Program logics and specification
        *   Type theory and its semantics
        *   Domain theory
        *   Linear logic and its semantics
(Continue reading)

Permalink | Reply | 0 comments |
headers
Samson Abramsky | 3 Sep 1992 21:07
Picon
Picon
Favicon

paper available by ftp

Date: Thu, 3 Sep 1992 14:13:30 +0100 (BST)

The following paper is now available by anonymous ftp from
theory.doc.ic.ac.uk, in papers/Abramsky. Anyone needing a hard copy
should send me their postal address.

--------

\documentstyle[11pt]{article} 

\begin{document} 
\bibliographystyle{alpha}
\title{Games and Full Completeness for Multiplicative Linear Logic}
\author{Samson Abramsky and Radha Jagadeesan \\
Imperial College.}

\maketitle

\begin{abstract}
We present a game semantics for Linear Logic, in which formulas denote
games and proofs denote winning strategies.  We show that our semantics
yields a categorical model of Linear Logic and prove  {\em full
completeness} for Multiplicative Linear Logic with the MIX rule: every
winning strategy is the denotation of a unique cut-free proof net.  A key
role is played by the notion of {\em history-free} strategy; strong connections
are made between history-free strategies and the Geometry of Interaction.
Our semantics incorporates a natural notion of polarity, leading to a
refined treatment of the additives.  We make comparisons with related work
by Joyal, Blass {\it et al}. 
\end{abstract}
(Continue reading)

Permalink | Reply | 0 comments |
headers
Klaus Grue | 7 Sep 1992 07:09
Picon
Favicon

Map theory

Date: Sun, 6 Sep 92 09:40:36 +0200

MAP THEORY

An index/glossary is now available by anonymous ftp
for the following paper:

Klaus Grue: Map theory,
Theoretical Computer Science 102 (1992) 1-133
Elsevier

Map theory is a foundation of mathematics based on lambda-
calculus instead of logic and sets, and thereby fulfills
Church's original aim of introducing lambda-calculus. Map
theory can do anything ZFC set theory can do. In particular,
all of classical mathematics is contained in map theory.
In addition, and contrary to set theory, map theory has
unlimited abstraction and contains a computer programming
language as a natural subset. Map theory is as simple and
homogeneous as ZFC set theory. The paper presents map theory,
develops ZFC within map theory and gives a relative
consistency proof for map theory.

The index is available in LaTeX format by anonymous ftp
>from the University of Copenhagen. Instructions:

* Connect to host ftp.diku.dk [129.142.96.1]
* Use login id "ftp" with your internet address as password
* go to directory /pub/diku/users/grue
* "get" the file "mapindex.tex" from that directory
(Continue reading)

Permalink | Reply | 0 comments |
headers
pratt | 8 Sep 1992 02:59
Picon

Re: Map theory

Date: 07 Sep 92 09:52:01 PDT (Mon)

	From: Klaus Grue <grue@...>
	Date: Sun, 6 Sep 92 09:40:36 +0200
	...
	In addition, and contrary to set theory, map theory has
	unlimited abstraction and contains a computer programming
	language as a natural subset.

Presumably these terms must be defined carefully in order to prevent
SETL from being a "natural subset" of set theory.

	Vaughan Pratt
Permalink | Reply | 1 comment |
headers
Klaus Grue | 8 Sep 1992 21:50
Picon
Favicon

Map theory--addendum

Return-Path: <grue@...>
Date: Tue, 8 Sep 92 15:54:52 +0200

...
In addition, and contrary to set theory, map theory has
unlimited abstraction and contains a computer programming
language as a natural subset.

        Klaus Grue

Presumably these terms must be defined carefully in order to prevent
SETL from being a "natural subset" of set theory.

        Vaughan Pratt

Here is a more complete (and longer) description:

Map theory has six basic concepts: Functional application,
lambda abstraction, if-then-else, a single atom T, Hilbert's
epsilon operator (also known as the choice operator) and a
'well-foundedness' predicate. Omitting Hilbert's epsilon
operator and the well-foundedness predicate yields a Turing
complete computer programming language.

On the contrary, ZFC has four basic concepts: Membership, negation,
implication and universal quantification. No subset of these
concepts form a Turing complete computer programming language.

ZFC has limited abstraction in that {x|p(x)} merely is guaranteed
to exist if x is restricted to some set.
(Continue reading)

Permalink | Reply | 0 comments |
headers
pratt | 8 Sep 1992 23:34
Picon

Re: 2 questions re: mapping from IL to ILL

To: linear@...
Date: 01 Sep 92 22:46:48 PDT (Tue)
Received: from Ghoti.Stanford.EDU by theory.lcs.mit.edu (5.65c/TOC-1.2S) 
	id AA06476; Tue, 08 Sep 92 17:23:42 EDT

>The first question concerns the mapping
>	| A -> B |   ==>   !| A | -o | B |
>I can't see why this isn't
>        | A -> B |   ==>   !( !| A | -o | B |)

Then it wouldn't follow that -> was intuitionistic implication.  In
particular you couldn't show A->(B->C) = (B&A)->C.  With the first
mapping this follows via
	A->(B->C) = !A-o(!B-oC) = (!B <at> !A)-oC = !(B&A)-oC = (B&A)->C.
With your mapping you get stuck thus:
	A->(B->C) = !(!A-o!(!B-oC)) = ?

(By A=B I mean constructive equivalence, i.e. isomorphism, of A and B
rather than their identity.  Nonconstructive equivalence would settle
for independent proofs of A|-B and B|-A, constructive equivalence adds
the further requirement that these proofs compose via cut to yield the
standard (identity) proofs of A|-A and B|-B.)

>or
>        | A -> B |   ==>   !| A | -o !| B |

Similar problem:
	A->(B->C) = !A-o!(!B-o!C) = ?

>The second question concerns
(Continue reading)

Permalink | Reply | 0 comments |
headers
Thomas Forster | 9 Sep 1992 18:29
Picon
Picon

quantum logics

Date: Wed, 9 Sep 92 09:55 BST
To: linear@...

Does anybody know anything about sequent calculi for quantum logics?
      Thomas Forster
Permalink | Reply | 0 comments |
headers
AUSTIN C. MELTON | 9 Sep 1992 18:31
Picon

MFPS IX

Date: Tue, 8 Sep 92 17:03:55 EDT

                              Call for Papers 

                                  MFPS IX 

                        The Ninth Conference on the 
              Mathematical Foundations of Programming Semantics 

                              April 7 - 10, 1993 
                             New Orleans, LA  USA 

The Ninth Conference on the Mathematical Foundations of Programming 
Semantics will be held at Tulane University, New Orleans, LA USA from 
April 7 to April 10, 1993.  The conference will consist of six one-hour 
invited talks and of talks selected from submissions.  There also will be 
two Special Sessions.  The MFPS conferences are devoted to those areas of 
mathematics, logic and computer science which are related to the semantics 
of programming languages.  The series has particularly stressed providing a 
forum where both mathematicians and computer scientists can meet and exchange 
ideas about problems of common interest.  We also welcome submissions by 
researchers in ``neighboring areas,'' since we have attempted to maintain some 
breadth in the scope of the series. 

The invited speakers for MFPS IX are: 

 Peter Aczel (Manchester)              Dale Miller (Pennsylvania)   
 Pierre-Louis Curien (LIENS-DMI)       Andrew Pitts (Cambridge)  
 Albert Meyer (MIT)                    Gordon Plotkin (Edinburgh)
(Continue reading)

Permalink | Reply | 0 comments |

Gmane