Diese Arbeit beschäftigt sich mit mechanisierter Konfluenzanalyse von Ersetzungssystemen. Ersetzungssysteme bestehen aus gerichteten Gleichungen, mit denen Berechnungen ausgeführt werden, indem wiederholt Instanzen von linken Seiten der Gleichungen durch die entsprechenden rechten Seiten ersetzt werden. Konfluenz ist eine fundamentale Eigenschaft von Ersetzungssystemen, die sicherstellt, dass verschiedene Berechnungspfade dasselbe Ergebnis liefern. Da Ersetzung Turing-vollständig ist, ist Konfluenz im Allgemeinen nicht entscheidbar. Nichtsdestotrotz wurden Techniken entwickelt, mit denen Konfluenz für viele Ersetzungssysteme bestimmt werden kann, und einige automatische Konfluenzbeweiser werden aktiv entwickelt. Unser Ziel ist es, drei Aspekte der automatischen Konfluenzanalyse zu verbessern, nämlich (a) Zuverlässigkeit, (b) Mächtigkeit, und (c) Vielseitigkeit. Die Bedeutung dieser Aspekte wird von einem jährlichen Konfluenzwettbewerb bezeugt, bei dem die führenden automatischen Beweiser Konfluenz von Ersetzungssystemen analysieren. Um die Zuverlässigkeit von automatischer Konfluenzanalyse zu verbessern, formalisieren wir Konfluenzkriterien in dem Beweisassistenten Isabelle/HOL, und erhalten so ein verifiziertes, ausführbares Programm zur Überprüfung von Konfluenzbeweisen. Um die Mächtigkeit von Konfluenzbeweisern zu erhöhen, präsentieren wir eine bemerkenswert einfache Technik, basierend auf dem Hinzufügen und Entfernen redundanter Gleichungen, die bestehende Techniken stärkt. Um die automatische Konfluenzanalyse vielseitiger zu machen, entwickeln wir einen Konfluenzbeweiser für Ersetzung mit Funktionsvariablen und gebundenen Variablen.
Titelaufnahme
- TitelMechanizing confluence : automated and certified analysis of first- and higher-order rewrite systems / Julian Nagele
- Weitere TitelMechanizing confluence
- verfasst von
- betreut von
- ErschienenInnsbruck, October 2017
- Umfangxii, 152 Seiten : Diagramme
- AnmerkungAbweichender Titel laut Übersetzung der Verfasserin/des Verfassers
- Datum der AbgabeOktober 2017
- SpracheEnglisch
- DokumenttypDissertation
- Schlagwörter
- Schlagwörter (DE)
- Schlagwörter (EN)
- URN
- Das Dokument ist online verfügbar
- Nachweis
This thesis is devoted to the mechanized confluence analysis of rewrite systems. Rewrite systems consist of directed equations and computation is performed by successively replacing instances of left-hand sides of equations by the corresponding instance of the right-hand side. Confluence is a fundamental property of rewrite systems, which ensures that different computation paths produce the same result. Since rewriting is Turing-complete, confluence is undecidable in general. Nevertheless, techniques have been developed that can be used to determine confluence for many rewrite systems and several automatic confluence provers are under active development. Our goal is to improve three aspects of automatic confluence analysis, namely (a) reliability, (b) power, and (c) versatility. The importance of these aspects is witnessed by the annual international confluence competition, here the leading automated tools analyze confluence of rewrite systems. To improve the reliability of automatic confluence analysis, we formalize confluence criteria for rewriting in the proof assistant Isabelle/HOL, resulting in a verified, executable checker for confluence proofs. To enhance the power of confluence tools, we present a remarkably simple technique, based on the addition and removal of redundant equations, that strengthens existing techniques. To make automatic confluence analysis more versatile, we develop a higher-order confluence tool, making automatic confluence analysis applicable to systems with functional and bound variables.
- Das PDF-Dokument wurde 63 mal heruntergeladen.