Mr Boss Many thanks for the correction - much appreciated. I'm sorry to have given you the trouble.
I will look forward to reading your papers. Regards On Fri, Apr 15, 2016 at 5:45 PM, R.E. Boss <[email protected]> wrote: > A small correction to start with: "There is more stuff at > http://www.learningj.COM/THEORIES.ZIP"; since you left out (.com). > > I am definitely interested, did not know about PVS and will (hopefully) > follow your progress with curiosity. > > If I will have time again, one of my plans will be to investigate > artificial intelligence with J; to my knowledge close to nothing has been > done in that direction. > > And in the meantime I will write a paper now and then about my attempts > with J in the past. > To be published in JoJ and/or Vector. > > > R.E. Boss > > > > -----Original Message----- > > From: Chat [mailto:[email protected]] On Behalf Of > > roger stokes > > Sent: donderdag 14 april 2016 17:06 > > To: [email protected] > > Subject: Re: [Jchat] Computationally Assisted Mathematical Discovery and > > Experimental Mathematics > > > > Mr Boss > > > > Thanks for the interesting links. > > > > On the subject of proof-assistants, you might be entertained > > by a little project I have been working at for some time, on and off. > > > > The aim is to produce a formal rigorous mathematical > > account of the semantics of the J programming language. > > > > Formality and rigor are ensured by using a widely-respected > > computer theorem-proving system. There are a number of these: > > Coq is one, as mentioned in the referenced article, but the one > > I like is the PVS system from SRI - see http://pvs.csl.sri.com/ > > > > Whether the result is about J or only about something similar > > to J would be a social process: my theorems are certainly true but > > would everyone agree that they are true of J? > > > > Have made only a very small beginning, with little theories > > (that is, definitions and some proved theorems) > > for nouns and and also for monadic and dyadic $ verb. > > > > Just to give a little of the flavor, here a short extract, about dyadic $ > > > > ========================================================= > > > > % the domain of Shape is a set of pairs of nouns (x,y) such that > > % if the product of x is nonzero then y is nonempty > > % A restriction is that x is currently limited to scalars or vectors. > > % This restriction is awaiting attention. > > > > SH : TYPE = {x, y:noun | (prodlist(atoms(x)) >0) implies (itemcount(y) > > > 0) } > > > > Shape (xy : SH) : noun = (dnn(xy`1, xy`2) , ann (xy) ) > > > > L29: LEMMA Shape(sa,sa) = va % 0 $ 0 is empty vector > > % sa is scalar zero > > % va is empty vector > > > > %|- L29: PROOF (grind) QED > > > > ========================================================== > > ==== > > > > There is more stuff at http://www.learningj/THEORIES.ZIP > > > > Regards > > > > On Wed, Apr 13, 2016 at 9:40 PM, R.E. Boss <[email protected]> wrote: > > > > > > From: Chat [mailto:[email protected]] On Behalf Of > > 'Jon > > > > Hough' via Chat > > > > Sent: woensdag 13 april 2016 16:26 > > > > > > > > Slightly off-topic, but also a little on-topic, your post reminded > me of > > > a slightly > > > > old article > > > > http://www.wired.com/2015/05/will-computers-redefine-roots-math/ > > > > about the use of coq, and other proof helpers, by mathematicians. It > > > seems > > > > computer aided proofs are going to become more important. > > > > > > I read the article, not that old btw, in Quanta Magazine and was amazed > > > that (the name of) Zeilberger was not mentioned, who is very outspoken > > on > > > this subject. > > > Read his http://www.math.rutgers.edu/~zeilberg/Opinion149.html where > > he > > > reminded that AlphaGo invented strategies unknown by the top world > > > Go-players in its games with the world champion. > > > He is convinced, and so am I, that computers, robots if you will, come > up > > > with math we people hardly will understand. > > > And so will happen for other parts of science, art and life. > > > (this is chat anyway) > > > > > > > > > R.E. Boss > > > ---------------------------------------------------------------------- > > > 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
