I believe there is [or can be proved to NOT be] 'simple provable
conclusions of certain algorithms' which can be arrived at by
automating the theory instead of messing with empirical
program & test methods.
A stupid analogy is the following:
If we have a board with holes to contain balls; where
each hole contains either a red or black ball,
and no holes are empty: the start state - data structure.
And we do the following algorithm:
1. move all the balls to a bucketA.
2. if there are more red than black balls then
move all bals to bucket B.
3. separate balls: red to bucket C & black to bucket D.
4. refill the board's holes from balls of bucket's C & D.
We know that after this foolishness [equivalent to programming
and testing - empirical working] that the board holes will be
exactly [re] filled. A possible proof being that 'none of the
balls left the environment during the algorithm execution, so ...'.
Now if we wanted to know if the board would be still exactly
filled after a complex sequence if steps, perhaps one summarising
test would be to know if the balls in the 'environment' had been
removed or added to....?
------------
We know that algorithms can-be/are transformed to different
formats/representations. Eg. for human consumption or machine
consumption. I suspect there are formats/representations which
are most suitable for proof of 'correctness' or of other attributes;
perhaps eg. 'halting'...etc.
And more importantly for automated proof of these attributes.
I had/have a book dating back decades [can anybody recall the title?]
where lisp programs analyse the structure of lisp programs.
------------
http://mitpress.mit.edu/sicp/full-text/book/book-Z-H-9.html
reads:
"....The language was conceived by John McCarthy and is based
on his paper ``Recursive Functions of Symbolic Expressions and Their
Computation by Machine'' (McCarthy 1960)."
What higher principle was he investigating ?
"Despite its inception as a mathematical formalism, Lisp is a practical
programming language. "
Yes, since McCarthy contributed lisp to society, it's been used to
scratch around: empirically do stuff, the same way as the first machine
code was used for humans to reiterate: think, code, test, modify..
What happened to the original mathematical formalism, that
STARTED McCarthy ? What was this mathematical formalism about ?
It seems that what I'm looking for, is related to what McCarthy started
with ? It's as if a sophisticated gadget is been used as a hammer.
Thanks for any feedback,
== Chris Glur.
On Tue, 16 Jan 2007 04:51:49 -0600, no-top-post wrote:
> I believe there is [or can be proved to NOT be] 'simple provable
> conclusions of certain algorithms' which can be arrived at by
> automating the theory instead of messing with empirical
> program & test methods.
>
[...]
> We know that algorithms can-be/are transformed to different
> formats/representations. Eg. for human consumption or machine
> consumption. I suspect there are formats/representations which
> are most suitable for proof of 'correctness' or of other attributes;
> perhaps eg. 'halting'...etc.
> And more importantly for automated proof of these attributes.
>
See Neil Jones's Computability and Complexity (which covers those
theories using denotational semantics and a little Scheme-like language)
and http://www.apronus.com/math/goedel.htm (or any other book/article on
Goedel's incompleteness theorems) for why you will never be able to
"automate the theory."
Unless you mean theory in the formal sense, in which case you want to
look at Simon Peyton Jones's Implementing Functional Languages or
Christian Queinnec's Lisp in Small Pieces. You still won't be able to
solve the halting problem.
Haskell and the ML family lend themselves to correctness proves, if you
have a formal specification. It's even been argued that Haskell is a
better formal specification language than formal specification languages.
I think that doing that kind of thing would be difficult with Common Lisp
because the language specification is so huge and sometimes vague, but I
guess you could do it with Scheme.
If you don't have a formal specification, you can't meaningfully prove
your program correct.
On Jan 16, 2:51 am, no-top-post wrote:
> Yes, since McCarthy contributed lisp to society, it's been used to
> scratch around: empirically do stuff, the same way as the first machine
> code was used for humans to reiterate: think, code, test, modify..
So which of these steps are you proposing to remove? Not the first, I
hope.
> What happened to the original mathematical formalism, that
> STARTED McCarthy ? What was this mathematical formalism about ?
What process will discover the mathematical formalism, if not creative
thinking, experimentation, hypotheses forming and validation, etc?
No matter how many meta-levels you escape through, at the top you are
always left with scratching around. For instance, in programming, you
can scratch around with the code itself, or you can scratch around with
the code that writes the code, or with the code that writes the code
that writes the code, ...
no-top-post writes:
> http://mitpress.mit.edu/sicp/full-text/book/book-Z-H-9.html
> reads:
> "....The language was conceived by John McCarthy and is based
> on his paper ``Recursive Functions of Symbolic Expressions and Their
> Computation by Machine'' (McCarthy 1960)."
>
> What higher principle was he investigating ?
>
> "Despite its inception as a mathematical formalism, Lisp is a practical
> programming language. "
>
> Yes, since McCarthy contributed lisp to society, it's been used to
> scratch around: empirically do stuff, the same way as the first machine
> code was used for humans to reiterate: think, code, test, modify..
>
> What happened to the original mathematical formalism, that
> STARTED McCarthy ? What was this mathematical formalism about ?
Well, what happenned to this mathematical formalism is what happens to
any mathematical formalism: it gets written into a couple of
papers. (See urls below). It is about computable functions.
> It seems that what I'm looking for, is related to what McCarthy started
> with ?
You can find everything you need either on Pr John McCarthy's web
site, or on CSAIL archives:
http://www-formal.stanford.edu/jmc/
http://www-formal.stanford.edu/jmc/basis.html
http://www-formal.stanford.edu/jmc/towards.html
http://www.ai.mit.edu/research/publications/browse/0000browse.shtml
Be sure to read:
ftp://publications.ai.mit.edu/ai-publications/pdf/AIM-008.pdf
http://www.informatimago.com/develop/lisp/small-cl-pgms/aim-8/aim-8.html
And you may have fun with:
http://www.informatimago.com/develop/lisp/small-cl-pgms/aim-8/
> It's as if a sophisticated gadget is been used as a hammer.
Well, perhaps one could say that of any mathematical theory applied to
any domain. ;-)
--
__Pascal Bourguignon__ http://www.informatimago.com/
PLEASE NOTE: Some quantum physics theories suggest that when the
consumer is not directly observing this product, it may cease to
exist or will exist only in a vague and undetermined state.
(message (Hello 'no-top-post)
(you :wrote :on '(Tue, 16 Jan 2007 04:51:49 -0600))
(
ntp> I believe there is [or can be proved to NOT be] 'simple provable
ntp> conclusions of certain algorithms' which can be arrived at by
ntp> automating the theory instead of messing with empirical
ntp> program & test methods.
take a look at ACL2 (A Computational Logic Applicative Common Lisp)
http://www.cs.utexas.edu/users/moore/acl2/
--
ACL2 is both a programming language in which you can model systems and a
tool to help you prove properties of those models.
--
AMD used ACL2 to verify the elementary floating-point operations for the
recently released Athlon.
--
)
(With-best-regards '(Alex Mizrahi) :aka 'killer_storm)
"People who lust for the Feel of keys on their fingertips (c) Inity")
"Alex Mizrahi" <········@users.sourceforge.net> writes:
> AMD used ACL2 to verify the elementary floating-point operations for the
> recently released Athlon.
I think it was used for to prove the floating point division in the
old Athlon processor, since this paper is more than 10 years old:
http://www.cs.utexas.edu/users/moore/publications/bkm96.pdf
Motorola used it to prove some microcode for FFT in their DSP
processor. Amazing tool, and even open-source. I'm hoping to get some
time to learn how to use it. Could save me a lot of simulation time...
Petter
--
A: Because it messes up the order in which people normally read text.
Q: Why is top-posting such a bad thing?
A: Top-posting.
Q: What is the most annoying thing on usenet and in e-mail?
no-top-post wrote:
> I had/have a book dating back decades [can anybody recall the title?]
> where lisp programs analyse the structure of lisp programs.
> ------------
> http://mitpress.mit.edu/sicp/full-text/book/book-Z-H-9.html
> reads:
> "....The language was conceived by John McCarthy and is based
> on his paper ``Recursive Functions of Symbolic Expressions and Their
> Computation by Machine'' (McCarthy 1960)."
>
> What higher principle was he investigating ?
>
> "Despite its inception as a mathematical formalism, Lisp is a practical
> programming language. "
>
> Yes, since McCarthy contributed lisp to society, it's been used to
> scratch around: empirically do stuff, the same way as the first machine
> code was used for humans to reiterate: think, code, test, modify..
>
> What happened to the original mathematical formalism, that
> STARTED McCarthy ? What was this mathematical formalism about ?
>
> It seems that what I'm looking for, is related to what McCarthy started
> with ? It's as if a sophisticated gadget is been used as a hammer.
See http://www-formal.stanford.edu/jmc/history/lisp/lisp.html and also
http://www8.informatik.uni-erlangen.de/html/lisp/histlit1.html and
http://www8.informatik.uni-erlangen.de/html/lisp/mcc91.html
As a follow up, http://www.dreamsongs.com/Files/Hopl2.pdf is also very
interesting.
Pascal
--
My website: http://p-cos.net
Common Lisp Document Repository: http://cdr.eurolisp.org
Closer to MOP & ContextL: http://common-lisp.net/project/closer/