Matroids Matheplanet Forum Index
Moderiert von Bilbo
Theoretische Informatik » Berechenbarkeitstheorie » Spezifikation des Halteproblems angeben
Autor
Universität/Hochschule Spezifikation des Halteproblems angeben
carlox
Aktiv Letzter Besuch: im letzten Quartal
Dabei seit: 22.02.2007
Mitteilungen: 1382
  Themenstart: 2019-11-26

Hallo allerseits, ===================================== In seinem Buch "Ideen der Informatik" schreibt Uwe Schöning: Gegeben ist ein auf Korrektheit zu analysierendes Programm A und eine Spezifikation S (die genau beschreibt, was es heißt formal korrekt zu sein). Dies ist eine Ansammlung von Formeln, die Aussagen darüber machen welche Eigenschaften die im Programm vorkommenden Variablen nach der Ausführung des Programms haben sollten unter Bezugnahme der Werte der Variablen, die vor Ausführung des Programms A galten. Wenn es einen solchen Verifikationsalgorithmus geben würde, könnte er das Halteproblem lösen (als Spezialfall einer Spezifikation, die man in Bezug auf A machen kann). ===================================== Frage: Wie kann man die Spezifikation des Halteproblem angeben ? Das muß doch eine prädikatenlogische Formel sein. mfg cx


   Profil
Zwerg_Allwissend
Senior Letzter Besuch: im letzten Monat
Dabei seit: 02.12.2013
Mitteilungen: 284
  Beitrag No.1, eingetragen 2019-11-28

\quoteon(2019-11-26 19:16 - carlox im Themenstart) Hallo allerseits, ===================================== In seinem Buch "Ideen der Informatik" schreibt Uwe Schöning: Gegeben ist ein auf Korrektheit zu analysierendes Programm A und eine Spezifikation S (die genau beschreibt, was es heißt formal korrekt zu sein). Dies ist eine Ansammlung von Formeln, die Aussagen darüber machen welche Eigenschaften die im Programm vorkommenden Variablen nach der Ausführung des Programms haben sollten unter Bezugnahme der Werte der Variablen, die vor Ausführung des Programms A galten. Wenn es einen solchen Verifikationsalgorithmus geben würde, könnte er das Halteproblem lösen (als Spezialfall einer Spezifikation, die man in Bezug auf A machen kann). ===================================== Frage: Wie kann man die Spezifikation des Halteproblem angeben ? Das muß doch eine prädikatenlogische Formel sein. \quoteoff Ja, das ist eine prädikatenlogische Formel. Die kann man hier aber nicht angeben. Man braucht dazu ja einige Begriffe mittels derer man die Spezifikation formulieren kann. Allein diese Begriffe formal zu definieren und damit dann die Spezifikation als Formel aufzuschreiben ist kein einfaches Unterfangen. Boyer und Moore haben die Unlösbarkeit des Halteproblems vor 35 Jahren mit ihrem Verifikationssystem bewiesen https://dl.acm.org/citation.cfm?doid=828.1882 . In dem Artikel findet man die Spezifikation - ist aber schwere Kost! PS1: "Prädikatenlogische Formel" heißt natürlich nicht "mittels Prädikatenlogik beweisbar". Da Programme Schleifen bzw. Rekursion enthalten braucht man Induktion. PS2: Was ist denn mit >solchen< Verifikationsalgorithmus gemeint?


   Profil
carlox
Aktiv Letzter Besuch: im letzten Quartal
Dabei seit: 22.02.2007
Mitteilungen: 1382
  Beitrag No.2, vom Themenstarter, eingetragen 2019-11-29

