Project Proposal Phase 2
Today I submitted my “phase 2” project proposal, for approval by the examiners. The text of the proposal is presented below.
This was also a test of how easy it is for me to include portions of markup (Org Mode) written for LaTeX in this HTML “blog”, and vice-versa to keep HTML markup as usable with LaTeX. In this instance I copied the file over and edited the parts that were LaTeX-specific. My notes (including the proposal text) and these posts live in different repositories, which is a problem for file-inclusion that I have not yet resolved. Org is quite suited both to including (portions of) other files, along with its own macros to paper over my liberal use of quoted HTML/LaTeX. Headings, quotation marks, and even citations are processed just fine by the export backend though, and I’m sure other features could be configured or reprogrammed so that I don’t need to use inline LaTeX so often. If I achieved my goals, you could maybe read these posts as beautifully typeset LaTeX too, wouldn’t that be grand?
Anyway, the proposal:
Abstract
Call-by-value and call-by-name are dual evaluation strategies in programming languages; when these are mixed in an effectful language, function composition ceases to be associative, rendering ordinary categories unsuitable for modelling their denotational semantics. Suitable constructs such as duploids have been studied in previous work, but in a univalent setting it is desirable to work with “univalent” versions, where equivalences correspond to identity types. In this work we will study and formalise the suitable notions of univalence for these constructs using the Rocq UniMath library.
Introduction, approach and outcomes
Call-by-value (CBV) and call-by-name (CBN) are two evaluation strategies in lambda calculus, corresponding to whether arguments are evaluated before application, or substituted without evaluation. CBV languages can variously be modelled by monads and their Kleisli categories [1], [2], or the related Freyd categories [3], or abstract Kleisli categories [4] (also called “thunk-force categories”). For mixed evaluation orders, categories are not sufficient: one must relax categories’ associativity condition. A suitable structure is the duploid by [5], [6] where objects are polarized depending on which of their incoming or outgoing maps associate.
From a different direction, univalent foundations (UF), built on dependent type theory, allow for internalising the identity of indiscernibles: equivalent mathematical structures, when correctly constructed, can be identified with each other. This is the univalence principle, which can be stated for many constructions [7], and where the univalence axiom states that it holds for types. In category theory, for instance, one can speak of univalent categories where isomorphic objects are identified [8]. Likewise, we would thus like to speak of univalent [duploids/Freyd categories/thunk-force categories], where suitably equivalent objects are identified.
The aim of this project is to formalise univalent [duploids and/or Freyd categories and/or thunk-force categories], for their use in denotational semantics involving computational effects, where UF have proven useful [9]. In particular, I intend to mechanise some of the existing theorems about [e.g. duploids] [6], hope to explore consequences of their univalence, and aspire to construct the “Rezk-completion” of non-univalent [duploids] into weakly equivalent univalent [duploids], by reference to Rezk-completion for categories [8]. I will be targeting and hoping to contribute to the UniMath [10] library of univalent mathematics, written using the Rocq Prover [11].