Main Page | Report this Page
 
   
Science Forum Index  »  Logic Forum  »  Existence of proof verifiers: A comedy
Page 1 of 1    
Author Message
Jan Burse
Posted: Wed Apr 30, 2008 12:44 pm
Guest
This reminds me of the battle between CBL and Meghill:

Taken from: Constructive Methods in Computing Science,
Manfred Broy ed., Series F, Computer and System Sciences,
Vol.55, Springer-Verlag, 1988

Remember romans counted like this:
I, II, III, IV, V, VI, VII, VIII, IX, X, etc..
Remember hindu system is close to our decimal system including zero.

Dijkstra: I have been most impressed by the elegance and
simplicity of calculations in the Roman System:
Simple concatenation for addition and pairing
for subtraction. They have avoided needless
complexities such as multiplication and division.
The Hindu System forces me to carry around many large
tables in one small head.
Hoare: One can clearly see the large number of algebraic
identities in the Roman System. Associativity of
concatenation immediately tells us that addition
is associative. Hindu System offers a poor basis
for such deductions.
Backhouse: I was using the Hindu System. Since the position
of each symbol in a number determines its value, I
had to carry around too much context. That is
why I switched to Roman numerals, and I have never
been happier.
Bird: The Roman System allows you to abstract away from the
actual numbers and study the operations, concatenation,
for instance. The Hindu System is operational; it gives
you an imperative procedure for addition and hence,
forces you down to the level of numbers.
Broy: The Hindu System forces you to add in a deterministic
fashion. The Roman System is clearly superior because
it avoids overspecification.
Constable: The Roman System is object-oriented. A model for a
Roman number is immediate—a flock of sheep, for instance.
The meaning function maps each vertical bar to a sheep,
and consistency of the whole system is immediately obvious.
Lampson: The Roman System maintains the relationship with
reality all through a computation. When you have counted
three bars, you have counted three sheep,
for instance. In the Hindu System what do the figures
represent halfway through an addition; what is the
physical meaning of a carry? It is a symbolic jungle
without any intuitive appeal. Then they have the most
unnatural way of working from right to left. Their system
is too complex for average people.
Moore: The Roman System is most attractive from a theorem-proving
viewpoint. It is faster to prove than compute.
van de Snepscheut: I see rich possibilities for symbol manipulation
in the Roman System. By inventing new symbols, such as “V”
and “X”, they can replace groups of other symbols. The
Hindu System offers no such symbol manipulation possibilities
because it lacks the flexibility of admitting new digits.
Also, using a symbol to represent nothing—they call it
a “zero”—is a poor design decision.
Hindu: Let us talk about multiplication. Consider the following
arithmetic problem dealing with consumptions of Christians
by lions. Suppose that a lion can consume two Christians
every hour. How do you compute the number of Christians
that must be supplied to keep three lions happy for two
hours?
Roman: That is simple. I will run a live simulation. (pause)
You have seen that we can conceptualize, animate and
communicate. We are now transferring this technology to the
city of Carthage. We are planning to destroy them shortly,
though.
Hindu: (Aside) Your number system will destroy them first.
(Pause) Let me make a last effort. How can you divide
in your notation?
Roman: People in the real world don’t divide.

http://www.cs.utexas.edu/users/misra/Speeches.dir/Marktoberdorf.88.speech.pdf
MoeBlee
Posted: Wed Apr 30, 2008 12:44 pm
Guest
On Apr 30, 10:44 am, Jan Burse <janbu...@fastmail.fm> wrote:
Quote:
This reminds me of the battle between CBL and Meghill

There is no battle between Charlie-Boo and Norm Megill. The former is
a loudmouth ignoramus continually spewing garbage while the latter is
just fending off certain of the spewage.

MoeBlee
MoeBlee
Posted: Wed Apr 30, 2008 12:44 pm
Guest
On Apr 30, 12:51 pm, Jan Burse <janbu...@fastmail.fm> wrote:

Quote:
fending off - like in defending?

No, like in dodging mud splattered from the gutter.

