Royal Society International Exchanges Grant, IES\R3\223051

Wider Research Context

Pure foundational research provides seeds for successful applications. A notable example in the context of our proposal is a tool, RaML: While based on implicit characterisations of feasible computation by Martin Hofmann to provide elegant descriptions, RaML is nowadays the most advanced tool to estimate resource consumptions of OCaml programs. Also the direction from applications to theory is significant. Deeply rooted in practical questions, Ashish Tiwari defined a restrictive class of linear loop programs and initiated an ongoing study into their termination. It emerged that this links intimately to Skolem's problem, a deep problem in number theory that attracted comments from Terence Tao.

Objectives

Inspired by these examples, we aim to study results between application-oriented areas in program analysis and foundational aspects in proof theory. More precisely, the analysis of feasible algorithms is concerned with the development of (often) automated methods to infer the runtime costs of programs. On the other hand, complexity theory, the study of the inherent complexity of given computational problems, is naturally couched in theories of Bounded Arithmetic (BA). Thus, questions of feasibility of algorithms and problems become questions of provability in BA.

Methods

In an initial phase of the project, we aim to validate our approach by investigating the transfer of methods in the study of rewriting systems and the analysis of proofs in BA. A second phase will explore methods used in the study of BA and program analysis with the aim to develop a long-term programme that can be sustained by follow-up funding.

FWF Project Number: P 36623

Wider Research Context

Amortised analysis is a method for the worst-case cost analysis of (probabilistic) data structures, where a single data structure operation is considered as part of a larger sequence of operations. The cost analysis of sophisticated data structures, such as self-adjusting binary search trees, has been a main objective already in the initial proposal of amortised analysis. Analysing these data structures requires sophisticated potential functions, which typically contain sublinear expressions (such as the logarithm). Apart from our pilot project, the analysis of these data structures has so far eluded automation.

Objectives

We target an automated analysis of the most common data structures with good, ie. sublinear, complexity, such as balanced trees, Fibonacci heaps, randomised search trees, skip lists, skew heaps, Union-find, etc. Our goals are the verification of textbook data structures, the confirmation and improvement (on coefficients) of previously reported complexity bounds, as well as the automated analysis of realistic data structure implementations. Initially, we will only consider strict (first-order) functional programming languages. Later on, we will extend our research towards lazy evaluation in order to allow for the analysis of persistent data structures. Moreover, we will also consider probabilistic data structures.

Methods

Based on the success of our pilot study, we envision the following steps for automatising amortised analysis: (i) Fix a parametrised potential function; (ii) derive a (linear) constraint system over the function parameters from the AST of the program; (iii) capture the required non-linear reasoning trough explicit background knowledge integrable into the constraint solving mechanism; and finally (iv) find values for the parameters by an (optimising) constraint solver.

Research Context

In recent years, advances in computational linguistics have shown that machine processing of natural language can support the use of a language and encourage its wider adoption. Modern writing assistants, for example, do more than detect spelling errors: they can analyze grammatical structures and offer context-aware suggestions and corrections. While widely spoken languages like English, German, or Spanish benefit significantly from these technologies and can rely on large language models, minority languages face substantial challenges. These languages often lack sufficient digital resources, which limits their access to technological advancements. Developing effective methods for low-resource languages requires approaches that work well with limited data, such as transfer learning, few-shot learning, or specialized correction systems. Although progress has been made in areas like machine translation, many questions in automatic text correction remain unresolved for smaller languages.

Goals

This research project focuses on addressing these challenges by developing a writing assistant for the Ladin language. Ladin exhibits strong regional variation in its written form, with differences in orthography, grammar, and vocabulary across valleys. Common errors in Ladin texts often stem from spoken variants or interaction with other languages, particularly Italian and German. The project aims to create a system that can:

• Detect and correct typical errors in Ladin texts
• Provide context-sensitive correction suggestions
• Adapt to the regional diversity of the language

Impact

An intelligent writing assistant for Ladin would not only help users produce correct and consistent texts but also support the consolidation of linguistic standards. By improving digital usability, the tool would strengthen the presence of Ladin in digital communication and contribute to the preservation and promotion of the language in both educational and professional contexts.