|
|
|
|
||
| Nutzungshinweise | Recherche | Gästebuch | ||
Dr. Dieter Hofbauer
Zusammenfassung:
Terme sind in der Informatik allgegenwärtig. In der Theorie der
deklarativen Programmierung spielen Termersetzungssysteme
traditionell ebenso eine Rolle wie beim maschinellen
Theorembeweisen.
Erst in den letzten Jahren haben verstärkt Konzepte und Methoden
aus der Theorie der Automaten und formalen Sprachen in diesen Bereich
Einzug gehalten.
Im Vortrag wird nach einer kurzen Darstellung grundlegender
Begriffe aus der Theorie der Baumsprachen eine exemplarische
Anwendung ausführlicher vorgestellt. Es wird gezeigt, wie
klassische algebraische und automatentheoretische Konzepte
verwendet
werden können, um sogenannte Testmengen für den universellen
Abschluss regulärer Baumsprachen zu berechnen und zu
minimieren. Solche Testmengen werden etwa benutzt, um
Grundreduzierbarkeit von Termen zu entscheiden, eine für
Induktionsbeweise wesentliche Eigenschaft.
Dr. Johannes Waldmann
Zusammenfassung:
Die folgenden Begriffe haben genau die gleiche Ausdruckskraft bei der
Beschreibung von Sprachen (von Wörtern und Bäumen):
Dr. Johannes Waldmann
Zusammenfassung:
Die set based program analysis gewinnt aus dem Text eines Programms
ein System von set constraints: Gleichungen und Ungleichungen
(Inklusionen) zwischen Mengen. Dessen Lösung approximiert die
möglichen Werte der Programmvariablen. Mit dieser Information
können wir Programmeigenschaften nachweisen. Diese verwenden wir
beispielsweise zum optimierenden Kompilieren.
Es ist entscheidbar, ob ein Set-Constraint-System lösbar ist. Falls
ja, dann erlaubt es sogar eine reguläre Lösung (ein Tupel
regulärer Baumsprachen). Diese beschreiben wir durch generalized
tree set automata. Das Problem ist NEXPTIME-vollständig. Durch
Einschränken der erlaubten Constraints können wir die
Komplexität reduzieren.
Literatur:
Dr. Johannes Waldmann
Leonid Bazhenov
Leonid Bazhenov
Dr. John O'Donnell
This is joint work with John Hughes.
Dipl.-Inf. Michael Hartwig
Nguyen Thanh Hai
Prof. Dr. Mamoru Kanek
Prof. Dr. Nobu-Yuki Suzuki
Dr. Johannes Waldmann
Insbesondere soll die transitive Hülle einer solchen Relation
berechenbar sein,
denn wir möchten damit Nachfolgermengen bezüglich eines
Term-Ersetzungs-Systems
(TRS) beschreiben oder doch wenigstens approximieren.
Dauchet, Tison, Heuillard und Lescanne definierten dafür 1987 Ground
Tree
Transducer (GTTs) und zeigten damit die Entscheidbarkeit der
Konfluenz
von Grund-TRS.
Ich schlage eine Klasse von Relationen MDGTT vor, die in gewissem
Sinne
dual zu GTT ist. Sie erbt viele der GTT-Eigenschaften. Auch
Beweisideen
lassen sich übertragen, benötigen aber Modifikationen.
An Beispielen zeige ich, wie sich GTTs und DGTTs bei der
Approximation von
Nachfolgermengen ergänzen.
Prof. Dr. Grigoris Antoniou, Griffith University, Australien
In diesem Vortrag werden die wesentlichen Begriffe der Inferenz mit
Standardannahmen besprochen. Es wird besonders auf neue Ergebnisse
auf den Gebieten der effizienten Inferenz, der Revision von
Wissensbasen, und Inferenz auf der Basis der logischen Programmierung
eingegangen. Anwendungsaspekte werden ebenfalls besprochen.
Nennen wir Sigma(n) die maximale Zahl der mit n Zuständen
schreibbaren 1.
Dann ist die Funktion Sigma nicht berechenbar (weil sie zu schnell
wächst).
Trotzdem gibt es Abschätzungen und auch konkrete Schranken
für kleine Argumente, erhalten durch vollständiges Aufzählen der interessierenden Maschinen.
Das geht natürlich im allgemeinen nicht gut - wir müssen sehr
viele Maschinen auflisten und für jede das Halteproblem lösen.
Für kleine n können wir aber in den meisten Fällen
die Bandmuster durch reguläre Sprachen beschreiben.
Im Vortrag wird für n = 5 auf diese Weise
der bisher aussichtsreichste Kandidat analysiert,
aber auch eine Maschine gezeigt, deren Bandmuster nicht periodisch,
sondern selbstähnlich explodieren.
Literatur: Heiner Marxen: Busy Beaver
(http://www.drb.insel.de/~heiner/BB/index.html)
Übungsaufgabe: Welche Maschine leistet Sigma(2) = 4 ?
(Zwei Zustände, und ein zusätzlicher Haltzustand.)
Sie erweisen sich dort als sehr nützlich,
weil sie Programmtexte strukturieren
und Programmeigenschaften leicht beweisbar machen.
Insbesondere gestatten Monaden den sauberen Import
der imperativen in die funktionale Welt,
wie am Beispiel der Ein/Ausgabe in Haskell deutlich wird.
Literatur:
Semantik-Ansätze für funktionale Sprachen -
1999
Forschungsgruppe Theoretische Informatik
des FB Mathematik / Informatik der
Universität Gesamthochschule Kassel
Testmengen und Automaten für den universellen Abschluss
regulärer Sprachen -
Formalsprachliche Methoden in der Termersetzung
Institut für Informatik (Uni Leipzig)
Logische Klassifizierung regulärer Sprachen
Durch Einschr"ankung erhalten wir Teilklassen. Eine interessante
Klasse
von Wortsprachen sind diejenigen, die beschrieben werden durch
Diese Klasse wird von der Straubing-Hierarchie ausgeschöpft.
Der Vortrag präsentiert dazugehörige Definitionen, Sätze und
Beweisideen und erwähnt offenen Probleme, insbesondere beim
Übertragen der Begriffe auf Baumsprachen.
Institut für Informatik (Uni Leipzig)
Set Constraints
Institut für Informatik (Uni Leipzig)
Top-Termination für CL(S)
Technische Universität Donezk
Object Oriented and Functional Approaches in Design of Dialog Systems for Massiv Parallel Simulation Environment
Technische Universität Donezk
Parallel Simulation of Dynamic Systems on SIMD supercomputer
University of Glasgow
Nondeterminism in Pure Nonstrict Functional Languages
Institut für Informatik, Universitüt Leipzig
Funktional-logisches Programmieren / Collecting of Facts
Im Anschluss soll die Idee des "Collecting of Facts"
(Faktensammeln) im Ansatz diskutiert werden.
Hierbei werden nicht strukturierte Graphen oder Bäume,
sondern Mengen von strukturarmen Termen (Fakten) reduziert.
Zum einen soll untersucht werden, ob dies mehr oder weniger als
bekannte Konzepte leistet, zum anderen dient diese
Herangehensweise dazu, sich an die Erweiterung
funktional-logischer Sprachen heranzuwagen.
Institut für Informatik, Universitüt Leipzig
Ontologische und begriffliche Grundlagen der objektorientierten Datenmodellierung
1998
Institute of Policy and Planning Sciences
University of Tsukuba, Ibaraki, Japan
Experiences and False Beliefs in a Game Theoretical Situation
Department of Mathematics, Shizuoka University, Japan
Possible world semantics with graded accessibility
Institut für Informatik, Universitüt Leipzig
Dual Ground Tree Transducer
Wissensrepräsentation und Inferenz mit Standardannahmen
Busy Beaver
Mathematische Grundlagen der Semantik funktional-logischer Sprachen
(Fortsetzung)
Mathematische Grundlagen der Semantik funktional-logischer Sprachen
Mereologie und Teil-Ganzes-Beziehung
Monaden für Funktionales Programmieren
(Fortsetzung)
Monaden für Funktionales Programmieren
Erweiterung der logischen Progammierung(Forts.)
Erweiterung der logischen Progammierung
Das System DESIRE zum Entwurf wissensbasierter Systeme im Überblick
Teil 2 mit Vorführung
Das System DESIRE zum Entwurf wissensbasierter Systeme im Überblick
Zur algebraischen Semantik logischer Sprachen
Zusammenhänge zwischen Term-Ersetzungs-Systemen und
regulären Baum-Sprachen
Das im Vortrag vom 21. 4. vorgestellte Resultat über die
Entscheidbarkeit der Normalisierung von S-Termen wird als
Beispiel unter Punkt 1 eingeordnet. Es läßt allerdings noch
Fragen offen, die kurz diskutiert werden sollen.
Term-Ersetzungs-Systeme und Reguläre Baum-Sprachen
am Beispiel des Kombinators S
Erweiterungen funktionaler Sprachen (Teil II)
Erweiterungen funktionaler Sprachen am Beispiel der Sprachen ProFun, VisBeta und M
Parallelisierungen in funktionalen Sprachen am Beispiel des
Concurrent Clean
Semantik-Ansätze für funktionale Sprachen (Fortsetzung)
Semantik-Ansätze für funktionale Sprachen. Teil III
Semantik-Ansätze für funktionale Sprachen. Teil II
Semantik-Ansätze für funktionale Sprachen. Teil I
Objektorientiertes Programmieren unter verschiedenen Sprachparadigmen
Zu semantischen Konzepten in LIFE (Teil 2):
OSF-Graphen und Graphalgebren
Multiple Redirection in funktional-logischen Sprachen
Zu semantischen Konzepten in LIFE
Die Methode des Narrowing - umgesetzt in BABEL
Impressum:
Herausgeber: Universität Leipzig, Institut für Informatik
Seitenbetreuer: Andreas Zerbst
(e-mail: zerbst@informatik.uni-leipzig.de)
Letzte Änderung:
02.09.99
Status: permanent