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
