I also find the steps non-intuitive, but then I feel the same way about many other proofs I have been shown (especially the clever ones).
Using equivalency proofs is an interesting approach to explaining the language at a deeper level and it could lead to an axiomatic way of looking at the language that I had not considered before. I found this article on the motivations for planning proofs http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.104.3678&rep=rep1&type=pdf as well as a wikipedia entry on the author, Alan Bundy https://en.wikipedia.org/wiki/Alan_Bundy These ideas suggest that there may be an opportunity to view J programming through a slightly different lens. The chapters of 50 Shades of J tend to get me thinking in new directions and I enjoy that. Cheers, bob > On Jun 16, 2018, at 6:32 AM, Raul Miller <rauldmil...@gmail.com> wrote: > > Mathematical reasoning approaches can be a useful tactic when coding. > > That may not lead to statements worth enshrining, but that's also not > necessary. > > Thanks, > > -- > Raul > > On Sat, Jun 16, 2018 at 9:06 AM Henry Rich <henryhr...@gmail.com> wrote: >> >> Certainly, J doesn't do math. The question is, Is the executable >> notation mathy enough that you can reason mathematically about the >> computations? I haven't been able to, but maybe someone could find a >> set of transformations that is enough for progress in this area. >> >> On your session-log problem: how about a script to take the session log, >> find the lines beginning with 3 spaces, treat the rest as results, and >> either create the assertions automatically or execute the sentences and >> compare them against the results? >> >> Henry Rich >> >> On 6/16/2018 7:18 AM, Ian Clark wrote: >>> Thanks, Henry. >>> >>> Yes… it's all very much not obvious to me too. >>> >>> I was going to mention NuVoc: >>> http://code.jsoftware.com/wiki/Vocabulary/ampdot — but I felt ignorance >>> would suit me better. >>> >>> How to present theorems (propositions?) in J would be good to standardize. >>> How to prove them (run them?) even better. >>> >>> Right now I'm writing test scripts and I'm bog-eyed with typing out assert >>> (".phrase) -: (result) over and over again in multifarious forms from an >>> extensive session log. Every six months I devise a new solution to this >>> perpetual problem – and six months later I reckon it's a dog! >>> >>> Until that's sorted, I can't pretend to myself J does math. J does >>> calculations. >>> >>> Ian >>> >>> On Sat, Jun 16, 2018 at 3:35 AM, Henry Rich <henryhr...@gmail.com> wrote: >>> >>>> It's a theorem: >>>> >>>> [x] >@(f each) y >>>> >>>> [x] >@(f&.>) y >>>> >>>> [x] >@((<@:f)&>) y >>>> >>>> [x] (>@(<@:f)&> y >>>> >>>> [x] (>@:<)@:f&> y >>>> >>>> [x] f&> y >>>> >>>> [x] (f every) y >>>> >>>> >>>> Some of these steps are very much not obvious IMO. And you have to get >>>> the rank of each right, that is, use the NuVoc definition of &. rather than >>>> the Dictionary one. >>>> >>>> Henry Rich >>>> >>>> >>>> On 6/15/2018 8:30 PM, Ian Clark wrote: >>>> >>>>> I've checked Chapter 1 off, but that's only to say I've checked out the >>>>> code and verified it gives the results claimed. I didn't see it as my job >>>>> to rewrite the treatment to make it clearer – which I can't do anyway >>>>> without being sure what the author is trying to convey. >>>>> >>>>> I must confess that first section completely baffles me. I cannot see how >>>>> to relate the "general rule" to actual examples of J code, although the >>>>> article goes on to do just that … it seems. Does the "rule" represent real >>>>> working J code? – even in a generic sense? Is it even true? (Theorems have >>>>> to be true, but rules only have to be obeyed.) If it isn't always true, am >>>>> I to understand it as a rule-of-thumb?And if it is in fact universally >>>>> true, what procedure must I, the novice reader, follow in order to convert >>>>> the "generics" into "specifics" to verify the fact? >>>>> >>>>> I'd be grateful for someone to cast light on the matter. Failing which, >>>>> maybe I ought to remove my green checkmark, stand aside to let someone >>>>> else >>>>> scratch their head over it. >>>>> >>>>> On Sat, Jun 16, 2018 at 12:41 AM, David Lambert <b49p23t...@gmail.com> >>>>> wrote: >>>>> >>>>> 50 Shades of j chapter 1 now says that rule is completely general. I'm >>>>>> somewhat weak on j transformations and proofs, although what was there >>>>>> was >>>>>> incorrect because of a counterexample: >>>>>> >>>>>> >>>>>> every=.&> NB. uses compose >>>>>> each=.&.> NB. uses under >>>>>> rule =: (f every) -: >@(f each) >>>>>> >>>>>> NB. Is completely general? >>>>>> >>>>>> >>>>>> thank you, Dave >>>>>> >>>>>> ---------------------------------------------------------------------- >>>>>> For information about J forums see http://www.jsoftware.com/forums.htm >>>>>> >>>>> ---------------------------------------------------------------------- >>>>> For information about J forums see http://www.jsoftware.com/forums.htm >>>>> >>>> >>>> --- >>>> This email has been checked for viruses by AVG. >>>> https://www.avg.com >>>> >>>> >>>> ---------------------------------------------------------------------- >>>> 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 > ---------------------------------------------------------------------- > For information about J forums see http://www.jsoftware.com/forums.htm ---------------------------------------------------------------------- For information about J forums see http://www.jsoftware.com/forums.htm
