Ada vs Ruby

[Arved Sandstrom]

Oh definitely. Testing that code performs correctly is essential to
any embedded development process, as is validating that the code
written solves the correct problem. The latter is by far the more
difficult though.

[ SNIP ]

On the latter note - validation as opposed to verification - it's important
to add that strictly speaking requirements should address the user's real
needs, not what the user thinks they are. Raise your hand if you've ever
worked on a project where you got some (ostensibly) fairly clear
requirements from a client, built an application that validates, presented
it to the client, and found out they really wanted something else.

It's why good business analysts should be worth more than architects or
coders. For the record, I'm not a BA - I just recognize their value.

AHS

 

[Robert Dober]

Any process that is algorithmic is necessarily implementable as a Turing
machine so I'd argue that the very act of coding the system with a proces= s
defines TNT(1) whilst the target system itself becomes TNT. Therefore unt= il
the system runs in situ and responds to its environment one cannot make a= ny
firm statements regarding when the system will halt. And if you can't tel= l
when an autopilot will halt, you have the potential for all kinds of
mayhem...

Of course this is a terrible abuse of Church-Turing, but it seems to fit
the real world pretty well.

Oh I was not clear enough I am afraid. I challenge that you can prove
that one cannot prove if your Aircraft control system can halt or not.
I even believe that in theory it can be proven. And if you are not
talking about theory than I agree with you
it is not a fair statement.
This is not nitpicking because I think that serious work is still done
in automatic proving of theorems and the day might come where even
complex systems can be proven to be correct.
G=F6del and Turing only show that *complete* systems cannot be correct,
they say nothing about *complex*.

Cheers
Robert

Ellie
Who wonders what the hell this thread will look like in Google searches.



Eleanor McHugh
Games With Brains
http://slides.games-with-brains.net

--=20
http://ruby-smalltalk.blogspot.com/

 

[Phillip Gawlowski]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Eleanor McHugh wrote:
|
| Much kudos to your friend. Twelve years ago I did the same thing in VB
| for helicopters and whilst it was pushing the hardware at that time, it
| was still usable. Of course these days most mobile phones have more
| computational grunt and memory than that

But the mobile phones aren't necessarily as reliable as, say, the
hardware and operating system of an avionics system.

