Hi, you should reply something meaningful unless you don’t know what’s your *real* problem (and what others are talking about).
"ML for the working programmer” is a book teaching you how to writing program in Standard ML, you’ll learn how to manipulate ML lists in that book. If you want to use HOL to prove something, you need to learn Standard ML first, as HOL’s proof scripts are also ML programs, even most of time you don’t see any “algorithm-like” thing in it. On the other side, if you’re trying to prove any theorem, better to show us your field and the target theorem that you’re trying to prove (but I highly doubt there is one). It may look that you’re using HOL’s listTheory and whileTheory, but I would say you’re actually doing normal programming at ML level, under HOL environment. (Thinking my own HOL learning curves, I touched listTheory very lately (after setTheory and arithmeticTheory) and so far I haven’t found any use of whileTheory yet) Blame me if I guessed wrongly. —Chun > Il giorno 05 giu 2018, alle ore 08:33, 尚亚龙 <2016210...@mail.buct.edu.cn> ha > scritto: > > Dear Thomas, > > > Thank you for your reply. > > I learned a lot from it. > > I am not very familiar with the functions mentioned in your article. > > I will spend time to study them. > > > Thank you again. > > > Shang > -----原始邮件----- > 发件人:"Thomas Tuerk" <tho...@tuerk-brechen.de> > 发送时间:2018-06-05 12:26:46 (星期二) > 收件人: hol-info@lists.sourceforge.net > 抄送: > 主题: Re: [Hol-info] Loops in HOL4 > > Dear Shang, > > reading your question, I was wondering, whether you really want to use a > WHILE loop. Usually you would rather use recursion in HOL. In higher order > logic you don't have a state that you can modify. Of course you can mimic a > state by passing it around explicitly. This is what the WHILE function does. > If you are new to HOL and have not done much functional programming before, I > recommend learning functional programming first. Prof. Larry Paulson's book > "ML for the working programmer" is available online and a very good > introductionhttp://www.cl.cam.ac.uk/~lp15/MLbook/pub-details.html > <http://www.cl.cam.ac.uk/~lp15/MLbook/pub-details.html>. > > I'm also uncertain what you want to do exactly, but for me it sounds like a > combination of standard list functions like MAP, TAKE or FOLDL might be what > you really want. In HOL you talk about the value of things, you don't have a > global state to manipulate and there is nothing like execution or an > execution order. So - while it is a common thing to say and people do it very > frequently as a shortcut - strictly speaking "removing the first n items of a > list" is not something you can do. You cannot modify an existing list. You > talk about the first n elements of a list (TAKE) or about the list you get by > removing the first n elements (DROP), but you don't have a concept of > execution there and the original list does not change. You talk about values > and pass different lists around explicitly. Similarly things like "operate on > them" sounds like doing something that modifies the global state (like e.g. > printing them). This is just nothing you can do in HOL. Timing is meaningless > as well. So things like first do something then "continue" to do something > else is meaningless. You talk about the value of a function, not how you > compute that value. > > Best > > Thomas > > On 05.06.2018 04:23, 尚亚龙 wrote: >> Hi Waqar, >> >> >> First of all thanks for the reply. Your answer is very helpful to me. >> >> What I want to achieve is to remove the first n items of the list each time >> and operate on them, >> >> and then continue to perform the same operation on the rest of the list >> until the list is empty. >> >> So after reading your reply, this problem can be solved. >> >> >> thank you >> >> >> Shang >> >> >> -----原始邮件----- >> 发件人:"Waqar Ahmad" <12phdwah...@seecs.edu.pk> >> <mailto:12phdwah...@seecs.edu.pk> >> 发送时间:2018-06-05 07:43:50 (星期二) >> 收件人: "尚亚龙" <2016210...@mail.buct.edu.cn> <mailto:2016210...@mail.buct.edu.cn> >> 抄送: hol-info <hol-info@lists.sourceforge.net> >> <mailto:hol-info@lists.sourceforge.net> >> 主题: Re: [Hol-info] Loops in HOL4 >> >> I'm not sure what actually you desired with WHILE function but I can explain >> its functioning that might help you to define your function. >> >> For instance, you can define a function that continue traversing over a list >> until "P h" is true otherwise return the remaining part of the list. >> >> !P L. dropWhile_new P L = WHILE (\a. P (HD a)) TL L >> >> a trivial example could be >> >> val dropWhile_eq = store_thm("dropWhile_eq", >> ``ALL_DISTINCT [a;b;c] ==> (dropWhile_new ($=a) [a;b;c] = [b;c])``, >> rw[dropWhile_new_def] >> \\ once_rewrite_tac[WHILE] >> \\ rw[] >> \\ once_rewrite_tac[WHILE] >> \\ rw[]); >> >> I hope this helps.... >> >> >> On Mon, Jun 4, 2018 at 10:08 AM, 尚亚龙 <2016210...@mail.buct.edu.cn >> <mailto:2016210...@mail.buct.edu.cn>> wrote: >> Hi everyone, >> >> >> I'm just beginning to learn HOL4. And I have a question. >> >> >> >> The problem is as follows: I have a list 'a', >> >> I want to use a loop to retrieve the number of 'num' in a each time until >> the list is empty, >> >> and I see WHILE theorems can be used in the HOL library, but I can not >> succeed, >> >> So I would like to ask how to implement the WHILE theorem, >> >> if you can, please attach an example to explain. Thank you! >> >> >> >> Shang >> >> ------------------------------------------------------------------------------ >> Check out the vibrant tech community on one of the world's most >> engaging tech sites, Slashdot.org! http://sdm.link/slashdot >> <http://sdm.link/slashdot> >> _______________________________________________ >> hol-info mailing list >> hol-info@lists.sourceforge.net <mailto:hol-info@lists.sourceforge.net> >> https://lists.sourceforge.net/lists/listinfo/hol-info >> <https://lists.sourceforge.net/lists/listinfo/hol-info> >> >> >> >> >> -- >> Waqar Ahmad, Ph.D. >> Post Doc at Hardware Verification Group (HVG) >> Department of Electrical and Computer Engineering >> Concordia University, QC, Canada >> Web: http://save.seecs.nust.edu.pk/waqar-ahmad/ >> <http://save.seecs.nust.edu.pk/waqar-ahmad/> >> >> >> >> ------------------------------------------------------------------------------ >> Check out the vibrant tech community on one of the world's most >> engaging tech sites, Slashdot.org! http://sdm.link/slashdot >> <http://sdm.link/slashdot> >> >> _______________________________________________ >> hol-info mailing list >> hol-info@lists.sourceforge.net <mailto:hol-info@lists.sourceforge.net> >> https://lists.sourceforge.net/lists/listinfo/hol-info >> <https://lists.sourceforge.net/lists/listinfo/hol-info> > > ------------------------------------------------------------------------------ > Check out the vibrant tech community on one of the world's most > engaging tech sites, Slashdot.org! > http://sdm.link/slashdot_______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
