Maßterme...

[oren78]

Sei folgende prozedur gegeben, wobei die implementierung von \(+\) vorrausgesetzt ist:

Code: Alles auswählen

function mystery(n : ℕ) : ℕ <=
if ?0(n)
  then 0
  else if ?0(⁻(n))
         then 1
         else if ?0(⁻(⁻(n)))
                then 1
                else mystery(⁻(n)) + mystery(⁻(⁻(n)))
              end_if
       end_if
end_if

verifun kann "mystery" problemlos automatisch beweisen....jedoch wäre ich hier an dem maßterm intressiert!
unter "termination details/ chosen measure terms" findet sich nur ein: $[n] - also nicht sehr hilfreich

mir ist schon klar das das, was bei jedem rekursionsschritt kleiner wird im prinzip die n sind...
Die menge der substitutionen müsste (hoffe ich) so aussehen: \(\Delta := \lbrace \lbrace n/pred(n) \rbrace, \lbrace n/pred(pred(n)) \rbrace \rbrace\)
aber n ist definitiv nicht der richtige maßterm

nach der expliziten (geschlossenen) Formel von Moivre-Binet (siehe Wiki: \(http://de.wikipedia.org/wiki/Fibonacci-Folge\))
haben wir es hier mit einem exponentiellen ausdruck zu tun, das heißt also das solche lustigen maßterme wie:
\(\lbrace n, \sum \limits_{i=1}^{n} i, n^{n}, \ldots \rbrace\) hier auch nicht viel bringen werden...

daher die frage, wie ermittelt man bei solchen zusammengesetzten rekursiven prozeduren die maßterme...?

[mister_tt]

aber n ist definitiv nicht der richtige maßterm

Warum denn nicht? DEN richtigen Maßterm gibt es ja eh nicht... Man kann ja die Terminierung durchaus mit unterschiedlichen Maßtermen beweisen, was manchmal auch Sinn macht, um mehrere Induktionsprinzipien ableiten zu können...

[oren78]

aber n ist definitiv nicht der richtige maßterm

Warum denn nicht? DEN richtigen Maßterm gibt es ja eh nicht... Man kann ja die Terminierung durchaus mit unterschiedlichen Maßtermen beweisen, was manchmal auch Sinn macht, um mehrere Induktionsprinzipien ableiten zu können...

hmmm, wenn das so ist dann müsste doch folgendes gelten:

Code: Alles auswählen

 ( n > pred(n) + pred(pred(n)) > pred(pred(n)) + pred(pred(pred(pred(n)))) > ... )

nun setze ich für n folgendes ein, n = 6 dann gilt wohl hoffentlich NICHT das folgende:

Code: Alles auswählen

 ( 6 > pred(6) + pred(pred(6)) > pred(pred(6)) + pred(pred(pred(pred(6)))) > ... )

 ( 6 > (5 + 4) > (4 + 2) > ... )

n ist also doch nicht angebracht...

[mister_tt]

Kann sein, hab ja auch noch nicht gelernt

Meine zweite Idee wäre n + n...

[pigbird]

n ist doch richtiger Massterm. Ausgehend von der Relation Description:

Code: Alles auswählen

{<{?0(n)}, {}>,
 <{?⁺(n),?0(⁻(n))}, {}>,
 <{¬ ?0(n),¬ ?0(⁻(n))}, {{n : ⁻(n)},{n : ⁻(⁻(n))}}>}

zu zeigen ist also n > pred(n) und n > pred(pred(n)), NICHT n > pred(n) + pred(pred(n))

[oren78]

n ist doch richtiger Massterm. Ausgehend von der Relation Description:

Code: Alles auswählen

{<{?0(n)}, {}>,
 <{?⁺(n),?0(⁻(n))}, {}>,
 <{¬ ?0(n),¬ ?0(⁻(n))}, {{n : ⁻(n)},{n : ⁻(⁻(n))}}>}

zu zeigen ist also n > pred(n) und n > pred(pred(n)), NICHT n > pred(n) + pred(pred(n))

hmmm...dann hab ich da was ganz essentielles nicht verstanden. Ich nahm bisher an, das ein maßterm der größte wert ist, welcher
zu anfang einer rekursion bzgl. der parameter existiert und das alles was die prozedur in jedem schritt ausgibt kleiner sein muss als dieser term...
beispiel: wenn ich also n = 7 eingebe, erhalte ich den fibonacci wert 13 was also größer ist als n selber...

anderes beispiel, die funktion length:

Code: Alles auswählen

function length(k : list[ℕ]) : ℕ <=
if ?ø(k)
  then 0
  else succ(length(tl(k)))
end_if

hier ist der maßterm die länge von der liste k - im grunde also length(k) selbst, da eben der eingabeparameter k durch tl(k)
in jedem schritt kleiner wird...bei der fibonacci funktion haben wir zwar, jeweils pred(n) und pred(pred(n)) aber ich dachte man müsste die
summe hierfür nehmen, da eben sonst die ausgabe größer wird als die eingabe...

also, um es mal informell festzuhalten: WAS GENAU ist nun ein maßterm und in welcher beziehung steht dieser zu den eingabeparametern...???

[mister_tt]

zu zeigen ist also n > pred(n) und n > pred(pred(n)), NICHT n > pred(n) + pred(pred(n))

Genau, so war das

Ein Maßterm ist das, was beim rekursiven Aufruf kleiner wird. Und das ist bei der Funktion nun mal das n...

[Simon Siegler]

Sei folgende prozedur gegeben, wobei die implementierung von \(+\) vorrausgesetzt ist:

Code: Alles auswählen

function mystery(n : ℕ) : ℕ <=
if ?0(n)
  then 0
  else if ?0(⁻(n))
         then 1
         else if ?0(⁻(⁻(n)))
                then 1
                else mystery(⁻(n)) + mystery(⁻(⁻(n)))
              end_if
       end_if
end_if

Dies ist Beispiel 2 aus Kapitel 8 (Folie 11), zum Terminierungsbeweis reicht der Maßterm "n" tatsächlich aus.

Ein Maßterm ist zunächst einfach ein Term vom Typ nat, der nur die formalen Parameter der Prozedur als Variablen enthält. Damit definiert ein Maßterm eine Maßfunktion für die aktualen Parameter eines Aufrufs der Prozedur. Für den Terminierungsbeweis wird nun gezeigt, dass die aktualen Parameter jedes Aufrufs der Prozedur bezüglich der Maßfunktion größer sind als die aktualen Parameter der rekursiven Aufrufe. Formal wird dies in Kapitel 8/Folie 15 beschrieben.

Zwischen Maßtermen und den Ergebnissen rekursiver Aufrufe besteht im Allgemeinen kein Zusammenhang.

[oren78]

Dies ist Beispiel 2 aus Kapitel 8 (Folie 11), zum Terminierungsbeweis reicht der Maßterm "n" tatsächlich aus.

Ein Maßterm ist zunächst einfach ein Term vom Typ nat, der nur die formalen Parameter der Prozedur als Variablen enthält. Damit definiert ein Maßterm eine Maßfunktion für die aktualen Parameter eines Aufrufs der Prozedur. Für den Terminierungsbeweis wird nun gezeigt, dass die aktualen Parameter jedes Aufrufs der Prozedur bezüglich der Maßfunktion größer sind als die aktualen Parameter der rekursiven Aufrufe. Formal wird dies in Kapitel 8/Folie 15 beschrieben.

Zwischen Maßtermen und den Ergebnissen rekursiver Aufrufe besteht im Allgemeinen kein Zusammenhang.

vielen dank für die aufklärung, ich denke jetzt weiß ich endlich bescheid