Doctoral Theses (Mathematical & Computer Sciences)
Permanent URI for this collectionhttps://dspace-upgrade.is.ed.ac.uk/handle/10399/37
Browse
479 results
Search Results
Item From formal specification to full proof : a stepwise method(Heriot-Watt University, 2020-07) Burski, Lavinia; Kamareddine, Professor Fairouz D.; Ireland, Professor AndrewHigh integrity system specifications are very difficult to analyse and check for correctness, whether they are written formally, informally, or are on the way to being formalised. Such specifications are often written by many different stakeholders and therefore it is a laborious task bringing all the components together. This thesis introduces and new and stepwise toolkit to assist the translation of formal specifications into theorem provers based on the MathLang Framework. Each step comes with it’s own correctness checks, some of which can be done on informal as well as formal specifications. Steps can be performed in isolation or all together in a sequence in order to translate a formal specification into a formal proof in Isabelle - even by someone who is not necessarily proficient in theorem proving. The ZMath-Lang toolkit allows users to bring their specifications together and helps to manage all the components.Item Aspects of braided field theories from homotopy algebras and the double copy of noncommutative gauge theories(Heriot-Watt University, 2025-04) Trojani, Guillaume; Szabo, Professor Richard JosephThe quantum Batalin–Vilkovisky (BV) formalism and its connection to homotopy Lie algebras is reviewed. The Drinfel’d twist deformation procedure is used to define braided homotopy Lie algebras, leading us to perform a detailed study of the braided cubic scalar and the braided quantum electrodynamics model in the first part of this thesis. The braided BV formalism is used to compute correlation functions for these models and we show the absence of UV/IR mixing up to one-loop order and three-point multiplicity. New homological techniques are presented to study the Schwinger–Dyson equation and the Ward–Takahashi identities of these braided theories respectively. In the later theory, the braided gauge symmetry is verified to be non-anomalous. We next study how conventional noncommutative field theories fit into the ho motopy double copy paradigm whose central idea is the factorisation of homotopy algebras. To perform this operation, a new twisted colour-kinematics duality is identified. This twist captures the (conventional) noncommutativity of the theory, hence the double copied theories are shown to match with their commutative coun terparts; a result that is expected from open-closed string duality in the presence of a background B-field. We conjecture that performing the homotopy double copy within the category of braided L∞-algebras is the correct way to probe twisted noncommutative gravity.Item (Non)-Morse directions in groups(Heriot-Watt University, 2025-02) Zbinden, Stefanie; Sisto, Associate Professor AlessandroIn this thesis, we study Morse directions and the Morse boundary of groups. We start by classifying the Morse boundary of all 3-manifold groups and showing that the Morse boundary of an orientable 3-manifold group only depends on the geometric decomposition of said manifold. This classification requires deep understanding of what it means to be Morse and how to manipulate Morse geodesics. While the theory of Morse boundaries and Morse geodesics is largely developed in analogy with Gromov boundaries, in the rest of this thesis, we focus on phenomena which are unique to the Morse boundary and non-hyperbolic groups. Firstly, we study the (non)-σ-compactness of the Morse boundary. The Gromov boundary of a group is always compact. In contrast, the Morse boundary of a group is only compact if it is empty or the group is hyperbolic. However, the Morse boundary exhibits more nuanced behaviour. Namely, we show that there are groups whose Morse boundary is σ-compact and groups where it is not. We give a full characterisation, which is purely combinatorial in terms of the presentation, of σ-compactness of the Morse boundary for classical small-cancellation groups. This can be used as a way to distinguish small-cancellation groups up to quasi-isometry. Furthermore, we show that for C ′ (1/9)– small-cancellation groups, the group satisfying the Morse local-to-global property is equivalent to its Morse boundary being σ-compact, implying that the topology of the Morse boundary has surprising implications on the concatenability of Morse geodesics. Secondly, in hyperbolic groups all geodesics are strongly contracting. This is precisely not the case for non-hyperbolic groups. We develop the notion of “anti-contracting geodesics segments”, that is, geodesic segments which are intrinsically not strongly contracting. We not only show that for any geodesic metric space, coning-off all anti-contracting geodesic segments results in a hyperbolic space (which we call the contraction space) but also show that if a finitely generated group acted properly on the geodesic metric space, then its action on the contraction space is non-uniformly acylindrical. Moreover, if the action was geometric and the original space was Morse-dichotomous (that is, all Morse geodesics are strongly contracting; this is the case in CAT(0) spaces and injective metric spaces), then the action on the contraction space is a universal WPD action.Item Simulation of Wishart processes and generalised Heston models(Heriot-Watt University, 2025-02) Davletzhanova, Aigerim; Wiese, Doctor Anke; Malham, Doctor Simon J. A.The topic of this work is in studying the Wishart processes in the extended Heston model framework, which is commonly used as a pricing tool in finance. A volatility process, which is driven by the Wishart process, is simulated by the exact splitting scheme of Ahdida and Alfonsi [2]. We enhance their approach by adding the component of a time integral of volatility to the existing generator of the Wishart process. We also avoid the expensive matrix exponentiation procedure, that Ahdida and Alfonsi [2] state about, by the change of measure approach from Malham et al. [50] and Gnoatto and Grasselli [28]. Using the composition techniques from Ninomiya and Victoir [55], we construct the three new schemes to sample the pairs of volatility and its time integral. One of the schemes has a local error of order two, whereas the other two schemes are based on the Strang splitting with the local errors of order three. The change of measure approach of Gnoatto and Grasselli [28] helps us to transfer between the restricted and full parameter cases of the Wishart processes. The sampled pairs of volatility and its time integral are then used during the pricing procedure. Comparison of the moment generating functions with Gnoatto and Grasselli [28], and comparison of the call option prices with Leung [45], are used to show a correctness of the implemented schemes.Item Modelling the impact of shared pathogens in wildlife communities(Heriot-Watt University, 2025-02) Howell, Elizabeth; White, Professor AndyThe thesis uses mathematical modelling to answer important eco-epidemiologial questions in scenarios where interacting species share an infectious disease. These questions are important as shared disease is often linked to successful species invasion and so the disease increases the threat for native species. Shared disease is also linked to spillover and zoonotic infection and so can pose a threat to human health. We develop a model to assess the threat of the shared disease, squirrelpox, carried by the invasive grey squirrel to the conservation of red squirrels in the UK. We show that the grey squirrel epidemiological dynamics include reinfection and partial immunity and that squirrelpox infection levels can be high. This can lead to spillover to red squirrels when the species are sympatric, leading to epidemic outbreaks in red squirrel populations. We analyse general models that examine the role of shared infectious disease on the spatial spread of invasive species and the replacement of native species. We show that shared infectious disease can increase the rate of replacement of a native species even when the disease is not supported in the native species system. We develop a model for a prey, specialist predator, and generalist predator system in which the predators can become infected through consumption of infected prey and can transmit infection back to the prey species. The analysis shows that predators can increase the persistence of infectious disease and may act as epidemic bridges that support the infection during low density phases in the prey species.Item Engaging older adults in cognitive activities through socially assistive robots and sensory feedback(Heriot-Watt University, 2025-01) Nault, Emilyann Lacroix; Baillie, Professor Lynne; Broz, Doctor FrankThis thesis investigates how the novel combination of socially assistive robots and sensory feedback can foster engagement in cognitive activities for the older adult population. Cognitive decline is a natural part of ageing, and whether it arises from pathological or non-pathological origins, nonpharmaceutical methods can retain cognitive function and delay cognitive decline. Namely, cognitive training and leisure-based cognitive activities can positively impact older adults’ cognition. While consistent long-term engagement is required to attain the cognitive benefits, adherence has been identified as a common challenge for older adults. Therefore, tools which can promote engagement in cognitive activities can benefit the ageing population. This doctoral work employed validated user-centred methodologies to investigate whether the unique combination of socially assistive robots and sensory feedback could promote older adults’ engagement in cognitive activities. This research began with a feasibility study with young adults and a usability study with older adults, which both confirmed the potential for combining socially assistive robots and sensory feedback to foster engagement in cognitive activities. This was followed by a Participatory Design workshop with older adults and therapists that identified concrete interaction designs and themes for encouraging cognitive activity engagement. These results were integrated into a prototype, and its evaluation with older adults confirmed its effectiveness in promoting engagement with cognitive activities. The subsequent study identified enhanced performance and usability of engaging with a cognitive activity through a socially assistive robot over a laptop, in addition to a preference for kinesthetic feedback over non-contact cutaneous feedback. This thesis further contributed a long-term experiment with eleven older adults to determine whether the promising results from the prior user-centred evaluations would promote sustained engagement. Contrary to other robotic experiments, this study led to a consistent level of engagement with the robot, and it was also preferred over typical interactions with cognitive activities. Haptic feedback also enhanced engagement for visual-based activities over the long term. The principal finding from this work is that the novel combination of a SAR and sensory feedback can promote short- and long-term engagement in cognitive activities for older adults, which has the potential to lead to benefits in cognition. The thesis concludes with a set of guidelines for designing socially assistive robots and sensory feedback to foster cognitive engagement for older adults. This work, along with these guidelines, can assist future researchers in human-robot interaction and human-computer interaction to develop mechanisms for enhancing cognitive engagement for the ageing population moving forward.Item Symmetries and gauge fixing of three dimensional quantum gravity(Heriot-Watt University, 2024-12) Morales Parra, Juan Carlos; Schroers, Professor Bernd J.In this thesis, we study mathematical aspects of three dimensional classical and quantum gravity. At the classical level we study the Poisson structures of gauge-fixed three dimensional Chern-Simons gravity, fully defined by classical dynamical r-matrices. We determine all the classical dynamical r-matrices associated to the Lie algebras of the local isometry groups of three dimensional spacetimes, for both the Euclidean and Lorentzian signatures and any value of the cosmological constant; highlighting these coindice with the solutions to the Classical Dynamical Yang-Baxter Equation that appear in the exchange algebra of WZNW models. At the quantum level we study two quantum group isometries of lorentzian quantum gravity: the quantum double of SL(2, R) and the quantum k-Poincaré. We prove these two Hopf algebras are twist-equivalent and examine their semiclassical counterparts.Item Instanton partition functions in eight-dimensional cohomological gauge theory(Heriot-Watt University, 2025-01) Tirelli, Michelangelo; Szabo, Professor Richard JosephWe elaborate on the analysis of noncommutative instantons on C4 with SU(4)- holonomy and their generalized ADHM construction. They are realized in a dimensional reduction of supersymmetric Yang–Mills theory from ten dimensions and also in string theory. The instanton partition function can be evaluated using torus equivariant localization, and we extend it to Calabi-Yau orbifolds C4/Γab with Γab a finite abelian subgroup of SU(4). For some classes of Γab, we exhibit the dimensional reduction to orbifold partition functions of Donaldson–Thomas theory on the toric Kähler three-orbifold C3/Γab. Through such reduction we conjecture closed formulas for the instanton partition function on the orbifolds C2/Zn × C2 and C3/(Z2 × Z2) × C. Solutions of the noncommutative instanton equations localized on collections of hyperplanes C3 in C4 are called tetrahedron instantons. They can be similarly studied as noncommutative six-dimensional instantons. We investigate their partition functions on orbifolds, generalising the discussion on Calabi-Yau orbifolds C4/τ (Γ), where τ is a homomorphism from a finite group Γ inside SU(4). When Γ is a finite abelian subgroup of SL(2, C), we show the reduction of of the 8d instanton partition functions on C2/Γ × C2 to tetrahedron instanton partition functions on C2/Γ × C2 . For Γ = Zn we expand our conjecturesItem Quantitative methods in sustainable investment(Heriot-Watt University, 2024-10) Marupanthorn, Pasin; Peters, Professor Gareth William; Ofosu-Hene, Doctor Eric Dei; Chantler, Professor Michael JohnThis dissertation conducts a thorough investigation into the integration of quantitative methods within sustainable investment frameworks, with a focus on strategic divestment from carbon-intensive assets and the incorporation of Environmental, Social, and Governance considerations into asset management. Utilizing a multidisciplinary approach that combines advanced computational models with analytical techniques, this research delves into the complexities of financial markets to unearth insights crucial for the advancement of sustainable finance. Central to this inquiry is a critique of traditional divestment strategies, which typically employ an instantaneous approach, and the introduction of a novel methodology advocating for a rate-controlled divestment process. Employing Multi-period Portfolio Optimization, this study meticulously examines the effects of divestment on portfolio stability, carbon footprint reduction, and diversification, advocating for sophisticated portfolio management strategies that align with sustainable investing principles and demonstrate practical viability. A significant portion of this research is devoted to addressing the lack of interactive, open-source tools for divestment analysis. Through the development and utilization of software solutions such as R Shiny, this dissertation contributes to democratizing investment analysis, enabling a wider audience of investors to make informed, sustainable investment decisions. Additionally, this dissertation investigates the temporal effects of sustainability risk factors on asset returns, integrating these into established financial models to provide a holistic perspective on investment strategies. This detailed analysis facilitates a deeper understanding of market complexities through a sustainability-focused lens. Empirical case studies, encompassing analyses of the S&P 500, global ETFs, the UK’s FTSE 100 index, and mixed pension funds in both the US and UK, highlight the practical applicability and effectiveness of the proposed divestment across a diverse range of market contexts. Additionally, the factor model incorporating sustainability factors is applied to assess the sustainability risk factor in Morningstar US indices. These studies provide valuable insights into the operationalization of sustainability considerations in investment strategies.Item Optimal transport theory and geometric modelling of polycrystalline materials(Heriot-Watt University, 2024-10) Pearce, Mason; Bourne, Doctor David; Roper, Doctor StevenThis thesis looks at an application of optimal transport theory in materials science and computational geometry. In particular, we use optimal transport to generate Laguerre tessellations that have cells of prescribed volumes and centroids. Laguerre tessellations can be used to model the microstructure of polycrystalline materials, such as metals. We study methods for generating synthetic microstructures and fitting Laguerre tessellations to Electron BackScattering Diffraction (EBSD) images of metals.