NUK - logo
FMF in IMFM, Matematična knjižnica, Ljubljana (MAKLJ)
  • Equality between programs with effects : doctoral dissertation
    Voorneveld, Niels, 1991-
    Disertacija preučuje pojem enakovrednosti programov za funkcijski programski jezik z algebrajskimi učinki in splošno rekurzijo, ki uporablja klic po naloženi vrednosti (call-by-push-value oz. na ... kratko cbpv). Osredotočamo se predvsem na vedenjsko ekvivalenco, pri čemer je obnašanje programa določeno z zbirko formul, ki so odvisne od učinkov. Dva programa istega tipa imamo za enakovredna, če zadoščata istim formulam. Za splošno interpretacijo obnašanja programa z učinki izračune ovrednotimo z drevesi, zgrajenimi iz učinkovnih operacij. Ta drevesa potem interpretiramo v logiki z modalnostmi, kar dvigne predikate na tipih vrednosti do predikatov na tipih izračunov. Eden glavnih prispevkov disertacije je določitev pogojev na modalnostih, pri katerih je vedenjska ekvivalenca, ki jo inducira logika, kongruenca. To pomeni, da enakovrednih izrazov ni mogoče razlikovati s programi. Za dokaz te lastnosti pokažemo, da vedenjska ekvivalenca sovpada z ustreznim pojmom aplikativne bipodobnosti, kjer učinke interpretiramo z uporabo relatorjev (ki dvigajo relacije). To nam omogoči, da dokažemo omenjeno kongruenco s pomočjo različice Howejeve metode. Algebrajski učinki, za katere veljajo rezultati, vključujejo napake, nedeterminizem, verjetnost, globalni pomnilnik, vhod/izhod in časomer. Z logiko lahko opišemo tudi različne kombinacije teh učinkov. Da bi lažje kombinirali učinke in naravneje opisovali obnašanje programov, posplošimo logiko na kvantitativno logiko. Tudi tu pokažemo lastnost kongruence in povezavo z aplikativno bipodobnostjo. Na koncu pokažemo, da podobni rezultati veljajo tudi, če jezik razširimo z dodatnimi konstruktorji tipov. Posebej preučimo univerzalne polimorfne in rekurzivne tipe.
    Vrsta gradiva - disertacija ; neleposlovje za odrasle
    Založništvo in izdelava - Ljubljana : [N. Voorneveld], 2019
    Jezik - angleški
    COBISS.SI-ID - 18936409

    Povezava(-e):

    Repozitorij Univerze v Ljubljani – RUL
    Digitalna knjižnica Slovenije - dLib.si

    Dostop z namenskih računalnikov v prostorih NUK



Signatura – lokacija, inventarna št. ... Status izvoda Rezervacija
Skladišče-Jadranska 21

0000014521/0000000035
Skladišče-Jadranska 21

14521/35
prosto - za čitalnico
loading ...
loading ...
loading ...