wffs vs graphs

schubert@cs.rochester.edu
Date: Fri, 25 Feb 1994 13:46:14 -0500
From: schubert@cs.rochester.edu
Message-id: <199402251846.NAA15811@cherry.cs.rochester.edu>
To: boley@dfki.uni-kl.de, cg@cs.umn.edu, fritz@rodin.wustl.edu,
        interlingua@ISI.EDU, phayes@cs.uiuc.edu, schubert@cs.rochester.edu
Subject: wffs vs graphs
> But look. Suppose I were to insist that since graphs must be printed or
> displayed, any perceptible 'token' graph will have its nodes and lines
> displayed in some position on the screen; therefore, the problem of graph
> matching is the problem of matching bitmapped pictures of graphs. This
> would clearly be a perverse position ...

Well, keystrokes are (at least at present) more tractable tokens for
on-line processing than bitmaps. But we *do* have to start with tokens.

You mention the possibility of wff-matching aided by a kind of graphical
representation of variable bindings, and remark,

> quantifier binding structure does not naturally 'fit' into the usual 
> recursive may of parsing syntax, and that bound variables are only 
> a device, and perhaps a rather artificial one, for making it fit

One way of making it fit is by skolemization, and I suppose that may be
why network theorists (inlcuding me) have tended to use some sort of 
skolem-like form of implicit quantification. But as far as I can tell,
this doesn't help with the matching problem. As you say,

> It will be necessary to consider permutations of &, of course, and that
> seems to me to be the real difficulty. Unfortunately it does not seem that
> anything is going to be able to help with the worst case ...

I've talked with a colleague about this, and he says

1. This does look like DAG-isomorphism, which is equivalent to graph
   isomorphism in general, for which it is still not known whether
   it's polynomial, just as Bob McGregor surmised (except for bounded 
   degree graphs, which we can't restrict ourselves to if we want 
   polyadic conjunction and disjunction)

2. A graphical representation of a formula could be exponentially
   more compact than a string representation, by avoiding subexpression
   repetition. 

The latter is an interesting point. But as I noted in my article in
John's book, one can augment standard logical syntax with subexpression
names, getting something even closer to network syntax. With these
names, the wff-syntax can completely avoid subexpression repetition,
and also allows cycles (e.g., Liar sentences, illustrated in the paper).
Feature logics, whose relevance to this discussion I previously
mentioned, also use names for shared functional expressions, avoiding
repetition. (Our input syntax for episodic logic in the EPILOG system
also allows subexpression naming.)

Len