🚀 go-pugleaf

In article <26841@optima.cs.arizona.edu>, gudeman@cs.arizona.edu (David Gudeman) writes:
|> In article  <BxzG21.Gnr@unx.sas.com> Gary Merrill writes:
|> ]
|> ]In article <26788@optima.cs.arizona.edu>, gudeman@cs.arizona.edu (David Gudeman) writes:
|> ]
|> ]|> I propose for discussion the
|> ]|> 
|> ]|>   Axiom of Definition: (X := E /\ Exist! X.X=E) => X = E
|> ]|> 
|> ]|> where "Exist! x" means "there exists a unique x such that".  What if you
|> ]
|> ]I have not *carefully* read the rest of this posting.  However, on
|> ]the face of it, it appears that this "axiom of definition" is quite
|> ]suspect.  I'm not sure what
|> ]
|> ]	X := E
|> ]
|> ]means.  If it is really intended to represent a *definition* of X,
|> ]then why is the new axiom necessary? What exactly is the symbol
|> ]':=' meant to express beyond (or short of) '='?
|> 
|> The symbol '=' alone does not point out what variable is being
|> defined, but ':=', (which is defined formally by its usage) does.  I
|> did not discuss the rules for introducing X := E because they seemed
|> uninteresting.  It is clear that you need syntactic rules to avoid
|> naming conflicts and that rules must cover a range of clauses in a
|> proof.  That is, a definition has a scope that includes more than just
|> the clause in which it is introduced.  Clearly, no axiom or normal
|> rule of inference is adequate to specify this.

"Defined formally by its usage"?? "They seemed uninteresting"?
Things are particularly confusing since in the proposed Axiom of Definition
it appears that what is "defined" in

	X := E

is a 0-place operation symbol (X) (i.e., a term).  What does it mean to
provide a recursive definition for such an expression?  If ':=' is a
binary relation symbol, it would be nice to have some clue concerning the
properties of the relation in question.  This is not uninteresting, but
essential.

As it is, all we have is the proposed Axiom of Definition, which we can
take as a *partial* formalization of ':='.  This is not enough.

For example, it is possible to think of the Axiom of Definition as being
proposed in a free logic where '=' has the usual semantics according to
which

	x = y

is true just in case x and y both denote and have the same extension,
but where ':=' has the semantics that

	x := y

is true just in case either both denote and have the same extension *or*
both are denotationless.  The Axiom of Definition is sound under such
an interpretation (given the usual interpretation of the quantifiers).
I am sure that this is not your intention, but nothing you say appears
to rule it out.

Either a little more precision and formalization or, failing that, some
specific examples of such "definitions" would be an aid to the understanding.
-- 
Gary H. Merrill  [Principal Systems Developer, C Compiler Development]
SAS Institute Inc. / SAS Campus Dr. / Cary, NC  27513 / (919) 677-8000
sasghm@theseus.unx.sas.com ... !mcnc!sas!sasghm