hallo Zwerg_Allwissend, Vielen Dank für deine Antwort. 1) >Ja, das ist eine prädikatenlogische Formel. >Die kann man hier aber nicht angeben > Man braucht dazu ja einige Begriffe mittels derer man >die Spezifikation formulieren kann. >Allein diese Begriffe formal zu definieren und >damit dann die Spezifikation als Formel aufzuschreiben ist >kein einfaches Unterfangen. > Das denke ich auch. Die Spezifikation besteht aus einer Vorbedingung P und einer Nachbedingung Q. P ist eine prädikatenlogische Formel, die die im Programm A vorkommenden Werte der Variablen vor der Programmausführung betrifft und Q ist eine prädikatenlogische Formel, die die in A vorkommenden Werte der Variablen nach der Programmausführung betrifft. In einer der in P vorkommenden Variablen (ich nenne sie e) steht dann das zu untersuchende Programm R, also (informal): e = R Das zu formalisieren dürfte kein Ptoblem sein: Man nimmt für R einfach die codierte Turingmaschine, die das Programm R darstellt, also eine Zahl. In einer der in Q vorkommenden Variablen (ich nenne sie o) steht dann eine Zeichenfolge "R hält an" oder "R hält nicht a" also: o = "R hält an" , wenn R anhält o = "R hält nicht an" , wenn R nicht anhält Das Problem ist, wie man diese Verzweigung durch eine prädikatenlogische Formel darstellt. Das dürfte schwierig sein (wie formalisiert man "R hält an" bzw "R hält nicht an"?) Oder sehe ich da was falsch ? 2) >Boyer und Moore haben die Unlösbarkeit des Halteproblems vor 35 Jahren >mit ihrem Verifikationssystem bewiesen dl.acm.org/citation.cfm?doid=828.1882 . >In dem Artikel findet man die Spezifikation - ist aber schwere Kost! > a) Habe versucht den Artikel runterzulade (obwohl ich vermutlich den nicht verstehen werde). Das kostet Geld oder gibt es den auch kostenlos? b) Bis jetzt dachte ich , daß man unter Programmverifikation (=Verifikationssystem) versteht, dass man die Korrektheit eines konkret vorgegebenen Programms beweist oder was verstehst du unter Verifikationssystem? 3) > >PS1: "Prädikatenlogische Formel" heißt natürlich nicht "mittels Prädikatenlogik beweisbar". > Ja, wie z.B. x=x oder auch durch Quantoren angereicherte Konstrukte. Warum erwähnst du das ? > >Da Programme Schleifen bzw. Rekursion enthalten braucht man Induktion. > Ich verstehe nicht, was du damit meinst. Kannst du mir das genauer (an einem Beispiel erklären)? was verstehst du unter Induktion ? Etwa Regelmenge bzw. induktiv definierte Mengen? 4) > >PS2: Was ist denn mit >solchen< Verifikationsalgorithmus gemeint? > Das frage ich mich auch. Uwe Schöning schreibt auf S.120 in „Ideen der Informatik“: ============================================= Programm A ----> | Verifikations- | A erfüllt S Spezifikation S ----> | Algorithmus | A ist inkorrekt Einen solchen Spezifikationsalgorithmus kann es nicht geben. Insbesondere würde er dem Satz von Rice widersprechen. Ein solcher Verifikationsalgorithmus könnte das Halteproblem lösen(als Spezalfall einer Spezifikation, die man in Bezug auf A mach en kann). … =============================================== Vermutlich meint U. Schöningh den Verifikationsalgorithmus mfg cx


   Profil
Zwerg_Allwissend
Senior Letzter Besuch: im letzten Monat
Dabei seit: 02.12.2013
Mitteilungen: 284
  Beitrag No.3, eingetragen 2019-11-29

