[net.math.symbolic] Responce to Fatemans article "Eleven Proofs of sin^2+cos^2=1"

playboy@wacsvax.UUCP (01/30/86)

In his article "Eleven Proofs of sin^2+cos^2=1", Fateman [1] 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

   2          2
Sin (x)  + Cos (x)   = 1.

It is possible with current pattern matching techniques [2]   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.  (To clear the record,
it was possible to implement this particular identity in earlier
releases.)


Here is an example of an SMP implementation of the rule taken from the
SMP library file XSimp.

/* Part of the XSimp file */ 

/*: CSsmp[$expr]
        simplifies Sin[x]^2 + Cos[x]^2 to 1 in $expr */
        
        CSsmp[$expr] :: Si[$expr,\ Cos[$x]^2 + Sin[$x]^2 -> 1, \
                           $$a*Cos[$x]^2 + $$a*Sin[$x]^2 --> $$a, \
                           Cos[$x]^2/$b + Sin[$x]^2/$b -> 1/$b, \
                           ($$a*Cos[$x]^2)/$b + ($$a*Sin[$x]^2)/$b -> $$a/$b]
 
We now give an example of this.

SMP 1.5.0
Thu Jan 30 15:57:54 1986


#I[1]::  <XSimp

#I[2]::  cs : Sin[x]^2+Cos[x]^2 + a Sin[y]^2+b Sin[3z]^2+a Cos[y]^2+b Cos[3 z]^2

		 2           2  	  2            2	 2         2
#O[2]:   a Cos[y]  + a Sin[y]  + b Cos[3z]  + b Sin[3z]  + Cos[x]  + Sin[x]

#I[3]::  CSsmp[%]

#O[3]:   1 + a + b

#I[4]::  <end>

It has long been realised [3] the advantage of pattern matching
is information is `expressed' not `encoded'. This greatly simplifies the
implementation of identities in a CAS. We here have been using pattern matching
on very complex problems with great success for over a year. It is time that
the main stream computer scientists caught up with this idea.

Disclaimer: 
I do not wish to fuel the bitter debate between different current
computer algebra groups. This is not intended as a product comparison
or a slight of Richard Fateman, MACSYMA or any other person, group or
CAS. I do not work for Inference Corp. I am a satisfied customer who thinks SMP
is a wonderful product.


1.	Fateman R J. Eleven proofs of sin^2+cos^2=1,
	SIGSAM Bull. 19, 2 (May 1985), 25-28

2.	McIsaac K Pattern Matching alegbraic Identities,
	SIGSAM Bull. 19, 2 (May 1985), 4-13

3.	Lafferty E L. Hypergeometric Function Reduction - An Adventure 
	in Pattern Matching, MACSYMA Users Conference,
	Snowbird, 1979, 466-481


--------------------------------------------------------------------------------

Kevin McIsaac			ACSnet:	playboy@wacsvax
Dept. Physics			UUCP:	seismo!munnari!wacsvax.oz!playboy
Uni. of Western Australia          	decvax!mulga!wacsvax.oz!playboy
Nedlands, 6009
AUSTRALIA 			ARPA:	munnari!wacsvax.oz!playboy@seismo.arpa
					decvax!mulga!wacsvax.oz!playboy@Berkeley

lseward@randvax.UUCP (Larry Seward) (02/03/86)

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

lseward@randvax.UUCP (Larry Seward) (02/11/86)

(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.

lseward@randvax.UUCP (Larry Seward) (02/11/86)

Received: from cbosgd.UUCP by rand-unix.ARPA; Sat, 8 Feb 86 08:44:36 pst
Received: by ihnp4.ATT.UUCP id AA28886; 8 Feb 85 08:29:02 CST (Fri)
Received: from watmum.UUCP (watmum) by watmath.UUCP (4.12/4.7)
        id AA28242; Thu, 6 Feb 86 17:40:28 est
Received: by watmum.UUCP (4.12/4.7)
        id AA09557; Thu, 6 Feb 86 17:38:09 est
Date: Thu, 6 Feb 86 17:38:09 est
From: Michael B. Monagan <ihnp4!watmath!watmum!mbmonagan@rand-unix.ARPA>
Message-Id: <8602062238.AA09557@watmum.UUCP>
Subject: Pattern matching in SMP
Cc: mbmonagan@rand-unix.ARPA

   ...
   It is possible with current pattern matching techniques to

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
======================================================================
The message got cut off but I agree 100% with what you are trying
to point out.  There is a limit to what one can do with syntactic
pattern matching as provided by SMP.  The example given of telling
SMP that sin(x)^2 + cos(x)^2 = 1 is full of holes.  SMP will not
be able to deduce that  (sin(x)^4 + 2*sin(x)^2*cos(x)^2 + cos(x)^4)
is also equal to 1.  Neither will it be able to simplify your example
above.  Thus I feel that Kevin's implication that pattern matching
a la SMP is the way to solve problems is wrong.  Syntactic pattern
matching is simply not powerful enough to do anything non-trivial.

In any case, on the topic of implementing sin(x)^2 + cos(x)^2 = 1,
we (Maple) have a good solution in sight - though not automatic.

        simplify( <expr>, {sin(x)^2 + cos(x)^2 = 1} );

Will simplify the expression <expr> with respect to the side relations
sin(x)^2 + cos(x)^2 = 1.  I would also have included  i^2 + 1 = 0  if
I was dealing with Gaussians.  Maple will compute a grobner basis for
the side-relations and reduce the expression with respect to the
Grobner basis.  In this case, sin(x)^2 + cos(x)^2 - 1  is the Grobner
trivially.