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)

Täs­sä teh­tä­väs­sä to­dis­te­taan eräs no­pea al­go­rit­mi oi­kein toi­mi­vak­si. Tar­koi­tuk­se­na on har­joi­tel­la oh­jel­mis­ta päät­te­le­mis­tä.

Al­go­rit­mi ja sen teh­tä­vä

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 b_nodes 17 f_nodes 25 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 b_nodes 23 f_nodes 27 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 b_nodes 17 f_nodes 21 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ä yk­sin­ker­tai­sel­la 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? Tes­ti voi­daan li­sä­tä al­go­rit­min lop­puun, ja se 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. Tes­tis­sä ei käy­te­tä muut­tu­jaa A[…]. Kir­joi­ta täl­lai­nen tes­ti. ok_text Oi­kein! fail_text Älä käy­tä muut­tu­jaa #<i#>A#</i#>[…]! f_nodes 3 presburger hide_expr a < y ⇔
tai

To­dis­tus­me­ne­tel­mä

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, y:tä ja n:ää 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. Teh­tä­vän hel­pot­ta­mi­sek­si ole­ta, et­tä tau­luk­ko ei ole tyh­jä. Vih­je 1Mi­kä on a:n ar­vo kun ri­vil­le 3 tul­laan en­sim­mäi­sen ker­ran, ja mi­ten se ke­hit­tyy sen jäl­keen? Vih­je 2Mi­kä on y:n ar­vo kun ri­vil­le 3 tul­laan en­sim­mäi­sen ker­ran, ja mi­ten se ke­hit­tyy sen jäl­keen? Vih­je 3Mi­ten a:n ja y:n ar­vot suh­tau­tu­vat toi­siin­sa, jos läh­de­tään uu­del­le kier­rok­sel­le? En­tä jos ei läh­de­tä?
ok_text Oi­kein! f_nodes 7 presburger hide_expr 1 ≤ a ≤ y ≤ n ⇔ tai

Tä­män koh­dan ta­voit­tee­na on ha­vain­nol­lis­taa, et­tä yleis­lin­jas­ta poik­kea­vat eri­kois­ta­pauk­set voi­vat häi­ri­tä pa­has­ti pää­ta­pauk­sen kä­sit­te­lyä. Vas­taa uu­del­leen edel­li­sen koh­dan ky­sy­myk­seen, mut­ta nyt älä luo­ta sii­hen, et­tä tau­luk­ko ei ole tyh­jä.
ok_text Oi­kein! f_nodes 17 presburger hide_expr 1 ≤ a ≤ y ≤ n ∨ a = 1 ∧ y = n = 0 ⇔ tai

Sik­si on ta­val­lis­ta kä­si­tel­lä sel­lai­set eri­kois­ta­pauk­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 kun tau­luk­ko A[…] on tyh­jä? Pe­rus­te­le vas­tauk­se­si. Open vas­tausKyl­lä toi­mii. Kun tau­luk­ko on tyh­jä, n = 0 ei­kä et­sit­ty­jä al­kioi­ta ole. 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ä mai­ni­tul­la tes­til­lä a < y, et­tä nii­tä ei ole.

Täs­tä eteen­päin ole­tam­me, et­tä ok_text Oi­kein! f_nodes 3 presburger hide_expr n > 0 ⇔
tai

Saim­me äs­ken yl­lä mai­ni­tul­la ole­tuk­sel­la, et­tä tä­mä1 ≤ a ≤ y ≤ n pä­tee ai­na kun suo­ri­tus on ri­vin 3 alus­sa. Se ta­kaa, 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).

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. (Se saa ol­la ti­la­päi­ses­ti pois voi­mas­ta sil­mu­kan kier­rok­sen ol­les­sa kes­ken.)
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.

Me­ne­tel­män koh­ta 4

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.

Me­ne­tel­män koh­ta 1

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 pyr­ki sii­hen, 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 koh­ta, on­ko tä­mä omi­nai­suus in­va­riant­ti. Si­tä en­nen kui­ten­kin kir­joi­tam­me sen kaa­va­na, kos­ka täl­lä kurs­sil­la nyt vaan ker­ta kaik­kiaan har­joi­tel­laan kaa­vo­ja, kos­ka nii­den käyt­tö pal­jas­taa pii­le­viä vää­rin­ym­mär­ryk­siä ajois­sa.

Va­li­tet­ta­vas­ti val­mii­seen kaa­vaan tu­li­si niin pal­jon muut­tu­jia, et­tä vas­taus­ten tar­kas­ta­mi­nen kuor­mit­tai­si yli­opis­ton pal­ve­lin­ta lii­kaa. Sik­si älä käy­tä al­la muut­tu­jaa x, vaan kir­joi­ta sen si­jaan 2.

Il­mai­se ”eh­dot täyt­tä­vä al­kio­pa­ri” kaa­va­na. Käy­tä in­dek­sei­nä i ja j.
ok_text Oi­kein! array_claim A[1...n] f_nodes 23 1 <= i <= n /\ 1 <= j <= n /\ i != j /\ A[i]+A[j] = 2 ⇔ tai

Il­mai­se kaa­va­na ”jos al­kio­pa­ri täyt­tää eh­dot, niin se si­jait­see vä­lil­lä 2, …, 3”. (Pal­ve­li­men kuor­mi­tuk­sen vä­hen­tä­mi­sek­si alueen rajoina ovat 2 ja 3 eivätkä a ja y.) Käy­tä nyt­kin in­dek­sei­nä i ja j.
ok_text Oi­kein! array_claim A[1...n] index i index j f_nodes 35 1 <= i <= n /\ 1 <= j <= n /\ i != j /\ A[i]+A[j] = 2 --> 2 <= i <= 3 /\ 2 <= j <= 3 ⇔ tai

