zu Terminierung WS 1718 nr. 7

Question

Answer 1

Oh je, das ist ein Beispiel, welches meist unterschätzt wird. Ich möchte gleich vorausschicken, dass die angegebene Lösung vermutlich die ist, die erwartet wird und die auch die volle Punktezahl bekommen könnte. Ich würde hier großzügig sein und die Punkte geben (aber das müssen die Korrektoren entscheiden). Die Gedanken dazu sind jedenfalls stimmig und plausibel, aber der Teufel steckt halt doch im Detail.

Der Algorithmus zur binären Suche wird seit 1946 diskutiert und ist erschreckenderweise auch heute noch in den meisten Fällen -- wie auch in diesem -- leider falsch. Die erste korrekte Implementierung gab es erst 1960, aber auch heute noch sind die meisten Implementierungen der binären Suche nicht korrekt und das betrifft auch welche, die sich noch vor kurzem in Klassenbibliotheken befanden. 

Insofern muss man hier auch heute noch mit falschen Implementierungen rechnen, auch wenn diese "verifiziert" worden sind. Verifikation muss halt doch mit Rechnern gemacht werden, wie einem dieses Beispiel eindrücklich zeigt. Ausgangspunkt der Aufgaben ist der folgende Algorithmus, den ich hier in F# kodiert habe:

let rec search (ar:int[]) lo hi x =
    printf "search ar %d %d %d\n" lo hi x
    if hi<lo then -1
    else
        let mid = lo + (hi-lo)/2
        if(x<ar.[mid]) then search ar lo mid x
        elif(ar.[mid]<x) then search ar mid hi x
        else mid

Der angegebene Algorithmus terminert zum Beispiel für die folgende Eingabe nicht, obwohl die angegebenen Vorbedingungen und Beweise sehr plausibel erscheinen:

let ar = [|0;1|]
let lo = 0
let hi = 1
let x = 1

In diesem Beispiel wird zunächst mid = 0 + (0+1)/2 = 0 ausgerechnet und dann ar[0], d.h, 0 mit x=1 verglichen. Da x=1<0=ar[0] falsch und ar[0]=0<1=x wahr ist, kommt es zu einer Endlosschleife in der das vorhandene Element 1 nie gefunden wird.

Schaut man sich den Algorithmus näher an, erkennt man, dass diese Endlosschleife vermieden werden könnte, wenn man bei den rekursiven Aufrufen mid inkrementiert oder dekrementiert, also folgenden Algorithmus verwendet:

let rec search (ar:int[]) lo hi x =
    printf "search ar %d %d %d\n" lo hi x
    if hi<lo then -1
    else
        let mid = lo + (hi-lo)/2
        if(x<ar.[mid]) then search ar lo (mid-1) x
        elif(ar.[mid]<x) then search ar (mid+1) hi x
        else mid

Damit funktioniert das obige Beispiel ohne Endlosschleife. Aber ich traue mich nicht zu sagen, dass dieser Algorithmus nun korrekt wäre. 

Ein weit verbreiteter Fehler bei diesem Algorithmus ist ferner, dass oftmals mid als (lo+hi)/2 berechnet wird. Hierbei ergibt sich ein weiteres Problem: Es kann nämlich passieren, dass lo+hi größer als die größte darstellbare Zahl im Rechner wird und dann negativ wird. Die Berechnung mid = lo + (hi-lo)/2 vermeidet dies und ist daher wirklich wichtig. Auch wenn bei reellen Zahlen (lo+hi)/2 = lo + (hi-lo)/2 gilt, ist dies im Rechner mit integer Werten nicht der Fall. Man muss daher auch bei arithmetischen Optimierungen sehr vorsichtig sein.

Wer mehr dazu lesen mag, dem empfehle ich 

1. BENTLEY, J. : Writing Correct Programs. In: Communications of the ACM 26 (1983), Nr. 12, S. 1040–1045

Answer 2

Noch ein paar Kommentare zur Lösung:

Aufgabenteil a) enthält ein Beispiel, das nicht terminiert. Die Eingaben des Beispiels werden aber von der angegeben Vorbedingung hier nicht eingehalten.

Was noch fehlt ist die Vorbedingung, dass das Eingabearray zwischen "lo" und "hi" den gesuchten Wert enthält.

Allgemein sollte man prüfen, dass zumindest die problematischen Beispiele aus Aufgabenteil a) von der Vorbedingung ausgeschlossen werden.

In Schritt 2 könnte man noch erwähnen, dass mid immer im Bereich [lo, hi) liegt und daher in den Arraygrenzen.

In Schritt 4 sollten beide rekursiven Aufrufe begründet werden.

Gerade wenn man mit der max-Funktion (oder mit Beträgen) rechnet sollte man erklären, warum die Ungleichheit nun gilt.

Wenn man das ordentlich macht, hätte man mit der fehlenden Vorbedingung auch gemerkt, dass man den Beweis so nicht zu Ende führen kann ohne die Vorbedingung zu stärken.

Comments

Wenn man diesen Kontext dazu kennt, kann man nicht mehr ganz so großzügig mit den Punkten sein ....