Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Limits? What Limits? Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

9. More Undecidable Problems

verfasst von : Bernhard Reus

Erschienen in: Limits of Computation

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

In this chapter we will look at more undecidable problems. We show a famous result, Rices theorem, that any non-trivial purely semantical property of programs undecidable. The proof uses a reduction from the Halting problem. Such reductions and the reasoning principles they give rise to are investigated. The concept of a semi-decidable problem is introduced, and it is shown that the Halting problem is semi-decidable by means of the self-interpreter.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel An Undecidable (Non-computable) Problem
Nächstes Kapitel Self-referencing Programs
Fußnoten
1
Henry Gordon Rice (July 18, 1920–April 14, 2003) was an American logician and mathematician. He proved “his” theorem in his doctoral dissertation of 1951.
 
2
Program verification is actually a thriving discipline and quite considerable progress has been made in the last few decades [21] and has even reached giants like Facebook [4].
 
3
Wang (20 May 1921–13 May 1995) was born in China but later taught at Harvard where he was also the thesis advisor of Stephen Cook (of whom we will hear more later).
 
4
Problem reduction is a strategy that human beings or companies use all the time in an informal manner. For instance to “solve” the problem of getting from home to work, one could reduce it for instance to the problem of getting to the train station and on the right train, provided one already has a ticket.
 
5
That means that for different \(x\ne y\in A\) we can still have \(f(x)=f(y)\).
 
6
More precisely, “recursive” refers to the class of “partial recursive functions” on numbers (as introduced by Kleene in the late 1930s) which one can show are also a reasonable notion of computation equivalent to all the one we have presented.
 
7
Again, note that this does not mean we cannot write a program that might produce the answer for a specific input value. If this input is finite then a brute force search will always work. For instance, we can clearly write a program that decides whether a floor of a given fixed size (say \(5\times 5\)) can be tiled with given, say k, tile types since there are \(k^{25}\) possible ways to tile such a floor. Note that there is a combinatorial explosion of the number of possible tilings but this does not concern us in computability. It will concern us in the part about complexity.
 
8
Haskell and ML are such programming languages but they exclude the type of all types.
 
9
It may also return false positives, i.e. accept programs that are not type sound, this happens e.g. in the case of division-by-zero.
 
10
For a good textbook on types see [16].
 
11
The characteristic function \(\chi \) of a set A of elements of type T is of type \(T\rightarrow \mathbb {B}\) and defined by \(\chi (d) = d\in A\).
 
12
Tibor Radó (June 2, 1895–December 29, 1965) was a Hungarian mathematician who moved to the USA and worked in Computer Science later in his life. The publication on the Busy Beaver function is maybe his most famous one [19].
 
13
This function is named after Wilhelm Friedrich Ackermann (29 March 1896–24 December 1962), a German mathematician, and Rózsa Péter, born Politzer, (17 February 1905–16 February 1977), a Hungarian mathematician.
 
Literatur
1.
Bar-Hillel, Y., Perles, M., Shamir, E.: On formal properties of simple phrase structure grammars. Z. Phonetik, Sprachwiss. Kommunikationsforsch. 14, 143–192 (1961)
2.
3.
Brady, A.H.: The determination of the value of Rado’s noncomputable function \(\Sigma (k)\) for four-state turing machines, Mathematics of Computation, 40(162), 647–665 (1983)
4.
Calcagno, C., Distefano, D., Dubreil, J., Gabi, D., Hooimeijer, P., Luca, M., O’Hearn, P., Papakonstantinou, I., Purbrick, J., Rodriguez, D.: Moving fast with software verification. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NASA Formal Methods. Lecture Notes in Computer Science, pp. 3–11. Springer International Publishing (2015)
5.
6.
Chomsky, N., Schützenberger, M.P.: The algebraic theory of context-free languages. In: Braffort, P., Hirschberg, D. (eds.) Computer Programming and Formal Systems, pp. 118–161. North Holland, Amestradam (1963)CrossRef
7.
8.
Floyd, R.W.: On ambiguity of phrase structure languages. Commun. ACM 5(10), 526–532 (1962)CrossRefMATH
9.
Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley, Reading (1979)MATH
10.
11.
Markoff, A.: On the impossibility of certain algorithms in the theory of associative system. Academ. Sci. URSS. 55, 83–586 (1947)MathSciNetMATH
12.
Matiyasevich, Y.V.: Hilbert’s Tenth Problem. MIT Press, Cambridge (1993)MATH
13.
Marxen, H., Bundtrock, J.: Attacking the Busy Beaver 5. Bull. EATCS 40, 247–251 (1990)MATH
14.
Michel, P.: The Busy Beaver Competition: a historical survey. Available via DIALOG. arXiv:​0906.​3749 (2012). Accessed 5 June 2015
15.
Novikov, P.S.: On the algorithmic unsolvability of the word problem in group theory. Proc. Steklov Inst. Math. (in Russian). 44, 1–143 (1955)
16.
Pierce, B.: Types and Programming Languages. MIT Press, Cambridge (2002)MATH
17.
18.
Presburger, M.: Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt.(English translation: Stansifer, R.: Presburger’s Article on Integer Arithmetic: Remarks and Translation (Technical Report). TR84-639. Ithaca/NY. Dept. of Computer Science, Cornell University) Comptes Rendus du I congrès de Mathématiciens des Pays Slaves, 1929, pp. 92–101 (1930)
19.
20.
21.
Silva, V.D., Kroening, D., Weissenbacher, G.: A survey of automated techniques for formal software verification. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 27(7), 1165–1178 (2008)CrossRef
22.
Soare, R.I.: The history and concept of computability. In: Griffor, E.R. (ed.) Handbook of Computability Theory, pp. 3–36. North-Holland, Amestradam (1999)CrossRef
23.
Turing, A.M.: On computable numbers, with an application to the Entscheidungsproblem. Proc. Lond. Math. Soc. Sec. Ser. 42, 230–265 (1936)MathSciNetMATH
24.
Wells, J.: Typability and type-checking in system F are equivalent and undecidable. Ann. Pure Appl. Logic 98(1–3), 111–156 (1999)MathSciNetCrossRefMATH
Metadaten
Titel
More Undecidable Problems
verfasst von
Bernhard Reus
Copyright-Jahr
2016
Buch
Limits of Computation

Print ISBN: 978-3-319-27887-2

Electronic ISBN: 978-3-319-27889-6

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-27889-6_9