Convergent Regression in Univalent Mathematics

My proposed research topic is concerned with the design and analysis of diagrammatic programming languages for practical use, inspired by insights and understanding of diagrammatic models and reasoning. The project is intended to have both theoretical and practical aspects. Diagrammatic programming and reasoning provide many benefits over the traditional, textual method. The ability to visualise a program, how its sub-programs and functions interconnect and their flow of control gives the programmer immediate, intuitive insight.Furthermore, representing programs as a data-flow graph allows for the design of completely new and interesting programming features - for example, TensorFlow (an embedded domain-specific diagrammatic language) introduces the concept of 'Graph Abstraction' for the purpose of machine learning. Finally, the profiling of functional programs (traditionallyan intractable process) is made more intuitive when considered with respect to a diagrammatic framework; a 2D cost-accurate graph representation is more illuminating than lines of code. Indeed, all of these reasons provide a clear motivation to develop practical, standalone
diagrammatic (functional) programming languages. Developing such languages is difficult,however, as the operational semantics behind diagrammatic programming languages and new features can be complex. This makes the addition of such new, interesting features into a diagrammatic language - while ensuring soundness of execution is maintained - difficult. The 'Dynamic Geometry of Interaction' (DGoI) is a recent diagrammatic abstract machine that efficiently formalises the semantics of the Lambda-calculus via a graphical representation. The Lambda-calculus is the basis of all functional programming languages and, therefore, DGoI is a simple, standalone diagrammatic programming language with higher-order functions. It can therefore be used as a framework for reasoning about features of diagrammatic programming languages, and furthermore for ratifying the operational semantics of such features for safe addition to the DGoI language. DGoI is used as such a framework for TensorFlow's aforementioned feature of 'Graph Abstraction' in 'The Geometry of ComputationGraph Abstraction'. TensorFlow is a popular open-source library (implemented as an embedded DSL for Python, C, and other languages) for diagrammatic programming. It is largely used for machine learning programming, wherein programs are bi-modal: there is the traditional mode (where specific inputs are given to achieve an output) and a 'learning' mode (where inputs are tuned by the program to achieve an optimal output with regards to some programmer-defined fitness function). The idea behind developing a standalone programming language with this bi-modal concept built in is referred to as "abductive programming" in 'Towards Abductive Programming', and represents the first step towards developing a bespoke, standalone machine learning functional programming language. [4] [2] TensorFlow achieves this functionality via the novel feature of 'Graph Abstraction' which is shown to be "a reasonable addition to a programming language", in that its addition to the DGoI framework is efficient and maintains soundness of execution, safe garbage collection and the Beta-law. Therefore, diagrammatic programming and reasoning has been instrumental in developing the first step towards a standalone machine learning programming language. Clearly, there is much more research to be done in this area in order to fully develop a standalone 'equivalent' to Tensor Flow. Also, there is potential for similar diagrammatic reasoning to aid the development of other standalone diagrammatic functional programming languages.