Proceedings of the ACM on Programming Languages, 6(OOPSLA2), 758-785

miniKanren ist eine leichtgewichtige eingebettete Sprache für logische und relationale Programmierung. Viele seiner nützlichen Eigenschaften beruhen auf einer besonderen Suchstrategie, der Verschachtelungssuche. Bei der verschachtelten Suche werden jedoch herkömmliche Überlegungen über die Komplexität und Leistung logischer Programme irrelevant. Wir identifizieren eine wichtige Schlüsselkomponente -Scheduling -, die die Argumentation für miniKanren so unterschiedlich macht, und stellen eine halbautomatische Technik vor, um die Auswirkungen des Schedulings durch symbolische Ausführung für eine recht breite Klasse von Programmen abzuschätzen.

49. ACM SIGPLAN-Symposium über Grundsätze der Programmiersprachen (POPL 2012)

Scientific and Technical Journal of Information Technologies, Mechanics and Optics

Syrcose'21

TFPIE-2021

Auszeichnung für hervorragende Forschungsarbeiten bei OOPSLA'21

OOPSLA

Programming and Computer Software Journal

Wir präsentieren eine neue, faire Konjunktionsbewertungsstrategie für die relationale Programmiersprache miniKanren. Anders als die ursprüngliche linksgerichtete Konjunktion steuert unser Ansatz die Reihenfolge der Ausführung der Konjunktionen auf der Grundlage der Eigenschaften der Beziehungsdefinitionen. Wir stellen sowohl die formale Untersuchung der Konjunktionsgerechtigkeit als auch die praktische Bewertung vor, die die wesentliche Verbesserung in Bezug auf Leistung und Konvergenz zeigt.

SEIM-2021

ICPP-2021

Wir präsentieren eine formale Studie der Semantik für die relationale Programmiersprache miniKanren. Zunächst formulieren wir eine denotationale Semantik, die dem minimalen Herbrand-Modell für definite logische Programme entspricht. Zweitens stellen wir eine operationale Semantik vor, die das Interleaving modelliert, das charakteristische Merkmal der miniKanren-Implementierung, und beweisen ihre Solidität und Vollständigkeit in Bezug auf die denotationale Semantik. Unsere Entwicklung wird durch eine COQ-Spezifikation unterstützt, aus der ein Referenzinterpreter entnommen werden kann. Aus unserem Hauptergebnis leiten wir auch eine zertifizierte Semantik (und einen Referenzinterpreter) für SLD-Auflösung mit Schnitt ab und beweisen deren Solidität.

Wir stellen einen vollständig deklarativen Ansatz zur Synthese von Pattern-Matching-Konstrukt-Implementierungen vor, der auf der Anwendung von relationaler Programmierung, einer speziellen Form der Constraint-Logik-Programmierung, basiert. Unser Ansatz basiert auf relationalen Darstellungen sowohl der High-Level-Semantik des Mustervergleichs als auch der Semantik einer Implementierungssprache auf mittlerer Ebene. Diese Wahl macht unseren Ansatz im Prinzip sehr skalierbar, da wir nur die High-Level-Semantik ändern müssen, um die Implementierung eines neuen, mustermäßigen Merkmals zu synthetisieren. Unsere Evaluierung einer Reihe von kleinen Beispielen, die teilweise aus der bestehenden Literatur stammen, zeigt, dass unser Framework in der Lage ist, schnell optimale Implementierungen zu synthetisieren. Unsere eingehende Stressbewertung anhand einer Reihe künstlicher Benchmarks hat jedoch gezeigt, dass weitere Verbesserungen erforderlich sind.

Kontextfreie Pfadabfragen (Context-free path queries, CFPQ) erweitern die regulären Pfadabfragen (Regular path queries, RPQ), indem sie es erlauben, kontextfreie Grammatiken als Constraints für Pfade zu verwenden. Algorithmen für CFPQ werden aktiv entwickelt, aber J. Kuijpers et al. sind kürzlich zu dem Schluss gekommen, dass die bestehenden Algorithmen nicht leistungsfähig genug sind, um in realen Anwendungen eingesetzt zu werden. Daher ist die Entwicklung neuer Algorithmen für CFPQ gerechtfertigt. In dieser Forschungsarbeit stellen wir einen neuen CFPQ-Algorithmus vor, der auf linearen Algebra-Operationen wie dem Kronecker-Produkt und der transitiven Schließung basiert und Grammatiken behandelt, die als rekursive Zustandsmaschinen dargestellt werden. Daher kann der vorgeschlagene Algorithmus mithilfe von Hochleistungsbibliotheken und moderner paralleler Hardware implementiert werden. Darüber hinaus vermeidet es ein Anwachsen der Grammatik, was die Möglichkeit zur Optimierung von Abfragen bietet.

