Seite 1 von 1

Beweis des Satzes von Rice

BeitragVerfasst: 29 Jan 2014, 19:01
von yannick.forster
Hallo zusammen,

Ich habe "moralische" Probleme mit dem Beweis des Satzes von Rice aus der Vorlesung heute. Wir hatten dort für beliebiges $A \subseteq \Sigma^*$ oBdA angenommen, dass $\exists x \in A, L x = \emptyset$ gilt.

Rein logisch ist das natürlich gültig: Wenn es keins gibt, liegt es eben im Komplement.

Mit "moralische" Probleme mein ich jetzt, dass der Beweis nicht nur logisch gültig sein sollte, sondern auch von einem Programmiersystem (zum Beispiel eine Turingmaschine) überprüft werden können sollte.

Ein solches Programm würde wahrscheinlich so funktionieren, dass es für beliebiges $A$ entscheidet, ob die Aussage von oben gilt oder nicht und dann ensprechend den Beweis mit $A$ oder dem Komplement von A weiterführt.

Jetzt mein konkretes Problem: Muss dafür nicht die Aussage $\exists x \in A, L x = \emptyset$ für alle $A$ entscheidbar sein? Wenn ja stoßen wir aber auf Probleme.

Ich kodiere $x \in A$ jetzt einfach mal als $\pi A x$, wobei A ein Programm ist, das die Menge repräsentiert. Dann muss folgende Menge entscheidbar sein, damit der Beweis von einem Programmiersystem nachvollzogen werden kann:

Code: Alles auswählen
{ y | \exists x, \pi y x \land L x = \emptyset}


Die ist aber nicht entscheidar. Ein Akzeptor $u$ würde so aussehen:

Code: Alles auswählen
\pi u z \equiv \exists x, \pi y x \land L x = \emptyset


Daraus kann man dann folgern, dass die Menge $\{x | L x = \emptyset \}$ akzeptierbar ist. Wir haben aber schon gezeigt, dass das nicht der Fall ist. Die Folgerung sieht so aus:

Code: Alles auswählen
\pi [\lambda \alpha.u @ (if \alpha T R)] z
\equiv \pi [u @ (if z T R)] \epsilon \\
\equiv \pi u [if z T R] \\
\equiv \exists x. \pi [if z T R] \land L x = \emptyset \\
\equiv \exists x. ((z = x \land True) \lor (z \neq x \land False)) \land L x = \emptyset \\
\equiv \exists x. z = x \land L x = \emptyset \\
\equiv L z = \emptyset


Statt der Kodierung von A als Automat kann ich auch einfach meinem Prüfer, ob ein solches x existiert das Singleton-Set nur mit x füttern. Der könnte dann auch sagen, ob die Sprache von xl eer ist.

Ich bin eigentlich ziemlich sicher, dass ich irgendwo einen Denkfehler habe. Alternativ kann auch irgendwo zwischendrin ein Fehler in der Argumentation stecken.

Jetzt komme ich nicht mehr weiter. Lukas Krämer hat mich noch darauf hingewiesen, dass die Aussage eine nichttriviale Eigenschaft beschreibt und damit durch den Satz selbst nicht entscheidbar wäre.

Kann mich jemand entwirren?

Danke
Yannick

PS: Ich hab das in Latex-Notation getippt, weil ich gehofft hab, das Forum könnte das irgendwie darstellen. Scheint leider nicht der Fall zu sein, zumindest finde ich den Knopf nicht. Dadurch ist das jetzt eher so mittelgut lesbar. Wenn ein Moderator weiß wie es schöner geht: Bitte Bescheid sagen.

Re: Beweis des Satzes von Rice

BeitragVerfasst: 30 Jan 2014, 10:09
von gert.smolka
Unentscheidbarkeitsbeweise werden üblicherweise mit tertium non datur geführt, so auch hier. Die Reduktion des Satzes von Rice auf das Lemma verwendet tertium non datur.

Klassische Beweise kann man genauso algorithmisch prüfen wie konstruktive. Es gibt einfach eine Beweisregel mehr (tertium non datur).

Das man mit tertium non datur über Algorithmen argumentiert ist sicher nicht unmoralisch.

Ob A ein Programm enthält, das die leere Sprache akzeptiert, ist ohne weitere Annahmen sicher unentscheidbar.

Es wäre aber sehr interessant, eine konstruktive Theorie von Programmiersystemen zu entwickeln und genau zu analysieren, wo tertium non datur mit welchen Konsequenzen zum Einsatz kommt. Also alle Beweise in Coq mit nur expliziten Annahmen und den konstruktiven Kern isolieren. Wunderbares Thema für Bachelorarbeit, bitte melden bei Interesse.

Re: Beweis des Satzes von Rice

BeitragVerfasst: 04 Feb 2014, 19:35
von yannick.forster
Ich hab mir mal noch weiter Gedanken darüber gemacht, ob man tertium non datur zumindest an dieser Stelle für unsere Formalisierung von Programmiersystemen umgehen kann. Unter der Annahme, dass man "nicht trivial" in

Code: Alles auswählen
(1) exists x, x \in A /\ exists x, x \not\in A


kodiert, denke ich, dass es funktioniert:

Wir wollen zeigen, dass A nicht entscheidbar ist. Dazu zeigen wir, dass sich die Entscheidbarkeit des Selbsthalteproblems auf die Entscheidbarkeit von A reduzieren lässt.

Sei A also entscheidbar. Es gibt dann Akzeptoren u und v sodass

Code: Alles auswählen
\pi u x \equiv x \in A und \pi v x \equiv x \in \barA


Wir nehmen nun r := [R] und überprüfen, ob

(2) pi u r oder pi v r gilt.

Falls pi v r galt, so führe den Beweis mit \barA und v statt A und u fort.

Wir haben damit aus (2) unsere Annahme
Code: Alles auswählen
 \exists x \in A, L(x) = \emptyset. Aus (1) folgt exists y \in \Sigma^* - A
Der restliche Beweis war, soweit ich das überblicke, bereits konstruktiv.

In unserem Beweis haben wir tertium non datur denke ich an dieser Stelle benötigt, weil wir unsere Annahme, dass A entscheidbar ist, sofort zu "A ist akzeptierbar" abgeschwächt haben. So sollte es aber auch ohne gehen.

Hab ich irgendwo einen Denkfehler gemacht oder eine weitere Anwendung von tertium non datur übersehen?