[GCL] Staart invarianten

[Verwijderd]

Na wat zoeken op GOT kwam ik een aantal topics tegen over het formeel bewijzen van repetitie op basis van een invariant. Hieruit kan ik afleiden dat er dus wel een aantal specialisten op dit forum aanwezig zijn (Overigens weet ik niet of dit het goede forum daarvoor is, maar Programming en formuleren van algoritmen liggen volgens mij dicht bij elkaar ).

Helaas moet ik nog steeds een tentamen doen over de basis van GCL, o.a. het bewijzen van lineaire repetities, (in)homogene staart invarianten en Lineair Search, Binaire Search en Slope Search.

Lineaire repetitie, zoals constante segment problemen e.d., lijk ik nu wel te begrijpen. Helaas heb ik nog geen kaas gegeten van staart invarianten. Het lijkt me dat als ik een staart invariant onder de knie heb, dat ik dan ook wel in staat moet zijn om de verschillende Search algoritmen te begrijpen.

Nu heb ik hier al een mooi voorbeeld van een staart invariant gevonden. Helaas wordt het niet verder uitgelegd of er op ingegaan.

Wat wil ik nu?
De uitleg op de universiteit (TU/e) is allemaal heel leuk, maar graag zou ik het wat concreter (lees: door een student) uitgelegd zien, zodat ik daarna alle abstracten theorie (hopelijk) wat beter kan begrijpen. Ik begrijp dat er twee soorten staart invarianten zijn (uit mijn blote hoofd, vertel het me als ik fout zit, want zoals ik al meldde heb ik er weinig kaas van gegeten):
- homogeen: invariant is bekend
- inhomogeen: invariant is niet bekend, vorm het gevraagde om naar

code:

resultaat = (wat er al gedaan is) 0 (wat er nog moet gebeuren)

met 0; een associatieve operator (? ofwel, elke mogelijke operator?)

Een homogene staart invariant, zou ik nog wel uit moeten komen. Zijn een Linear Search en een Binairy Search geen homogene staart invarianten?

Van een inhomogene staart invariant heb ik het volgende voorbeeld. Helaas gaat mij dit te snel:

code:

f:0 = 1; f:1 = 13; f:2 = 37
f:(n + 3) = f:n - f:(n + 2) for n >= 0

In de uitwerking, wordt vervolgens de volgende invariant voorgesteld:

code:

mu.a.b.c.n = a * f:n + b * f:(n+1) + c * f:(n+2)

In de les heb ik begrepen dat je bijvoorbeeld f.13 moet nemen, en deze vervolgens moet unfolden. Dat is niet wat ze hier doen (volgens mij). Kan iemand mij vertellen hoe ze aan deze invariant komen? En is er een mogelijkheid om een andere invariant te krijgen o.b.v. unfolding?

Een heel verhaal, maar hopelijk kan iemand mij het één en ander verduidelijken.

[ Voor 3% gewijzigd door Verwijderd op 07-06-2006 10:37 ]

[Ivo]

Wat ze bedoelen met het ``unfolden'' van een f.x is dat je dan ziet wat het patroon is. Dit kan je helpen bij het vinden van een invariant. Het idee is het volgende: Je stelt als invariant dat f.N gelijk is aan een of andere expressie. Die expressie in je voorbeeld is dus mu.a.b.c.n.

code:

f.N = mu.a.b.c.n

Je initialiseert een invariant (meestal zijn er vele mogelijkheden), zodat deze triviaal waar is. In het voorbeeld is je intialisatie bijvoorbeeld:

code:

a := 1;
b := 0;
c := 0;
n := N;

De invariant geldt nu.
Nu ga je kijken wat er gebeurt als je n verlaagt. Hoe moet je a,b,c aanpassen bij een verlaging van n? Je gaat dus gewoon zitten rekenen totdat je f.(n-1) uitgedrukt hebt als a'*f.n + b'*f.(n+1) + c'*f.(n+2). De waarden van a', b' en c' respectievelijk vormen dan je assignments aan a,b en c. Als je niet uit deze laatste stap komt wil ik het wel uitrekenen.

[ Voor 4% gewijzigd door Ivo op 07-06-2006 10:48 ]

[Soultaker]

Ik heb geen idee wat een 'staartinvariant' is (een invariant voor het laatste deel van een recursieve functie?) maar je voorbeeld lijkt me meer een differentievergelijking. Ik ken de termen homogeen/inhomogeen ook wel van differentiaalrekening, maar niet in programmeer-context.
Een differentievergelijking van de vorm:
x_n + a₁x_n-1 + a₂x_n-1 + .. + + a_kx_n-k = f_n
noemt men simpelweg homogeen als f_n is 0.

[Ivo]

Ik heb die term homogeen/inhomogeen ook nooit gehoord in programmeercontext en ik studeer zelf ook aan de TU/e.

Ik was trouwens de laatste stap van mijn uitleg vergeten, want je moet ook nog weten wat nu het resultaat is. Dit weet je zodra n=0, want de f.0, f.1 en f.2 zijn bekend. Volgens de invariant staat er dan iets als:

