Maßterme...

Benutzeravatar
oren78
BSc Spammer
BSc Spammer
Beiträge: 1373
Registriert: 17. Nov 2006 17:47
Wohnort: Darmstadt

Maßterme...

Beitrag von 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...?
"Unter allen menschlichen Entdeckungen sollte die Entdeckung der Fehler die wichtigste sein.", Stanisław Jerzy Lec

mister_tt
Kernelcompilierer
Kernelcompilierer
Beiträge: 502
Registriert: 29. Sep 2008 15:54

Re: Maßterme...

Beitrag von mister_tt »

oren78 hat geschrieben: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...

Benutzeravatar
oren78
BSc Spammer
BSc Spammer
Beiträge: 1373
Registriert: 17. Nov 2006 17:47
Wohnort: Darmstadt

Re: Maßterme...

Beitrag von oren78 »

mister_tt hat geschrieben:
oren78 hat geschrieben: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... :D 8)
"Unter allen menschlichen Entdeckungen sollte die Entdeckung der Fehler die wichtigste sein.", Stanisław Jerzy Lec

mister_tt
Kernelcompilierer
Kernelcompilierer
Beiträge: 502
Registriert: 29. Sep 2008 15:54

Re: Maßterme...

Beitrag von mister_tt »

Kann sein, hab ja auch noch nicht gelernt :D

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

pigbird
Windoof-User
Windoof-User
Beiträge: 26
Registriert: 28. Apr 2008 23:34

Re: Maßterme...

Beitrag von 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))

Benutzeravatar
oren78
BSc Spammer
BSc Spammer
Beiträge: 1373
Registriert: 17. Nov 2006 17:47
Wohnort: Darmstadt

Re: Maßterme...

Beitrag von oren78 »

pigbird hat geschrieben: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...???
"Unter allen menschlichen Entdeckungen sollte die Entdeckung der Fehler die wichtigste sein.", Stanisław Jerzy Lec

mister_tt
Kernelcompilierer
Kernelcompilierer
Beiträge: 502
Registriert: 29. Sep 2008 15:54

Re: Maßterme...

Beitrag von mister_tt »

pigbird hat geschrieben: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
Computerversteher
Computerversteher
Beiträge: 369
Registriert: 16. Apr 2007 09:12

Re: Maßterme...

Beitrag von Simon Siegler »

oren78 hat geschrieben: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.

Benutzeravatar
oren78
BSc Spammer
BSc Spammer
Beiträge: 1373
Registriert: 17. Nov 2006 17:47
Wohnort: Darmstadt

Re: Maßterme...

Beitrag von oren78 »

Simon Siegler hat geschrieben: 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 ;-)
"Unter allen menschlichen Entdeckungen sollte die Entdeckung der Fehler die wichtigste sein.", Stanisław Jerzy Lec

Antworten

Zurück zu „Archiv“