1  a := 1
2  y := n
3  while a < y && A[a] + A[ y] ≠ x do
4      if A[a] + A[ y] < x
5      then a := a + 1
6      else y := y − 1

Teh­tä­vä:
Kah­den sum­ma

Ly­hyt Math­Check-oh­je (uu­teen vä­li­leh­teen)

Tau­luk­ko A[1…n] on kas­va­vas­sa suu­ruus­jär­jes­tyk­ses­sä. Ohei­sen al­go­rit­min teh­tä­vä­nä on löy­tää sii­tä kak­si al­kio­ta, joi­den sum­ma on x.

1  a := 1
2  y := n
3  while a < y && A[a] + A[ y] ≠ x do
4      if A[a] + A[ y] < x
5      then a := a + 1
6      else y := y − 1

Huo­maat­ko, et­tä vaa­ti­mus­mää­rit­te­lym­me on hie­man epä­tark­ka? Esi­merk­ki syöt­tees­tä, jol­la et­si­tyt al­kiot ovat toi­sen tul­kin­nan mu­kaan ole­mas­sa ja toi­sen tul­kin­nan mu­kaan ei­vät ole, löy­tyy täs­täA = [1, 3, 4] ja x = 6. Vaa­ti­mus­mää­rit­te­ly on epä­tark­ka si­kä­li, et­tä …Täl­lai­sis­sa ti­lan­teis­sa ei ai­na ole sel­vää, saa­vat­ko mai­ni­tut kak­si al­kio­ta ol­la sa­ma al­kio. Kun sa­no­taan ”kah­den pa­rit­to­man lu­vun sum­ma on ai­na pa­ril­li­nen”, niin ne lu­vut saa­vat ol­la sa­ma lu­ku. Jos pyy­dät mi­nua mai­nit­se­maan kak­si eläin­tä, niin var­maan­kin hy­väk­syt vas­tauk­sek­si ”koi­ra ja kis­sa” mut­ta et hy­väk­sy ”koi­ra ja koi­ra”.

Kir­joi­ta seu­raa­vat väit­teet.

• A:ssa on kak­si eri al­kio­ta, joi­den sum­ma on x.
  ok_text Oi­kein! array_claim A[1...n] index x hide_expr ∃ i: ∃ j; 1 ≤ i < j ≤ n: A[i]+A[j] = x ⇔
  tai
• A:ssa on kak­si eri­suur­ta al­kio­ta, joi­den sum­ma on x.
  ok_text Oi­kein! array_claim A[1...n] index x hide_expr ∃ i: ∃ j; 1 ≤ i < j ≤ n: A[i]≠A[j] ∧ A[i]+A[j] = x ⇔
  tai
• A:ssa on kak­si al­kio­ta, joi­den sum­ma on x. Ne ei­vät vält­tä­mät­tä ole eri al­kio.
  ok_text Oi­kein! array_claim A[1...n] index x hide_expr ∃ i: ∃ j; 1 ≤ i ≤ j ≤ n: A[i]+A[j] = x ⇔
  tai

Käy­täm­me jat­kos­sa tul­kin­taa ”kak­si eri al­kio­ta, jot­ka saa­vat ol­la yh­tä­suu­ret”.

Olet­taen, et­tä al­go­rit­mi toi­mii oi­kein, mil­lä tes­til­lä voi­daan sen lo­pe­tet­tua sel­vit­tää, on­ko eh­dot täyt­tä­vää al­kio­pa­ria ole­mas­sa? Siis kir­joi­ta tes­ti, jo­ka voi­daan li­sä­tä al­go­rit­min lop­puun, ja jo­ka tuot­taa T, jos ja vain jos on ole­mas­sa kak­si eri al­kio­ta (jot­ka saa­vat ol­la yh­tä­suu­ret), joi­den sum­ma on x. ok_text Oi­kein! fail_text #<i#>A#</i#>[#<i#>a#</i#>] + #<i#>A#</i#>[ #<i#>y#</i#>] = #<i#>x#</i#> ei toi­mi jos #<i#>A#</i#> = [1, 3, 4] ja #<i#>x#</i#> = 6. f_nodes 3 modulo 5 hide_expr a < y ⇔
tai

