Dear Chun,
Thank you for your reply. It made me know where I got it wrong.
First of all, I apologized for my very brief reply.Then I will describe my
work. I am formalizing a data transmission protocol, and I abstract the total
data that the protocol needs to transmit into a list, and then I want to
express the data transmission by reducing n by a list. For each piece of data
that was taken out, there will be subsequent processing functions. I felt that
the entire step was like a loop but I wasn't sure if it could be implemented
that way, so I asked the previous question.
Then since the problem is still in the process of modeling the implementation,
the proof of the theorem has not yet been involved.
Finally because I had only study the basic usage of SML and did not
systematically study the theoretical knowledge, I will follow the book "ML for
the working programmer" and then rethink the issue.
Thank you for your reply！
Shang
-----原始邮件-----
发件人:"Chun Tian" <binghe.l...@gmail.com>
发送时间:2018-06-05 17:18:42 (星期二)
收件人: "尚亚龙" <2016210...@mail.buct.edu.cn>
抄送: "hol-info@lists.sourceforge.net" <hol-info@lists.sourceforge.net>
主题: Re: [Hol-info] Loops in HOL4
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 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
------------------------------------------------------------------------------
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
