Oops. Sorry, no offense intended.
A picture is worth a thousand words.
Thanks for the FYI and the link.
http://en.wikipedia.org/wiki/Unisex_name
Leslie Lamport says "Since then, I have never believed a result without a careful, structured proof". She seems to be saying that there are a lot of true conjectures that are supported by proofs that contain "serious mistakes". So, a proof such as the one that I wrote is worth very little. If one is going to write a proof they must get serious, learn how to write structured proofs and take the time to do a thorough job.
Is this correct? Is there a computerized (affordable) assistant available to help me?
In the following “s” is short for “start”, “m” is short for “middle” and “f” is short for “finish”:
On the first call to BinarySearch f-s is the length of the dictionary less one. On every recursive call to BinarySearch (calls after the first), f-s is less than it was in the previous (higher level) call. This is because s <= m <= f and either the value of s is replaced by m+1 or the value of f is replaced by m-1. Termination is certain because either the dictionary entry is found or f-s becomes zero and BinarySearch ends with the dictionary entry not found.
Is that a proof?
Can you recommend a reference on how to prove stuff?
I thought that I had found a case that didn't work and I was far too intrigued by that possibility.
I or someone smarter than me could perform mathematical induction on f-s and the Maple procedure could still have a bug in it. Isn’t that something that I should be concerned about?
Robert Israel,
Thank you. It's always a pleasure to read what you type.
''To me (as a mathematician) "demonstrate" means "prove". Moreover "always" means "always"...''
You live a hard life [but the difficulties are worth it and so it’s a good life?].
As you typed: “…it’s really good to have a proof.” and “Maple is not much help in this,…” but this is an exercise in an introductory book about Maple...
What should be proved? Although, I can’t find any, there must be many proofs of the binary search. It seems more important to prove that this particular implementation of a binary search always terminates with the correct answer.
“Software testing alone cannot prove that a system does not contain any defects. Neither can it prove that it does have a certain property. Only the process of formal verification can prove that a system does not have a certain defect or does have a certain property. It is impossible to prove or test that a system has "no defect" since it is impossible to formally specify what "no defect" means. All that can be done is prove that a system does not have any of the defects that can be thought of, and has all of the properties that together make it functional and useful.”
http://en.wikipedia.org/wiki/Formal_verification
On the other hand:
“Binary search is one of the trickiest "simple" algorithms to program correctly. A study has shown that an astounding 91.379 percent of professional programmers fail to code a binary search correctly after a whole hour of working on it, and another study shows that accurate code for it is only found in five out of twenty textbooks. (Kruse, 1999) Given this insight, it is important to remember that the best way to verify the correctness of a binary search algorithm is to thoroughly test it on a computer. It is difficult to visually analyze the code without making a mistake.”
http://en.wikipedia.org/wiki/Binary_search
Please provide additional direction.
Thank you.
It's hard for me to tell what's going on even with the printlevel set to 1000. Apparently I did see the values 3 and 6 evaluated.
It has been said about lisp practitioners, probably by C or assembly programmers, that they “know the value of everything and the cost of nothing.” Computers are so fast and numerous these days that no one would say that anymore.
In the following worksheet printlevel:=1000: shows that in the last expression 3 and 6 are computed. So in that case, which is what curry(map, (`@`(`+`, op))/nops) yields, the division is not distributed.
View 4937_Chapter6Exercise5a.mw on MapleNet or
Download 4937_Chapter6Exercise5a.mwView file details
Your understanding of Maple is so much better than mine that you will never and can never know how much that helped. Thank you all, Robert Israel in particular.
Although the magic is no longer so black, this:
Means3 := () -> map((`+` @ op)/nops, args);
still seems miraculous because the function, (`+`@op)/nops, needs and gets the elements of args, the lists not the list of lists, in two places.
The map help page says the equivalent of:
"map(fcn, expr) executes fcn(elem) for each element ..."
if doesn't say:
"map(fcn, expr) executes fcn(elem, elem) for each element ..."
Also, in the case of the test data that I used ([[1,2],[1,2,3]]) is (1+2)/2 computed or is 1/2 + 2/2 computed? From the output that results from printlevel:=1000: I think that (1+2)/2 is computed. So, is division being distributed over the elements of the list?
I've been looking at the subject line for a while now.
In that line nops causes the sums to be divided by the number of terms in each sum to produce the desired means. I would like to know if there is a way to divide the sums by the number of sums, lists or columns. The input is a list of lists. Is there a way to divide the sums by the number of lists rather than by the number of terms in each sum?
I happy that the subject line doesn't work this way but, I don't understand why it doesn't. Does Maple know that that would be silly and means are obviously desired? Naa...
No one would ever want to do this except for someone who wanted to be able to get Maple to do whatever he or she wanted no mater how whimsical.
posint does just what I want.
i::And(integer, positive) looks like it could be very useful in cases where the equivalent (posint) doesn't exist. i.e.: posreal::And(numeric,positive)
Does assume() have an application in this area? I've tried to use assume() several times and it didn't make-it-happen for me.
When should _passed (args) be used rather than something like the passed that I used?
Can _passed be typed? Should it be typed? Would typing _passed be a good thing?
Thank you, thank you, thank you, ...
Cheating, what is cheating?
I assume that CSisms refers to the C programming language and not Caesars, the emperors of Rome. CSisms is a cool word. Why isn't the word "Cisms"?
http://en.wikipedia.org/wiki/C_(programming_language)
I hope to 'get' Maple one day.
This: "Means3 := curry(map,`+`@op/nops);" is magic. I have no idea how it works. Finding out will entertain me for some time. I've read the "curry" help page once but once isn't enough. I'll have to read it a few more times. That Morse Code stuff at the end of the "curry" help page looks cool too.
I wrote "local i::integer,positive,"... I don't think that that does what I wanted. How do I declare a local variable to be a positive integer?
Is declaring a local integer variable "i" a CSism?
"The point is that arg(z) = Im(ln(z)) and the derivative of ln(f(t)) is f'(t)/f(t)."
That makes it so clear! Darwin was so right when he said:
"I have deeply regretted that I did not proceed far enough at least to understand something of the great leading principles of mathematics, for men [and women] thus endowed seem to have an extra sense"
Is this a Maple enabled (golden road) to argument(z)? Before Maple the DE that results would scare a lot of folks off of this path to argument(z).
"The point is that arg(z) = Im(ln(z)) and the derivative of ln(f(t)) is f'(t)/f(t)."
That makes it so clear! Darwin was so right when he said:
"I have deeply regretted that I did not proceed far enough at least to understand something of the great leading principles of mathematics, for men [and women] thus endowed seem to have an extra sense"
Is this a Maple enabled (golden road) to argument(z)? Before Maple the DE that results would scare a lot of folks off of this path to argument(z).
Robert Israel:
It came to me in a dream last night:
Im((diff(r(x)*exp(I*theta(x)), x))/(r(x)*exp(I*theta(x)))) = diff(theta(x), x);
<\pre>
At least it was in my head when I woke up this morning.
Do you find applications for this gem frequently?