\quoteon(2019-11-29 11:26 - carlox in Beitrag No. 2) 1) >Ja, das ist eine prädikatenlogische Formel. >Die kann man hier aber nicht angeben > Man braucht dazu ja einige Begriffe mittels derer man >die Spezifikation formulieren kann. >Allein diese Begriffe formal zu definieren und >damit dann die Spezifikation als Formel aufzuschreiben ist >kein einfaches Unterfangen. > Das denke ich auch. Die Spezifikation besteht aus einer Vorbedingung P und einer Nachbedingung Q. P ist eine prädikatenlogische Formel, die die im Programm A vorkommenden Werte der Variablen vor der Programmausführung betrifft und Q ist eine prädikatenlogische Formel, die die in A vorkommenden Werte der Variablen nach der Programmausführung betrifft. In einer der in P vorkommenden Variablen (ich nenne sie e) steht dann das zu untersuchende Programm R, also (informal): e = R Das zu formalisieren dürfte kein Ptoblem sein: Man nimmt für R einfach die codierte Turingmaschine, die das Programm R darstellt, also eine Zahl. In einer der in Q vorkommenden Variablen (ich nenne sie o) steht dann eine Zeichenfolge "R hält an" oder "R hält nicht a" also: o = "R hält an" , wenn R anhält o = "R hält nicht an" , wenn R nicht anhält Das Problem ist, wie man diese Verzweigung durch eine prädikatenlogische Formel darstellt. Das dürfte schwierig sein (wie formalisiert man "R hält an" bzw "R hält nicht an"?) Oder sehe ich da was falsch ? \quoteoff Wie ich schon schrieb ist das nicht so einfach. Zunächst muß man ja die Turingmaschine und ihre Arbeitsweise formal definieren und mit diesen Begriffen dann das Halteproblem. Allgemein braucht man irgendein Berechnungsmodell. Nimmt man Turingmaschinen, dann hat man schon verloren. In Termini der Informatik würde man sagen, daß das eine maximal ungeeignete Repräsentation ist. Boyer & Moore haben die Programmiersprache LISP verwendet, genaugenommen PURE LISP. \quoteon(2019-11-29 11:26 - carlox in Beitrag No. 2)2) >Boyer und Moore haben die Unlösbarkeit des Halteproblems vor 35 Jahren >mit ihrem Verifikationssystem bewiesen dl.acm.org/citation.cfm?doid=828.1882 . >In dem Artikel findet man die Spezifikation - ist aber schwere Kost! > a) Habe versucht den Artikel runterzulade (obwohl ich vermutlich den nicht verstehen werde). Das kostet Geld oder gibt es den auch kostenlos? \quoteoff Hier: www.cs.utexas.edu/users/boyer/unsolv.ps.Z \quoteon(2019-11-29 11:26 - carlox in Beitrag No. 2)2) b) Bis jetzt dachte ich , daß man unter Programmverifikation (=Verifikationssystem) versteht, dass man die Korrektheit eines konkret vorgegebenen Programms beweist oder was verstehst du unter Verifikationssystem? \quoteoff Ein Programm mittels dessen die Korrektheit von korrekten Programmen bewiesen werden kann. Solch ein Verifikationssystem ist unvollständig, d.h. es gibt unendlich viele korrekte Programme deren Korrektheit nicht mit dem System bewiesen werden kann. Das folgt aus dem 1. Gödelschen Unvollständigkeitssatz. \quoteon(2019-11-29 11:26 - carlox in Beitrag No. 2) 3) > >PS1: "Prädikatenlogische Formel" heißt natürlich nicht "mittels Prädikatenlogik beweisbar". > Ja, wie z.B. x=x oder auch durch Quantoren angereicherte Konstrukte. Warum erwähnst du das ? \quoteoff Als Hinweis, daß man Induktion braucht - ohne geht es i. A. nicht. \quoteon(2019-11-29 11:26 - carlox in Beitrag No. 2) >Da Programme Schleifen bzw. Rekursion enthalten braucht man Induktion. > Ich verstehe nicht, was du damit meinst. Kannst du mir das genauer (an einem Beispiel erklären)? was verstehst du unter Induktion ? Etwa Regelmenge bzw. induktiv definierte Mengen? \quoteoff Beispielsweise will man {x ≥ 0} y := 1; while x > 0 do y := x * y; x := x - 1 end {y = x!} zeigen, d.h. daß mit der while-Schleife die Fakultätsfunktion berechnet wird. Das kann man nur durch Induktion zeigen: Der Schleifenrumpf wird offensichtlich x mal ausgeführt. Induktionsanfang x = 0: 1 = 0! Induktionsschritt: Nach x Ausführungen des Schleifenrumps gilt y = x! (Induktionshypothese). Nach x + 1 Ausführungen des Schleifenrumps gilt y = x! *(x + 1) = (x + 1)! \quoteon(2019-11-29 11:26 - carlox in Beitrag No. 2)4) > >PS2: Was ist denn mit >solchen< Verifikationsalgorithmus gemeint? > Das frage ich mich auch. Uwe Schöning schreibt auf S.120 in „Ideen der Informatik“: ============================================= Programm A ----> | Verifikations- | A erfüllt S Spezifikation S ----> | Algorithmus | A ist inkorrekt Einen solchen Spezifikationsalgorithmus kann es nicht geben. Insbesondere würde er dem Satz von Rice widersprechen. Ein solcher Verifikationsalgorithmus könnte das Halteproblem lösen(als Spezalfall einer Spezifikation, die man in Bezug auf A mach en kann). … =============================================== Vermutlich meint U. Schöningh den Verifikationsalgorithmus \quoteoff Ich verstehe nicht, was mit "Verifikationsalgorithmus" gemeint ist. Falls ein terminierender Algorithmus gemeint ist, dann erhält man nicht nur einen Widerspruch zum Satz von Rice, sondern auch zum 1. Gödelschen Unvolsständigkeitssatz. Falls ein nicht notwendigerweise terminierender Algorithmus gemeint ist, dann erhält man einen Widerspruch zum 1. Gödelschen Unvollsständigkeitssatz.


   Profil