Sil­mu­kan oi­keak­si to­dis­ta­mi­ses­sa käy­te­tään usein vii­si­koh­tais­ta me­ne­tel­mää:

1. Kek­si­tään väi­te, jo­ta kut­su­taan sil­muk­ka­in­va­rian­tik­si.
2. Osoi­te­taan, et­tä se pä­tee kun sil­muk­kaan tul­laan sil­mu­kan edel­tä.
3. Osoi­te­taan, et­tä jos se ja sil­mu­kan eh­to pä­te­vät kun ol­laan sil­mu­kan alus­sa, niin se pä­tee myös kun ol­laan uu­del­leen sil­mu­kan alus­sa. Toi­sin sa­noen osoi­te­taan, et­tä sil­mu­kan kier­ros ei voi saa­da in­va­riant­tia pois voi­mas­ta.
4. Osoi­te­taan, et­tä sil­muk­kaa ei voi­da kier­tää lo­put­to­mas­ti.
5. Osoi­te­taan, et­tä jos in­va­riant­ti pä­tee ja sil­mu­kan eh­to ei pä­de, niin sil­mu­kan lop­pu­tu­lok­sel­ta ha­lut­tu asia pä­tee.

Usein kan­nat­taa aloit­taa tun­nis­ta­mal­la hel­pos­ti pää­tel­tä­vis­sä ole­via asioi­ta, joil­la voi to­dis­taa esi­mer­kik­si et­tä sil­muk­ka ei tee mi­tään lai­ton­ta ja et­tä se py­säh­tyy lo­pul­ta. Kir­joi­ta mah­dol­li­sim­man vah­va a:ta ja y:tä mut­ta ei A:ta ei­kä x:ää kos­ke­va väi­te, jo­ka on voi­mas­sa ai­na kun suo­ri­tus on ri­vin 3 alus­sa. Math­Check hy­väk­syy tä­hän koh­taan si­säl­löl­li­ses­ti eri­lai­sia väit­tei­tä, kun­han ne ovat tie­tyl­tä loo­gi­sel­ta vä­lil­tä. Kun tul­kit­set Math­Checkin an­ta­mia vir­he­il­moi­tuk­sia, ota huo­mioon, et­tä oma kaa­va­si voi ol­la se­kä ”left” et­tä ”right”.
ok_text Oi­kein il­man ruk­sia! fail_text Ri­vin 3 alus­sa voi pä­teä #<i#>a#</i#> = #<i#>y#</i#>. f_nodes 17 modulo 19 hide_expr 1 ≤ a ≤ y ≤ n ∨ a=1 ∧ y=n ⇐ ⇐ hide_expr 1 ≤ a ≤ y ≤ n tai

Lai­ta tä­hän pik­ku­laa­tik­koon ruk­si ja ko­kei­le edel­li­sen ky­sy­myk­sen na­peil­la, kel­paa­ko edel­li­sen ky­sy­myk­sen vas­tauk­se­si yhä. Jos ei kel­paa, niin syy­nä on mel­ko var­mas­ti se, et­tä vas­tauk­se­si ei pä­de erääs­sä eri­kois­ta­pauk­ses­sa, jo­ka on tau­lu­koil­le mah­dol­li­nen, mut­ta jo­ka jää hel­pos­ti huo­maa­mat­ta tä­män­kal­tai­ses­sa ti­lan­tees­sa. Se eri­kois­ta­paus on …tyh­jä tau­luk­ko eli n = 0.

Yleis­lin­jas­ta poik­kea­vat eri­kois­ta­pauk­set häi­rit­se­vät usein pa­has­ti pää­ta­pauk­sen kä­sit­te­lyä. Sik­si on ta­val­lis­ta kä­si­tel­lä sel­lai­set erik­seen ja olet­taa pää­ta­pauk­sen koh­dal­la, et­tä ei ol­la niis­sä. Toi­mii­ko al­go­rit­mi oi­kein edel­lä mai­ni­tus­sa eri­kois­ta­pauk­ses­sa? Pe­rus­te­le vas­tauk­se­si. Open vas­tausKyl­lä toi­mii. Kun n = 0, tau­luk­ko on tyh­jä ei­kä et­sit­ty­jä al­kioi­ta ole. Sil­loin al­go­rit­mi lo­pet­taa he­ti saa­vut­tuaan en­sim­mäi­sen ker­ran ri­vil­le 3, ja a:n ja y:n ar­vois­ta nä­kyy edel­lä ole­val­la tes­til­lä, et­tä nii­tä ei ole. Täs­tä eteen­päin ole­tam­me, et­tä ok_text Oi­kein! f_nodes 3 modulo 5 hide_expr n > 0 ⇔
tai

