[Jprogramming] Goal Directed Construction

[Roger Hui]

Re:
   (v0;v0a;v0b;v0c;v0d;v1)"1 i. 3 4

The data is highly patterned, and the patterns for each of
the three sets are similar.  Random data would be better:

   (v0;v0a;v0b;v0c;v0d;v1)"1 x=: 3 4 ?@$ 0



----- Original Message ----- 
From: "Mike Day" <mike_liz.day at tiscali.co.uk>
To: "Programming forum" <programming at jsoftware.com>
Sent: Saturday, January 28, 2006 10:12 AM
Subject: Re: [Jprogramming] Goal Directed Construction

I drafted this earlier,  before your (June's) later exchanges with
Raul, which might supersede this...

================================================================
Here's a stab at a "proof" of the variance variants,  by showing
tautologous expressions on successive lines:
   v0  =: +/@:*:@(- m)                NB. definition version
   v0a =: +/@:*:@(] - m)              NB. hook ==> fork
     dif0=: ] - m                     NB. consider difference
     dif1=: ] - (## m)                NB. equivalent
   v0b =: (+/@:*:) - (+/@:*:@(## m))  NB. expand factors
   v0c =: (+/@:*:) - (+/@ (## (*:@m)))NB. reorder second term
   v0d =: (+/@:*:) - (# * (*:@m)) NB. sum of n identical = n * one
   v1  =:  +/@:*:  -  # * *:@m        NB. clean up ==> QED

... but I wouldn't say it's crystal clear, especially the jump
from v0a to v0b.

eg
   (v0;v0a;v0b;v0c;v0d;v1)"1 i. 3 4
+-+-+-+-+-+-+
|5|5|5|5|5|5|
+-+-+-+-+-+-+
|5|5|5|5|5|5|
+-+-+-+-+-+-+
|5|5|5|5|5|5|
+-+-+-+-+-+-+

It's interesting that the statistician's preferred method,
v1, is a more complicated tacit expression in J than v0.

Mike

June Kim wrote:

>Hello
>
>I read Mathematics and Programming : A Revolution in the Art of
>Effective Reasoning by Roland Backhouse, which you can get from
>http://www.cs.nott.ac.uk/~rcb/inaugural.pdf
>
>It was very interesting and enlightening and I'd like to share my
>experience, and also would like to hear your comments -- I always
>learn so much from this mailing list.
>
>In the paper, the author shows, to prove ((%:2) + %:7) is greater than
>(%:3) + %:5, one can follow the verification, but cannot easily create
>the proof with the approach -- it is a succession of guess and
>try(please have a look at the proof in the paper). One need a
>constructive approach, an instance of which the paper calls Goal
>Directed Construction.
>
>Firstly, describe the goal straightforwardly.
>........
>Now here is another example. A friend of mine asked why the expression
>of variance(((+/@:*:@(- m)) can be shortly calculated as sum of sqr
>minus num multiplied by mean(+/@:*:  -  # * *:@m), where m is +/%#.
>
>Following is my answer:
>
>m=:+/%#
>x=:?.10$10
>R=:-: NB. the relationship could be "equal" or "non-equal"
>M=:-: NB. match
>
>((+/@:*:@(- m)) R (+/@:*:  -  # * *:@m)) x NB. we don't know whether R
>is equal or non-equal (but for instrumental purpose, let's suppose it
>as equal and verify each step)
>
>NB. whether we add, subtract, multiply, or divide with the same
>number, the relationship R doesn't change.
>
>NB. because (expand the squared expression)
>((*: + _2&*@(* m) + *:@m) M *:@(- m))  x
>NB. that
>(+/@:(*: + _2&*@(* m) + *:@m) R +/@:*: - # * *:@m) x
>
>
>NB. because (summation can be applied to each term, except when the
>term is scalar, which should be multiplied by #, simply)
>(+/@:(*: + _2&*@(* m) + *:@m) M +/@:*: + +/@:(_2&*)@(* m) + # * *:@m) x
>NB. that
>((+/@:*: + +/@:(_2&*)@(* m) + # * *:@m) R +/@:*: - # * *:@m) x
>
>
>NB. subtract +/@:*: from each side
>((+/@:(_2&*)@(* m) + # * *:@m) R -@(# * *:@m)) x
>
>NB. lets put
>nms=:# * *:@m
>
>
>((+/@:(_2&*)@(* m) + nms) R - at nms) x
>((_2&*@(+/)@:(* m) + nms) R - at nms) x
>(((m * _2 * +/) + nms) R - at nms) x
>(((m * _2 * +/) + nms) R - at nms) x
>((2 * nms) R 2 * m * +/) x
>(nms R m * +/) x
>((# * *:@m) R m * +/) x
>
>NB. divide by m
>((# * m) R +/) x
>(m R +/ % #) x
>
>NB. by definition
>
>m f.`'' M (+/ % #)`''
>
>You can run this and see all of them return 1 (I could've used assert
>or user-defined assert for convenience, instead)
>
>I intentionally stuck to tacit programming, as an experiment. Perhaps
>more explicit approach would have made the process easier to construct
>and follow, for e.g. using forms like (*:x) + (m x) * (# x) and/or
>m=:+/%#x and use the noun m instead of as a verb.
>
>June
>----------------------------------------------------------------------
>For information about J forums see http://www.jsoftware.com/forums.htm
>
>
>  
>
----------------------------------------------------------------------
For information about J forums see http://www.jsoftware.com/forums.htm