[CL] Why Don't We Need Free Variables?
welty at us.ibm.com
Wed Aug 3 10:43:50 CDT 2005
These threads tend to get very intense - I wanted to be sure a few things
You wrote on 08/02/2005 11:37:12 AM:
> > 1 Adopt a notation in which variables can be distinguished from
> > constants orthographically, say, with preposed question marks:
> > (if (loves John ?x) (species ?x feline))
> For the record, I very much like having a lexical convention that
> distinguishes variables from other names. This is common practice in
> technical publications involving mathematical, logical and physical
> formulas, and to me it's just confusing to obliterate the lexical
> distinction between variables and other linguistic entities that have
Then CL is for you. Remember that CL is not a language itself. It is
easy to define a language using CL that has a special notation for
> > What else do you need? If you want a standard _semantics_ for such
> > formulas, you could adopt the convention that free variables are
> > implicitly universally quantified, but in my experience this
> > convention is often violated. Anyone can extend CL to include this
> > convention (I assume; who would prevent them?). But there doesn't
> > seem to be any particular reason for CL to adopt it. I'd be much
> > more interested in seeing 'lambda' added to the language.
> Is it so outlandish to want to convey FOL-like formulas that have no
> fixed semantics established by the standard? If CL is so constrained
> that only facts can be conveyed, it seems to have excluded practical
I suspect there is confusion here that has to do with what a "variable"
is. I really think that, according to several common notions of what a
variable is in logic, CL does have variables, and you are tilting at
windmills (ie there is nothing here to disagree with).
If your intention is to define a SYNTAX that allows for: visually
identifiable variables names (eg ?x) and formulae with such names that do
not appear in a quantifier, then you can do that. You can define in CL a
language in which the interpretation of such formulae is defined to have a
quantifier (ie the convention is formally defined). You can define
different languages with different conventions, and through CL they will
be interchangeable (although what appears in one language to be a sentence
w/ free variables will not be in the other language, since the meaning of
free variables is different).
If your intention is to allow such a syntax to have no "convention", so
that variables in a sentence w/o quantifiers can mean anything, or more
importantly, that a sentence w/ free variables would look the same in any
language that allows it, even though they mean something different, then i
don't think you can do that in CL. If that is what you wanted, you don't
need an interchange language at all, you just want a string copy. I
strongly suspect you do not, it sounded like you simply wanted a syntax
that allowed for free variables.
More information about the CL