U L i k o o L matemaatika-informaatikateaduskond



Yüklə 0,53 Mb.

səhifə21/23
tarix13.11.2017
ölçüsü0,53 Mb.
1   ...   15   16   17   18   19   20   21   22   23

Rekursiivse rec-deklaratsiooni korral on annotatsioonina antud ka rekur-

siivse funktsiooni t¨u¨up, mis lisatakse enne seda funktsiooni kirjeldava avaldise

t¨u¨ubi leidmist konteksti. D¨unaamilises semantikas kasutatakse p¨usipunkti-

operaatorit fix, et lisada defineeritava funktsiooni v¨a¨artuse sellesse samasse

keskkonda, milles see funktsioon v¨a¨artustatakse.

data-deklaratsiooni korral leitakse algebralise andmet¨u¨ubi t¨u¨ubikonstruk-

tori semantika ning selle abil ka andmekonstruktorite semantikad ning lisa-

takse need konteksti ja keskkonda.

newmonad-, unmonad- ja nomonads-deklaratsioonid muudavad kontekstis

olevat kujutust zMonad, mis seab t¨u¨ubikonstruktori unikaalsele identifikaato-

rile vastavusse ¨uhikt¨u¨ubi elemendi. Sisuliselt on tegemist t¨u¨ubikonstruktorite

hulgaga. See on nende t¨u¨ubikonstruktoride hulk, mille abil defineeritud mo-

naade k¨asitletakse monaadidena monaadiliste v¨a¨artuste pol¨umorfismi m˜ottes

(vt ka jaotist 7.5.3).

type-deklaratsioon lisab konteksti t¨u¨ubitaseme objekti ning seob selle

muutujanimega. Seda vaatleme ka jaotises 7.6. class-deklaratsiooni vaatleme

jaotises 7.6.4.

7.5


Funktsiooni rakendamise semantikast

7.5.1


Funktsiooni rakendamine

Fumontrixi funktsiooni rakendamise semantika on oluliselt keerulisem kui

matemaatiline funktsiooni rakendamine. Funktsiooni rakendamiseks kasuta-

tav operaator s˜oltub funktsiooni ja argumendi t¨u¨upidest, mis v˜oivad sisaldada

tipmisel tasemel ¨uldisuskvantoreid ja monaadikonstruktoreid.

Funktsiooni rakendamise semantika on kirjeldatud p˜ohiliselt moodulis

SemUnify. Funktsioon unifyPolymorphic m¨a¨arab funktsiooni ja argumendi

t¨u¨ubi ning konteksti p˜ohjal rakendamise tulemuse t¨u¨ubi ning andmetasemel

rakendamiseks kasutatava operaatori t¨u¨upi

Value -> Value -> Environment -> Value

Lisaks kasutatakse parameetreid generalOpenVForall ja

getMonadInstanceForType, et saaks kasutada neid moodulis Denot definee-

ritud funktsioone, kuna moodulit Denot moodulisse SemUnify importida ei

saa, sest vastupidine s˜oltuvus on juba olemas.

7.5.2

¨

Uldisuskvantorite avamine



Fumontrixis toimub universaalsete t¨u¨upide (parameetrilise ja t¨u¨ubiklassi-)

pol¨umorfismi realiseerimiseks funktsiooni rakendamise korral funktsiooni ja

67



argumendi t¨u¨ubi tipmiste ¨uldisuskvantorite avamine. Olgu funktsiooni t¨u¨up

kujul


forall C

f

1



. . . . forall C

f

n



f

. (forall C

d

1

. . . . forall C



d

n

d



. t

d

) -> t



c

ning argumendi t¨u¨up kujul

forall C

a

1



. . . . forall C

a

n



a

. t


a

Siis k˜oigepealt avatakse kvantorid funktsiooni t¨u¨ubi eest (mis seovad muutu-

jaid C

f

1



, . . . , C

f

n



f

). Seej¨arel vaadatakse, kas kvantoreid on rohkem argumendi

(n

a

kvantorit) v˜oi m¨a¨aramispiirkonna t¨u¨ubi (n



d

kvantorit) ees. Esimesel juhul

avatakse argumendi eest tipmised n

a

−n



d

kvantorit (muutujad C

a

1

. . . C



a

n

a



−n

d

).



Teisel juhul on tegemist t¨u¨ubiveaga, kuna argument ei ole piisavalt pol¨umorf-

ne.


Avatud kvantifitseeritud muutujaid v¨a¨artustatakse unifitseerimise k¨aigus

(vt jaotist 7.5.4). Need muutujad, mis j¨a¨avad v¨a¨artustamata (kitsendamata),

seotakse uuesti kvantoritega, mis l¨ahevad tulemuse t¨u¨ubi ette selles j¨arjekor-

ras nagu nad avati (k˜oige ette funktsiooni ees olnud ja seej¨arel argumendi ees

olnud).

Lihtsuse m˜ottes vaatlesime selles n¨aites parameetriliselt seotud kvanto-



reid. Tegelikult v˜oib (m˜one) kvantori juures olla ka t¨u¨ubiklassikitsendus. Sel-

lisel juhul tuleb see info ka avamisel s¨ailitada (koodis v¨a¨artused openPIKinds’

ja openPIKinds2), et m¨a¨arata pol¨umorfse funktsiooni ja argumendi spetsia-

liseerimisel kasutatavate eksemplaride v¨a¨artusi (generalOpenVForall abil),

