Component-based synthesis using combinatory logic, intersection types and predicates
Loading...
Date
2025
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Alternative Title(s)
Abstract
In dieser Arbeit wird eine neue Version des Combinatory Logic Synthesizer ((CL)S) vorgestellt, der Combinatory Logic Synthesizer with Predicates (CLSP) genannt wird. Dieses neue Framework verwendet Inhabitation in der kürzlich entwickelten Finite Combinatory Logic with Predicates (FCLP) anstelle der Finite Combinatory Logic (FCL), die in früheren Iterationen verwendet wird. FCLP bietet neue Spezifikationsmöglichkeiten durch die Hinzufügung von parametrisierten Typen, die es erlauben, von einer endlichen Menge von Literalen abzuhängen und durch Prädikate eingeschränkt zu werden. Der Fokus von CLSP unterscheidet sich von früheren Iterationen von (CL)S darin, dass er mit Schwerpunkt auf Ausführungsgeschwindigkeit und Benutzerfreundlichkeit entwickelt wurde, anstatt auf beweisbare Korrektheit. Sowohl die theoretischen Grundlagen des Frameworks als auch die Implementierung in Python werden diskutiert. Eine Evaluation
des Frameworks in Form von Benchmarks wird präsentiert, die verschiedene Modellierungstechniken des neuen Frameworks miteinander vergleicht, sowie die
Synthesegeschwindigkeit von CLSP mit früheren Iterationen von (CL)S. Letzteres zeigt eine Verbesserung der Laufzeit von bis zu 100-fach, verglichen mit der schnellsten (CL)S Version, in bestimmten Benchmarks. Weiterhin wird eine prototypische parallele Implementierung des Inhabitationsalgorithmus vorgestellt, der eine beinahe lineare Beschleunigung in der Anzahl der verwendeten CPU-Kerne zeigt. Abschließend werden zwei Anwendungen des Frameworks diskutiert, eins, zum Finden von Strategien in einem Fragment von LTL, und eins, im Kontext von Simulationsmodellen in Materialflusssystemen. Dies zeigt, wie das Framework sowohl in theoretischen und praktischen Anwendungen genutzt werden kann.
Description
Table of contents
Keywords
Combinatory logic, Intersection types, Program synthesis
Subjects based on RSWK
Kombinatorische Logik, Programmsynthese