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
