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 introduction
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>
发送时间:2018-06-05 07:43:50 (星期二)
收件人: "尚亚龙" <2016210...@mail.buct.edu.cn>
抄送: hol-info <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> 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
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
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/
------------------------------------------------------------------------------
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.nethttps://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
