7.6A programkonstrukciók és a kiszámíthatóság

Ebben az alfejezetben kis kitérőt teszünk a kiszámíthatóság-elmélet felé, és megmutatjuk, hogy az imént bevezetett három programkonstrukció segítségével minden – elméletileg megoldható – feladatot meg tudunk oldani. Ehhez kapcsolatot létesítünk a kiszámítható függvények és a „jól konstruált” programok között.

7.6.1Parciális rekurzív függvények

A Church tézis szerint a kiszámítható függvények halmaza megegyezik a parciális rekurzív függvények halmazával. A kiszámíthatóság ezen modelljében csak típusú függvények szerepelnek. Először az alapfüggvényeket definiáljuk:

  • :

  • :

  • :

A továbbiakban definiálunk néhány elemi függvény-operátort: Kompozíció Legyen és . Az és kompozíciója az alábbi függvény:

, és :

Vegyük észre, hogy ez az operátor megegyezik az alapfogalmaknál bevezetett relációk közötti kompozícióval (tulajdonképpen a szigorú kompozícióval, de függvények esetén ez a kettő azonos). Unió Legyen rögzített, és . E függvények uniója és :

Rekurzió Legyen rögzített, és . Az függvény szerinti rekurziója , és

A függvényhez hasonlóan rekurzívan definiálhatnánk ennek a függvénynek az értelmezési tartományát, de ez kívül esik a jelenlegi vizsgálódásunk körén. Ezért csak azt mondjuk, hogy az értelmezési tartomány azon pontok halmaza, ahonnét kiindulva a fenti rekurzió elvégezhető. -operátor Legyen . A -operátort erre a függvényre alkalmazva azt a függvényt kapjuk, amelyre , és :

A fenti alapfüggvények és a bevezetett operátorok segítségvel már definiálható a parciális rekurzív függvények halmaza.

7.6. Definíció (PARCIáLIS REKURZíV FüGGVéNY).

Az függvény akkor és csak akkor parciális rekurzív, ha az alábbiak egyike teljesül:

  • az alapfüggvények valamelyike

  • kifejezhető a fenti operátorok parciális rekurzív függvényekre történő alkalmazásával.

7.6.2A parciális rekurzív függvények kiszámítása

Ahhoz, hogy a fenti függvényeket kiszámító programokat tudjunk adni, definiálnunk kell az ilyen függvények által meghatározott feladatot. Legyen egy tetszőleges függvény ( rögzített). Az által meghatározott feladat specifikációja:

Most megmutatjuk, hogy minden parciális rekurzív függvény által meghatározott feladat megoldható „jól konstruált” programmal (jól konstruáltnak tekintünk egy programot, ha elemi programokból a fenti három konstrukcióval megkapható). A bizonyításhoz csak annyit kell feltételeznünk, hogy az alapfüggvények kiszámíthatók (megengedett) elemi programokkal.

A fenti feltételezést felhasználva elegendő azt megmutatni, hogy az elemi függvény-operátorok (kompozíció, unió, rekurzió, -operátor) kiszámíthatók jól konstruált programokkal.

Kompozíció

Legyen és . Ekkor az által meghatározott feladat specifikációja:

Jelöljük -mel azt a programot, amely kiszámítja -et, és hasonlóan -nel azt, amelyik kiszámítja -t. Tegyük fel, hogy ez a két program vagy elemi értékadás, vagy jól konstruált program. Ebben az esetben a két program szekvenciája kiszámítja -et, azaz megoldja a fent specifikált feladatot. Legyen a második program utófeltételhez tartozó leggyengébb előfeltétele:

Most vizsgáljuk meg az első program ezen utófeltételhez tartozó leggyengébb előfeltételét:

Könnyen látható, hogy ez a leggyengébb előfeltétel következik -ból, és így a szekvencia levezetési szabálya és a specifikáció tételének alkalmazásával beláttuk, hogy a

program megoldja a fent specifikált feladatot, azaz kiszámítja és kompozícióját.

Unió

Legyen rögzített, és . Ekkor az e függvények uniója által meghatározott feladat specifikációja:

Tegyük fel, hogy a komponens függvények kiszámíthatók jól konstruált programmal, vagy elemi értékadással. Jelölje az -edik függvényt kiszámító programot. Ekkor ezeknek a programoknak a szekvenciája megoldja a fenti feladatot. Legyen a -adik program utófeltételhez tartozó leggyengébb előfeltételét:

Továbbá minden esetén jelölje az -edik program -hez tartozó leggyengébb előfeltételét. Könnyen látható, hogy az értékadás leggyengébb előfeltételére vonatkozó szabályt alkalmazva:

Ha most -t és -et összehasonlítjuk, észrevehetjük, hogy megegyeznek. A szekvencia levezetési szabálya és a specifikáció tétele alapján a

program megoldása a fent specifikált feladatnak, azaz kiszámítja -t.

Rekurzió

Legyen rögzített, és . Tegyük fel, hogy mindketten kiszámíthatók jól konstruált programokkal vagy egyszerű értékadásokkal. Az függvény szerinti rekurziója által meghatározott feladat specifikációja:

Jelölje az -et és a -t kiszámító programot illetve . Oldjuk meg a feladatot egy olyan ciklussal, amelynek invariáns tulajdonsága:

A ciklus levezetési szabályát vizsgálva azt találjuk, hogy -ból nem következik . Ezért adunk egy olyan feltételt, amelyből már következik , és adunk egy programot, amely -ból -be jut (így a megoldóprogram egy szekvencia lesz, amelynek második része egy ciklus). Legyen az alábbi:

Ez a szimultán értékadással elérhető. Az értékadás leggyengébb előfeltételére vonatkozó szabály felhasználásával könnyen látható, hogy az következik -ból.

