Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
To: Victor "A." Carreno <vac@air16.larc.nasa.gov>
Cc: info-hol@cs.uidaho.edu
Subject: Re: FM etiquette and accuracy
In-Reply-To: Your message of "Thu, 14 Jul 94 15:54:42 EDT." <9407141954.AA14524@air52.larc.nasa.gov>
Date: Fri, 15 Jul 94 10:57:20 +0100
From: Richard Boulton <Richard.Boulton@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:249340:940715095732"@cl.cam.ac.uk>

Victor Carreno writes:

> If I have an expression that says:
> 
> All cats have four legs, this is a cat, therefore it has four legs.
> 
> That *is* a formal expression.
> 
> I can replace cat and four legs and preserve the truth of the statement:
> 
> All x have P, this is x, therefore it has P.

Here, Victor appears to be using English, or something very like English,
as a `formal' language. The problem I have with this is that English is
ambiguous. The recognised semantics is such that multiple interpretations
are possible for most statements. In other words, the meaning of a
statement is not uniquely defined.

If Victor really is using English here then he is imposing a more rigid
semantics than the generally accepted one. He has not defined this semantics
but seems instead to be relying on the conventional one. In the example,
this seems to me to work well -- I cannot see an ambiguity. However, I could
ask what `this is a' really means, or what `it' refers to. With more complex
statements the ambiguities soon arise.

If English is not being used, but some formal language that looks like it,
then the danger is that readers will not realise that this is the case and
will use their own semantics based on what they know of English.

Similar arguments apply to HOL. If I don't know the semantics of the
language then a HOL expression is as meaningless or as ambiguous as any
English phrase. Perhaps, though, it is the unfamiliarity of HOL that is a
benefit here. People have to find out the semantics of HOL in order to
understand a HOL expression. When English is used for formal description
the risk is that they won't realise that a special interpretation is
intended or, even if they do, find it difficult to overcome `prejudices'
about the meaning because of the familiarity of English.

In summary then, I agree with Victor that English (or any natural language)
*can* be used for formal description, and that we should be careful not to
assume that all English descriptions are informal. However, I don't think
using English for formal description is a good idea on the whole because it
is very difficult to use it in an unambiguous way.

[I may well be misusing the words `formal' and `informal'. There was a
 discussion on this some time ago on info-hol. I think it starts with
 message 1749 (in the Cambridge archive), 14 Mar 1994.]

Hopefully, even if the argument intended to be carried by this message
does not convince you that English is ambiguous, the message itself will!

---------------------------------------------------------------------------
Richard Boulton
University of Cambridge Computer Laboratory

The opinions stated above are my own and do not necessarily reflect those
of my employer.
---------------------------------------------------------------------------