izpis_h1_title_alt

Equality between programs with effects : doctoral dissertation
ID Voorneveld, Niels Frits Willem (Avtor), ID Simpson, Alex (Mentor) Več o mentorju... Povezava se odpre v novem oknu

.pdfPDF - Predstavitvena datoteka, prenos (2,42 MB)
MD5: FF0AD475DC00AC65D716EEE940CE1203

Izvleček
This thesis studies notions of program equivalence for a call-by-push-value functional language with algebraic effects and general recursion. We mainly focus on behavioural equivalence, where program behaviour is specified by a collection of effect-specific formulas. Two programs of the same type are deemed equivalent if they satisfy the same formulas. To interpret effectful behaviour in a generic way, computation terms are evaluated to trees built from effect operators. These trees are then interpreted in a logic using modalities, which lift predicates on value types to predicates on computation types. One of the main contributions of this thesis is identifying conditions on the modalities under which the behavioural equivalence induced by the logic is a congruence. This means equivalent terms cannot be distinguished by programs. To prove this property, we show that the behavioural equivalence coincides with an appropriate notion of applicative bisimilarity, where effects are interpreted using relators (which lift relations). This allows us to prove the aforementioned congruence using a variation of Howe's method. The algebraic effects to which the results apply include error, nondeterminism, probability, global store, input/output, and timer. Several combinations of these effects can also be described with the logic. However, in order to combine effects more easily, and to give more natural descriptions of program behaviour, the logic is generalised to a logic with quantitative formulas. Once again, the congruence property and connections with applicative bisimilarity are established. Finally, we show that similar results hold also if the language is extended with additional type constructors. In particular, we consider universal polymorphic and recursive types.

Jezik:Angleški jezik
Ključne besede:Program equivalence, functional programming, call-by-push-value, behavioural logic, modalities, algebraic effects, applicative bisimilarity, Howe’s method, complete lattices
Vrsta gradiva:Doktorsko delo/naloga
Tipologija:2.08 - Doktorska disertacija
Organizacija:FMF - Fakulteta za matematiko in fiziko
Leto izida:2020
PID:20.500.12556/RUL-113745 Povezava se odpre v novem oknu
UDK:510.6
COBISS.SI-ID:18936409 Povezava se odpre v novem oknu
Datum objave v RUL:30.01.2020
Število ogledov:3190
Število prenosov:452
Metapodatki:XML RDF-CHPDL DC-XML DC-RDF
:
Kopiraj citat
Objavi na:Bookmark and Share

Sekundarni jezik

Jezik:Slovenski jezik
Naslov:Enakost med programi z učinki
Izvleček:
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.

Ključne besede:Enakovrednost programov, funkcijsko programiranje, klic po naloženi vrednosti (call-by-push-value), vedenjska logika, modalnosti, algebrajski učinki, aplikativna bipodobnost, Howejeva metoda, polne mreže

Podobna dela

Podobna dela v RUL:
Podobna dela v drugih slovenskih zbirkah:

Nazaj