Löst das Anhalten Problem einfacher als Leute denken?

Question

Obwohl der allgemeine Fall unentscheidbar ist, lösen viele Menschen immer noch Probleme, die für den täglichen Gebrauch gut genug sind.

In Cohen's Doktorarbeit über Computerviren zeigte er, wie Virenscanning dem Stillstandproblem entspricht, aber wir haben eine ganze Industrie, die auf dieser Herausforderung basiert.

Ich habe auch Microsofts Terminator Projekt gesehen - http://research.microsoft.com/Terminator/

Was mich zu fragen, führt - wird das Halteproblem überbewertet - tun wir über den allgemeinen Fall kümmern?

Werden Typen im Laufe der Zeit vollständig turing - abhängige Typen scheinen eine gute Entwicklung zu sein?

Oder, um weg zu schauen, werden wir beginnen, nicht turing volle Sprachen zu verwenden, um die Vorteile der statischen Analyse zu nutzen?

Answer 1

Das Halting-Problem ist eigentlich nur interessant, wenn man es im allgemeinen Fall betrachtet, denn wenn das Halting-Problem entscheidbar wäre, wären alle anderen unentscheidbaren Probleme auch durch Reduktion entscheidbar.

Also, meine Meinung zu dieser Frage ist, nein, es ist nicht einfach in den Fällen, die von Bedeutung sind. Das heißt, in der realen Welt ist es vielleicht keine so große Sache.

Siehe auch: http://en.wikipedia.org/wiki/Halting_problem#Importance_and_consequences

Answer 2

Als Tag zu Tag Programmierer, würde ich sagen, es lohnt sich, wie weit unten auf der Weg fortzusetzen zögernden Stil Probleme zu lösen, auch wenn Sie nur diese Grenze nähern und erreiche es nie. Wie Sie hervorgehoben haben, erweist sich das Scannen von Viren als wertvoll. Die Google-Suche gibt nicht die absolute Antwort auf "finde das beste X für Y", aber sie ist auch besonders nützlich. Wenn ich einen neuartigen Virus (muwahaha) entfessle, schafft das dann eine größere Lösungsmenge oder wirft man nur ein Licht auf einen bestehenden Problembereich? Ungeachtet des technischen Unterschieds werden einige pragmatisch Folgedienste für "Erkennung und Entfernung" entwickeln und Gebühren erheben.

Ich freue mich auf echte wissenschaftliche Antworten auf Ihre Fragen ...

Answer 3

löst das Halteproblem leichter als die Leute denken?

Ich denke, es ist genau so schwierig wie die Leute denken.

Werden die Typen im Laufe der Zeit vollständig turing?

My dear, they already are!

abhängige Typen wie eine gute Entwicklung scheinen?

Sehr sehr.

Ich denke, es könnte ein Wachstum in nicht-Turing vollständig, aber beweisbare Sprachen geben. SQL war lange Zeit in dieser Kategorie (es ist nicht mehr), aber das hat seinen Nutzen nicht wirklich verringert. Es gibt sicherlich einen Platz für solche Systeme, denke ich.

Answer 4

Übrigens denke ich, dass die Turing-Vollständigkeit der Vorlagen zeigt, dass das Anhalten überbewertet wird. Die meisten Sprachen garantieren, dass ihre Compiler aufhören werden; nicht so C++. Verringert dies C++ als Sprache? Ich denke nicht; es hat viele Fehler, aber kompiliert, die nicht immer anhalten, sind nicht einer von ihnen.

Answer 5

Ich weiß nicht, wie hart Leute denken, dass es ist, also kann ich nicht sagen, ob es einfacher ist. Sie haben jedoch Recht, dass die Unentscheidbarkeit eines Problems (im Allgemeinen) nicht bedeutet, dass alle Fälle dieses Problems unentscheidbar sind. Zum Beispiel kann ich Ihnen leicht sagen, dass ein Programm wie while false do something endet (unter der Annahme der offensichtlichen Semantik von while und false).