code:

f.N = a*f.0 + b*f.1 + c*f.2

Hieruit kun je je resultaat bepalen.

Edit: Soultaker: Hier een verhaal over staartrecursie als het je interesseert: http://en.wikipedia.org/wiki/Tail_recursion

Een staartinvariant is simpelweg een invariant, waarbij je resultaat gelijk is aan een deel wat bekend is en een deel wat nog berekend moet worden. Op het moment dat je deel dat nog berekend moet worden leeg is ben je klaar.

[ Voor 36% gewijzigd door Ivo op 07-06-2006 11:30 ]

[Verwijderd]

Ivo schreef op woensdag 07 juni 2006 @ 11:11:
Ik heb die term homogeen/inhomogeen ook nooit gehoord in programmeercontext en ik studeer zelf ook aan de TU/e.

Zo staat het in hoofdstuk 7 van Bijlsma's lecture notes. Vraag mij niet waarom

Ivo schreef op woensdag 07 juni 2006 @ 11:11:
Een staartinvariant is simpelweg een invariant, waarbij je resultaat gelijk is aan een deel wat bekend is en een deel wat nog berekend moet worden. Op het moment dat je deel dat nog berekend moet worden leeg is ben je klaar.

Dus als ik je goed begrijp is elke tail invariant van de vorm:

code:

resultaat = (wat er al gedaan is) 0 (wat er nog moet gebeuren)

Wat ik vaak niet begrijp (en dat is ook zo bij de voorbeelden van Anne Kaldewaij: Derivations of Algorithms) is dat ze een invariant nemen (zoals die in mijn voorbeeld), maar dan niet even fijn uitleggen hoe je eraan komt.

Die invariant in de link in mijn startpost, is wel duidelijk G.x.y = x^y

[Ivo]

Dat is het punt waar je wat creatief voor moet zijn, maar bij dit soort (jouw voorbeeld) recursieve definities waar de f.(n+x) gelijk is aan de c1*f.(n) + c2*f.(n+1) + ... + cx*f.(n+x-1), dan is je invariant gewoon f.n = c1*f.0 + c2*f.1 + ... + cx*f.(x-1).

[Grijze Vos]

Afgelopen jaar is er nogal wat omgegooid bij de vakken "Ontwerp van Algoritmen X" (voorheen Programmeren X). De stof is ook ietwat veranderd. Ik zal eens kijken of ik iets zinnigs vind in dat boek van Kaldewaij, anders moet ik kijken of ik mijn aantekeningen nog ergens kan vinden. (kan niks beloven)

[ Voor 6% gewijzigd door Grijze Vos op 07-06-2006 14:41 ]

[Verwijderd]

Het is me nu wel wat meer helder, in die zin dat je eigenlijk van te voren moet bepalen wat het betekent als "je klaar bent" en als "er nog iets overblijft, dus nog niet klaar". (Dit is anders dan lineair, omdat je in dat geval dan 'domweg' n ophoogt met 1.)

Maar dat is dus als je de invariant al beschikbaar hebt. Wanneer ik bijvoorbeeld een patroon moet ontdekken in:

code:

f.0 = 1; f.1 = 13; f.2 = 37
f.(n + 3) = f.n - f.(n + 2) for n >= 0

Dan zou ik bijvoorbeeld f.4 nemen (even heel simpel):

code:

f.4
=
f.(1+3)
=
f.1 - f.(1+2)
= {is dit nu niet: f.1 = "het deel wat je al weet", f.(1+2) = "het deel wat nog moet"?}
f.1 - f.3
=
f.1 - ( f.(0+3) )
=
f.1 - ( f.0 -f.2 )

Ook wanneer ik nu met bijv. f.13 zou beginnen, kom ik nooit uit op een patroon van de vorm a * f.n + b * f.(n+1) + c * f.(n+2)

Of mis ik nu iets?

Grijze Vos schreef op woensdag 07 juni 2006 @ 14:33:
Afgelopen jaar is er nogal wat omgegooid bij de vakken "Ontwerp van Algoritmen X" (voorheen Programmeren X). De stof is ook ietwat veranderd.

Was inderdaad niet zo'n mooie actie van de TU/e. Ik doe zelf het schakelprogramma en ben in 2004 begonnen. Toen kreeg ik nog ontwerp van algoritmen van Feijen en was het de helft minder stof waarvoor we twee keer zoveel tijd kregen. Maar ja.

[Grijze Vos]

Verwijderd schreef op woensdag 07 juni 2006 @ 15:11:
Was inderdaad niet zo'n mooie actie van de TU/e. Ik doe zelf het schakelprogramma en ben in 2004 begonnen. Toen kreeg ik nog ontwerp van algoritmen van Feijen en was het de helft minder stof waarvoor we twee keer zoveel tijd kregen. Maar ja.

Met de notie dat je een onvoldoende had als je een dom foutje maakte. Ikzelf heb gelukkig die serie vakken al afgesloten. Dat boek van kaldewaij staat het idd niet zo duidelijk in, en ik heb mijn aantekeningen niet kunnen vinden, helaas.