Considering that an operating system is an abstraction, and that
abstractions, more often than not, are leaky, I contend that specialized
hardware doesn't use much of an operating system, thusly eliminating a
large set of undefined (rather, unprovable as per Godel) states,
correct? Only providing the bare minimum of APIs needed for the software
on the application level to function properly, or dispersing with
operating systems entirely, working on the bare metal (I think that the
Apollo project computers functioned like that, but correct me if I'm wrong.)

In my experience, the more complex software gets, the more error-prone
it is. I notice that in my PDA, which performs rock solid, only needing
a driver upgrade for SD cards above 64 MB (well, at the time this thing
was made, cards larger than 64MB weren't widely available yet; which
shows that not all requirements can be gathered beforehand), my old
smart phone which failed on every possible situation, and all the
operating systems I've used with some depth so far.

So, isn't it part of the requirement gathering process, or the design
process, during software engineering to cut down on unnecessary
complexities and abstractions, too?

And that influences interface design for the user, too, I've noticed.
After all, the guidelines of the US Air Force for user interfaces
compose a 486 page book:

"From 1984 to 1986, the U.S. Air Force compiled existing usability
knowledge into a single, well-organized set of guidelines for its user
interface designers. I was one of several people who advised the project
(in a small way), and thus received a copy of the final 478-page book in
August 1986."

http://www.useit.com/alertbox/20050117.html

Hm, it seems to always come down to near-perfect requirements during design.

- --
Phillip Gawlowski
Twitter: twitter.com/cynicalryan

Don't stop with your first draft.
~ - The Elements of Programming Style (Kernighan & Plaugher)
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.8 (MingW32)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iEYEARECAAYFAkgHAyEACgkQbtAgaoJTgL9T/ACfbW68rjje9gJR4vKKEEjyLuem
evwAnRjmnWbJeZCO4yi5gcd3ALNv8maU
=oYsQ
-----END PGP SIGNATURE-----

 

[Eivind Eklund]

Now the Halting Problem is fascinating because it's very simple in
conception: given a program and a series of inputs (which in Godel's terms
comprises a mathematical system and a set of axioms) determine whether or
not the program will complete. Turing proved that in the general case this
problem is insoluble, and not only does this place an interesting
theoretical limitation of all software systems but it also applies to
sub-programs right the way down to the finest grain of detail. Basically
anytime a program contains a loop condition the Halting Problem will apply
to that loop.

So in essence we're left with a view of software development in which we
can never truly know if a program is correct or even if it will halt.

In general, proofs around Turing machines only applies with an
infinite length tape - in other words, about a computer with infinite
memory.

The Halting proof only proves that there exists programs that we can't
prove halting about, not that it isn't possible to prove things around
some programs.

The Goedel proof is about complete logical systems; in the case of a
computer program, we are working with a system where we have other
formalisms under it that's providing axioms that we don't prove, just
assume.

In the absence of hardware failure (something we of course can't prove
and is a problem in the real world), we can trivially prove halting
for a lot of cases. E.g, the simple program "halt" halts. halt if
true halts. halt if 1 == 1 would generally halt, assuming no
redefinition of ==. An so on.

I appreciate and respect your general contributions in this thread; I
just couldn't let this particular argument stand, as it confuse people
about what the theorems say.

Eivind.

 

[Phillip Gawlowski]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Eivind Eklund wrote:

|
| The Goedel proof is about complete logical systems; in the case of a
| computer program, we are working with a system where we have other
| formalisms under it that's providing axioms that we don't prove, just
| assume.

But a language that is Turing-complete is a complete logical system, is
it not?

Since you can express any Turing machine in a Turing-complete language,
you have to necessarily deal with Goedel's incompleteness, don't you?

And language side-effects are there, no matter what language, due to the
way it (or its compiler) are implemented.

| In the absence of hardware failure (something we of course can't prove
| and is a problem in the real world), we can trivially prove halting
| for a lot of cases. E.g, the simple program "halt" halts. halt if
| true halts. halt if 1 == 1 would generally halt, assuming no
| redefinition of ==. An so on.

There are logical proofs that P is non-P (details of which are an
exercise to the reader since I have misplaced Shaum's Outline of Logic).

That a state is provable says nothing about the *conditions* that this
proof is valid. In a complete system, any proof is valid, so that the
proof that halt == true equates to false is a side-effect under the
(in-)correct circumstances.

Now, most applications don't reach this level of complexity, but the
level of complexity is there, you usually don't have to care about it.

Conversely, if every state of a program were provable, the processes
like DO-178B wouldn't be necessary, would they?

- --
Phillip Gawlowski
Twitter: twitter.com/cynicalryan

~ Why do we drink cow's milk? Who was the first guy who first looked at
a cow and said "I think I'll drink whatever comes out of these things
when I squeeze 'em!"? -- Calvin
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.8 (MingW32)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iEYEARECAAYFAkgHJd0ACgkQbtAgaoJTgL9s4QCbBUjq4oK2p5AkQmreI4TmyzTj
DggAnA7rG8GsVcCbyvJBdM8KlHMSqE5E
=RMV1
-----END PGP SIGNATURE-----

 

[Eleanor McHugh]

Oh I was not clear enough I am afraid. I challenge that you can prove
that one cannot prove if your Aircraft control system can halt or not.
I even believe that in theory it can be proven. And if you are not
talking about theory than I agree with you
it is not a fair statement.
This is not nitpicking because I think that serious work is still done
in automatic proving of theorems and the day might come where even
complex systems can be proven to be correct.
G=F6del and Turing only show that *complete* systems cannot be = correct,
they say nothing about *complex*.

It's an interesting semantic point, in that complex is not necessarily =20=

the same as complete. But likewise a Turing machine is an ideal device =20=

which cannot exist in the real world: it requires both infinite =20
storage and infinite time so perforce there are computations which it =20=

could make that cannot be made using the means available within our =20
physical environment. However for sake of argument let's suppose that =20=

our complex system is being implemented on such an ideal device and =20
that our interest is in determining whether or not Godel =20
incompleteness is significant.

What matters is not specifically how complex the system is, in that a =20=

highly complex system from our perspective may still be composed of =20
provable states, but how many of its states are unprovable within the =20=

context of the complete system of which it forms a subset. We can =20
therefore see that the application of Godel to a complex but =20
incomplete system operating in ideal conditions would result in a =20
probabilistic incompleteness in that system that at least =20
theoretically could be measured.

However this then leads to the question of whether or not the complex =20=

system is in fact only a subset of a larger complete system, or a =20
complete system in its own right. Considering that it is itself based =20=

on a set of axioms (the requirements for the system) and therefore in =20=

that regard complete, I would argue that it was not a subset at all. =20
This appears to create a probabilistic, relativistic incompleteness =20
(which is analogous to the viewpoint that physics has reached =20
regarding our physical universe).

But even if we allow the subset to be an incomplete system we can see =20=

that increasing complexity increases the number of states in the =20
system, thus increasing the likelihood of included states being drawn =20=

from the full set of states possible in the complete system. Yet =20
again, we can see that there is a probability of included states being =20=

unprovable which beyond a certain level of complexity specific to the =20=

system would be significant in preventing a formal proof of all the =20
included states.

Given that Godel's incompleteness applies to systems as simple as =20
arithmetic, and that even simple desktop applications often contain =20
many more orders of axioms than this, the concept of formal proof =20
should always be seen in light of this probabilistic incompleteness. =20
That is not to say that attempting to prove a system is futile, but =20
merely a recognition that beyond a certain level of complexity =20
specific to a given system there will always be an element of =20
unpredictability even when environmental adjustment of the system does =20=

not apply.


Ellie

Eleanor McHugh
Games With Brains
http://slides.games-with-brains.net

 

[Eleanor McHugh]

The Halting proof only proves that there exists programs that we can't
prove halting about, not that it isn't possible to prove things around
some programs.

The Goedel proof is about complete logical systems; in the case of a
computer program, we are working with a system where we have other
formalisms under it that's providing axioms that we don't prove, just
assume.

In the absence of hardware failure (something we of course can't prove
and is a problem in the real world), we can trivially prove halting
for a lot of cases. E.g, the simple program "halt" halts. halt if
true halts. halt if 1 == 1 would generally halt, assuming no
redefinition of ==. An so on.

I appreciate and respect your general contributions in this thread; I
just couldn't let this particular argument stand, as it confuse people
about what the theorems say.

I fully agree with you that for degenerate cases the halting problem
is trivial. Unfortunately these tend to be the exceptions in real
world programs as opposed to the rule. For safety-critical systems
where unexpected halting is a run-time exception that needs to be
handled I think it is highly relevant, although it can rapidly become
a red herring if viewed out of context.


Ellie

Eleanor McHugh
Games With Brains
http://slides.games-with-brains.net

 

[Rick DeNatale]

Eleanor McHugh wrote:

| It's a lovely idea, but ponder the impact of G=F6del's Incompleteness
| Theorems or Turing's proof of the Halting Problem. In practice there a= re
| program states which can occur which cannot be identified in advance
| because they are dependent on interactions with the environment, or ar= e
| artefacts of the underlying problem space.
|
| That's why run-time error handling and fail-safe behaviour are so
| important regardless of the rigour of Q&A processes.

Sure. But to know these states, the software should be tested as
thoroughly as possible. I somehow doubt that anybody using something
mission-critical to flying or medical health wants to call the hotline
during the final approach of a plane or when a surgical robot gets
fantasies of being SkyNET.

Yes, testing, not a blind faith in whatever language is being used,
and it's compiler.

Anyway, this problem is (AFAIK, anyway), countered by using redundant
implementations of the hardware and software (well, as far as possible,
anyway), to minimize the effect of unknown states.

Of course this isn't perfect either. In fact "The Bug Heard Round the
World." which I mentioned earlier in this thread, was a failure of
redundancy.

The Shuttle has, or at least did in the early days, redundant on-board
computers which monitor the health and behavior of shuttle systems,
with voting used to find discrepencies. The hardware is/was comprised
of (3 I think) identical IBM 4Pi computers with 1 of those having a
totally independently implemented software load. When control of the
launch/mission is transferred to this system, the separate processors
run in parallel, and their outputs are compared. If they disagree,
the launch is aborted.

Of course all of this worked well during the pre-STS1 mission sims.

However, on the day of the launch, there was a clock skew between the
redundant computers, so the output from one lagged just a bit behind
the others, and the system halted the launch, unnecessarily as it
turned out, at T-3

--=20
Rick DeNatale

My blog on Ruby
http://talklikeaduck.denhaven2.com/

 

[Sean O'Halpin]

In the absence of hardware failure (something we of course can't prove
and is a problem in the real world), we can trivially prove halting
for a lot of

(trivlal

cases. E.g, the simple program "halt" halts.

If 'halt' is defined as implying that the program halts, then you're
not really proving anything here. Like saying that true implies true.
You have to take that as an axiom.

halt if
true halts. halt if 1 == 1 would generally halt, assuming no
redefinition of ==. An so on.

Once you invoke conditions, you are invoking some formal system of
axioms (like your assumption above) which you have to define. I grant
that there are very simple formal systems which are 'complete' but
they are generally not 'interesting'. If you want even simple integer
arithmetic[1], you're subject to Goedel's incompleteness theorem. And
this is just in the abstract. As soon as you put even the 'halt'
program on real hardware, all bets are off. You simply cannot prove
anything about it.

I think I'd rather fly on plane whose avionics software had been
written by someone who assumed that they had made mistakes somewhere
and that both their software and the hardware it was running on were
going to fail in some unforeseeable way (and had implemented the
appropriate safeguards both in process and error recovery) than by
someone who assumed that proving their software correct was sufficient
(though I realise that is a bit of a straw man

On a separate note, I'm continually surprised that computer 'science'
is so heavily biased to the mathematical theoretical side at the
expense of the empirical and pragmatic. Almost every single code
example in all textbooks and papers has 'error handling omitted for
clarity'! It's no wonder we have all these planes falling out of the
sky

Best regards,
Sean

[1] The number theorists are now shrieking in disbelief: Simple?
Integers? Arithmetic?!

 

[Phillip Gawlowski]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Rick DeNatale wrote:

|
| Yes, testing, not a blind faith in whatever language is being used,
| and it's compiler.

Indeed.

|> Anyway, this problem is (AFAIK, anyway), countered by using redundant
|> implementations of the hardware and software (well, as far as possible,
|> anyway), to minimize the effect of unknown states.
|
| Of course this isn't perfect either. In fact "The Bug Heard Round the
| World." which I mentioned earlier in this thread, was a failure of
| redundancy.

Perfection is an ideal, that we can only approach asymptotically, never
achieve (since we, as human beings, aren't perfect).

| Of course all of this worked well during the pre-STS1 mission sims.
|
| However, on the day of the launch, there was a clock skew between the
| redundant computers, so the output from one lagged just a bit behind
| the others, and the system halted the launch, unnecessarily as it
| turned out, at T-3
|

That is it was an unnecessary halt is probably the benefit of hindsight.
Unfortunately, I can only assume that it was so, since I cannot find a
free version of the paper you linked to earlier.

Without the benefit of hindsight, the problem of the skewed clocks could
have a much wider impact than it actually had, masking deeper problems
of the software and / or hardware used.

In such a case, we enter the area of risk management: Is it worth to
risk the whole mission on something that hasn't been done before at this
scale? While there was knowledge, at the time, of space flight thanks to
the Apollo and Mercury programs, something like the Space Shuttle was
new, and very different from the "throw away" capsules used before, with
different approaches to solve the problem of getting something into
orbit and back again, preferably all in one piece.

With the lives and money at stake with the Shuttle program, the decision
to cancel was wise, IMO, even though it turned out to be unnecessary.

One could even claim, that the systems performed as planned, and
prevented a catastrophe. Without actual empirical testing we probably
won't know for sure, and can only speculate.


In the end, though, this shows that no amount of software nor hardware
can replace judgment calls made by human beings. Technology can only
assist in making decisions. And in the cases where humans cannot make
decisions (like a Shuttle launch, where automation has to be used), a
use of technology (and not just languages and compilers and processes)
still requires humans for the get go.

I think that the movie Wargames touched on this topic in a good, and
decent, way, as well as Crimson Tide (in a not very related way, though,
but it demonstrates my point of not putting too much trust into process).

- --
Phillip Gawlowski
Twitter: twitter.com/cynicalryan

Zero G and I fell fine.
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.8 (MingW32)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iEYEARECAAYFAkgHOa8ACgkQbtAgaoJTgL/EsgCfWwHO2OoGyM+8rtM7j9MOlk1Z
48YAn3vtgcnZiMVQy02jwmqwVUNaWRPO
=ZpIR
-----END PGP SIGNATURE-----

 

[Eleanor McHugh]

My thanks to the core contributors to this fascinating thread. It's
stretched me well past my boundaries on several points, but also
clarified some key learning I've picked from my own field
(psychology & psychotherapy).

For me, the take-away here (and this is not at all news to me) is
that valid formal approaches to reliability are efficient (at least
at times) and powerful, and should definitely be used - WHEN WE HAVE
THEM. The problem is that they all stop short of the full spectrum
of reality in which our processes must survive. Thus we must leave
ultimately the comfort of deduction and dive into dragon realm of
inferential processes. Ultimately, there simply is not substitute,
or adequate simulation of, reality. Sigh.

That's the new physics for you


Ellie

Eleanor McHugh
Games With Brains
http://slides.games-with-brains.net

 

[Eivind Eklund]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Eivind Eklund wrote:

|
| The Goedel proof is about complete logical systems; in the case of a
| computer program, we are working with a system where we have other
| formalisms under it that's providing axioms that we don't prove, just
| assume.

But a language that is Turing-complete is a complete logical system, is
it not?

No. A computer language is a different kind of beast; it is not a way
to state truths about things, but a set of rules for mathematical
operations.

The relevance of the incompleteness is in the space of what programs
can exist, and what we can prove about them.

The incompleteness theorem says that there will be statements we can
make about some programs that will be true but that we will not be
able to prove true.

The halting theorem says that, specifically, that there exists
programs that will halt that we cannot prove if halts - under the
assumption of infinite memory. Under the assumption of finite memory,
we are dealing with a finite state machine, and a proof is *in theory*
possible by enumerating all all the states and which other state
follows that state.

In practice, of course, enumerating all states and the transition from
them very very quickly becomes intractable.

But as far as I can tell, incompleteness does not enter into it; only
practical feasibility.

| In the absence of hardware failure (something we of course can't prove
| and is a problem in the real world), we can trivially prove halting
| for a lot of cases. E.g, the simple program "halt" halts. halt if
| true halts. halt if 1 == 1 would generally halt, assuming no
| redefinition of ==. An so on.

There are logical proofs that P is non-P (details of which are an
exercise to the reader since I have misplaced Shaum's Outline of Logic).

That a state is provable says nothing about the *conditions* that this
proof is valid. In a complete system, any proof is valid, so that the
proof that halt == true equates to false is a side-effect under the
(in-)correct circumstances.

I have no idea what you are trying to say here. Could you reformulate?

Specifically, the following makes no sense to me:

"In a complete system, any proof is valid" (this seems to depend on
some weird definition of complete system)
"There are logical proofs that P is non-P" (this seems like either an
example of a proof with subtle errors or proof-by-contradiction
proving that a particular statement X is false; ie, if we can prove
P!=P if we assume of X, then we know that X is false.)

Now, most applications don't reach this level of complexity, but the
level of complexity is there, you usually don't have to care about it.

Conversely, if every state of a program were provable, the processes
like DO-178B wouldn't be necessary, would they?

If we knew we had a perfect spec and could practically prove all the
relevant aspects of transformation from spec to software/hardware, I
guess we would be able to just say "Prove spec to software" instead of
having any other standard. Alas, to make software and hardware is a
human endeavor - even assuming we could prove halting properties of
our real world state machines on a perfect computer, this is only a
small part of systems development.

Eivind.

 

[Eivind Eklund]

(trivlal

A surprisingly non-trivial number of cases are trivial.

If 'halt' is defined as implying that the program halts, then you're
not really proving anything here. Like saying that true implies true.
You have to take that as an axiom.

I am proving that a specific program will halt. This is a very
trivial proof; that was the intent. You could of course use an "X:
goto X" for the halt example; it does the same thing.

halt if
true halts. halt if 1 == 1 would generally halt, assuming no
redefinition of ==. An so on.

Once you invoke conditions, you are invoking some formal system of
axioms (like your assumption above) which you have to define. I grant
that there are very simple formal systems which are 'complete' but
they are generally not 'interesting'. If you want even simple integer
arithmetic[1], you're subject to Goedel's incompleteness theorem.

My claim wasn't that reasoning about the system is not subject to
Goedel's incompleteness theorem - it is. It was that the properties
that was described as being a result of Goedel's incompleteness
theorem was in fact not related to that theorem. That state proving
is impossible in the case of an infinite memory computer and often
infeasible the case of finite memory computers is, to the best of my
knowledge, a fully separate result.

Eivind.

 

[Phillip Gawlowski]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Eivind Eklund wrote:

|
| No. A computer language is a different kind of beast; it is not a way
| to state truths about things, but a set of rules for mathematical
| operations.

Which makes it a complete logical system, though not necessarily in the
sense of abstract logic.

| I have no idea what you are trying to say here. Could you reformulate?

Sure.

| Specifically, the following makes no sense to me:
|
| "In a complete system, any proof is valid" (this seems to depend on
| some weird definition of complete system)

Logically complete. That is, a system that implements abstract logic in
tis entirety. Abstract logic is at the root of Godel's incompleteness
theorem. Essentially, you either have something that can be expressed
with abstract logic. But that means, that there are things that cannot
be proven with abstract logic *within the logical system itself*.
Whence, an incompleteness theorem.

| "There are logical proofs that P is non-P" (this seems like either an
| example of a proof with subtle errors or proof-by-contradiction
| proving that a particular statement X is false; ie, if we can prove
| P!=P if we assume of X, then we know that X is false.)

1. P → Q Premise
2. P → (Q → ¬P) Premise
~ 3. P Assumption
~ 4. Q 1,3 MP
~ 5. Q → ¬P 2,3 MP
~ 6. ¬P 4,5 MP
~ 7. P & ¬P 3,6 Conj
8. ¬P

Ergo: P = not-P.

(Note: The character are UTF-8, in case you can't see them.)

The complete discussion of this proof:
http://www.iep.utm.edu/p/prop-log.htm#SH5e

Godel's first theorem:
"For any consistent formal, recursively enumerable theory that proves
basic arithmetical truths, an arithmetical statement that is true, but
not provable in the theory, can be constructed. That is, any effectively
generated theory capable of expressing elementary arithmetic cannot be
both consistent and complete."

Which drives logicians mad, since abstract logic has to be both complete
and non-contradictory.

Anyway: Computer languages that are Turing complete are both complete
and contradictory (since Godel's theorem exists), given a sufficient
algorithm. However, in >=90% of cases, this doesn't matter.

|
| If we knew we had a perfect spec and could practically prove all the
| relevant aspects of transformation from spec to software/hardware, I
| guess we would be able to just say "Prove spec to software" instead of
| having any other standard. Alas, to make software and hardware is a
| human endeavor - even assuming we could prove halting properties of
| our real world state machines on a perfect computer, this is only a
| small part of systems development.

Not really, thanks to Godel. If we can prove it, it's either incomplete
(so we don't have the perfect specs), or contradictory (so we don't have
the perfect specs either).

I hold the opinion that Godel's Incompleteness Axiom is a misnomer, and
it should be called Godel's Incompleteness Paradox.

- --
Phillip Gawlowski
Twitter: twitter.com/cynicalryan

Abstain from wine, women, and song; mostly song.
%Abstinence is as easy to me, as temperance would be difficult.
~ -- Samuel Johnson
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.8 (MingW32)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iEYEARECAAYFAkgHUnAACgkQbtAgaoJTgL/phACeMJaxYkj54DGzqYcLTQNO5a3X
WgwAnjWRPr2Og+LrUGgmELEYUFDvJkJo
=sZ1C
-----END PGP SIGNATURE-----

 

[Robert Dober]

Forgive me to add a comment as Eivind has been much clearer than me on
the description of what is the Halting Problem and Completeness. I
also think it was nice to add that your posts are very valuable
usually, I agree indeed.
But your last question can maybe be explained in simple words.

Being turing-complete means in theory that you can solve all problems
that a Turing Machine can solve (given unlimited memory) (1).
E.g.
Ruby being turing-complete means therefore that you can write a Ruby
program of which one can not determine if it will halt or not. But
chances are slim that such a Ruby program is written by chance, and
furthermore it would need infinite memory.



(1) A TM that solves a problem halts and it if halts it can only use a
finite amount of its endless tape, so theoretically Ruby
can do the same thing even if there is no limit of memory that can be
established

<snip>

Cheers
Robert

 

[Robert Dober]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Eivind Eklund wrote:

|
| No. A computer language is a different kind of beast; it is not a way
| to state truths about things, but a set of rules for mathematical
| operations.

Which makes it a complete logical system, though not necessarily in the
sense of abstract logic.


| I have no idea what you are trying to say here. Could you reformulate?

Sure.


| Specifically, the following makes no sense to me:
|
| "In a complete system, any proof is valid" (this seems to depend on
| some weird definition of complete system)

Logically complete. That is, a system that implements abstract logic in
tis entirety. Abstract logic is at the root of Godel's incompleteness
theorem. Essentially, you either have something that can be expressed
with abstract logic. But that means, that there are things that cannot
be proven with abstract logic *within the logical system itself*.
Whence, an incompleteness theorem.


| "There are logical proofs that P is non-P" (this seems like either an
| example of a proof with subtle errors or proof-by-contradiction
| proving that a particular statement X is false; ie, if we can prove
| P!=P if we assume of X, then we know that X is false.)

1. P $B"*(B Q Premise
2. P $B"*(B (Q $B"*(B $B"L(BP) Premise

De falsum quodlibet, nice try
IOW You can prove anything with a wrong premise as false -> X is
always true indeed what you proved was
false -> (P && !P)
which is correct of course.

Anyway: Computer languages that are Turing complete are both complete
and contradictory (since Godel's theorem exists), given a sufficient
algorithm. However, in >=90% of cases, this doesn't matter.


|
| If we knew we had a perfect spec and could practically prove all the
| relevant aspects of transformation from spec to software/hardware, I
| guess we would be able to just say "Prove spec to software" instead of
| having any other standard. Alas, to make software and hardware is a
| human endeavor - even assuming we could prove halting properties of
| our real world state machines on a perfect computer, this is only a
| small part of systems development.

Not really, thanks to Godel. If we can prove it, it's either incomplete
(so we don't have the perfect specs), or contradictory (so we don't have
the perfect specs either).

I hold the opinion that Godel's Incompleteness Axiom is a misnomer, and
it should be called Godel's Incompleteness Paradox.

Is it really called an axiom? An axiom cannot be proven, it should be
called a Theorem.

Cheers
Robert

 

[Phillip Gawlowski]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Robert Dober wrote:
|> 1. P $B"*(B Q Premise
|> 2. P $B"*(B (Q $B"*(B $B"L(BP) Premise
| De falsum quodlibet, nice try
| IOW You can prove anything with a wrong premise as false -> X is
| always true indeed what you proved was
| false -> (P && !P)
| which is correct of course.

Outside of propositional logic, yes. But I did warn that this doesn't
necessarily apply, too, and provided a link for thorough critique of the
proof by the reader.

| Is it really called an axiom? An axiom cannot be proven, it should be
| called a Theorem.

Sorry, my mistake. It *is* a theorem. Still a misnomer since the theorem
is more of a paradox.

- --
Phillip Gawlowski
Twitter: twitter.com/cynicalryan

~ "When life gives you a lemon, make lemonade." -Susie "I say, when
life gives you a lemon, wing it right back and add some lemons of your
own!" -Calvin
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.8 (MingW32)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iEYEARECAAYFAkgHYacACgkQbtAgaoJTgL9mbgCgkK2JMounvNuucP9HMaLPHcvC
YjoAn2okGjTi/OAGWGiz5kQl5hm6w0f3
=zHaV
-----END PGP SIGNATURE-----

 

[Sean O'Halpin]

My claim wasn't that reasoning about the system is not subject to
Goedel's incompleteness theorem - it is.

Ah, I see.

It was that the properties
that was described as being a result of Goedel's incompleteness
theorem was in fact not related to that theorem. That state proving
is impossible in the case of an infinite memory computer and often
infeasible the case of finite memory computers is, to the best of my
knowledge, a fully separate result.

I just looked up Wikipedia on the halting problem[1] - I quote:

"...any finite-state machine, if left completely to itself, will fall
eventually into a perfectly periodic repetitive pattern. The duration
of this repeating pattern cannot exceed the number of internal states
of the machine..."

which agrees with your statement, though the article continues:

Minsky warns us, however, that machines such as computers with e.g. a
million small parts, each with two states, will have on the order of
21,000,000 possible states:

"This is a 1 followed by about three hundred thousand zeroes ...
Even if such a machine were to operate at the frequencies of cosmic
rays, the aeons of galactic evolution would be as nothing compared to
the time of a journey through such a cycle" (Minsky p. 25)

Minsky exhorts the reader to be suspicious -- although a machine may
be finite, and finite automata "have a number of theoretical
limitations":

"...the magnitudes involved should lead one to suspect that
theorems and arguments based chiefly on the mere finiteness [of] the
state diagram may not carry a great deal of significance" (ibid).

When you consider that 1 million bits is about 128K, that is a sobering thought.

Regards,
Sean

[1] http://en.wikipedia.org/wiki/Halting_problem#Common_pitfalls

 

[Phillip Gawlowski]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Robert Dober wrote:

| Oops I missed it, nice trick anyway.

Yeah, abstract logic allows for neat stunts (and a lot of sales for
aspirin, too).

| I see no paradox in it, the paradox is the proof of the theorem right?
| The theorem itself just says that such paradoxes will occur in a
| complete system, but I admit it is difficult to accept that as not
| being paradoxal itself. :=)
| IIRC even Bertrand Russel did not believe Gödel's theorem and there
| were other prominent mathematicians defying it.
| Gödel was waaaay ahead of his time.

Well, the theorem is counter-intuitive in its nature, and paradoxical.

After all, any consistent system should be provable, but isn't. But if
it isn't provable, it isn't consistent, but yet it is.

The theorem is, in a way, its own proof.

- --
Phillip Gawlowski
Twitter: twitter.com/cynicalryan

~ - You know you've been hacking too long when...
...you think "grep keys /dev/pockets" or "grep homework /dev/backpack"
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.8 (MingW32)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iEYEARECAAYFAkgHikkACgkQbtAgaoJTgL8PYwCfehqRFbf/BHY8fH8IBw0MqaYL
gikAoKewZclVZoJmLvmhxvbH4HjEJ0xP
=gGU1
-----END PGP SIGNATURE-----

 

[Robert Dober]

After all, any consistent system should be provable, but isn't. But if
it isn't provable, it isn't consistent, but yet it is.

No G=F6del is not talking about consistent systems, he has only (that is
a strange adjective in this context, but you know how I mean it)
proven that all *complete* systems are inconsistent.

Eivind can you explain this better? Or am I wrong after all? I really
liked how you put things last time, felt kind of, gosh that is exactly
what I should have sayed...

Cheers
Robert