((+*-) -: (-&*:))~ 10x^308 1 But mine goes to eleven:
((+*-) -: (-&*:))~ 11x^308 1 On Mon, Dec 10, 2012 at 12:46 PM, Roger Stokes < [email protected]> wrote: > 1e308 ((+*-) -: (-&*:)) 1e308 > NaN error > 1e308 ((+*-)-:(-&*:))1e308 > > > ----- Original Message ----- From: "Don Guinn" <[email protected]> > To: <[email protected]> > Sent: Monday, December 10, 2012 3:57 PM > Subject: Re: [Jprogramming] Proofs in J > > > > Changing the thread. >> >> No. This is a way to check one's work in deriving a proof. And it is not >> too difficult to convert the tacit expression to explicit then make the >> proof. See example below. Interesting that you chose a monadic test. Tacit >> verb phrases are ambivalent. Therefore there must be two proofs. Actually, >> the monadic form is not an identity. Easily shown by: >> >> ((+*-) -: (-&*:))1j1 >> 0 >> >> It is an identity for real numbers, but not complex. It fails because >> monadic + is defined as conjugate, not same. >> >> p=:] : + >> ((p*-) -: (-&*:))0j1+i.10 >> 1 >> >> J is excellent as a computation tool. Doing proofs in J syntax is a bit >> awkward. >> >> Here is my proof: >> >> proof=: 4 : 0 NB. That (+*-) -: >> (-&*:) >> a=.x(+*-)y >> assert. a -: ((x+y)*(x-y)) NB. Definition of >> fork >> assert. a -: ((x*x)+(x*(-y)) +(y*x) +(y*(-y))) NB. * distributive >> over + and - >> assert. a -: ((x*x)+((x*(-y)) +(x*y))) +(y*(-y)) NB. * is >> commutative >> assert. a -: ((x*x)+((x*(_1)*y)+(x*(1)*y)))**+(y*(_1)*y) NB. Definition >> of >> dyadic + and - >> assert. a -: ((x*x)+(((_1)*x*y)+((1)*x*y)))**+((_1)*y*y) NB. * is >> commutative >> assert. a -: ((x*x)+((_1)+(1))*(x*y)) +((_1)*y*y) NB. >> * distributive over + and - >> assert. a -: ((x*x)+((0)*(x*y)) -(y*y)) NB. Don`t remember >> why >> assert. a -: (x*x) -(y*y) NB. 0 times >> anything >> is 0 >> assert. a -: (x^2) -(y^2) NB. Definition of ^ >> assert. a -: (*:x) -(*:y) NB. Definition of >> *: >> assert. a -: x(-&*:)y NB. Definition of & >> (compose) >> a >> ) >> proof"0/~_2 _1 0 1 2 3j4 >> 0 3 3 0 11j_24 >> _3 0 0 _3 8j_24 >> _3 0 0 _3 8j_24 >> 0 3 3 0 11j_24 >> _11j24 _8j24 _8j24 _11j24 0 >> >> The fact that it got to the end says that each statement is correct for >> the >> given data. Not that some other value could cause a failure, but a pretty >> good way to catch errors in the proof. Gives me confidence that my proof >> is >> valid. >> >> Can this be done with a program? What about proofs when dealing with >> defined names instead of primitives? And is there a way to do this proof >> without converting tacit to explicit? >> >> Notice that I had to set the rank of proof to zero. Not too much of a >> problem in this proof, but not sure what to do if non-scalar primitives >> are >> present. >> >> On Sun, Dec 9, 2012 at 4:04 PM, Raul Miller <[email protected]> >> wrote: >> >> On Sun, Dec 9, 2012 at 4:38 PM, Don Guinn <[email protected]> wrote: >>> > More fun to try to do it using tacit expressions. One toy I tried > >>> without >>> > too much success is: >>> > (+*-) -: ((-&*:) >>> > I wanted to do it without using any explicit expressions. >>> >>> Do you mean something like this? >>> ((+*-) -: (-&*:)) i. 10 >>> 1 >>> >>> I'm not quite clear on what you are trying to do here... >>> >>> Thanks, >>> >>> -- >>> Raul >>> ------------------------------**------------------------------** >>> ---------- >>> For information about J forums see >>> http://www.jsoftware.com/**forums.htm<http://www.jsoftware.com/forums.htm> >>> >>> ------------------------------**------------------------------** >> ---------- >> For information about J forums see >> http://www.jsoftware.com/**forums.htm<http://www.jsoftware.com/forums.htm> >> >> > > ------------------------------**------------------------------**---------- > For information about J forums see > http://www.jsoftware.com/**forums.htm<http://www.jsoftware.com/forums.htm> > -- Devon McCormick, CFA ^me^ at acm. org is my preferred e-mail ---------------------------------------------------------------------- For information about J forums see http://www.jsoftware.com/forums.htm