carlox
Aktiv Letzter Besuch: im letzten Quartal
Dabei seit: 22.02.2007
Mitteilungen: 1382
  Beitrag No.4, vom Themenstarter, eingetragen 2019-12-04

\quoteon(2019-11-29 15:34 - Zwerg_Allwissend in Beitrag No. 3) Ich verstehe nicht, was mit "Verifikationsalgorithmus" gemeint ist. Falls ein terminierender Algorithmus gemeint ist, dann erhält man nicht nur einen Widerspruch zum Satz von Rice, sondern auch zum 1. Gödelschen Unvolsständigkeitssatz. Falls ein nicht notwendigerweise terminierender Algorithmus gemeint ist, dann erhält man einen Widerspruch zum 1. Gödelschen Unvollsständigkeitssatz. \quoteoff Hallo Zwerg_Allwissend Vielen Dank für dein Posting. Annahme: Es gibt einen "Verifikationsalgorithmus" : Programm A ----> | Verifikations- | A erfüllt S bzw. Spezifikation S ----> | Algorithmus | A ist inkorrekt Im Folgenden will ich zeigen, dass diese Annahme falsch ist. Man wählt speziell A = Algorithmus, der von einer beliebigen, wahren prädikatenlogischen Formel (ohne freie Variablen) den Beweis (Beweisfolge) berechnet. x0, x1, …, xm seien die Variablen des Programms. Die Werte der Variablen vor der Programmausführung seien: x0=a_0, x1=a_1, … , xm=a_m Die Werte der Variablen nach der Programmausführung seien: x0=e_0, x1=e_1, … , xm=e_m Es sei a_0 = alpha , wobei alpha eine beliebige wahre prädikatenlogische Formel (ohne freie Variablen) ist. b_0 = alpha --> bf wobei bf eine Beweisfolge (also eine Folge von Formeln) für alpha (d.h. die letzte Fornel in bf ist alpha) ist. Die Spezifikation S sei wie folgt gewählt: Vorbedingung P: [alpha ist eine wahre prädikatenlogischen Formel (ohne freie Variablen)] ist wahr. Nachbedingung Q: [alpha --> bf] ist wahr Da dies dem 1. Gödelschen Unvollständigkeitssatz widerspricht, ist die obige Annahme falsch. Frage: Ist meine Argumentation richtig ? Problem: Die Vorbedingung P und die Nachbedingung Q ist nicht in PL1 (Prädikatenlogik 1. Stufe) formalisiert. Wie kann man das machen ? PS: Was mir dazu nachträglich noch einfällt (wie man es "hinbiegen kann"): Man kann eine Formel durch eine Zahl codieren. Genauso kann man eine Beweisfolge durch eine Zahl codieren. Die prädikatenlogische Formel Fz (wobei z eine Konstante ist) wird dann interpretiert als: Die zu z zugehörige Zahl ist eine Formel. Die prädikatenlogische Formel Bz (wobei z eine Konstante ist) wird dann interpretiert als: Die zu z zugehörige Zahl ist eine Beweisfolge. mfg cx


   Profil
Zwerg_Allwissend
Senior Letzter Besuch: im letzten Monat
Dabei seit: 02.12.2013
Mitteilungen: 284
  Beitrag No.5, eingetragen 2019-12-04

\quoteon(2019-12-04 12:04 - carlox in Beitrag No. 4) Programm A ----> | Verifikations- | A erfüllt S bzw. Spezifikation S ----> | Algorithmus | A ist inkorrekt \quoteoff Was soll das bedeuten?


   Profil
