izpis_h1_title_alt

Equality between programs with effects : doctoral dissertation
ID Voorneveld, Niels Frits Willem (Author), ID Simpson, Alex (Mentor) More about this mentor... This link opens in a new window

.pdfPDF - Presentation file, Download (2,42 MB)
MD5: FF0AD475DC00AC65D716EEE940CE1203

Abstract
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.

Language:English
Keywords:Program equivalence, functional programming, call-by-push-value, behavioural logic, modalities, algebraic effects, applicative bisimilarity, Howe’s method, complete lattices
Work type:Doctoral dissertation
Organization:FMF - Faculty of Mathematics and Physics
Year:2020
PID:20.500.12556/RUL-113745 This link opens in a new window
UDC:510.6
COBISS.SI-ID:18936409 This link opens in a new window
Publication date in RUL:30.01.2020
Views:2460
Downloads:405
Metadata:XML RDF-CHPDL DC-XML DC-RDF
:
Copy citation
Share:Bookmark and Share

Secondary language

Language:Slovenian
Title:Enakost med programi z učinki
Abstract:
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.

Keywords: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

Similar documents

Similar works from RUL:
Similar works from other Slovenian collections:

Back