Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Posting-Version: version B 2.10.2 9/5/84; site randvax.UUCP
Path: utzoo!watmath!clyde!cbosgd!ukma!psuvm.bitnet!psuvax1!burdvax!sdcrdcf!randvax!lseward
From: lseward@randvax.UUCP (Larry Seward)
Newsgroups: net.math.symbolic
Subject: Re: Responce to Fatemans article "Eleven Proofs of sin^2+cos^2=1"
Message-ID: <20@randvax.UUCP>
Date: Tue, 11-Feb-86 11:42:05 EST
Article-I.D.: randvax.20
Posted: Tue Feb 11 11:42:05 1986
Date-Received: Fri, 14-Feb-86 03:23:33 EST
References: <258@wacsvax.OZ>
Reply-To: JPG@MC.LCS.MIT.EDU
Organization: Rand Corp., Santa Monica
Lines: 56

(retransmission. previous message was truncated.)

Received: from MC.LCS.MIT.EDU by rand-unix.ARPA; Sun, 2 Feb 86 22:51:44 pst
Date: Mon,  3 Feb 86 01:52:17 EST
From: "Jeffrey P. Golden" <JPG@MC.LCS.MIT.EDU>
Subject: RE: Response to Fateman's article "Eleven Proofs of sin^2+cos^2=1"
To: lseward@rand-unix.ARPA
Cc: JPG@MC.LCS.MIT.EDU
Message-Id: <[MC.LCS.MIT.EDU].805557.860203.JPG>

(for submission to net.math.symbolic)

   From: playboy%wacsvax.OZ@rand-unix.ARPA (McIsaac K)
   Newsgroups: net.math.symbolic
   Subject: Response to Fateman's article "Eleven Proofs of sin^2+cos^2=1"
   Date: 30 Jan 86 09:29:14 GMT
   Apparently-To: symalg-news-fwd
   In his article "Eleven Proofs of sin^2+cos^2=1", Fateman points out
   "a deficiency of our current way of putting together algebra systems as
   `encodings' of mathematical information" by showing that MACSYMA can't
   `express' the identity  Sin(x)^2 + Cos(x)^2 = 1.
   ...
   It is possible with current pattern matching techniques to
   `express' this, and much more complex identities, in an efficient and
   simple fashion. This idea has been taken up by Inference Corp. and used
   to extend the scope of the SMP pattern matcher.
   ...
   This is not intended as a product comparison ...

I don't agree with what you say Fateman was trying to show.  He says in the
first sentence of the Introduction that he was exploring `proving' the
identity with Macsyma, not simply `expressing' it.  He says at the end,
Macsyma has no knowledge of the truth of the fact, if directly asked.

I think the key point is to be able to automatically and efficiently
simplify expressions such as sin(x)^2+cos(x)^2 to 1.  By `automatically' I
mean without having the user call an auxiliary function.  It is difficult to
do this both automatically and efficiently.  You say that you can express
this efficiently in SMP with pattern matching.  You said that you did not
intend this as a product comparison, so I will simply note that you can
express this quite simply in Macsyma as well, and presumably in other
computer algebra systems (CAS).  `Efficiency' is more difficult to
demonstrate, as it is a relative and often subjective term.

Making use of the identity can be quite interesting.  Your SMP program
simplifies sin(x)^2+cos(x)^2 to 1, but does it also simplify
sin(x)^4-cos(x)^4  to  sin(x)^2-cos(x)^2   and
cos(x)*sin(x)^3+cos(x)^3*sin(x)  to  cos(x)*sin(x)
which follow trivially from the same identity?
Sometimes it is useful to replace sin(x)^2 by 1-cos(x)^2  or
cos(x)^2 by 1-sin(x)^2.  How about that?

Perhaps the meat of your response is the distinction between `expressing'
(perhaps by pattern matching rules) and `encoding' (i.e. directly into code)
information in CAS.  I agree that this is an important issue and you have
done a good job in raising it.