Il­mai­se kaa­va­na ”jo­kai­nen eh­dot täyt­tä­vä al­kio­pa­ri si­jait­see vä­lil­lä a, …, y”. Muut­tu­jien a ja y ar­vo­aluet­ta kos­ke­van eh­don pi­tää ol­la kaa­vas­sa mu­ka­na.
ok_text Oi­kein! array_claim A[1...n] index a index y f_nodes 45 b_nodes 33 1 ≤ a ≤ y ≤ n ∧ ∀ i: ∀ j; 1 ≤ i < j ≤ n: A[i]+A[j] ≠ 2 ∨ a ≤ i < j ≤ y ⇔ tai

Täs­tä eteen­päin kir­joi­ta x:n pai­kal­le x ei­kä 2.

Me­ne­tel­män koh­ta 2

Kun sil­muk­kaan tul­laan sen edel­tä, äs­ken kir­joit­ta­mam­me in­va­riant­ti on tri­viaa­lis­ti tot­ta, kos­ka …Sil­loin vä­li a, …, y kat­taa ko­ko tau­lu­kon, kos­ka a = 1 ja y = n. In­va­rian­tin kaa­vas­sa tä­mä nä­kyy si­ten, et­tä jo­kai­sel­la i ja j, joil­la pä­tee 1 ≤ i < j ≤ n, pä­tee myös a ≤ i < j ≤ y ja sa­mal­la ko­ko kvan­ti­fioi­tu osuus. Me­ne­tel­män koh­ta 2 on val­mis.

Me­ne­tel­män koh­ta 5

Me­ne­tel­män koh­das­sa 5 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. Myös on osoi­tet­ta­va, 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. Al­kiot A[a] ja A[ y] ovat eri al­kio, kos­ka …a ≠ y kos­ka a < y.

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.

Me­ne­tel­män koh­ta 3

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ä ta­pah­du mui­ta muu­tok­sia muut­tu­jien ar­vois­sa. 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! f_nodes 15 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. On siis osoi­tet­ta­va, et­tä ∀ j; 1 ≤ j ≤ n: A[a] + A[ j] ≠ x.

  Saam­me tä­män osal­le j:n ar­vois­ta edel­li­sen koh­dan vas­tauk­ses­ta ja sii­tä, et­tä A on kas­va­vas­sa suu­ruus­jär­jes­tyk­ses­sä. Niis­tä seu­raa A[a] + A[ j] < x, mis­tä vä­lit­tö­mäs­ti seu­raa A[a] + A[ j] ≠ x. Mil­le j:n ar­voil­le saam­me tä­män?
  ok_text Oi­kein! f_nodes 5 hide_expr presburger 1 ≤ j ≤ y ⇔
  tai
  Vie­lä tar­vi­taan
  ok_text Oi­kein! f_nodes 22 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 ∧ ∀ j;: A[a] + A[j] ≠ x.
  Se saa­daan sii­tä, et­tä …In­va­riant­ti 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. Niin­pä ne ei­vät muo­dos­ta sel­lais­ta al­kion A[a] kans­sa.
  tai

  Olem­me osoit­ta­neet, et­tä 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. Kir­joi­ta kaa­va, jo­ka sa­noo, mi­tä täs­sä ta­pauk­ses­sa on osoi­tet­ta­va. Ar­vo­aluet­ta ra­jaa­van eh­don voi täs­sä ta­pauk­ses­sa aja­tel­la eri ta­voil­la tuot­taen eri lop­pu­tu­lok­sia. Jot­ta se ei han­ka­loit­tai­si vas­taa­mis­ta, lai­toin eh­don puo­les­ta­si val­miik­si.
  ok_text Oi­kein! f_nodes 20 array_claim A[1...n] index y hide_expr 1 < y ≤ n ∧ ∀ i; 1 ≤ i ≤ n: A[i] + A[y] ≠ x ⇔ 1 < y ≤ n ∧
  tai
  Muut­tu­jan y ar­vo pie­ne­nee, jos ja vain jos ri­vil­lä 3 pä­tee (muis­ta ar­vo­aluet­ta kos­ke­va eh­to)
  ok_text Oi­kein! f_nodes 15 array_claim A[1...n] index a index y hide_expr 1 ≤ a < y ≤ n ∧ A[a]+A[y] > x ⇔
  tai

  Mik­si edel­li­ses­sä koh­das­sa ei käy­tet­ty ri­vin 4 if-lau­seen eh­don A[a] + A[ y] < x ne­gaa­tio­ta A[a] + A[ y] ≥ x? Vas­tausKun A[a] + A[ y] = x, niin ri­vil­le 6 ei men­nä, kos­ka ei men­nä edes ri­vil­le 4.

  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] f_nodes 22 f_ban !=; index a index y hide_expr 1 ≤ a < y ≤ n ∧ ∀ i; a ≤ i ≤ n: A[i]+A[y] > x ⇔ 1 ≤ a < y ≤ n ∧
  tai

  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­riant­ti 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.

  Olem­me osoit­ta­neet, et­tä y:n voi jät­tää pois et­sin­tä­alueel­ta.

Me­ne­tel­män koh­ta 3 ja sa­mal­la ko­ko al­go­rit­min to­dis­tus on val­mis.