Polynomial Functors in Agda: Theory and Practice
Ladda ner
Typ
Examensarbete för masterexamen
Master's Thesis
Master's Thesis
Program
Complex adaptive systems (MPCAS), MSc
Computer science – algorithms, languages and logic (MPALG), MSc
Computer science – algorithms, languages and logic (MPALG), MSc
Publicerad
2023
Författare
Jörgensson, Marcus
Muricy Santos, André
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
The category of polynomial functors - Poly - has been studied for over two decades and is well known for its relevance to computer science [1] and deep mathematical structure [2]. In recent years, new interpretations of Poly have been found in dynamical systems theory [3]. This thesis formalizes Poly in Cubical Agda and showcases its use in dynamical systems, contributing to the Poly code ecosystem.
The first part, theory, formalizes the category Poly itself and many of its categorical constructs, including the initial and terminal objects, product, coproduct, equalizer, composition and parallel product. Then Chart is formalized, together with its own categorical constructs. Finally, Poly and Chart morphisms are combined via commuting squares.
The second part, practice, builds upon the theory by using these categories to implement dynamical systems. It covers how morphisms in Poly represent dynamical systems, how polynomials act as interfaces, how systems are wired together, how behavior is installed into wiring diagrams, and how to run systems arriving at concrete programs. Many dynamical system examples are given, such as a Fibonacci sequence generator, the Lorenz system, the Hodkgin-Huxley model, and an Echo-State Network that learns the Lorenz dynamics. Commuting squares are used as a way of showing that one dynamical system can be made to simulate another.
Beskrivning
Ämne/nyckelord
Category theory , Dependent types , Agda , Cubical , Polynomial functors , Dynamical systems , Complex systems