fun f (x, y) = if (x + y) < 0 then ~1 else 1 + f(x + 2, y - 3)
Beweisen Sie, dass die Berechnung von f(x, y) für alle Werte
(x, y) 2 Z × Z terminiert.
Dies soll mit Induktion bewiesen werden. Ich vermute mit Hilfe einer Abstiegsfunktion, aber genau davon habe ich keine Ahnung. Wie sucht man so eine Funktion und mit welchen Kriterien?
p.s der Code ist in SML NJ geschrieben aber betrachtet den ruhig als Pseudo-Code^^
