No Cover Image

E-Thesis 187 views 132 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
first_indexed 2025-09-16T15:29:19Z
last_indexed 2025-09-17T05:54:05Z
id cronfa70368
recordtype RisThesis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2025-09-16T16:48:49.3550410</datestamp><bib-version>v2</bib-version><id>70368</id><entry>2025-09-16</entry><title>Towards a General Theory of Solving for Dependent Type Theory. Formalisations of Monadic Constructions Applicable to Solving for Recursive Data.</title><swanseaauthors><author><sid>a1ac7f11ad9443b3904b0f8d77623cf5</sid><firstname>ARVED</firstname><surname>FRIEDEMANN</surname><name>ARVED FRIEDEMANN</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2025-09-16</date><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.</abstract><type>E-Thesis</type><journal/><volume/><journalNumber/><paginationStart/><paginationEnd/><publisher/><placeOfPublication>Swansea University, Wales, UK</placeOfPublication><isbnPrint/><isbnElectronic/><issnPrint/><issnElectronic/><keywords>Dependent Type Theory, Solving, Agda</keywords><publishedDay>5</publishedDay><publishedMonth>5</publishedMonth><publishedYear>2025</publishedYear><publishedDate>2025-05-05</publishedDate><doi>10.23889/SUThesis.70368</doi><url/><notes>A selection of content is redacted or is partially redacted from this thesis to protect sensitive and personal information.</notes><college>COLLEGE NANME</college><CollegeCode>COLLEGE CODE</CollegeCode><institution>Swansea University</institution><supervisor>Seisenberger, M., and Berger, U.</supervisor><degreelevel>Doctoral</degreelevel><degreename>Ph.D</degreename><degreesponsorsfunders>SURES (Swansea University Research Excellence Scholarship)</degreesponsorsfunders><apcterm/><funders>SURES (Swansea University Research Excellence Scholarship)</funders><projectreference/><lastEdited>2025-09-16T16:48:49.3550410</lastEdited><Created>2025-09-16T15:49:08.5625418</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>ARVED</firstname><surname>FRIEDEMANN</surname><order>1</order></author></authors><documents><document><filename>70368__35097__5bb4d95454594e83aa7a01d83d2116f9.pdf</filename><originalFilename>2025_Friedemann_A.final.70368.pdf</originalFilename><uploaded>2025-09-16T16:02:57.3449433</uploaded><type>Output</type><contentLength>62738524</contentLength><contentType>application/pdf</contentType><version>E-Thesis &#x2013; open access</version><cronfaStatus>true</cronfaStatus><documentNotes>Copyright: The author, Arved Reinhard Harald Friedemann, 2025 Distributed under the terms of a Creative Commons Attribution 4.0 License (CC BY 4.0)</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language><licence>https://creativecommons.org/licenses/by/4.0/</licence></document></documents><OutputDurs/></rfc1807>
spelling 2025-09-16T16:48:49.3550410 v2 70368 2025-09-16 Towards a General Theory of Solving for Dependent Type Theory. Formalisations of Monadic Constructions Applicable to Solving for Recursive Data. a1ac7f11ad9443b3904b0f8d77623cf5 ARVED FRIEDEMANN ARVED FRIEDEMANN true false 2025-09-16 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. E-Thesis Swansea University, Wales, UK Dependent Type Theory, Solving, Agda 5 5 2025 2025-05-05 10.23889/SUThesis.70368 A selection of content is redacted or is partially redacted from this thesis to protect sensitive and personal information. COLLEGE NANME COLLEGE CODE Swansea University Seisenberger, M., and Berger, U. Doctoral Ph.D SURES (Swansea University Research Excellence Scholarship) SURES (Swansea University Research Excellence Scholarship) 2025-09-16T16:48:49.3550410 2025-09-16T15:49:08.5625418 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science ARVED FRIEDEMANN 1 70368__35097__5bb4d95454594e83aa7a01d83d2116f9.pdf 2025_Friedemann_A.final.70368.pdf 2025-09-16T16:02:57.3449433 Output 62738524 application/pdf E-Thesis – open access true Copyright: The author, Arved Reinhard Harald Friedemann, 2025 Distributed under the terms of a Creative Commons Attribution 4.0 License (CC BY 4.0) true eng https://creativecommons.org/licenses/by/4.0/
title Towards a General Theory of Solving for Dependent Type Theory. Formalisations of Monadic Constructions Applicable to Solving for Recursive Data.
spellingShingle Towards a General Theory of Solving for Dependent Type Theory. Formalisations of Monadic Constructions Applicable to Solving for Recursive Data.
ARVED FRIEDEMANN
title_short Towards a General Theory of Solving for Dependent Type Theory. Formalisations of Monadic Constructions Applicable to Solving for Recursive Data.
title_full Towards a General Theory of Solving for Dependent Type Theory. Formalisations of Monadic Constructions Applicable to Solving for Recursive Data.
title_fullStr Towards a General Theory of Solving for Dependent Type Theory. Formalisations of Monadic Constructions Applicable to Solving for Recursive Data.
title_full_unstemmed Towards a General Theory of Solving for Dependent Type Theory. Formalisations of Monadic Constructions Applicable to Solving for Recursive Data.
title_sort Towards a General Theory of Solving for Dependent Type Theory. Formalisations of Monadic Constructions Applicable to Solving for Recursive Data.
author_id_str_mv a1ac7f11ad9443b3904b0f8d77623cf5
author_id_fullname_str_mv a1ac7f11ad9443b3904b0f8d77623cf5_***_ARVED FRIEDEMANN
author ARVED FRIEDEMANN
author2 ARVED FRIEDEMANN
format E-Thesis
publishDate 2025
institution Swansea University
doi_str_mv 10.23889/SUThesis.70368
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
document_store_str 1
active_str 0
description 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.
published_date 2025-05-05T18:06:30Z
_version_ 1850692590077214720
score 11.08899

Similar Items