[Jprogramming] Proofs in J

[Raul Miller]

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 <donguinn at gmail.com> 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 <rauldmiller at gmail.com> wrote:
>
>> On Sun, Dec 9, 2012 at 4:38 PM, Don Guinn <donguinn at gmail.com> 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