Equality between programs with effects

doctoral dissertation

Niels Voorneveld (Author), Alex Simpson (Mentor)

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

mathematics;program equivalence;functional programming;call-by-push-value;behavioural logic;modalities;algebraic effects;applicative bisimilarity;Howe method;complete lattices;

Data

Language:	English
Year of publishing:	2019
Typology:	2.08 - Doctoral Dissertation
Organization:	UL FMF - Faculty of Mathematics and Physics
Publisher:	[N. Voorneveld]
UDC:	510.6:004.43(043.3)
COBISS:	18936409
Views:	2742
Downloads:	411
Average score:	0 (0 votes)
Metadata:

Other data

Secondary language:	Slovenian
Secondary title:	Enakost med programi z učinki
Secondary 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.
Secondary keywords:	matematika;enakovrednost programov;funkcijsko programiranje;klic po naloženi vrednosti;vedenjska logika;modalnosti;algebrajski učinki;aplikativna bipodobnost;Howejeva metoda;polne mreže;
Type (COBISS):	Doctoral dissertation
Study programme:	0
Embargo end date (OpenAIRE):	1970-01-01
Thesis comment:	Univ. Ljubljana, Fak. za matematiko in fiziko, Oddelek za matematiko, Matematika - 3. stopnja
Pages:	IX, 198 str.
ID:	11394027