ADBIS 2020. Advances in Databases and Information Systems. Vorlesungsnotizen in Informatik.

Reguläre Ausdrücke werden in SPARQL-Eigenschaftspfaden zur Abfrage von RDF-Graphen verwendet. Mit regulären Ausdrücken lässt sich jedoch nur eine sehr begrenzte Klasse von Sprachen definieren, die so genannten regulären Sprachen. Kontextfreie Sprachen sind eine größere Klasse, die alle regulären Sprachen umfasst. Es gibt keine kontextfreien Ausdrücke, um sie zu definieren, so dass es notwendig ist, Grammatiken zu schreiben. Wir schlagen eine Erweiterung der regulären Ausdrücke vor, rekursive Ausdrücke genannt, um die Definition einer Teilmenge kontextfreier Sprachen zu unterstützen. Das Ziel unserer Arbeit ist es daher, einfache Operatoren bereitzustellen, die die Definition von Sprachen ermöglichen, die kontextfreien Sprachen so nahe wie möglich kommen.

ADBIS, TPDL und EDA 2020 Gemeinsame Workshops und Doktorandenkonsortium

The European Conference on Object-Oriented Programming (ECOOP)

Die kontextfreie Pfadabfrage (CFPQ) wird in verschiedenen Bereichen für die Analyse graphstrukturierter Daten eingesetzt. Die Entwicklung hocheffizienter Algorithmen für CFPQ ist von entscheidender Bedeutung, da die Größe der Eingabedaten in der Regel groß ist. Wir zeigen, wie man die CFPQ-Auswertung auf die Lösung von Matrixgleichungssystemen über R reduzieren kann – ein Problem, für das es leistungsstarke Lösungen gibt. Außerdem demonstrieren wir die Anwendbarkeit unseres Ansatzes in der realen Welt der Datenanalyse.

Ergebnisse der 2020 ACM SIGMOD Internationalen Konferenz über Datenmanagement

In dieser Forschungsarbeit wird eine Modifikation des Valiant-Algorithmus vorgestellt, deren Hauptvorteil in der Möglichkeit besteht, die Parsing-Tabelle in nacheinander berechnete Schichten disjunkter Submatrizen zu unterteilen, wobei jede Submatrix der Schicht unabhängig bearbeitet werden kann. Außerdem lässt sich unser Ansatz leicht an das String-Matching-Problem anpassen.

Ergebnisse des Institute for System Programming

Eine kürzlich durchgeführte Studie hat gezeigt, dass die Anwendbarkeit von Algorithmen für kontextfreie Pfadabfragen (CFPQ) mit relationaler Abfragesemantik, die in Graphdatenbanken integriert sind, aufgrund der geringen Leistung und des hohen Speicherverbrauchs der bestehenden Lösungen begrenzt ist. In dieser Arbeit implementieren wir einen matrixbasierten CFPQ-Algorithmus unter Verwendung geeigneter Hochleistungsbibliotheken für lineare Algebra und integrieren ihn in die Graphdatenbank RedisGraph. Darüber hinaus führen wir einen neuen CFPQ-Algorithmus mit der Semantik der Einzelpfadabfrage ein, der es uns ermöglicht, einen gefundenen Pfad für jedes Knotenpaar zu extrahieren. Abschließend stellen wir die Evaluierung unserer Algorithmen für beide Semantiken vor, die zeigt, dass die matrixbasierte CFPQ-Implementierung für die Redis-Graph-Datenbank leistungsfähig genug für die Datenanalyse in der realen Welt ist.

GRADES-NDA'20: Ergebnisse des 3. gemeinsamen internationalen Workshops über Graphdatenmanagement-Erfahrungen und -Systeme (GRADES) und Netzwerkdatenanalyse (NDA)

