 Mi,10.5.2000
|
Christine Röckl
Über die Prozeßanalyse in Higher Order Abstract Syntax
|
Theorembeweiser wie Isabelle oder Coq
unterscheiden zwei Argumentationsebenen. Auf
einer durch die Implementierung
bereitgestellten "Metalogik" lassen sich
"Objektlogiken" formalisieren, in denen
Datenstrukturen definiert, und auf deren Basis
Beweise abgeleitet werden
können. Programmiersprachen oder
Kalküle können vollständig auf
der Objektebene eingeführt werden, aber
auch unter Verwendung der funktionalen
Mechanismen der Metaebene.
Der erste Ansatz, das deep embedding,
wird üblicherweise dann verwendet, wenn
vorwiegend theoretische Aspekte über die
zu untersuchende Sprache gezeigt werden
sollen. Ein Hauptnachteil ist, daß der
Ansatz die Einführung von Substitutionen
notwendig macht, um Alphakonversion sowie
Betareduktion zu implementieren.
Der zweite Ansatz, das shallow
embedding, benutzt die funktionalen
Mechanismen zur Alphakonversion und
Betareduktion der Metaebene, und vermeidet
dadurch die Einführung von
Substitutionen. Gerade für das Beweisen
über konkreten Programmen ist dieser
Ansatz geeignet. Allerdings bringt auch er
Probleme mit sich: (1) Die Formalisierung
beinhaltet "exotische" Programme; und (2) es
gibt kein funktionierendes strukturelles
Induktionsprinzip mehr.
Um nun genau die Menge der korrekten
Formalisierungen in higher order abstract
syntax (HOAS) sowie ein anwendbares
strukturelles Induktionsprinzip zu erhalten,
schlagen Despeyroux, Felty und Hirschowitz die
Verwendung induktiv definierter
Wohlgeformtheitsprädikate
vor.
Wir wenden diese Technik an, um die Syntax des
Pi-Kalkuels in HOAS zu formalisieren, und um
drei essentielle syntaktische Eigenschaften zu
beweisen. Die Beweise dieser Eigenschaften
sind gerade deshalb interessant, weil sich in
ihnen die Verquickung der Objekt- und
Metaebene in HOAS stark widerspiegelt.
Die Formalisierung sowie alle Beweise wurden
in der aktuellen Version von Isabelle/HOL durchgefuehrt. Die Skripten stehen unter http://wwwbrauer.informatik.tu-muenchen.de/~roeckl/PI/syntax.shtml zur Verfügung.
Der Vortrag führt grundlegend in
das Thema ein. Spezialisierte Kenntnisse
über Theorembeweiser sind nicht
notwendig.
|
|
|
Mi,24.5.2000
|
Mark Scharbrodt
Maintenance Scheduling
|
This talk concerns a variant of scheduling
with limited machine availibility where
unavailibility constraints are soft. In
contrast to the well known fixed pattern
models, the schedulers may assign the jobs at
any period of time, however they have to
make sure that processing is periodically
interrupted in order to allow for machine
services such as cleaning, preventive
maintenance or other machine check ups. Our
model defines a maximum time slack between two
machine services. The jobs and the machine
services are to be scheduled in such a way
that the maximum time slack is never
exceeded.
In this talk we consider the approximability
status of this scheduling problem. Seen first
from a pure theoretical point of view we prove
the existence of a polynomial time
approximation scheme in the constant machine
case and of an asymptotic polynomial time
approximation scheme in the variable machine
case. As negative results we prove that an
FPTAS resp. PTAS cannot exist, unless P =
NP. In regard to the practical applications
of the problem we consider the online version
of the problem and show that a simple
LIST--type algorithm achieves a worst case
ratio of 2.
|
|
|
Di,30.5.2000, 13:00
|
Thomas Bayer (Universität Kaiserslautern)
Ein Algorithmus zur Berechnung des
Durchschnittes von Invariantenringen
|
|
Es wird ein Algorithmus vorgestellt, der den
Durchschnitt von zwei Invariantenringen von
endlichen Matrixgruppen berechnet,
vorausgesetzt, daß die Ordnungen der beiden
Matrixgruppen nicht von der Charakteristik des
Grundkörpers geteilt werden. Zusammen mit der
Tatsache, daß Invariantenringe von zyklischen
Matrixgruppen über algebraisch abgeschlossenen
Körpern ohne Gröbner Basen berechnet werden
können, ergibt sich eine alternative Methode
zur Berechnung von Invariantenringen. Weiters
soll auf eine mögliche Erweiterung zur
Berechnung des Durchschnittes von durch
endlich viele homogene Polynome erzeugten
Unterringe des multivariaten Polynomringes
hingewiesen werden. Das Problem, ob der
Durchschnitt solcher Unterringe endlich
erzeugt ist, ist aber noch
offen.
|
|
|
Mi,31.5.2000
|
Hannah Bast (Max-Planck-Institut für Informatik)
On Scheduling Parallel Tasks at Twilight
|
We consider the problem of processing a given
number of tasks on a given number of
processors as quickly as possible when only
vague information on the processing times of
the tasks is available in advance. The tasks
are assigned to the processors in chunks
consisting of several tasks at a time, and the
difficulty lies in finding the optimal
tradeoff between the processors' load balance,
which is favoured by having small chunks, and
the total scheduling overhead, which will be
the lower the fewer chunks there are.
We argue why traditional approaches like
competitive or probabilistic analysis are
inappropriate to model the uncertainty
inherent to this kind of online problem, and
present a novel approach that captures the
issues of both incomplete and imprecise
information while maintaining the amenability
to mathematical analysis.
We exemplify the power of our approach by a
problem from automatic loop parallelization,
for which a large variety of heuristics have
been proposed in the past, but hardly any
rigorous analysis has previously been known.
|
|
|
Mi,7.6.2000
|
Anusch Taraz (Humboldt-Universität zu Berlin)
Randomisierte Algorithmen zur Erzeugung spezieller Graphenklassen
|
Wie generiert man zufällige Graphen mit
bestimmten Eigenschaften? Wir betrachten das
folgende einfache Verfahren, das Graphen
erzeugt, die keine Dreiecke enthalten und
diesbezüglich maximal sind. Beginnend mit
dem leeren Graphen auf n Knoten wählt man in
jedem Schritt eine Kante zufällig aus und
fügt sie - falls dabei kein Dreieck entsteht
- zu dem Graphen hinzu. Das Verfahren endet,
wenn alle Kanten ausprobiert worden sind.
Offensichtlich ist das Endergebnis ein
maximaler dreiecksfreier Graph. Seine
Kantenanzahl kann zwischen linear (z.B. bei
einem Stern) und quadratisch (z.B. bei einem
vollständig bipartiten Graphen mit gleich
großen Klassen) liegen, je nachdem in welcher
Reihenfolge die Kanten ausprobiert
wurden. Erdös, Suen und Winkler konnten aber
beweisen, daß die Kantenanzahl fast immer
eine Größenordnung von n^{3/2} hat. Sie
zeigten allerdings auch, daß das (scheinbar)
restriktivere Verfahren, bei dem nicht nur
Dreiecke, sondern alle Kreise ungerader Länge
verboten werden, fast immer quadratisch viele
Kanten hervorbringt.
Um diese überraschende Tatsache besser zu
verstehen, regte Erdös die allgemeine
Betrachtung des Problems an, bei der statt
eines Dreiecks ein beliebiger Graph verboten
wird. Im Vortrag zeigen wir, daß sich hier
für eine große Klasse von Graphen eine
ähnlich präzise Vorhersage der Kantenanzahl
machen läßt, und erörtern,
warum dies in gewisser Weise für
beliebige Graphen nicht machbar sein wird.
|
|
|
Mi,21.6.2000
|
Jochen Alber
(Universität Tübingen)
Fixed Parameter Algorithms for Planar
Dominating Set and Related Problems
|
We present an algorithm for computing the
domination number of a planar graph that uses
O(c^{\sqrt{k}} n) time, where k
is the domination number of the given planar
input graph and c is a constant.
To obtain this result, we show that the
treewidth of a planar graph with domination
number k is O(\sqrt{k}). This
can be done by constructing appropriate
separators of small size. The algorithm then
builds a corresponding tree decomposition, and
uses the tree decomposition to compute the
domination number and a minimum size
dominating set.
The same technique can be used to show that
the disk dimension problem (find a minimum set
of faces that cover all vertices of a given
plane graph) can be solved in
O(c_1^{\sqrt{k}} n) time for
c_1=2^{6\sqrt{34}}. Similar results
can be obtained for some variants of
dominating set, e.g., independent dominating
set.
|
|
|
Mi,28.6.2000
|
|
|
Mi,5.7.2000
|
Peter Rossmanith
Neues über Dominating Sets für Planare Graphen
|
|
Vor zwei Wochen wurde bereits von Jochen Alber
ein Algorithmus vorgestellt, der einen
Dominating Set der Größe k in nur
O(1)^sqrt(k) Schritten finden kann, falls der
Graph planar ist. Dieser Vortrag bringt zwei
Ergänzungen. Die erste ist eine
Problemkernreduktion, also ein polynomieller
Algorithmus, der das Problem auf einen Graphen
zurückführt, dessen Größe nur noch
polynomiell in k ist. Dann folgt noch ein
neuer Algorithmus, der das selbe Problem
löst, aber einige Vorteile bietet. Er basiert
wieder auf Separatoren, aber auf wesentlich
einfacheren, die im Vortrag vorgestellt werden
können. Die Laufzeit ist aber ebenfalls
besser. Diese Arbeit entsteht zusammen mit
Jochen Alber.
|
|
|
Mi,12.7.2000
|
Marcus Hutter (BrainLAB GmbH)
Error Bounds for Universal Solomonoff Sequence Prediction
|
Several new relations between universal
Solomonoff sequence prediction and informed
prediction and general probabilistic
prediction schemes will be proved. Among
others, they show that the number of errors
in Solomonoff prediction is finite for
computable prior probability, if finite in the
informed case, where the prior is
known. Deterministic variants will also be
studied. The most interesting result is that
the deterministic variant of Solomonoff
prediction is optimal compared to any other
probabilistic or deterministic prediction
scheme apart from additive square root
corrections only. This makes it well suited
even for difficult prediction problems, where
it does not suffice when the number of errors
is minimal to within some factor greater than
one. Solomonoff's original bound and the ones
presented here complement each other in a
useful way.
Keywords: induction;
Solomonoff,Bayesian,deterministic prediction;
Kolmogorov complexity.
|
|
|
Mi,19.7.2000
|
Jens Gramm (Universität Tübingen)
Neue Obere Schranken für MAX-2-SAT und
ihre Anwendung auf MAX-CUT
|
Das Maximum 2-Satisfiability Problem
(MAX-2-SAT) ist: Gegeben eine Boolsche Formel
in 2-KNF, finde eine Belegung, unter der eine
möglichst grosse Anzahl von Klauseln
erfüllt wird. MAX-2-SAT ist
MAX-SNP-vollständig und wurde bisher vor
allem hinsichtlich approximativer
(Polynomzeit-) Algorithmen untersucht,
hinsichtlich exakter (Exponentialzeit-)
Algorithmen nur als allgemeineres MAX-SAT
Problem.
In diesem Vortrag stellen wir einen exakten
Algorithmus vor, der MAX-2-SAT in Laufzeit
löst, wobei K die Anzahl der Klauseln und
L ihre Länge ist. Da wir in unserer
Analyse nur Klauseln zählen, die genau
zwei Literale enthalten, folgt daraus eine
Schranke von . Unsere Ergebnisse
verbessern deutlich bisherige Schranken, die
für das allgemeine MAX-SAT Problem
bekannt sind: in Bezug auf K eine Schranke von
, in
Bezug auf L eine Schranke von . Dabei sind unser
Algorithmus und seine Analyse einfacher als
frührere MAX-SAT Algorithmen.
Durch
Anwendung unserer Algorithmen auf das
(MAX-SNP-vollständige) Maximum Cut
Problem (MAX-CUT) zeigen wir, dass es in
Laufzeit
gelöst werden kann, wobei M die Anzahl
der Kanten im gegebenen Graphen ist. Besonders
interessant ist dies Ergebnis für
dünne Graphen.
Gemeinsame Arbeit mit Edward A. Hirsch
(St. Petersburg), Rolf Niedermeier
(Tübingen) und Peter Rossmanith
(München).
|
|
|
Mi,26.7.2000
|
Martin Skutella (TU Berlin)
On the single source unsplittable min-cost flow problem
|
We consider the following single source
unsplittable flow problem with costs: A set of
commodities must be routed simultaneously from
a common source vertex to certain destination
vertices in a given graph with capacities and
costs on the edges; for each commodity, there
is a specified demand that must be routed
unsplittably (on a single path) from the
source to its destination; the flow value on
any edge in the graph must not violate its
capacity and the total cost of the flow must
not exceed a given budget.
This problem has been introduced by Kleinberg;
it contains and can thus be seen as a
generalization of several NP-complete problems
from various areas in combinatorial
optimization such as packing, partitioning,
scheduling, load balancing, and
virtual-circuit routing problems.
Recently, Kolliopoulos and Stein and later
Dinitz, Garg, and Goemans developed algorithms
improving the first approximation results of
Kleinberg for various variants of the problem.
In these algorithms, the capacity constraints
are relaxed or eluded, either by allowing a
bounded violation of edge capacities, or by
routing only a subset of demands, or by
routing all commodities in several rounds.
However, none of the developed techniques is
capable of providing solutions without
relaxing the cost constraint; so far, all
known approximation algorithms for the problem
with costs are bicriteria approximations.
For the optimization versions of the problem
mentioned above, we give the first
approximation results without relaxing the
cost constraint. Moreover, all results
presented in this paper dominate the best
previously known bicriteria approximations.
At the core of our approximation algorithms is
a procedure that, given a splittable flow
satisfying all demands and respecting
capacities of edges, computes an unsplittable
solution without increasing cost such that the
sum of all but one demand routed across any
edge is less than twice the flow value on this
edge in the splittable flow. These results
partly build upon techniques developed by
Kolliopoulos and Stein and Dinitz, Garg, and Goemans.
Finally, we give the currently best known
results on the hardness of approximation
for several variants of the problem under
consideration (even without costs).
|
|
|