carlox
Aktiv Letzter Besuch: im letzten Quartal
Dabei seit: 22.02.2007
Mitteilungen: 1382
  Beitrag No.6, vom Themenstarter, eingetragen 2019-12-05

\quoteon Programm A ----> | Verifikations- | A erfüllt S bzw. Spezifikation S ----> | Algorithmus | A ist inkorrekt \quoteoff > >Was soll das bedeuten? > Zitat: (S.121-122) "Ideen der Informatik" von U. Schöning: ==================================== Das Problem der Programmverifikation ist das Folgende: Gegeben ist ein auf Korrektheit zu analysierenes Programm A. Was es genau heißt, korrekt zu sein, also die Wunschvorstellung, die man von dem Programm A hat, wid formal spezifiziert in eine Spezifikation S. Dies ist eine Ansammlung von Formeln (vgl. Kapitel 5), die Aussagen darüber machen, welche Eigenschaften die im Programm A vorkommenden Variablen nach der Ausführung des Programms A haben sollten - unter Bezugnahme auf die Werte der Variablen, die vor Ausführung des Programms A galten. Die Wunschvorstellung wird durch folgendes Bild dargestellt: +---------------+ Programm A ----> | Verifikations- | --> "Prog. A erfüllt Spez. S" Spezifikation S ----> | Algorithmus | --> "Prog. A ist inkorrekt" +---------------+ Einen solchen Spezifikationsalgorithmus kann es nicht geben. Insbesondere würde er dem Satz von Rice widersprechen. Ein solcher Verifikationsalgorithmus könnte das Halteproblem lösen (als Spezialfall einer Spezifikation, die man in Bezug auf A machen kann). ==================================== mfg cx


   Profil
Zwerg_Allwissend
Senior Letzter Besuch: im letzten Monat
Dabei seit: 02.12.2013
Mitteilungen: 284
  Beitrag No.7, eingetragen 2019-12-05

\quoteon(2019-12-05 10:29 - carlox in Beitrag No. 6) \quoteon Programm A ----> | Verifikations- | A erfüllt S bzw. Spezifikation S ----> | Algorithmus | A ist inkorrekt \quoteoff > >Was soll das bedeuten? > Zitat: (S.121-122) "Ideen der Informatik" von U. Schöning: ==================================== Das Problem der Programmverifikation ist das Folgende: Gegeben ist ein auf Korrektheit zu analysierenes Programm A. Was es genau heißt, korrekt zu sein, also die Wunschvorstellung, die man von dem Programm A hat, wid formal spezifiziert in eine Spezifikation S. Dies ist eine Ansammlung von Formeln (vgl. Kapitel 5), die Aussagen darüber machen, welche Eigenschaften die im Programm A vorkommenden Variablen nach der Ausführung des Programms A haben sollten - unter Bezugnahme auf die Werte der Variablen, die vor Ausführung des Programms A galten. Die Wunschvorstellung wird durch folgendes Bild dargestellt: +---------------+ Programm A ----> | Verifikations- | --> "Prog. A erfüllt Spez. S" Spezifikation S ----> | Algorithmus | --> "Prog. A ist inkorrekt" +---------------+ Einen solchen Spezifikationsalgorithmus kann es nicht geben. Insbesondere würde er dem Satz von Rice widersprechen. Ein solcher Verifikationsalgorithmus könnte das Halteproblem lösen (als Spezialfall einer Spezifikation, die man in Bezug auf A machen kann). ==================================== \quoteoff Ich hatte ja schon in #3 geantwortet: Falls ein terminierender Verifikationsalgorithmus gemeint ist, dann erhält man nicht nur einen Widerspruch zum Satz von Rice, sondern auch zum 1. Gödelschen Unvolsständigkeitssatz. Dein Beipiel aus #4 ist viel zu kompliziert: Nehme eine Programmiersprache Deiner Wahl, definiere darin die natürlichen Zahlen, die Addition + und die Multiplikation * darauf. Dann hast Du ein Fragment der Arithmetik. Unter den unendlich vielen wahren Aussagen über + und * gibt es nach dem 1. Gödelschen Unvollständigkeitssatz unendlich viele, die ein korrektes Verifikationssystem für die Programmiersprache nicht beweisen kann. Es gibt inzwischen viele, im freien Download erhältliche, Beweissysteme mit denen man Programme verifizieren kann. Diese Systeme sind notwendigerweise alle unvollständig. Die Systeme sind "interaktiv", d.h. wenn der Beweiser eine Aussage nicht beweisen kann, dann kann der Benutzer dem System "helfen". Beweise von einfachen Aussagen, wie Assoziativität, Kommutativität und Distributivität von + und * gelingen automatisch.


   Profil
