izpis_h1_title_alt

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

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

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 (mb31)
Organization:FMF - Faculty of Mathematics and Physics
Year:2020
UDC:510.6
COBISS.SI-ID:18936409 Link is opened in a new window
Views:200
Downloads:126
Metadata:XML RDF-CHPDL DC-XML DC-RDF
 
Average score:(0 votes)
Your score:Voting is allowed only to logged in users.
:
Share:AddThis
AddThis uses cookies that require your consent. Edit consent...

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:

Comments

Leave comment

You have to log in to leave a comment.

Comments (0)
0 - 0 / 0
 
There are no comments!

Back