41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2020)

41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2020)

Während die GPU-Nutzung es ermöglicht, Berechnungen um Größenordnungen zu beschleunigen, bleibt die Speicherverwaltung der Engpass, so dass es oft eine Herausforderung ist, die gewünschte Leistung zu erreichen. Daher werden verschiedene Speicheroptimierungen eingesetzt, um den Speicher effektiver zu nutzen. Wir schlagen einen Ansatz zur Automatisierung der Speicherverwaltung durch partielle Evaluierung vor, eine Programmtransformationstechnik, die es ermöglicht, Datenzugriffe vorzuberechnen, zu optimieren und in den Code einzubetten, wodurch Speichertransaktionen eingespart werden. Eine empirische Bewertung unseres Ansatzes zeigt, dass das umgewandelte Programm bis zu achtmal effizienter sein kann als das ursprüngliche Programm im Falle der Implementierung des naiven String-Mustervergleichsalgorithmus in CUDA C.

PPoPP '20: Ergebnisse des 25. ACM SIGPLAN-Symposiums über Prinzipien und Praxis der parallelen Programmierung

Tagungsband des ISP RAS

Pfadabfragen mit konjunktiven Grammatiken sind bekanntermaßen unentscheidbar. Es gibt einen Algorithmus für Pfadabfragen mit linearen konjunktiven Grammatiken, der eine Über-Approximation des Ergebnisses liefert, aber es gibt keinen Algorithmus für beliebige konjunktive Grammatiken. Wir schlagen den ersten Algorithmus für Pfadabfragen mit beliebigen konjunktiven Grammatiken vor. Der vorgeschlagene Algorithmus ist matrixbasiert und ermöglicht die effiziente Anwendung von GPGPU-Rechentechniken und anderen Optimierungen für Matrixoperationen.

Programming and Computer Software

BMC Bioinformatics

Ergebnisse der 19. internationalen Konferenz über formale Methoden im computergestützten Design, FMCAD 2019

33rd European Conference on Object-Oriented Programming (ECOOP 2019)

Der kürzlich vorgeschlagene, auf Matrixmultiplikation basierende Algorithmus für kontextfreie Pfadabfragen (CFPQ) verlagert die leistungsintensivsten Teile auf die Multiplikation boolescher Matrizen. So ist es möglich, mit Hilfe moderner paralleler Hard- und Software eine hohe Leistungsfähigkeit von CFPQ zu erreichen. In dieser Forschungsarbeit werden die Ergebnisse eines empirischen Leistungsvergleichs verschiedener Implementierungen dieses Algorithmus sowohl mit realen Daten als auch mit synthetischen Daten für die schlimmsten Fälle vorgestellt.

Ergebnisse des 2. gemeinsamen internationalen Workshops über Graphdatenmanagement-Erfahrungen und -Systeme (GRADES) und Netzwerkdatenanalyse (NDA)

Das Bar-Hillel-Theorem besagt, dass kontextfreie Sprachen durch die Schnittmenge mit einer regulären Menge geschlossen sind. Dieses Theorem hat einen konstruktiven Beweis und liefert somit eine formale Begründung für die Korrektheit der Algorithmen für die oben genannten Anwendungen. Die Mechanisierung des Bar-Hillel-Theorems ist daher sowohl ein grundlegendes Ergebnis der Theorie der formalen Sprache als auch eine Grundlage für die zertifizierte Implementierung der Algorithmen für Anwendungen. In dieser Arbeit präsentieren wir den mechanisierten Beweis des Bar-Hillel-Theorems in Coq.

Logic, Language, Information, and Computation

Wir schlagen einen Weg vor, formale Grammatiken und künstliche neuronale Netze für die Verarbeitung biologischer Sequenzen zu kombinieren. Formale Grammatiken kodieren die Sekundärstruktur der Sequenz, und neuronale Netze befassen sich mit Mutationen und Rauschen. Im Gegensatz zur klassischen Methode, bei der probabilistische Grammatiken für die Modellierung von Sekundärstrukturen verwendet werden, schlagen wir vor, beliebige (nicht probabilistische) Grammatiken zu verwenden, was die Erstellung von Grammatiken vereinfacht. Anstatt die Struktur der gesamten Sequenz zu modellieren, erstellen wir eine Grammatik, die nur Merkmale der Sekundärstruktur beschreibt. Dann verwenden wir matrixbasiertes Parsing, um Merkmale zu extrahieren: Die Tatsache, dass ein Teilstring aus einem Nichtterminal abgeleitet werden kann, ist ein Merkmal. Danach verwenden wir ein dichtes neuronales Netz, um die Merkmale zu verarbeiten.