MoeBlee
Marshall
Posted: Wed Apr 30, 2008 12:44 pm
Guest
On Apr 30, 10:44 am, Jan Burse <janbu...@fastmail.fm> wrote:
Quote:
This reminds me of the battle between CBL and Meghill:
[...]
Backhouse: I was using the Hindu System.

(Probably the author meant Jim Backus?)


That was pretty funny.

Some time ago in comp.databases.theory I parodied
a blog post entitled "Is Codd Dead?", Codd being Ted Codd,
the father of modern data management techniques.
The blogger was no fan of the relational algebra, and
advocated a return to pre-theoretic approaches to
data management.

My post was titled:

Is AbÅ« Ê¿Abd AllÄh Muḥammad ibn MÅ«sÄ al-KhwÄrizmÄ« Dead?

and took the position that our decimal number system
was taught uncritically to unthinking students, even though
it had only reached its position due to a firestorm of marketing
hype backed by Big Math. Of course the solution to this
problem was "RN."

http://groups.google.com/group/comp.databases.theory/browse_frm/thread/ed3649a48bb2ab61/e7f14df018ec6a32

Possibly slightly amusing if your the sort of person who
dislikes XML.


Marshall
Jan Burse
Posted: Wed Apr 30, 2008 2:51 pm
Guest
MoeBlee schrieb:
Quote:
On Apr 30, 10:44 am, Jan Burse <janbu...@fastmail.fm> wrote:
This reminds me of the battle between CBL and Meghill

There is no battle between Charlie-Boo and Norm Megill. The former is
a loudmouth ignoramus continually spewing garbage while the latter is
just fending off certain of the spewage.

MoeBlee

fending off - like in defending?

Sounds like a kind of battle to me...
herbzet
Posted: Wed Apr 30, 2008 3:03 pm
Guest
Jan Burse wrote:
Quote:

This reminds me of the battle between CBL and Meghill:

Taken from: Constructive Methods in Computing Science,
Manfred Broy ed., Series F, Computer and System Sciences,
Vol.55, Springer-Verlag, 1988

Remember romans counted like this:
I, II, III, IV, V, VI, VII, VIII, IX, X, etc..

An early version of Roman numerals had four as IIII, nine
as VIIII, forty as XXXX etc. In this version any permutation
of the numerals is equivalent, e.g. MMLXXVIII = IXVMXIILM.

Addition and subtraction are, indeed, especially easy in this system.

Quote:
Remember hindu system is close to our decimal system including zero.

Dijkstra: I have been most impressed by the elegance and
simplicity of calculations in the Roman System:
Simple concatenation for addition and pairing
for subtraction. They have avoided needless
complexities such as multiplication and division.
The Hindu System forces me to carry around many large
tables in one small head.
Hoare: One can clearly see the large number of algebraic
identities in the Roman System. Associativity of
concatenation immediately tells us that addition
is associative. Hindu System offers a poor basis
for such deductions.
Backhouse: I was using the Hindu System. Since the position
of each symbol in a number determines its value, I
had to carry around too much context. That is
why I switched to Roman numerals, and I have never
been happier.
Bird: The Roman System allows you to abstract away from the
actual numbers and study the operations, concatenation,
for instance. The Hindu System is operational; it gives
you an imperative procedure for addition and hence,
forces you down to the level of numbers.
Broy: The Hindu System forces you to add in a deterministic
fashion. The Roman System is clearly superior because
it avoids overspecification.
Constable: The Roman System is object-oriented. A model for a
Roman number is immediate—a flock of sheep, for instance.
The meaning function maps each vertical bar to a sheep,
and consistency of the whole system is immediately obvious.
Lampson: The Roman System maintains the relationship with
reality all through a computation. When you have counted
three bars, you have counted three sheep,
for instance. In the Hindu System what do the figures
represent halfway through an addition; what is the
physical meaning of a carry? It is a symbolic jungle
without any intuitive appeal. Then they have the most
unnatural way of working from right to left. Their system
is too complex for average people.
Moore: The Roman System is most attractive from a theorem-proving
viewpoint. It is faster to prove than compute.
van de Snepscheut: I see rich possibilities for symbol manipulation
in the Roman System. By inventing new symbols, such as “V”
and “X”, they can replace groups of other symbols. The
Hindu System offers no such symbol manipulation possibilities
because it lacks the flexibility of admitting new digits.
Also, using a symbol to represent nothing—they call it
a “zero”—is a poor design decision.
Hindu: Let us talk about multiplication. Consider the following
arithmetic problem dealing with consumptions of Christians
by lions. Suppose that a lion can consume two Christians
every hour. How do you compute the number of Christians
that must be supplied to keep three lions happy for two
hours?
Roman: That is simple. I will run a live simulation. (pause)
You have seen that we can conceptualize, animate and
communicate. We are now transferring this technology to the
city of Carthage. We are planning to destroy them shortly,
though.
Hindu: (Aside) Your number system will destroy them first.
(Pause) Let me make a last effort. How can you divide
in your notation?
Roman: People in the real world don’t divide.