Projekte wie das Terminator-Projekt, das Sie erwähnt haben, existieren offensichtlich (und funktionieren wahrscheinlich sogar in einigen Fällen), also ist es klar, dass nicht alles hoffnungslos ist. Es gibt auch einen Wettbewerb (ich glaube jedes Jahr) für Werkzeuge, die versuchen, die Beendigung für Rewrite-Systeme zu beweisen, die im Grunde ein Modell der Berechnung sind. Aber in vielen Fällen ist eine Kündigung sehr schwer nachzuweisen.

Der einfachste Weg, um es zu betrachten, ist vielleicht, die Unentscheidbarkeit als ein Maximum an Komplexität der Instanziierungen eines Problems zu sehen. Jede Instanziierung ist irgendwo auf der Skala von trivial zu diesem Maximum und mit einem höheren Maximum haben Sie typischerweise, dass die Instanziierungen im Durchschnitt auch härter sind.

Answer 6

Es gibt viele Programme, bei denen das Halteproblem gelöst werden kann und viele dieser Programme nützlich sind.

Wenn Sie einen Compiler hätten, der Ihnen "Halt", "Halt nicht" oder "Weiß nicht" sagen würde, könnte er Ihnen sagen, welcher Teil des Programms den "Halt" oder "Don" verursacht hat. Ich weiß "Zustand. Wenn Sie wirklich ein Programm wollten, das definitiv angehalten oder nicht gestoppt wurde, dann würden Sie diese "Weiß nicht" -Einheiten auf die gleiche Weise reparieren, wie wir Compiler-Warnungen loswerden. Ich denke, wir wären alle überrascht, wie oft es sich als nützlich erwies, dieses allgemein unmögliche Problem zu lösen.

Answer 7

Wow, das ist eine verwirrte Frage.

Erstens: Das Halteproblem ist im praktischen Sinne kein "Problem", wie in "ein Problem, das gelöst werden muss". Es ist vielmehr eine Aussage über das Wesen der Mathematik, analog zu Gödels Unvollständigkeitssatz.

Zweitens: Die Tatsache, dass der Aufbau eines perfekten Virenscanners schwierig ist (weil er dem Halting-Problem entspricht), ist genau der Grund, warum "eine ganze Industrie um diese Herausforderung herum aufgebaut ist". Wenn ein Algorithmus für ein perfektes Virenscannen entwickelt werden könnte, wäre es einfach eine Person, die es einmal tun würde, und dann gibt es keine Notwendigkeit für eine Industrie mehr. Geschichte vorbei.

Drittens: Arbeiten in einem Turing Komplette Sprache eliminiert nicht "die Vorteile der statischen Analyse" - es bedeutet lediglich, dass der statischen Analyse Grenzen gesetzt sind. Das ist in Ordnung - es gibt sowieso Grenzen für fast alles, was wir tun.

Endlich: Wenn das Halteproblem in irgendeiner Weise "gelöst" werden könnte, wäre es definitiv "einfacher als die Leute denken", wie Turing gezeigt hat, dass es unlösbar ist. Der allgemeine Fall ist aus mathematischer Sicht der einzig relevante Fall. Sonderfälle sind Ingenieursfragen.

Answer 8

Die Tatsache, dass ein Problem unentscheidbar ist, bedeutet nicht, dass es nicht interessant ist: im Gegenteil! Also ja, die Tatsache, dass wir kein effektives und einheitliches Verfahren haben, um die Kündigung für alle Programme (sowie viele andere Probleme über Software) zu adressieren bedeutet nicht, dass es nicht lohnt, nach Teillösungen zu suchen.In gewissem Sinne brauchen wir deshalb Software-Engineering: Weil wir die Aufgabe nicht einfach an Computer delegieren können.

Der Titel Ihrer Frage ist jedoch ein wenig irreführend. Ich stimme Dr.Pizza zu: Das Kündigungsproblem ist genau so schwierig, wie die Leute denken. Darüber hinaus bedeutet die Tatsache, dass wir uns nicht unbedingt mit dem allgemeinen Fall befassen müssen, nicht, dass das Beendigungsproblem überbewertet wird: es lohnt sich, nach Teillösungen zu suchen weil wir wissen, dass die allgemeine Lösung schwierig ist.

Schließlich sind die Probleme über abhängige Typen und subrecursive Sprachen, obwohl teilweise verwandt, wirklich andere Fragen, und ich bin nicht sicher, den Punkt zu sehen, sie alle zusammen zu mischen.