Re: functions that halt
From: Stephan Schulz (schulz_at_sunbroy2.informatik.tu-muenchen.de)
Date: 04/09/04
- Next message: Alexander Baranovsky: "LISPPA (List Processing based on the Polymorphic Arrays)"
- Previous message: Laconic2: "Re: How is this collection called?"
- In reply to: |-|erc: "Re: functions that halt"
- Next in thread: |-|erc: "Re: functions that halt"
- Reply: |-|erc: "Re: functions that halt"
- Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
Date: Fri, 9 Apr 2004 12:51:35 +0000 (UTC)
In article <4071ec2c$0$16965$afc38c87@news.optusnet.com.au>, |-|erc wrote:
>
>
> thats conjecture. noone in industry what so ever writes programs
> that don't halt.
> why are mathematicians allowed this freedom?
Well, if you are very finicky, all our computers are just finite
automata, and the Halting Problem is decidable. Even in that case:
Counterexample 1: Any UNIX d(a)emon.
If you allow for the usual abstraction (unlimited resources), you get
better counterexamples:
Counterexample 2: Any program that tries to find special solutions to
generally undecidable programs, e.g. theorem provers for first or
higher-order logic (plug: check www.eprover.org) or model finders.
Note that there is no (computable) syntactic characterisation for the
class of all programs that always halt (simple diagonalisation
proof).
Bye,
Stephan
-- -------------------------- It can be done! --------------------------------- Please email me as schulz@informatik.tu-muenchen.de (Stephan Schulz) ----------------------------------------------------------------------------
- Next message: Alexander Baranovsky: "LISPPA (List Processing based on the Polymorphic Arrays)"
- Previous message: Laconic2: "Re: How is this collection called?"
- In reply to: |-|erc: "Re: functions that halt"
- Next in thread: |-|erc: "Re: functions that halt"
- Reply: |-|erc: "Re: functions that halt"
- Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
Relevant Pages
|