carlox
Aktiv Letzter Besuch: im letzten Quartal
Dabei seit: 22.02.2007
Mitteilungen: 1382
  Beitrag No.8, vom Themenstarter, eingetragen 2019-12-09

Hallo ZA, 1) \quoteon Ich hatte ja schon in #3 geantwortet: Falls ein terminierender Verifikationsalgorithmus gemeint ist, dann erhält man nicht nur einen Widerspruch zum Satz von Rice, sondern auch zum 1. Gödelschen Unvolsständigkeitssatz. \quoteoff Ich will diesen Widerspruch zeigen unter den Voraussetzungen, die Schöning macht: (siehe die entsprecheden Zitate in diesem Thread): "Einen solchen Spezifikationsalgorithmus kann es nicht geben. Insbesondere würde er dem Satz von Rice widersprechen. Ein solcher Verifikationsalgorithmus könnte das Halteproblem lösen (als Spezialfall einer Spezifikation, die man in Bezug auf A machen kann)." D.h. man muß eine Spezifikation S zu A angeben. wobei A = Algorithmus, der von einer beliebigen, wahren prädikatenlogischen Formel (ohne freie Variablen) den Beweis (Beweisfolge) berechnet. Wie kann man diese Spezifikation S formalisieren ? bzw. wenn es diese Spezifikation S geben würde, warum gibt dann es einen Widerspruch zum Satz von Rice ? 2) \quoteon Dein Beipiel aus #4 ist viel zu kompliziert: \quoteoff Ist es aber korrekt ? mfg cx


   Profil
Zwerg_Allwissend
Senior Letzter Besuch: im letzten Monat
Dabei seit: 02.12.2013
Mitteilungen: 284
  Beitrag No.9, eingetragen 2019-12-10

Das Buch von Herrn Schöning kenne ich nicht. Für weiteres fehlen mir daher die Details. Z.B. habe ich den Begriff "Spezifikationsalgorithmus" noch nie gehört. Am besten fragst Du ihn selbst (per Email). Ob Deine Beweisskizze aus #4 korrekt ist weiß ich nicht, ist mir zu kompliziert zum Nachrechnen.


   Profil
carlox
Aktiv Letzter Besuch: im letzten Quartal
Dabei seit: 22.02.2007
Mitteilungen: 1382
  Beitrag No.10, vom Themenstarter, eingetragen 2019-12-11

\quoteon(2019-12-10 11:42 - Zwerg_Allwissend in Beitrag No. 9) Das Buch von Herrn Schöning kenne ich nicht. \quoteoff Die Bücher von U. Schöning sind wirklich gut! \quoteon Für weiteres fehlen mir daher die Details. Z.B. habe ich den Begriff "Spezifikationsalgorithmus" noch nie gehört. Am besten fragst Du ihn selbst (per Email). Ob Deine Beweisskizze aus #4 korrekt ist weiß ich nicht, ist mir zu kompliziert zum Nachrechnen. \quoteoff Ich werde versuchen, ihn per email zu kontaktieren. mfg cx


   Profil
carlox hat die Antworten auf ihre/seine Frage gesehen.
carlox wird per Mail über neue Antworten informiert.

Wechsel in ein anderes Forum:
 Suchen    
 
All logos and trademarks in this site are property of their respective owner. The comments are property of their posters, all the rest © 2001-2022 by Matroids Matheplanet
This web site was originally made with PHP-Nuke, a former web portal system written in PHP that seems no longer to be maintained nor supported. PHP-Nuke is Free Software released under the GNU/GPL license.
Ich distanziere mich von rechtswidrigen oder anstößigen Inhalten, die sich trotz aufmerksamer Prüfung hinter hier verwendeten Links verbergen mögen.
Lesen Sie die Nutzungsbedingungen, die Distanzierung, die Datenschutzerklärung und das Impressum.
[Seitenanfang]