Olet­taen, et­tä ei ol­la edel­lä mai­ni­tus­sa eri­kois­ta­pauk­ses­sa, kir­joi­ta mah­dol­li­sim­man vah­va a:ta ja y:tä mut­ta ei A:ta ei­kä x:ää kos­ke­va väi­te, jo­ka on voi­mas­sa ai­na kun suo­ri­tus on ri­vin 3 alus­sa.
ok_text Oi­kein! fail_text Ri­vin 3 alus­sa voi pä­teä #<i#>a#</i#> = #<i#>y#</i#>. f_nodes 7 modulo 19 hide_expr 1 ≤ a ≤ y ≤ n ⇔ tai

Al­go­rit­mi lo­pet­taa var­mas­ti, kos­ka …Jo­kai­sel­la kier­rok­sel­la y − a pie­ne­nee yh­del­lä, kos­ka jo­ko a kas­vaa yh­del­lä il­man et­tä y muut­tuu, tai y vä­he­nee yh­del­lä il­man et­tä a muut­tuu. Al­go­rit­mi lo­pet­taa vii­meis­tään kun y − a = 0.

Tä­mä a:ta ja y:tä kos­ke­va väi­te ta­kaa myös, et­tä (olet­taen, et­tä lu­ku­alue ei lo­pu kes­ken) al­go­rit­mi ei kos­kaan suo­ri­ta mi­tään lai­ton­ta. Mi­ten se sen te­kee? …Se ta­kaa, et­tä tau­lu­kon A in­dek­sit ovat ai­na lail­li­sia. Muu­ta po­ten­tiaa­li­ses­ti lai­ton­ta al­go­rit­mi ei tee (olet­taen, et­tä lu­ku­alue ei lo­pu kes­ken).

Alam­me nyt tut­kia, mik­si al­go­rit­mi löy­tää mi­tä pi­tää­kin. Al­go­rit­min suun­nit­te­li­ja lie­nee tar­koit­ta­nut, et­tä jo­kai­nen eh­dot täyt­tä­vä al­kio­pa­ri si­jait­see vä­lil­lä a, …, y. Tar­kas­tam­me, on­ko tä­mä omi­nai­suus in­va­riant­ti.

Kun sil­muk­kaan tul­laan sen edel­tä, väi­te on tri­viaa­lis­ti tot­ta, kos­ka …Sil­loin vä­li a, …, y kat­taa ko­ko tau­lu­kon. In­va­rian­til­ta vaa­dit­tu omi­nai­suus 2 siis to­teu­tuu.

Omi­nai­suu­den 5 to­dis­ta­mi­sek­si on osoi­tet­ta­va, et­tä sil­mu­kan lo­pe­tet­tua jo­ko A[a] ja A[ y] muo­dos­ta­vat eh­dot täyt­tä­vän al­kio­pa­rin tai sel­lais­ta ei ole ole­mas­sa, ja et­tä va­lin­ta näi­den kah­den vä­lil­tä mää­räy­tyy sii­tä, pä­tee­kö a < y. Jos sil­mu­kan lo­pe­tet­tua a < y, niin al­go­rit­mi lo­pet­ti sik­si, et­tä …A[a] + A[ y] = x Jos sil­mu­kan lo­pe­tet­tua ¬(a < y), niin …Vä­lin a, …, y pi­tuus on enin­tään 1, jo­ten vä­liin ei mah­du kah­ta eri al­kio­ta. Sik­si eh­dot täyt­tä­vää al­kio­pa­ria ei ole ole­mas­sa.

