Royal Society International Exchanges Grant, IES\R3\223051

Breiterer Forschungskontext

Reine Grundlagenforschung liefert die Grundlage für erfolgreiche Anwendungen. Ein bemerkenswertes Beispiel im Kontext unseres Vorschlags ist ein Tool, RaML: Während RaML auf impliziten Charakterisierungen möglicher Berechnungen von Martin Hofmann basiert, um elegante Beschreibungen zu liefern, ist es heutzutage das fortschrittlichste Tool zur Schätzung des Ressourcenverbrauchs von OCaml-Programmen. Auch die Richtung von der Anwendung zur Theorie ist bedeutsam. Tief verwurzelt in praktischen Fragen definierte Ashish Tiwari eine restriktive Klasse linearer Schleifenprogramme und initiierte eine laufende Studie zu deren Beendigung. Es stellte sich heraus, dass dies eng mit Skolems Problem zusammenhängt, einem tiefgreifenden Problem der Zahlentheorie, das Kommentare von Terence Tao hervorrief.

Ziele

Inspiriert durch diese Beispiele wollen wir Ergebnisse zwischen anwendungsorientierten Bereichen der Programmanalyse und grundlegenden Aspekten der Beweistheorie untersuchen. Genauer gesagt geht es bei der Analyse realisierbarer Algorithmen um die Entwicklung (häufig) automatisierter Methoden zur Ableitung der Laufzeitkosten von Programmen. Andererseits ist die Komplexitätstheorie, die Untersuchung der inhärenten Komplexität gegebener Rechenprobleme, natürlich in Theorien der begrenzten Arithmetik (BA) verankert. So werden Fragen der Machbarkeit von Algorithmen und Problemen in der BA zu Fragen der Beweisbarkeit.

Methoden

In einer ersten Phase des Projekts wollen wir unseren Ansatz validieren, indem wir den Methodentransfer bei der Untersuchung von Rewriting-Systemen und der Analyse von Beweisen in BA untersuchen. In einer zweiten Phase werden die Methoden des BA-Studiums und der Programmanalyse erforscht, mit dem Ziel, ein langfristiges Programm zu entwickeln, das durch eine Folgefinanzierung aufrechterhalten werden kann.

FWF Projektnummer: P 36623

Breiterer Forschungskontext

Die amortisierte Analyse ist eine Methode zur Worst-Case-Kostenanalyse von (probabilistischen) Datenstrukturen, bei der eine einzelne Datenstrukturoperation als Teil einer größeren Folge von Operationen betrachtet wird. Die Kostenanalyse anspruchsvoller Datenstrukturen, wie etwa selbstanpassender binärer Suchbäume, war bereits im ursprünglichen Vorschlag einer amortisierten Analyse ein Hauptziel. Die Analyse dieser Datenstrukturen erfordert ausgefeilte Potentialfunktionen, die typischerweise sublineare Ausdrücke (wie den Logarithmus) enthalten. Abgesehen von unserem Pilotprojekt entzog sich die Analyse dieser Datenstrukturen bislang einer Automatisierung.

Ziele

Unser Ziel ist eine automatisierte Analyse der gängigsten Datenstrukturen mit guten, d.h. sublinearer, Komplexität, wie ausgeglichene Bäume, Fibonacci-Heaps, randomisierte Suchbäume, Skip-Listen, Skew-Heaps, Union-Find usw. Unsere Ziele sind die Überprüfung von Lehrbuch-Datenstrukturen, die Bestätigung und Verbesserung (an Koeffizienten) der zuvor gemeldeten Komplexität Grenzen sowie die automatisierte Analyse realistischer Datenstrukturimplementierungen. Zunächst betrachten wir nur streng funktionale Programmiersprachen (erster Ordnung). Später werden wir unsere Forschung auf Lazy Evaluation ausweiten, um die Analyse persistenter Datenstrukturen zu ermöglichen. Darüber hinaus werden wir auch probabilistische Datenstrukturen berücksichtigen.

Methoden

Basierend auf dem Erfolg unserer Pilotstudie stellen wir uns die folgenden Schritte zur Automatisierung der amortisierten Analyse vor: (i) Fixieren einer parametrisierten potenziellen Funktion; (ii) ein (lineares) Einschränkungssystem über die Funktionsparameter aus dem AST des Programms ableiten; (iii) Erfassen der erforderlichen nichtlinearen Argumentation durch explizites Hintergrundwissen, das in den Mechanismus zur Lösung von Zwangsbedingungen integrierbar ist; und schließlich (iv) Werte für die Parameter durch einen (optimierenden) Constraint-Löser finden.

Breiterer Forschungskontext

In den letzten Jahren haben Fortschritte in der Computerlinguistik gezeigt, dass die maschinelle Verarbeitung natürlicher Sprache die Nutzung einer Sprache fördern und ihre Verbreitung stärken kann. Moderne Schreibassistenten erkennen nicht nur Rechtschreibfehler, sondern können auch grammatikalische Strukturen analysieren und kontextabhängige Verbesserungsvorschläge liefern. Während weit verbreitete Sprachen wie Englisch, Deutsch oder Spanisch stark von diesen Technologien profitieren und auf große Sprachmodelle zurückgreifen können, stehen Minderheitensprachen vor erheblichen Herausforderungen. Diese Sprachen verfügen oft nicht über ausreichend digitale Ressourcen, was ihren Zugang zu technologischen Entwicklungen einschränkt. Für weniger stark digitalisierte Sprachen sind Methoden erforderlich, die auch mit begrenzten Datenmengen effektiv arbeiten, beispielsweise durch Transfer Learning, Few-Shot Learning oder spezialisierte Korrektursysteme. Obwohl im Bereich maschineller Übersetzung Fortschritte erzielt wurden, bleiben viele Fragen zur automatischen Textkorrektur für kleinere Sprachen offen.

Ziele

Dieses Forschungsprojekt konzentriert sich darauf, diese Herausforderungen zu bewältigen und einen Schreibassistenten für die ladinische Sprache zu entwickeln. Das Ladinische weist starke regionale Unterschiede in der Schriftsprache auf, mit Variationen in Orthografie, Grammatik und Wortschatz zwischen den Tälern. Typische Fehler in ladinischen Texten entstehen häufig durch gesprochene Varianten oder die Einwirkung anderer Sprachen, insbesondere Italienisch und Deutsch. Das Projekt zielt darauf ab, ein System zu entwickeln, das:

• Typische Fehler in ladinischen Texten erkennt und korrigiert
• Kontextabhängige Korrekturvorschläge liefert
• Sich an die regionale Vielfalt der Sprache anpasst

Auswirkung

Ein intelligenter Schreibassistent für Ladin würde nicht nur dabei helfen, korrekte und konsistente Texte zu erstellen, sondern auch zur Festigung sprachlicher Standards beitragen. Durch die Verbesserung der digitalen Nutzungsmöglichkeiten würde das Tool die Präsenz des Ladinischen in digitalen Kommunikationskontexten stärken und somit den Erhalt und die Förderung der Sprache in Bildungs- und Berufsbereichen unterstützen.