A ciklus levezetési szabályának második pontja alapján a ciklusfeltétel lesz.

A harmadik pontnak megfelelően válasszuk a kifejezést termináló függvénynek.

Az ötödik pont azt írja le, hogy az imént definiált termináló fügvény értékének a ciklusmagban csökkennie kell. Ez elérhető a eggyel való növelésével.

A négyes pont kielégítéséhez vizsgáljuk meg, hogy mi lesz a leggyengébb előfeltétele a -t növelő értékadásnak a -re vonatkozóan.

Most már – a szekvencia levezetési szabálya alapján – csak egy olyan programot kell találnunk, amelyre . Ez a program a rekurzió definíciójához illeszkedően épp lesz.

Így a szekvencia és a ciklus levezetés szabálya valamint a specifikáció tétele garantálja, hogy a

program megoldja a által meghatározott feladatot, azaz kiszámítja szerinti rekurzióját.

-operátor

Legyen , és tegyük fel, hogy kiszámítható egyszerű értékadással vagy jól konstruált programmal. Tekintsük a által meghatározott feladatot:

Jelölje az -et kiszámító programot. Oldjuk meg a feladatot egy olyan ciklussal, melynek invariánsa:

Az invariáns a szimultán értékadással teljesíthető. Könnyen látható, hogy ennek a programnak a -re vonatkozó leggyengébb előfeltétele

következik -ból. A ciklus levezetési szabályának második pontja alapján a ciklusfeltétel lesz.

A feladat előfeltétele garantálja, hogy van olyan szám, amelyre fennáll. Legyen egy ilyen tulajdonságú, rögzített természetes szám. Ennek az értéknek a segítségével definiálhatjuk a termináló függvényt: . Ez kielégíti a levezetés szabály harmadik pontját.

Az ötödik pont megkívánja, hogy a termináló függvény a ciklusmag lefutása során csökkenjen. Ezt elérhetjük eggyel való növelésével.

A negyedik pont teljesítéséhez legyen ennek a növelésnek a -re vonatkozó leggyengébb előfeltétele:

Most már csak találnunk kell egy programot a és állítások közé. A értékadásra teljesül, hogy

A specifikáció tétele, valamint a ciklus és a szekvencia levezetési szabálya garantálja, hogy a

program megoldja a által meghatározott feladatot, azaz kiszámítja -et.

7.6.3Következmény

Az előzőekben megmutattuk, hogy ha az alapfüggvények kiszámíthatók egyszerű értékadással, akkor a belőlük – a parciális rekurzív függvényeknél megengedett – operátorokkal felépített függvények kiszámíthatók jól konstruált programokkal. A Church tézis szerint a kiszámítható függvények halmaza megegyezik a parciális rekurzív függvények halmazával. Ezek alapján kimondhatjuk az alábbi tételt:

7.6. TéTEL: STRUKTURáLT PROGRAMOZáS éS KISZáMíTHATóSáG Minden kiszámítható függvény kiszámítható egy jól konstruált programmal.

7.6.4Relációk

Eljutván az előző tételhez, fordítsuk most figyelmünket a relációk felé. Ahhoz, hogy a relációk kiszámíthatóságát megvizsgálhassuk, definiálnunk kell a kiszámítható reláció fogalmát.

7.2. Definíció (REKURZíVAN FELSOROLHATó RELáCIó).

Legyen tetszőleges reláció. akkor és csak akkor rekurzívan felsorolható, ha van olyan parciális rekurzív függvény, amelynek értelmezési tartományára: .

A kiszámíthatóság-elmélethez igazodva, a továbbiakban csak rekurzívan felsorolható relációkkal fogunk foglalkozni. Ahhoz, hogy megmutassuk, hogy minden kiszámítható (rekurzívan felsorolható) feladat – emlékezzünk, hogy minden feladat egy reláció – megoldható strukturált programmal, először megadjuk a rekurzívan felsorolható relációk egy másik jellemzését.

7.2. TéTEL: KLEENE[1936] Ha egy tetszőleges reláció, akkor az alábbi három állítás ekvivalens:

  1. rekurzívan felsorolható

  2. egy parciális rekurzív függvény értékkészlete

  3. vagy egy rekurzív függvény értékkészlete.

Ennek a tételnek a bizonyítása lásd Ref??? konstruktív, azaz megadja mind , mind pedig felépítését. Mi ezt a függvényt fogjuk használni a kiszámítható feladatunk megoldóprogramjában.

Legyen egy rekurzívan felsorolható reláció, és jelölje az előző tétel konstrukciójával kapott (totális) rekurzív függvényt. Specifikáljuk a feladatot az alábbi módon:

Ez a feladat megoldható egy olyan ciklussal, amelynek invariáns tulajdonsága:

A ciklus levezetési szabályának felhasználásával könnyen belátható, hogy az alábbi program megoldása a fenti feladatnak:

A bizonyításban a termináló függvény megadásánál ugyanazt a technikát alkalmazzuk, mint a -operátornál.

Ezzel az előzőleg függvényekre kimondott tételünket általánosíthatjuk relációkra:

7.3. TéTEL: STRUKTURáLT PROGRAMOZáS éS KISZáMíTHATó RELáCIóK Minden kiszámítható reláció kiszámítható egy jól konstruált programmal.

Megjegyzés

Az egyetlen feltevés, amit a fenti meggondolásokban használtunk az volt, hogy az alapfüggvények kiszámíthatóak. Így aztán ezek az eredmények kiterjeszthetők a relatíve kiszámítható függvények (ugyanezen operátorokkal egy tetszőleges alaphalmazból képzett függvények), vagy a parciális rekurzív funkcionálok halmazára is (Ref[1, page 174]).