Jäl­jel­lä on omi­nai­suus 3. Sil­mu­kan var­ta­los­sa jo­ko a kas­vaa tai y vä­he­nee, ei­kä sii­nä ta­pah­du mi­tään muu­ta. On osoi­tet­ta­va, et­tä tä­mä ei voi pois­taa in­va­riant­tia voi­mas­ta.

• Tar­kas­te­lem­me en­sin ta­paus­ta, jos­sa a kas­vaa. Niin käy, jos ja vain jos ri­vil­lä 3 pä­tee
  ok_text Oi­kein! array_claim A[1...n] index a index y hide_expr 1 ≤ a < y ≤ n ∧ A[a]+A[y] < x ⇔ 1 ≤ a < y ≤ n ∧
  tai
  On osoi­tet­ta­va, et­tä a:n ar­vo en­nen kas­vua ei voi ol­la eh­dot täyt­tä­vän al­kio­pa­rin osa­puo­li. Sii­tä, et­tä A on kas­va­vas­sa suu­ruus­jär­jes­tyk­ses­sä, seu­raa, et­tä A[a] + A[ j] < x, kun 1 ≤ a < y ≤ n ja
  ok_text Oi­kein! hide_expr modulo 5 1 ≤ j ≤ y ⇔
  tai
  Kun A[a] + A[ j] < x, pä­tee myös A[a] + A[ j] ≠ x. Vie­lä tar­vi­taan
  ok_text Oi­kein! array_claim A[1...n] index a index y hide_expr 1 ≤ a < y ≤ n ∧ ∀ j; y < j ≤ n: A[a]+A[j] ≠ x ⇔ 1 ≤ a < y ≤ n ∧.
  Se saa­daan sii­tä, et­tä …In­va­rian­tik­si tar­koi­tet­tu väi­te lu­paa, et­tä vä­lil­lä y + 1, …, n si­jait­se­vat al­kiot ei­vät muo­dos­ta eh­dot täyt­tä­vää pa­ria min­kään al­kion kans­sa, ja niin ol­len ei­vät al­kion A[a] kans­sa.
  tai

  Niin­pä A[a] ei voi muo­dos­taa eh­dot täyt­tä­vää pa­ria min­kään al­kion kans­sa. Sik­si a:n voi jät­tää pois et­sin­tä­alueel­ta.

• Ta­paus, jos­sa y pie­ne­nee, on hy­vin sa­man­kal­tai­nen. Sii­tä, et­tä A on kas­va­vas­sa suu­ruus­jär­jes­tyk­ses­sä, seu­raa (älä käy­tä ope­raat­to­ria ≠)
  ok_text Oi­kein! array_claim A[1...n] index a index y hide_expr 1 ≤ a < y ≤ n ∧ ∀ i; a ≤ i ≤ n: A[i]+A[y] > x ⇔ 1 ≤ a < y ≤ n ∧.
  Lo­put A[i] ei­vät voi muo­dos­taa eh­dot täyt­tä­vää al­kio­pa­ria A[ y]:n kans­sa, kos­ka …In­va­rian­tik­si tar­koi­tet­tu väi­te lu­paa, et­tä vä­lil­lä 1, …, a − 1 si­jait­se­vat al­kiot ei­vät muo­dos­ta eh­dot täyt­tä­vää pa­ria min­kään al­kion kans­sa, ja niin ol­len ei­vät al­kion A[ y] kans­sa. Sik­si y:n voi jät­tää pois et­sin­tä­alueel­ta.
  tai

Omi­nai­suu­den 3 ja sa­mal­la ko­ko al­go­rit­min to­dis­tus on val­mis.

Tä­hän voit kir­joit­taa juu­ri to­dis­ta­mam­me sil­muk­ka­in­va­rian­tin kaa­va­na. Kaa­vas­sa on niin pal­jon muut­tu­jia, et­tä Math­Checkil­lä saat­taa men­nä muu­ta­ma se­kun­ti sen tar­kas­ta­mi­ses­sa.
ok_text Oi­kein! array_claim A[1...n] index a index y 1 ≤ a ≤ y ≤ n ∧ ∀ i: ∀ j; 1 ≤ i < j ≤ n: A[i]+A[j] ≠ x ∨ a ≤ i < j ≤ y ⇔ 1 ≤ a ≤ y ≤ n ∧ ( )
tai