ning v¨a¨artustamata j¨a¨anud muutujate taaskvantifitseerimiseks.

7.5.3


Monaadiliste v¨

artuste pol¨



umorfism

Fumontrixi monaadiliste v¨a¨artuste pol¨umorfismi realiseerimiseks funktsiooni

rakendamisel toimub funktsiooni ja argumendi t¨u¨upides tipmiste (newmonad-

deklaratsioonidega m¨a¨aratud konstruktorite abil defineeritud) monaadide ava-

mine sarnaselt ¨uldisuskvantorite avamisega. Olgu funktsiooni t¨u¨up kujul

M

f



1

(. . .(M


f

n

f



(M

d

1



(. . .(M

d

n



d

t

d



)...)) -> t

c

)...)



ning argumendi t¨u¨up kujul

M

a



1

(. . .(M


a

n

a



t

a

)...)



Siis k˜oigepealt avatakse monaadid funktsiooni eest. Seej¨arel vaadatakse, kas

monaade on rohkem argumendi v˜oi m¨a¨aramispiirkonna t¨u¨ubi ees ning avatak-

se nii palju monaade, et argumendi ja m¨a¨aramispiirkonna tipmiste monaadi-

de arv saaks v˜ordseks. Erinevalt ¨uldisuskvantoritest v˜oib m¨a¨aramispiirkonna

68



t¨u¨ubi ees olla rohkem monaade kui argumendi ees, kuna monaadide jaoks on

olemas return-funktsioon, mis v˜oimaldab v¨a¨artuse monaadi sisse viia. Lisaks

avatakse siin muutumispiirkonna t¨u¨ubi t

c

tipmisel tasemel olevad monaadid,



kuigi siin on oluline ainult k˜oige tipmine monaad, mida v˜oidakse koonda-

da (monaadi join-funktsiooni abil), kui see satub tulemuse t¨u¨ubis k˜orvuti

v˜ordse monaadiga.

Funktsiooniga constructMonadicAp konstrueeritakse avatud monaadide

return-, fmap- ja join-funktsioonide abil monaadiline funktsiooni raken-

damise operaator (andmetasemel rakendamise l¨abiviimiseks). Funktsiooniga

monadicApResMonads m¨a¨aratakse need monaadid, mis lisatakse tagasi tule-

muse t¨u¨ubi ette.

7.5.4

Unifitseerimine



P¨arast ¨uldisuskvantorite ja monaadide avamist on vaja m¨a¨aramispiirkonna

t¨u¨up ja argumendiks antud v¨a¨artuse t¨u¨up unifitseerida, et kontrollida, kas

funktsiooni rakendamine on ¨uldse v˜oimalik, ning m¨a¨arata avatud kvantorite-

ga seotud muutujate v¨a¨artustused. Selleks kasutatakse funktsioone

unifyMonomorphic ja unifySolve.

unifyMonomorphic v˜otab kaks t¨u¨upi ja v˜ordleb rekursiivselt nende struk-

tuure. Kui ¨uhes struktuuris on mingi koha peal unifitseeritav muutuja (sel-

leks kasutatakse predikaati isVar, mis eristab unifitseeritavaid muutujaid

tavalistest konstruktoritest), siis see on unifitseeritav suvalise t¨u¨ubiga teises

struktuuris ning siit saadakse v˜orrand kujul muutuja = t¨u¨ubiavaldis. Kui

kummaski struktuuris ei ole antud koha peal unifitseeritav muutuja, siis pea-

vad struktuurid kokku langema ning nende alamstruktuurid unifitseeruma.

Sellise rekursiivse v˜ordlemise teel saadakse l˜opuks mingi hulk v˜orrandeid

eespool toodud kujul. See v˜orrandis¨usteem ei anna veel l˜oplikku muutujate

v¨a¨artustust, kuna ¨uks muutuja v˜oib olla mitme erineva v˜orrandi vasakuks

pooleks ning paremad pooled v˜oivad samuti sisaldada unifitseeritavaid muu-

tujaid. Seega see v˜orrandis¨usteem on vaja lahendada.

Selleks kasutatakse funktsiooni unifySolve, mis lahendab v˜orrandis¨us-

teemi asendusmeetodi abil. V˜orrandite nimekirjast v˜oetakse ¨uks v˜orrand ning

kontrollitakse, et see ei oleks rekursiivne (kui parem pool sisaldab vasakuks

pooleks olevat muutujat, siis unifitseerimine eba˜onnestub, v.a triviaalse v˜or-

randi korral, mis n˜ouab muutuja v˜ordumist iseendaga, mille v˜oib lihtsalt

minema visata). Seej¨arel asendatakse see v˜orrand ¨ulej¨a¨anud v˜orranditesse,

kaotades selle v˜orrandi vasakuks pooleks oleva muutuja ¨ulej¨a¨anud v˜orran-

ditest (kui see muutuja esineb veel m˜one teise v˜orrandi vasaku poolena, siis

tuleb nende v˜orrandite paremad pooled unifitseerida, saades mingi hulga (mis

v˜oib olla ka t¨uhi) uusi v˜orrandeid). Kui nii on tehtud k˜oigi v˜orranditega, siis

69





Dostları ilə paylaş:
1   ...   15   16   17   18   19   20   21   22   23


Verilənlər bazası müəlliflik hüququ ilə müdafiə olunur ©genderi.org 2019
rəhbərliyinə müraciət

    Ana səhifə