Campus Event Calendar
Event Entry
What and Who
Subtype Satisfiability and Entailment
Tim Priesnitz
Promotionskolloquium
AG 1, AG 2, AG 3, AG 4, AG 5
AG Audience
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 1 April 2005
16:00
-- Not specified --
45
HS 001
Saarbrücken
Abstract
Die Arbeit untersucht zwei logische Probleme der
programmiersprachlichen Typinferenz: Erfüllbarkeit und Subsumption von
Teiltyp-Constraints. Diese Probleme werden systematisch für eine Reihe
von Constraintsprachen untersucht. Dabei wird auf Methoden der
computationalen Logik, Unifikations- und Automatentheorie zurückgegriffen.
Teiltyp-Erfüllbarkeit ist für den Fall wohl verstanden, dass die
Typkonstanten in einem Verband angeordnet sind (Palsberg und O’Keefe
(1995), Pottier (1996), Palsberg, Wand und O’Keefe (1997). Der
allgemeinere Fall mit beliebig angeordneten Konstanten wurde bislang
weniger untersucht. Es wird ein erster universeller Ansatz vorgestellt,
indem erstmals ein Zusammenhang zwischen Teiltyp-Constraints und
Modallogik aufgezeigt wird. Dadurch wird u.a. ein seit 1993 offenes
Komplexitätsproblem von Wand und Tiuryn gelöst.
Teiltyp-Subsumption ist selbst für einfachste Constraintsprachen von
hoher Komplexität. Rehof und Henglein zeigten dies für den strukturellen
Verbandsfall (mit zwei Typkonstanten 1997, 1998), ließen jedoch den
nicht-strukturellen Fall offen. In dieser Arbeit wird der einfachste
nicht-strukturelle Fall betrachtet. Es wird aufgezeigt, dass versteckte
Wortgleichungen neue Schwierigkeiten verursachen. Hierzu wird
Teiltyp-Subsumption durch spezielle endliche Automaten mit
Wortgleichungen charakterisiert. Die Charakterisierung dieser Arbeit
liefert partiellre Entscheidbarkeitsresultate zur nicht-strukturellen
Teiltyp-Subsumption und kann als Grundlage für künftige Untersuchungen
dienen.
programmiersprachlichen Typinferenz: Erfüllbarkeit und Subsumption von
Teiltyp-Constraints. Diese Probleme werden systematisch für eine Reihe
von Constraintsprachen untersucht. Dabei wird auf Methoden der
computationalen Logik, Unifikations- und Automatentheorie zurückgegriffen.
Teiltyp-Erfüllbarkeit ist für den Fall wohl verstanden, dass die
Typkonstanten in einem Verband angeordnet sind (Palsberg und O’Keefe
(1995), Pottier (1996), Palsberg, Wand und O’Keefe (1997). Der
allgemeinere Fall mit beliebig angeordneten Konstanten wurde bislang
weniger untersucht. Es wird ein erster universeller Ansatz vorgestellt,
indem erstmals ein Zusammenhang zwischen Teiltyp-Constraints und
Modallogik aufgezeigt wird. Dadurch wird u.a. ein seit 1993 offenes
Komplexitätsproblem von Wand und Tiuryn gelöst.
Teiltyp-Subsumption ist selbst für einfachste Constraintsprachen von
hoher Komplexität. Rehof und Henglein zeigten dies für den strukturellen
Verbandsfall (mit zwei Typkonstanten 1997, 1998), ließen jedoch den
nicht-strukturellen Fall offen. In dieser Arbeit wird der einfachste
nicht-strukturelle Fall betrachtet. Es wird aufgezeigt, dass versteckte
Wortgleichungen neue Schwierigkeiten verursachen. Hierzu wird
Teiltyp-Subsumption durch spezielle endliche Automaten mit
Wortgleichungen charakterisiert. Die Charakterisierung dieser Arbeit
liefert partiellre Entscheidbarkeitsresultate zur nicht-strukturellen
Teiltyp-Subsumption und kann als Grundlage für künftige Untersuchungen
dienen.
Contact
--email hidden
passcode not visible
logged in users only
Bahareh Kadkhodazadeh, 03/31/2005 12:08
Bahareh Kadkhodazadeh, 03/29/2005 15:10
Bahareh Kadkhodazadeh, 03/29/2005 15:10 -- Created document.
Bahareh Kadkhodazadeh, 03/29/2005 15:10
Bahareh Kadkhodazadeh, 03/29/2005 15:10 -- Created document.