offizieller terminierungsthread

Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

offizieller terminierungsthread
vielleicht koennen wir die ganzen fragen / antworten etwas ordnen
==> alle sachen zur terminierung hier rein.

damit kommt auch schon die erste frage, und zwar zur klausur vom 3.4.97, aufgabe 5b):

da ist eine diff-fkt. folgendermassen definiert:

             |0               fuer x<=y
diff (x,y) = {
             |diff(x,y-1) + 1 sonst

meiner verinnerlichten standardloesung folgend wuerde ich schreiben:

             |0               fuer x<=y
t (x,y)    = {
             |y               sonst

c0(x,y) => t(x,y)=0
c1(x,y) => t(x,y)=y > t(x',y') = t(x,y-1) = y-1   >= 0

allerdings stimmt das ganze nicht, deshalb hab ich mir die ursprungsfunktion nochmal angeschaut: ich wuerde sagen, sie soll den abstand zwischen zwei zahlen ausrechnen (und damit im endeffekt die differenz). fuer die anfangswerte x und y gibt es zwei moeglichkeiten:

  1. x > y: dann wird y immer weiter runtergezaehlt und die terminierungsbedingung greift nie, y wird immer kleiner und negativ und es gibt eine endlosschleife, die nie terminiert!

  2. x <= y: dann greift die terminierungsbedingung sofort und es kommt sofort 0 raus!

das kann doch nicht sinn der sache sein, oder? kann das sein, dass da eigentlich die bedingung x >= y heissen muesste? der witz ist, drueber steht, dass man zeigen soll, dass die funktion terminiert. das impliziert, DASS sie terminiert.

vielleicht habe ich das ganze auch einfach nur falsch verstanden, ich muss dazusagen, ich glaube terminierungsfunktionen erst seit ca. 20 min zu verstehen :).


ich will ja nicht gleich mit der tuer ins haus fallen, aber noch eine zweite frage ist in einem anderen thread gestellt worden, die mich auch brennend interessiert:

wie definiert man formal die terminierungsfunktion?


Naja, y-1 is zwar kleiner als y, aber ob des immer >=0 is, weiß ich net, da man ja nur weiß, dass x > y ist im 2. Fall. D.h. mit x+y, kommt man glaub ich besser hin, weil es dann heißt:

c1(x,y)=>t(x,y)=x-y > t(x’,y’)=t(x,y-1)=x+y-1 und dass is >=0, da x>y, d.h. x-y>=1, damit is x+y-1>=0


@Steppenwolf

Also ich denke mal, dass die Angabe falsch ist, weil so wie die Funktion auf dem Blatt steht, macht sie wenig Sinn.
Wenn die Abbruchbedingung x = y heißen würde, müsste aber auch t(x,y)=y funktionieren.
Da z.B. für diff(0,1) die Terminierungsfunktion so aussieht:
t(0,1) = 1 > t(0,0) = 0

Zu deiner zweiten Frage. Ich würde die Definition so hinschreiben, wie sie im Skript steht.


@dawell:

hmm, klingt nicht schlecht, allerdings verstehe ich nicht, wie du eine terminierungsfunktion angeben konntest, ohne dass die ursprungsfunktion ueberhaupt terminiert!

btw:

da muesste es x+y heissen, nachdem was du drueber geschrieben hast, oder?


thx, da bin ich also nicht der einzige, der sie, so wie sie dasteht, nicht versteht.
und zur def. meinst du, soll man einfach die allgemeine terminierungsfunktion hinbatzen. den „beweis“ mit der unendlichen folge, die es in n0 nicht gibt, auch?

btw: habe noch eine meiner meinung nach nicht terminierende funktion gefunden: klausur 6.10.93, aufgabe 5b, sum.
schaut euch die mal an und sagt mir, wofuer die gut sein soll und wie die terminieren soll?!


Freilich muss es x+y heißen, ich Depp.

Naja, habs halt nach Schema gemacht, stimmt schon, eigentlich terminiert die Funktion wirklich nicht, da ja für x>y x ja nicht kleiner wird, bzw y größer. Seltsam…


Zur 5b:
Is eigentlich des selbe, aber da ja dortsteht, dass die Funktion terminiert und man es nur beweisen soll, muss es dann auch so ähnlich gehen:

t(a,b)={0 für a<b, a-b sonst

c0(a,b)=> t(a,b)=0
c1(a,b)=> t(a,b)=a-b>t(a’,b’)=t(a,b-1)=a-b-1>=0

Hier gehts mit minus, müsste oben auch gehen.


Diese sum(a,b) Funktion terminiert auch nicht und man kann dafür keine Terminierungsfunktion angeben.

Das sieht schon mal sehr gut aus, weil für den Fall c1(a,b) die 0 nie Unterschritten wird. Der Witz bei den Terminierungsfunktionen ist aber (wenn ich das richtig verstanden habe), dass die Funktion irgendwann in den Fall c0(a,b) laufen soll, was diese Funktion aber niemals tun wird, wenn man a>b wählt, da ich in jedem Schritt das b um 1 erniedrige und damit der Fall a>b immer gegeben sein wird. Damit wird c0(a,b) nie erreicht und wir haben die unerwünschte Endlosschleife.

Wenn das kein Druckfehler ist, dann scheint man das evtl. bewusst so gemacht zu haben, um die Studenten hinters Licht zu führen.


da müsste auf jeden fall x>= y stehn… sonst macht das gar keine sinn! UNd dann stimmt auch die terminierungsfunktion t(x y): 0 (c0) / y (c1)

ich stime the void absolut zu…


hmm, aber du hast dich da etwas vertan: t(a’,b’) ist bei deiner terminierungsfunktion (a-b) doch dann (a-(b-1))=a-b+1 und damit groesser als t(a,b)?!
also irgendwie nerven mich diese terminierungsfunktionen. aber was macht ihr, wenn in der klausur so eine nicht terminierende funktion drankommt? einfach schema runterrattern und das ganze ignorieren, oder hinschreiben, dass es nicht terminiert und man somit keine terminierungsfunktion hinschreiben kann?


Ja, kann sein, dass ich die Klammer nach dem Minus übersehen hab.
Ich würd des Schema einfach nehmen, wenn ne nicht-terminierende Funktion drankommt.


Ich würde ein Aufrufbeispiel nennen, für das die Funktion nicht terminiert.

Falls genug Zeit bleiben sollte, würde ich die geg. Funktion so modifizieren, daß sie Sinn ergibt und dafür dann eine Terminierungsfunktion angeben.


jetzt mal im ernst: es macht doch keine sinn in ner Klausur zu verlangen, für eine nicht-terminierende Funktion einen Terminierungsbeweis anzugeben…

…ich würde mir jetzt da mal keine allzu großen gedanken machen. :smiley:


das klingt doch mal nach einer guten strategie! das wird wohl das sinnvollste sein. einfach nur das schema hinbatzen, obwohl die funktion nicht terminiert, zeigt wohl kaum, dass man es verstanden hat. allerdings bin ich mir da bei mir auch nicht so sicher …

@tsunami: ja, hoffen wir das beste. das waere am einfachsten, wenn halt einfach terminierende funktionen drankommen.


bin ich jetzt blöd?
kannst du mir bitte mal verraten, wo du diese „formale definition“ im skript gefunden hast? ich würd die auch gerne auswendig lernen…
(dass ich wenigstens etwas weiß)


ich denk mal, er meint damit einfach die allgemeine terminierungsfunktion! oder? die werde ich jedenfalls hinschreiben:

betrachte f(x,y) …

definiere eine funktion t(x,y) …
wobei fuer alle (x,y) gelten muss …


eine “allgemeine terminierungsfunktion”??
ich dachte, es gibt noch nichtmal zu einer funktion f eine eindeutige lösung… wie sieht dann die allgemeine lösung aus?

für f(x) = x
→ t(x) = 0
oder wie?

ich hab einfach keine ahnung, wie man auf diese blöden termiten da kommen soll… ich denk ich vergess das jetzt einfach und schau am dienstag halt mal, ob ich da in dem speziellen fall zufällig eine geistige erleuchtung erfahren sollte… soll ja vorkommen. ging mir schon ein paar mal so, dass ich was erst in einer prüfung verstanden hab und dann zum ersten mal eine solche aufgabe lösen konnte!


@Yves
Das steht doch im Skript irgendwo so definiert:

         | g(x)             <= c0(x,y)
f(x,y) = {
         | h(...f(x'y')...) <= c1(x,y)

Und das ist total korrekt, wenn du dafür eine Terminierungsfunktion finden kannst, die wiefolgt definiert ist:

         | 0               <= c0(x,y)
t(x,y) = {
         |t(x',y')<t(x,y)  <= c1(x,y)

(Ich denke das <t(x,y) muss mit rein, weil der Funktionswert von t(x’y’) kleiner sein muss als t(x,y) ).

So ist das allgemein hingeschrieben.
Und du musst für t(x,y) eigentlich nur irgendeine x-beliebige Funktion finden, hauptsache t(x’y’) < t(x,y).

Und das Teil terminiert deswegen, weil damit irgendwie eine noethersche Partialordnung auf den Natürlichen Zahlen beschrieben wird. Und da man in den natürlichen Zahlen nicht unendlich weit absteigen kann (bei 0 ist Schluss, also bei c0(x,y)), ist damit gezeigt, dass die Funktion terminiert.