cards-deck: university::theo_complexity

Satz von Rice:

broad part of [[112.00_anchor_overview]]


Motivation für Satz von Rice:

Wir haben zuvor bereits betrachtet, dass diverse kritische Eigenschaften von Turingmaschinen / Programmen nicht immer entscheidbar sind. Dabei stellt sich die Frage, ob diese Eigenschaften in den Betrachtungen dann nur Ausnahmen oder Regel sind. MIt dieser Eigenschaft können wir weitere Betrachtungen schlussfolgern.

So gut, wie alle interessanten Eigenschaften von TMs sind (leider) unentscheidbar.

Definition von interessanten Eigenschaften: #card

Wir interessieren uns meist nur für die Ausgaben, denn wenn wir später äquivalente TMs betrachten, ist es interessant, ihre Eigenschaften zu betrachten. Wir wollen also Eigenschaften von TMs anschauen, die sich nur an der von ihr erkannten Sprachen festmachen lassen –> wir lassen also die konkrete Implementierung und ihre Struktur heraus/weg. ^1686505898165

EIne Äquivalenz von Turingmaschinen haben wir so definiert, dass beide Turingmaschinen, die gleiche Sprache entscheiden können.

ferner benötigen wir erneut die Definition von nicht trivialen Sprachen: ![[theo2_SprachenUnendlichkeit#Nicht-triviale Sprachen]]

Semantisches Entscheidungsproblem:

Definition:

Sei eine Sprache, deren Wörter nur aus Codes von TM bestehen –> also gleich einer nicht-trivialen Sprache! -> Jedes Wort ist Code einer TM. Wir nennen diese Sprache jetzt semantisch #card:

  • Wenn und äquivalente TMs sind, Dann sind entweder beide in L oder beide nicht in L enthalten:

Satz von Rice:

Wie lautet er? Jedes semantische, nichttriviale Entscheidungsproblem ist unentscheidbar.

Beweisidee:

Wir betrachten einen Beweis, welcher multiple Fälle betrachten muss, um sinnvoll gelöst werden zu können. was sind nötige Grundstrukturen für einen solchen Beweis? #card Dabei legen wir jetzt folgende Parameter fest:

  • Sei eine nichttriviale, semantische Sprache
  • wir wollen das Halteproblem auf diese Sprache reduzieren
  • Sei dazu eine TM, welche kein einziges Wort akzeptiert.
    • beschrieben wird sie mit: ^1686505898173

können wir eine solche TM konstruieren? #card:

  • Ja, sie soll einfach bei jeder Eingabe direkt rejecten und somit nicht entscheiden!

Wir können jetzt passend reduzieren, jenachdem, ob ist oder nicht: also wie können wir die beiden Fälle definieren? #card

  • Falls , dann konstruieren wir eine passend Reduktion als Fall 1
  • und Falls m dann konstruieren wir eine Reduktion als Fall 2
  • Wir wissen noch, dass und nicht entscheidbar sind und können jetzt schon erkennen, dass auch untenscheidbar sein muss! ^1686505898177

Beweis:

Starten wir nun den Beweis des Satz von Rice. #card Dafür sei gegeben: eine nicht triviale, semantische Sprache Da nicht trivial ist, gibt es also :

  • eine mit und
  • eine mit Wir werden beide diese TMs später wieder anwenden müssen, wenn wir zeigen, dass sie equivalent in der Ausführung sind. Fall 1 - Also :
    Wir möchten nun eine Reduktion von konstruieren und haben dann eine TM die L entscheiden kann. Das Ziel unserer Reduktion ist dann:
  • wir betrachten eine Eingabe und wollen dann entscheiden, ob N auf stoppt oder nicht
  • wir wollen so transformieren, dass wir sie in die Form bekommen, um sie dann der TM als Argument geben zu können. Es soll dann also gelten: also, wenn N sich in Komplement der Menge des Halteproblemes befindet, dann ist auch die verarbeitende TM M in der Sprache ^1686505898182

Fall 1 - Konstruktion zum Lösen: Stellen wir eine Turingmaschine zur Lösung von bei Eingabe auf:

  • Die Eingabe entspricht des Codes einer TM – also dessen Gödelnummer beispielsweise
  • Die gewünschte Ausgabe gibt dann an, ob auf stoppt Um dies zu bewerkstelligen gehen wir folgend for:
  1. Konstruiere Gödel-Code einer TM , die dann die folgende Berechnung durchführen würde, also nur konzeptuell gedacht:
    1. Simulieren von (muss es nicht berechnen, bzw keine Ausgabe geben, sondern nur zeigen, wie es ungefähr funktionieren würde)
    2. zurückgeben ( also einfach die TM, die auf nichts eine Ausgabe gibt) DIe TM M wird hier nicht ausgeführt!, wir berechnen nur ihren Code. Dieser Schritt entspricht der Berechnung der neuen Instanz in der Reduktion.
  2. Wir geben jetzt zurück, also wir geben die konvertierte Instanz zurück und rufen dann die TM mit diesem Wert auf

Ist diese Konstruktion abgeschlossen, dann müssen wir folglich die Äquivalenz der Aussagen zeigen. Dafür müssen wir auch wieder zwei Fälle betrachten: Fall 1, von 1: Sei :

  • Gelte dieser fall, dann heißt das, dass , also hält nur bei **eingabe **an.
  • In diesem Fall ist dann die obige TM (welche simuliert und zurückgibt) äquivalenz zur TM –> sie gibt ja die gleiche TM zurück xd;
  • Da semantisch ist, gilt also unsere Betrachtung des Satzes von Rice:
  • Wir wissen aber weiterhin, dass gilt. Also folgt daraus dann auch

Fall 2, von 1: Sei :

  • Gelte dieser Fall, dann gilt also also hält bei einer Eingabe von nicht an
  • Tritt dieser Fall ein, dann ist unsere obige TM ( die simuliert!) äquivalent zur TM , denn beide liefern genau das gleiche Ergebnis: Die Simulation hält nie an, egal was die Eingabe z in M war. die TM M akzeptiert hier also auch kein einziges Wort
  • Da L semantisch ist, können wir auch wieder anwenden:
  • Wir wissen ferner, dass gilt und somit dann auch

Resultat der Betrachtung: Wir haben gesehen, dass die Reduktionseigenschaft mit erfüllt wird. Diese Reduktion ist berechenbar! (wir beweisen sie aber nicht)

Fall 2 - Analog zum ersten Fall: In dieser Instanz gehen wir ähnlich, wie oben vor, jedoch reduzieren wir jetzt anstatt ! Weiterhin nutzen wir jetzt die Sprache , statt , in unserer Konstruktion. Wire resultieren dann mit folgender Konstruktion: Turingmaschine zur Lösung von auf Eingabe :

  • Eingabe entspricht Code einer TM
  • Gewünschte Ausgabe der Konstruktion: N stopp auf oder nicht Wir konstruieren hierfür dann:
  1. Gödel-Code einer TM M, die die folgende Berechnung durchführen würde:
  2. TM m auf Eingabe :
    1. Simuliere
    2. Return
  3. Am Ende geben wir auch hier dann die Transformation in der neuen Eingabe zurück, also

zusammengefasst Betrachtung des Beweis: Wir haben beide Fälle betrachtet und resultieren folgend: Fall 1: , also stoppt, was impliziert die konstruierte TM ist äquivalent zu , und da folgt auch Fall 2: als stopp nicht, woraus folgt die konstruierte TM ist äquivalent zu und im Fall 2 gilt dann also dann auch !

Umkehrung ist im Allgemeinen falsch: #card

Das Theorem von Rice sagt intuitiv:

semantisch ==> unentscheidbar

aber logischerweise gilt die Umkehrung nicht!

  • Es gibt untenscheidbare Sprachen, die nicht semantisch sind! ^1686505898187

Bedeutung des Satzes:

Was können wir aus dem Satz schließen? #card Wir haben demnach erkennen können, dass eine allgemeine Verifikation von Programmen eigentlich unmöglich ist. Das ist doof, wenn wir sicherheitskritische Funktionen von irgendwelchen Computern ausführen lassen wollen.
Beispielsweise etwa ein Autopilot für Flugzeuge oder eine automatische Steuerung von Atomkraftwerken. ^1686505898191

Ein spezifisches Code-Beispiel:

def halloo():
	print("Hello World")
hallo()

In diesem Beispiel können wir schon aussagen, ob das Programm terminieren würde, denn wir können es als eine einmalige Ausführung betrachten.

Weiter können wir also Betrachten, ob eine Einschränkung der Sorte von Programmen helfen könnte, über ihre Eigenschaften von Terminierung zu urteilen. Welchen Schluss können wir ziehen? #card

  • Programme die keine Schleifen, Variablen benutzen, halten an!
  • Wir nehmen als Einschränkungen in Kauf: Programme dürfen nur bestimmte DInge tun, etwa bestimmte Stellen im Speicher beschreiben oder nur diverse Invarianzen aufweisen.
  • Eine tiefere Betrachtung liefert dann das Fachgebiet der Software-Verifikation! ^1686505898194