@Bob, thanks for that link. I read it with amusement. Yes I knew about Alan Bundy. As an HF wallah, I used to keep an eye on the AI community like Jesuits keep an eye on the Wiccans. Brian Gaines once told me that Artificial Intelligence appealed to people short on the natural variety. (But I doubt AB can be accused of that.)
"We propose a science of reasoning…" …perhaps that should be: "We propose yet another science of reasoning…" The seminal text for HF people of my generation was Newell and Simon's Human Problem Solving: a method of evolving heuristics by inspired modification of what's worked in the past. But they weren't armchair theorists: they wrote a program called Logic Theorist https://en.wikipedia.org/wiki/Logic_Theorist that they used to find mathematical proofs. I'm surprised AB doesn't reference N&S: I can't believe he doesn't know about them. That's the thing about AI people. They don't seem to be aware of antecedents, but in a decade or two they catch up. I had a smart cat once… actually he wasn't smart, but he was persistent. Rather like me. His areas of research centred on opening doors and unearthing possibly tasty morsels, but – hey! – what did mine centre on? I used to sit and watch him following Newell and Simon to the letter. Scrabble-scrabble/inspect. Scrabble-scrabble/inspect. Change the approach slightly. Scrabble-scrabble/inspect. Feline Problem Solving. (It never failed.) I learned from him that just because cats lack manual dexterity it doesn't mean they're short on the intellectual variety. Ian On Sat, Jun 16, 2018 at 4:17 PM, robert therriault <[email protected]> wrote: > 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 <[email protected]> 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 <[email protected]> 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 <[email protected]> > 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 < > [email protected]> > >>>>> 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 > ---------------------------------------------------------------------- For information about J forums see http://www.jsoftware.com/forums.htm
