No Cover Image

E-Thesis 186 views 131 downloads

Towards a General Theory of Solving for Dependent Type Theory. Formalisations of Monadic Constructions Applicable to Solving for Recursive Data. / ARVED FRIEDEMANN

Swansea University Author: ARVED FRIEDEMANN

  • 2025_Friedemann_A.final.70368.pdf

    PDF | E-Thesis – open access

    Copyright: The author, Arved Reinhard Harald Friedemann, 2025 Distributed under the terms of a Creative Commons Attribution 4.0 License (CC BY 4.0)

    Download (59.83MB)

DOI (Published version): 10.23889/SUThesis.70368

Abstract

This thesis presents several results towards a general theory of solving. We create a formalism for monadic variables that can be used to enhance the capabilities of monads used for search. These monadic variables are created using a form of lattice-based variables, extending the concepts introduced...

Full description

Published: Swansea University, Wales, UK 2025
Institution: Swansea University
Degree level: Doctoral
Degree name: Ph.D
Supervisor: Seisenberger, M., and Berger, U.
URI: https://cronfa.swan.ac.uk/Record/cronfa70368
Abstract: This thesis presents several results towards a general theory of solving. We create a formalism for monadic variables that can be used to enhance the capabilities of monads used for search. These monadic variables are created using a form of lattice-based variables, extending the concepts introduced in [61,62,75]. The pre-order of the lattice is used to ensure that variables keep their assignments on all successive states until a conflict occurs. Further, the lattice structure ensures that regardless of the assignment order, the variables always give the same result. Similar to other lattice-solving based formalisms [33] we generalise this idea to model partial solutions as an ever increasing search state. To make this idea more concrete however, we additionally give constructions toturn almost arbitrary data types into lattices that can be used in this generalised solving process. To express assignments resulting from arbitrary computation, we formalise how recursive functions expressed via folds can run on our lattice representation of data types. We provide improvements to the type representing the syntax of type theory [8,24] and give a type-theoretic interpretation ofthe results from [84] to move towards incorporating the idea of self-improving solvers into type theory within the framework of our generalised solving theory. We present a range of examples of solvers created from our concepts and define a trajectory towards a general theory of solving.
Item Description: A selection of content is redacted or is partially redacted from this thesis to protect sensitive and personal information.
Keywords: Dependent Type Theory, Solving, Agda
College: Faculty of Science and Engineering
Funders: SURES (Swansea University Research Excellence Scholarship)

Similar Items