Vinsamlegast notið þetta auðkenni þegar þið vitnið til verksins eða tengið í það: https://hdl.handle.net/1946/48228
We study interaction laws of monads and comonads in the interactive theorem prover Agda. Effectful computations are modeled as monads, while comonads model computation-running machines. Interaction laws describe how computations may be uniformly run to yield values. We study monads and comonads on an arbitrary monoidal category, assuming properties such as symmetry only if needed. We do not assume any axioms from classical mathematics which are noncomputable or those which would be incompatible with univalence such as choice, LEM or K.
Our formalization is carried out using the agda-categories mathematical library. It describes interaction laws for functors in general, as well as between monads and comonads. We describe the monoidal category of functor-functor interaction laws. Furthermore, we prove that monoid objects in the category of functor-functor interaction laws are equivalent to monad-comonad interaction laws. Finally, we develop the end calculus in agda-categories and define the dual endofunctor.
In this work, we demonstrate several common computationally motivated examples. We show that the monads involved interact with the expected comonads. We also give examples of the dual. As all formalization is completed in a computable mathematical foundation, this thesis gives a computable theory of computations. This enables future creation of programs which manipulate computations in a verified and general way, for example, compilers or program analyzers.
Við munum rannsaka samverkunarlögmál mónaða og hjámónaða í gagnvirka sannaranum Agda. Mónöður eru líkön fyrir útreikninga með aukaverkunum og hjámónöður fyrir sýndarvélar sem geta leitt til aukaverkana. Samverkunarlögmálin lýsa hvernig sýndarvélar keyra útreikninga til að gefa niðurstöður. Við vinnum í almennu einungsríki en gefum okkur víxlni ef þörf krefur. Engar óreiknanlegar frumsendur eða frumsendur sem stangast á við eingildislögmál Voevodsky eru notaðar; svo sem valfrumsendan, lögmálið um annað tveggja eða K-frumsendan.
Formlega sannprófunin okkar fer fram með hjálp stærðfræðigagnagrunnsins adga-categories. Við skilgreinum samverkunarlögmál fyrir almenna varpa auk mónaða og hjámónaða. Út frá því skilgreinum við einungsríki samverkunarlögmála milli tveggja varpa og sönnum að einungar í því ríki eru jafngildi samverkunarlögmálum milli mónaða og hjámónaða. Að lokum þróum við endareikning út frá agda-categories og skilgreinum nykrun innanvarpa.
Í þessu verkefni eru mörg sýnidæmi sem hafa reiknifræðilegan bakgrunn. Við sýnum að mónöðurnar í öllum dæmunum samverka við hjámónöðurnar eins og búist var við.
Við gefum líka dæmi um nykrun. Stærðfræðilegar undirstöður formlegu sannprófunarinnar okkar eru reiknanlegar og því leiðir þetta verkefni af sér reiknanlega kenningu um útreikninga með aukaverkunum. Það opnar möguleika á formlega sannprófuðum forritum sem eiga við þannig útreikninga, til dæmis þýðendur eða forritagreinendur.
Skráarnafn | Stærð | Aðgangur | Lýsing | Skráartegund | |
---|---|---|---|---|---|
msc-calvin-2024.pdf | 387.71 kB | Opinn | Heildartexti | Skoða/Opna |