Gegenstand dieser Arbeit ist CL(S), das Termersetzungssystem mit der einzigen Regel: Sxyz -> xz(yz) Sie ist ein Schritt auf dem Weg, an dessen Ziel man sich die Lösung des Wortproblems für CL(S) erhofft. Waldmann zeigte, daß in CL(S) die Termination entscheidbar ist und daß jede unendliche Reduktion top-terminiert. Daraus folgt, daß unendliche Normalformen existieren und das Wortproblem gelöst wäre, könnte man diese Normalformen effektiv finden und vergleichen. Deswegen untersuche ich in der vorliegenden Arbeit unendliche Reduktionsketten in CL(S). Es wird vermutet, daß sie im wesentlichen durch Muster wie z.B. M^n+1 := SS M^n beschreibbar sind. ... Darüberhinaus wird vermutet, daß tatsächlich jeder Term aus CL(S) ohne endliche Normalform eine unendliche Reduktionskette mit einem Muster Muster aufweist. Ich präsentiere vier Beweisschemata, mit deren Hilfe sich unendliche Reduktionsketten in allen bisher untersuchten Termen ohne Normalform beweisen lassen. Zudem definiere ich das Konzept der allgemeinsten Muster, mit denen sich Muster klassifizieren lassen, und beweise, daß die Menge der allgemeinsten Muster unendlich ist. Außerdem beschreibe ich, wie man Muster automatisch findet und verifiziert. Schließlich stelle ich einen Beweisansatz vor, mit dem die zwingende Existenz von Mustern belegbar wäre. Als eine Folgerung aus diesem Beweis ergäbe sich weiterhin die Schleifenfreiheit von CL(S). ...
| Identifer | oai:union.ndltd.org:DRESDEN/oai:qucosa:de:qucosa:16521 |
| Date | 20 October 2017 |
| Creators | Dörges, Till |
| Contributors | Universität Leipzig |
| Source Sets | Hochschulschriftenserver (HSSS) der SLUB Dresden |
| Language | German |
| Detected Language | German |
| Type | info:eu-repo/semantics/acceptedVersion, doc-type:masterThesis, info:eu-repo/semantics/masterThesis, doc-type:Text |
| Rights | info:eu-repo/semantics/openAccess |
| Relation | urn:nbn:de:bsz:15-qucosa2-163403, qucosa:16340 |
Page generated in 0.0018 seconds