http://www.cs.utexas.edu/users/misra/Speeches.dir/Marktoberdorf.88.speech.pdf
Jan Burse
Posted: Wed Apr 30, 2008 3:20 pm
Guest
herbzet schrieb:
Quote:
An early version of Roman numerals had four as IIII, nine
as VIIII, forty as XXXX etc. In this version any permutation
of the numerals is equivalent, e.g. MMLXXVIII = IXVMXIILM.

Cool

And rewriting rules like:

VI --> IV
IIIII --> V

So that:

IIIVIII = IVV

You know, after adding IIIV and III.
herbzet
Posted: Wed Apr 30, 2008 3:24 pm
Guest
Jan Burse wrote:
Quote:
herbzet schrieb:

An early version of Roman numerals had four as IIII, nine
as VIIII, forty as XXXX etc. In this version any permutation
of the numerals is equivalent, e.g. MMLXXVIII = IXVMXIILM.

Cool

And rewriting rules like:

VI --> IV
IIIII --> V

So that:

IIIVIII = IVV

You know, after adding IIIV and III.

Right! It's really a much more elegant system.

--
hz
Jan Burse
Posted: Wed Apr 30, 2008 3:29 pm
Guest
Jan Burse schrieb:
Quote:
herbzet schrieb:
An early version of Roman numerals had four as IIII, nine
as VIIII, forty as XXXX etc. In this version any permutation
of the numerals is equivalent, e.g. MMLXXVIII = IXVMXIILM.

Cool

And rewriting rules like:

VI --> IV
IIIII --> V

So that:

IIIVIII = IVV

You know, after adding IIIV and III.

Well the amputated roman can then be called "peano".
You know that roman that only works with I.
herbzet
Posted: Wed Apr 30, 2008 6:20 pm
Guest
Marshall wrote:
Quote:

On Apr 30, 10:44 am, Jan Burse <janbu...@fastmail.fm> wrote:
This reminds me of the battle between CBL and Meghill:
[...]
Backhouse: I was using the Hindu System.

(Probably the author meant Jim Backus?)

That was pretty funny.

Some time ago in comp.databases.theory I parodied
a blog post entitled "Is Codd Dead?", Codd being Ted Codd,
the father of modern data management techniques.
The blogger was no fan of the relational algebra, and
advocated a return to pre-theoretic approaches to
data management.

My post was titled:

Is AbÅ« Ê¿Abd AllÄh Muḥammad ibn MÅ«sÄ al-KhwÄrizmÄ« Dead?

and took the position that our decimal number system
was taught uncritically to unthinking students, even though
it had only reached its position due to a firestorm of marketing
hype backed by Big Math. Of course the solution to this
problem was "RN."

http://groups.google.com/group/comp.databases.theory/browse_frm/thread/ed3649a48bb2ab61/e7f14df018ec6a32

Possibly slightly amusing if your the sort of person who
dislikes XML.

The hyperlink doesn't work for me (google says "no subject").

