Re: Provability

On Oct 24, 9:28 pm, Marshall <marshall.spi...@xxxxxxxxx> wrote:
On Oct 24, 8:58 pm, Michael Press <rub...@xxxxxxxxxxx> wrote:



In article
<1193251799.743613.21...@xxxxxxxxxxxxxxxxxxxxxxxxxxxx>,

Marshall <marshall.spi...@xxxxxxxxx> wrote:
On Oct 24, 10:57 am, Michael Press <rub...@xxxxxxxxxxx> wrote:

An algorithm is a procedure that takes input and
terminates with a well-defined and asserted result.
That it does terminate with the asserted result must be
proven. Until we accept the proof, it is not an
algorithm. The notion of right answer is not part of
the definition of algorithm.

That definition is extremely narrow, and does not correspond
to any usage of the term that I can recall in many years
of being a programmer.

I'm not even sure I'd buy in to the "well-defined" part.
Having a "probabilistic algorithm" doesn't sound like
a contradiction in terms. In fact, Googling it just
now it gets a lot of hits. Neither does "proven correct,
proven terminating algorithm" sound redundant.

I fail to see the utility in defining an algorithm
to be no more than a partial recursive function.
A theorem is not a theorem until it is proven.
What is your standard for implementing a method
into production code?

To be fair, there is a world of difference between
the standards of ordinary commercial software and
the standards of rigor for a mathematical proof.
In general, the former is driven by marketplace
concerns, meaning whatever can be banged out
most quickly that works a majority of the time.
I think it was Scott McNealy that said that most
software has the shelf life of a banana. Whereas
math is for the ages.

I vaguely suppose that what is CS is called an
algorithm is more like what in math would be
called a formula.

i think the part of cs you refer
is the engineer's cs

the infrastructurists
who use it loosely
because such distinctions do not help their daily work

theoretical foundations of cs
often take the approach
as indicated michael

this is inherently a verificationist
or operationalist
approach to algorithmic properties
and mathematical properties in general

constructivists do not assign truth
until a sentence is proven

because of the curry-howard isomorphism
there is an isomorphism
between sentences and types
so this gives a type theory

this guarantees
functions definable in this type theory
are all computable

developing this as a foundation for computer science
has evolved considerably over the years
from rough BHK (brouwer-heyting-kolmogorov) types
to martin-lof types
to the more reflexive one's of artemov

constructivists in this tradition
do not derive ullrich's dichotomy

-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
galathaea: prankster, fablist, magician, liar

.

Relevant Pages

  • Re: Provability
    ... terminates with a well-defined and asserted result. ... the definition of algorithm. ... computer science does consider a partial recursive function is to be "an ... situations exist is most of classical mathematics: ...
    (sci.math)
  • Re: Provability
    ... terminates with a well-defined and asserted result. ... the definition of algorithm. ... the standards of rigor for a mathematical proof. ... math is for the ages. ...
    (sci.math)
  • Re: Provability
    ... terminates with a well-defined and asserted result. ... the definition of algorithm. ... fact is that standard terminology in mathematics and theoretical ... situations exist is most of classical mathematics: ...
    (sci.math)
  • Re: Provability
    ... terminates with a well-defined and asserted result. ... the definition of algorithm. ... the standards of rigor for a mathematical proof. ... math is for the ages. ...
    (sci.math)
  • Re: How to encrypt a string with des in pure C?
    ... I'm sure you can find plenty of DES encryption programs by ... There are certainly lots of places to find the algorithm as well, ... Bureau of Standards which originally published it. ... after being superseded by AES (the Advanced ...
    (comp.lang.c)