Ergebnisse der 12. internationalen gemeinsamen Konferenz über biomedizinische technische Systeme und Technologien – BIOINFORMATIK

Eines der Probleme bei der Analyse von Graphdaten ist die Abfrage nach bestimmten Pfaden. Solche Abfragen werden in der Regel mit Hilfe einer formalen Grammatik durchgeführt, die die zulässige Kantenbeschriftung der Pfade beschreibt. Eine Pfadabfrage soll mit Hilfe der relationalen Abfragesemantik berechnet werden, wenn sie zu einem Tripel ausgewertet wird (A,v1,v2), so dass es einen Pfad vonv1 nach v2 gibt, sodass die Beschriftungen an den Kanten dieses Pfades eine vom Nichtterminal A ableitbare Zeichenkette bilden. Wir konzentrieren uns auf die booleschen Sprachen, die boolesche Grammatiken zur Beschreibung der Beschriftung von Pfaden verwenden. Obwohl die Pfadabfrage mit relationaler Abfragesemantik und booleschen Grammatiken bekanntermaßen unentscheidbar ist, schlagen wir in dieser Arbeit einen Algorithmus zur Pfadabfrage auf azyklischen Graphen vor, der relationale Abfragesemantik und boolesche Grammatiken verwendet und die exakte Lösung annähert. Um eine bessere Leistung im Vergleich zum naiven Algorithmus zu erzielen, wurden die betrachteten Klassen von Graphen auf azyklische Graphen beschränkt.

Ergebnisse des Institute for System Programming

Ergebnisse des miniKanren- und Relationale-Programmierung-Workshops 2019

SEIM-19

Vorläufige Ergebnisse des 13. Frühjahr/Sommer-Kolloquiums für junge Forscher*innen über Softwaretechnik (SYRCoSE 2019), 29. bis 31. Mai 2019 – Saratow, Russische Föderation

Ergebnisse des miniKanren- und Relationale-Programmierung-Workshops 2019

Ergebnisse des miniKanren- und Relationale-Programmierung-Workshops 2019

Programming and Computer Software

Erweiterte Zusammenfassung auf dem TyDe 2018 (auf der ICFP).

Die transparente Integration einer domänenspezifischen Sprache zur Spezifikation von kontextfreien Pfadabfragen (CFPQs) in eine allgemeine Programmiersprache sowie die statische Überprüfung von Fehlern in Abfragen können die Entwicklung von Anwendungen, die CFPQs verwenden, erheblich vereinfachen. LINQ und ORM können für die Integration verwendet werden, aber sie haben Probleme mit der Flexibilität: Die Zerlegung von Abfragen und die Wiederverwendung von Unterabfragen sind eine Herausforderung. Die Anpassung der Technik der Parser-Kombinatoren für die Abfrage von Pfaden kann diese Probleme lösen. Konventionelle Parser-Kombinatoren verarbeiten lineare Eingaben, und nur von der Trails-Bibliothek ist bekannt, dass sie diese Technik für Pfadabfragen anwendet. Wir zeigen, dass es möglich ist, allgemeine Parser-Kombinatoren für CFPQ zu erstellen, die beliebige kontextfreie Grammatiken und beliebige Eingabegraphen unterstützen. Wir implementieren eine Bibliothek solcher Parser-Kombinatoren und zeigen, dass sie für realistische Aufgaben anwendbar ist.

Ergebnisse des 9. ACM SIGPLAN Internationalen Symposiums über Scala

NTV SPbSTU

GRADES-NDA'18: Ergebnisse des 1. gemeinsamen internationalen ACM-SIGMOD-Workshops über Graphdatenmanagement-Erfahrungen und -Systeme (GRADES) und Netzwerkdatenanalyse (NDA)

