# wffs vs graphs

John McCarthy <jmc@sail.stanford.edu>
Date: Fri, 25 Feb 94 11:39:37 -0800
From: John McCarthy <jmc@sail.stanford.edu>
Message-id: <9402251939.AA14284@SAIL.Stanford.EDU>
To: schubert@cs.rochester.edu
Cc: boley@dfki.uni-kl.de, cg@cs.umn.edu, fritz@rodin.wustl.edu,
interlingua@ISI.EDU, phayes@cs.uiuc.edu, schubert@cs.rochester.edu
In-reply-to: <199402251846.NAA15811@cherry.cs.rochester.edu> (schubert@cs.rochester.edu)
Subject: wffs vs graphs
Reply-To: jmc@cs.stanford.edu

My own opinion is that the inability of standard syntax formalisms to
handle bound variables decently is the fault of the syntax formalisms
and not a reason to abandon bound variables. It is rather a reason to
invent new syntax formalisms.
Here is an example in what may be a simpler context. Consider
programs with labels and gotos. The condition that every label occur
just once, and every goto have a label to go to is a syntactic
condition that context free languages don't handle decently. Here
is how to handle it.
The syntactic entities are triples of the form
(<program fragment>, <set of labels in the fragment>, <set of
destinations of unsatisfied gotos in the fragment>
Two fragments are compatible if their sets of labels are disjoint and
if so can be confined to give a new fragment with the concatenation
of the fragments, the union of the sets of labels, and the set of
unsatisfied destinations the union of the previous sets reduced by
the sets of labels.
A proper program is one with empty set of unsatisfied destinations.
I have not been looking at the literature so maybe someone did this
long ago, and if so, I would like to know about it.
A proper syntactic formalism for expressions with bound variables is
an extension of this problem.