You might also want to check out http://tinyurl.com . Tinyurl is your
friend.

--
hz
Jan Burse
Posted: Thu May 01, 2008 3:34 am
Guest
Jan Burse schrieb:
Quote:
This reminds me of the battle between CBL and Meghill:

Taken from: Constructive Methods in Computing Science,
Manfred Broy ed., Series F, Computer and System Sciences,
Vol.55, Springer-Verlag, 1988
http://www.cs.utexas.edu/users/misra/Speeches.dir/Marktoberdorf.88.speech.pdf


Check this out:

Gregor Reisch: Margarita Philosophica, 1508
http://en.wikipedia.org/wiki/Image:Gregor_Reisch%2C_Margarita_Philosophica%2C_1508_%281230x1615%29.png

I think she is looking to the left.
Jan Burse
Posted: Thu May 01, 2008 3:36 am
Guest
Jan Burse schrieb:
Quote:
Check this out:

Gregor Reisch: Margarita Philosophica, 1508
http://en.wikipedia.org/wiki/Image:Gregor_Reisch%2C_Margarita_Philosophica%2C_1508_%281230x1615%29.png


I think she is looking to the left.

Leonardo Fibonacci brought this system to Europe, translating the Arabic
text into Latin, calling it Liber Abaci. The numeral system came to be
called "Arabic" by the Europeans. It was used in European mathematics
from the 12th century, and entered common use from the 15th century.
Robert Chester translated the Latin into English.
Marshall
Posted: Thu May 01, 2008 5:04 am
Guest
On Apr 30, 4:20 pm, herbzet <herb...@gmail.com> wrote:
Quote:
Marshall wrote:

On Apr 30, 10:44 am, Jan Burse <janbu...@fastmail.fm> wrote:
This reminds me of the battle between CBL and Meghill:
[...]
Backhouse: I was using the Hindu System.

(Probably the author meant Jim Backus?)

That was pretty funny.

Some time ago in comp.databases.theory I parodied
a blog post entitled "Is Codd Dead?", Codd being Ted Codd,
the father of modern data management techniques.
The blogger was no fan of the relational algebra, and
advocated a return to pre-theoretic approaches to
data management.

My post was titled:

Is AbÅ« Ê¿Abd AllÄh Muḥammad ibn MÅ«sÄ al-KhwÄrizmÄ« Dead?

and took the position that our decimal number system
was taught uncritically to unthinking students, even though
it had only reached its position due to a firestorm of marketing
hype backed by Big Math. Of course the solution to this
problem was "RN."

http://groups.google.com/group/comp.databases.theory/browse_frm/threa...

Possibly slightly amusing if your the sort of person who
dislikes XML.

The hyperlink doesn't work for me (google says "no subject").

Weird. It works for me.


Quote:
You might also want to check outhttp://tinyurl.com. Tinyurl is your
friend.

Try some of these:

http://groups.google.com/group/comp.databases.theory/msg/e7f14df018ec6a32

http://tinyurl.com/4nrw5l

http://groups.google.com/group/comp.databases.theory/browse_frm/thread/ed3649a48bb2ab61/e7f14df018ec6a32?#e7f14df018ec6a32


I suppose I could consider that tinyurl is my friend, but I think
what I feel much more strongly is that web developers who
produce ginormous urls are my enemies.


Marshall
herbzet
Posted: Thu May 01, 2008 8:55 pm
Guest
Marshall wrote:


This works.

Quote:
http://tinyurl.com/4nrw5l

This works.

Quote:
http://groups.google.com/group/comp.databases.theory/browse_frm/thread/ed3649a48bb2ab61/e7f14df018ec6a32?#e7f14df018ec6a32

This doesn't work for me.

Quote:
I suppose I could consider that tinyurl is my friend, but I think
what I feel much more strongly is that web developers who
produce ginormous urls are my enemies.

Tinyurl like you. Tinyurl like any you.

--
hz
 
Page 1 of 1       All times are GMT - 5 Hours
The time now is Thu Jul 24, 2008 10:32 pm