18th International Symposium on Trends in Functional Programming

Ergebnisse des 20. internationalen Symposiums über Prinzipien und Praxis der deklarativen Programmierung

Ergebnisse der ML/OCAML 2016

40th ACM/IEEE International Conference on Software Engineering, ICSE 2018

NTV SPbSTU

Es gibt mehrere Lösungen für CFPQ, aber wie man eine strukturelle Darstellung des Abfrageergebnisses bereitstellen kann, die für die Verarbeitung von Antworten und die Fehlersuche praktisch ist, ist noch ein offenes Problem. In dieser Forschungsarbeit schlagen wir eine Graph-Parsing-Technik vor, die es erlaubt, eine solche Repräsentation in Bezug auf eine gegebene Grammatik in polynomieller Zeit und Raum für eine beliebige kontextfreie Grammatik und einen beliebigen Graphen zu erstellen. Der vorgeschlagene Algorithmus basiert auf einem verallgemeinerten LL-Parsing-Algorithmus, während bisherige Lösungen meist auf CYK- oder Earley-Algorithmen beruhen, was die Zeitkomplexität in einigen Fällen verringert.

Ergebnisse der 13. Mittel- und Osteuropäischen Softwareentwicklungskonferenz in Russland (CEE-SECR '17)

Tagungsband des ISP RAS

arXiv

The European Conference on Object-Oriented Programming (ECOOP)

Ergebnisse des ACM-SIGPLAN-Workshops 2017 zu partieller Bewertung und Programmmanipulation

St. Petersburg State Polytechnical University Journal. Computer Science. Telekommunikation und Kontrollsysteme

Izvestia vuzov. North Caucasus Region. Technical Sciences, 2017, Nr. 4, Seiten 5-12

Ergebnisse des Institute for System Programming

arXiv

Wir stellen eine Methode zur Syntaxanalyse eines regulären Satzes von Eingabezeichenfolgen vor. Dieses Problem ist für die Analyse von in Strings eingebetteten Sprachen relevant, wenn ein Host-Programm zur Laufzeit Klauseln einer eingebetteten Sprache erzeugt. Unsere Methode basiert auf einer Verallgemeinerung des RNGLR-Algorithmus, der es uns ermöglicht, eine endliche Repräsentation des Parse-Forest für eine regelmäßig approximierte Menge von Eingabestrings zu konstruieren. Diese Repräsentation kann für semantische Analysen und Transformationen im Rahmen von Reengineering, Codewartung, Programmverständnis usw. weiterverwendet werden. Der fragliche Ansatz implementiert Relaxed-Parsing: Nicht erkannte Zeichenketten in der Approximationsmenge werden ohne Fehlererkennung ignoriert.

Perspectives of System Informatics

Systems and Means of Informatics

META 2016 5. internationaler Valentin-Turchin-Workshop über Metacomputation

SEIM-16

NTV SPbSTU 4 (224)

Systems and Means of Informatics

Science of Computer Programming

Ergebnisse der 11. Mittel- und Osteuropäischen Softwareentwicklungskonferenz in Russland

Ergebnisse der 9. Internationalen Andrei-Ershov-Gedenkkonferenz über Perspektiven der Systeminformatik

Ergebnisse der 10. Mittel- und Osteuropäischen Softwareentwicklungskonferenz in Russland 2014

Ergebnisse der 10. Mittel- und Osteuropäischen Softwareentwicklungskonferenz in Russland

Ergebnisse der 9. Mittel- und Osteuropäischen Softwareentwicklungskonferenz in Russland

Workshop zu ML

Ergebnisse des Ost-West-Design- und Test-Symposiums 2010

Ergebnisse der 6. Internationalen Andrei-Ershov-Gedenkkonferenz über Perspektiven der Systeminformatik

Workshop über Multiparadigmen-Programmierung mit objektorientierten Sprachen

System Informatics

System Programming

System Programming

Ergebnisse der Europäischen Konferenz über Software-Wartung und Reengineering, CSMR 995802, S. 177-185

Ergebnisse der 4. Internationalen Andrei-Ershov-Gedenkkonferenz über Perspektiven der Systeminformatik

Automated Reengeneering of Programs, Saint Petersburg