headers
Gyorgy Revesz | 2 Feb 1990 04:39
Picon

Re: note on graph vs. term reduction

Date: Thu, 1 Feb 90 17:28:45 EST

A note by John C. Mitchell is concerned with the correspondance between
graph-reduction and term reduction. This issue is obviously related to the
translation of lambda-expressions from string-representation to graph-
representation and vice versa. It is discussed to some extent in section
6.1 of my book "Lambda-calculus, Combinators, and Functional Programming".
In particular, on page 118 it is stated that the output routine to print
lambda-expressions in string format by traversing their graphs is precisely
the inverse of the parser which builds the graphs from the input strings.
The graph reduction rules presented in the next section are in one-to-one
correspondance with their string versions, hence the confluence property
of graph reduction follows immediately from the same property of the string
version.
I would say that "string-reduction" rather than "term-reduction" is, in fact,
the counterpart of "graph-reduction", since terms can be represented in both
ways.
If term-reduction is implemented by a sequence of more elementary graph-
reduction steps than, of course, these elementary steps must represent a
"compatible refinement" (see Barendregt) of the original reduction rules.
Best Regards,
- Gyorgy Revesz
Permalink | Reply | 0 comments |
headers
Richard Kennaway | 2 Feb 1990 16:48
Picon

Re: Note on graph vs. term reduction

Date: Fri, 2 Feb 90 13:24:40 GMT

In response to John Mitchell's question about the relationship between
term and graph reduction, see:

H.P. Barendregt, M.C.J.D. van Eekelen, J.R.W. Glauert, J.R. Kennaway, 
M.J. Plasmeijer and M.R. Sleep.
  Term graph rewriting, Proc. PARLE Conference, LNCS 259, 141-158, 1987.

or the slightly longer version with more proofs:

  Term graph rewriting, Report 87, Department of Computer Science,
  University of Nijmegen, and Report SYS-C87-01, School of Information
  Systems, University of East Anglia.

Concerning Mitchell's axioms:
>Property 1.
>   If term t -> s, and T(g) = t, then there is some graph
>   h with g -> h and s ->> T(h).

>Property 2.
>   If graph g -> h, then T(g) ->> T(h).

The above paper doesn't take an axiomatic approach, but it proves these
and other relationships between any weakly regular term rewrite system
and its obvious interpretation as a graph rewrite system.  The
correspondence between evaluation strategies for term and graph systems
is also treated.  Counterexamples are illustrated when weak regularity
does not hold.
(Continue reading)

Permalink | Reply | 0 comments |
headers
John C. Mitchell | 4 Feb 1990 15:40
Picon

Complexity questions on linear logic

To: types@..., logic <at> theory.lcs.mit.edu, THEORYNT <at> vm1.nodak.edu
Date: Sat, 03 Feb 90 15:31:52 PST

Does anybody know anything about the complexity of decision
problems for propositional linear logic? I have a vague 
recollection of hearing something, but no concrete memory
of it. For example, what is the complexity of deciding whether
a propositional formula with connectives -o and ! is provable?
Or with tensor product added?

A specific question that has come up in type inference for 
linear logic is, given a propositional formula B, deciding
the set of formulas A such that A -o B is provable/valid.
In relevance logic terms, this is like the problem to 
deciding, for formula B, which A are relevant to inferring
B. Come to think of it, does anyone know if this is even
decidable for reasonable fragments of relevance logic R?

Thanks,
John Mitchell
Permalink | Reply | 0 comments |
headers
gunter | 4 Feb 1990 18:12

Complexity questions on linear logic


I'm also curious about the status of the propositional linear logic
decision problem.

Research on connections between Petri nets (vector addition systems)
and fragments of propositional linear logic has shown that the
decision problem for linear logic with the connectives:

  -o (linear implication)  ox  (tensor product)  ! (of course)

must be at least has hard as the decision problem for forward
markings.  Since the latter was a significant topic of research for
some time, it seems that propositional linear logic (with the
modalities) must encode some quite difficult decision problems.

---carl gunter
Permalink | Reply | 0 comments |
headers
gunter | 4 Feb 1990 23:08

Complexity questions on linear logic

Date: Sun, 4 Feb 90 12:12:33 EST

I'm also curious about the status of the propositional linear logic
decision problem.

Research on connections between Petri nets (vector addition systems)
and fragments of propositional linear logic has shown that the
decision problem for linear logic with the connectives:

  -o (linear implication)  ox  (tensor product)  ! (of course)

must be at least has hard as the decision problem for forward
markings.  Since the latter was a significant topic of research for
some time, it seems that propositional linear logic (with the
modalities) must encode some quite difficult decision problems.

---carl gunter
Permalink | Reply | 0 comments |
headers
watro | 5 Feb 1990 22:13
Picon

Re: Note on graph vs. term reduction

Date: Mon, 5 Feb 90 13:49:47 -0500
To: types@..., rewriting-list%loria.crin.FR <at> princeton.edu

The discussion of graph rewriting for functional programming has yet
to mention that graphs may contain directed cycles, due to the cyclic
Y-combinator reduction rule.  In this case, one generally cannot map a
graph to a finite term; possibly infinite tress are the natural
substitute.  The MITRE papers "A correctness proof for combinator
reduction with cycles", (to appear, Jan 1990 TOPLAS) and "Redex
capturing in term graph rewriting" (Tech Report M89-36, July 89,
submitted for publication) contain results on implementing term
rewriting systems with cyclic graph rewriting rules.  The first paper
uses a simple trick to prove correctness for the Y-rule without any
use of infinite objects.  The second paper formalizes a notion of
convergence for infinite tree rewritings sequences, and proves a
general result comparing cyclic graph rewriting to tree rewriting
sequences.  The infinite rewriting development is related to work of
Dershowitz, Kaplan, and Plaisted from POPL-89 and ICALP-89.

--  Bill Farmer
--  John Ramsdell      <last_name> <at> mitre.org         
--  Ron Watro
Permalink | Reply | 2 comments |
headers
Vladimir Lifschitz | 6 Feb 1990 00:06
Picon

re: Complexity questions on linear logic

To: types@..., logic <at> theory.lcs.mit.edu

[In reply to message from gunter@... sent Sun, 4 Feb
90 17:08:16 EST.]

[Message from Grigori Mints, who is visiting Stanford and can be reached
through Vladimir Lifschitz (VAL@...) until the end
of March.]

Upper bound is probably P-space by Gentzen-type argument, probably taking
notice of Kripke trick for relevant implication, due to possible absence
of thinning rule. Lower bound is P-space via Girard translation of
intuitionistic implication in terms of linear implication and ! (of course).
Decidable fragments of relevance logic R  are in: G. Mints, A cut elimination
theorem for relevance logics, J. Soviet Math, V. 6 (1976), which is based on
the decidability of relevant implication (Kripke, abstract in JSL about
1965), and of relevant implication with negation (Belnap and Wallace, Z. fur
Math. Logik, after 1965).

--Grigori Mints
Permalink | Reply | 0 comments |

Gmane