Yes... proofs are a topic that require some thought. In J, I would usually do a proof as a sequence of statements that I expect are all tautologies and where each sentence involves only a minor changes from previous/next statements.
And, I would expect the reader to be verifying that they were happy with each of the changes. Some statements (for example, those involving addition or subtraction of independent values in a multiplication or division expression) require careful constraints before they can be considered valid in a proof. -- Raul On Mon, Dec 10, 2012 at 10:57 AM, Don Guinn <[email protected]> wrote: > 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 >> > ---------------------------------------------------------------------- > For information about J forums see http://www.jsoftware.com/forums.htm ---------------------------------------------------------------------- For information about J forums see http://www.jsoftware.com/forums.htm
