Refine
Year of publication
- 2010 (84) (remove)
Document Type
- Working Paper (84) (remove)
Has Fulltext
- yes (84)
Is part of the Bibliography
- no (84) (remove)
Keywords
- Film (4)
- Formale Semantik (4)
- Argumentationstheorie (3)
- Finanzkrise (3)
- Internetsprache (3)
- Logik (3)
- Normative Ordnungen (3)
- Verifikation (3)
- Asset Allocation (2)
- Außenpolitik (2)
Institute
- Center for Financial Studies (CFS) (29)
- Exzellenzcluster Die Herausbildung normativer Ordnungen (12)
- Institute for Law and Finance (ILF) (11)
- Informatik (6)
- Institute for Monetary and Financial Stability (IMFS) (6)
- Extern (4)
- Wirtschaftswissenschaften (4)
- Gesellschaftswissenschaften (3)
- Institut für sozial-ökologische Forschung (ISOE) (2)
- Medizin (2)
Towards correctness of program transformations through unification and critical pair computation
(2010)
Correctness of program transformations in extended lambda-calculi with a contextual semantics is usually based on reasoning about the operational semantics which is a rewrite semantics. A successful approach is the combination of a context lemma with the computation of overlaps between program transformations and the reduction rules, which results in so-called complete sets of diagrams. The method is similar to the computation of critical pairs for the completion of term rewriting systems. We explore cases where the computation of these overlaps can be done in a first order way by variants of critical pair computation that use unification algorithms. As a case study of an application we describe a finitary and decidable unification algorithm for the combination of the equational theory of left-commutativity modelling multi-sets, context variables and many-sorted unification. Sets of equations are restricted to be almost linear, i.e. every variable and context variable occurs at most once, where we allow one exception: variables of a sort without ground terms may occur several times. Every context variable must have an argument-sort in the free part of the signature. We also extend the unification algorithm by the treatment of binding-chains in let- and letrec-environments and by context-classes. This results in a unification algorithm that can be applied to all overlaps of normal-order reductions and transformations in an extended lambda calculus with letrec that we use as a case study.
The interactive verification system VeriFun is based on a polymorphic call-by-value functional language and on a first-order logic with initial model semantics w.r.t. constructors. It is designed to perform automatic induction proofs and can also deal with partial functions. This paper provides a reconstruction of the corresponding logic and semantics using the standard treatment of undefinedness which adapts and improves the VeriFun-logic by allowing reasoning on nonterminating expressions and functions. Equality of expressions is defined as contextual equivalence based on observing termination in all closing contexts. The reconstruction shows that several restrictions of the VeriFun framework can easily be removed, by natural generalizations: mutual recursive functions, abstractions in the data values, and formulas with arbitrary quantifier prefix can be formulated. The main results of this paper are: an extended set of deduction rules usable in VeriFun under the adapted semantics is proved to be correct, i.e. they respect the observational equivalence in all extensions of a program. We also show that certain classes of theorems are conservative under extensions, like universally quantified equations. Also other special classes of theorems are analyzed for conservativity.
The interactive verification system VeriFun is based on a polymorphic call-by-value functional language and on a first-order logic with initial model semantics w.r.t. constructors. This paper provides a reconstruction of the corresponding logic when partial functions are permitted. Typing is polymorphic for the definition of functions but monomorphic for terms in formulas. Equality of terms is defined as contextual equivalence based on observing termination in all contexts. The reconstruction also allows several generalizations of the functional language like mutual recursive functions and abstractions in the data values. The main results are: Correctness of several program transformations for all extensions of a program, which have a potential usage in a deduction system. We also proved that universally quantified equations are conservative, i.e. if a universally quantified equation is valid w.r.t. a program P, then it remains valid if the program is extended by new functions and/or new data types.
The well-known proof of termination of reduction in simply typed calculi is adapted to a monomorphically typed lambda-calculus with case and constructors and recursive data types. The proof differs at several places from the standard proof. Perhaps it is useful and can be extended also to more complex calculi.
Dieses Arbeitspapier geht aus einem Hauptseminar zur Argumentationstheorie hervor, das [von Leila Behrens] im Wintersemester 2008/09 am Institut für Linguistik der Universität zu Köln gehalten [wurde]. In den beiden Arbeiten in diesem Band (Badtke et al. und Benning et al.) stellen die Studierenden dieses Hauptseminars die Ergebnisse vor, die sie (in zwei parallelen Projektgruppen mit unterschiedlichen Diskussionsgegenständen) bei der empirischen Analyse von Argumentationen in einem Internet-Forum gewonnen haben. Der Gegenstand der Diskussion betraf bei der einen Gruppe (Badtke et al.) die Unabhängigkeit des Kosovo, bei der anderen Gruppe (Benning et al.) die Einführung eines generellen Rauchverbots in europäischen Hauptstädten.
Das Diskussionspapier versucht Dimensionen und Ausmaße von Ökonomisierungs- und Kommerzialisierungsprozessen in OECD-Gesundheitssystemen explorativ zu erörtern. Hierzu wird zunächst die Hypothese entwickelt, dass sich in den (meisten) OECD-Staaten eine hegemoniale gesundheitspolitische Strategie herausbildet, die als wettbewerbsbasierte Kostendämpfungspolitik bezeichnet wird. In der Folge werden die (mutmaßlichen) Auswirkungen von Ökonomisierungs- und Kommerzialisierungsprozessen diskutiert. Erstens wird beschrieben, wie die Monetarisierung der Arzt-Patienten-Beziehung zu einer Privatisierung des Gesundheitssystems führt. Zweitens wird die sich transformierende Arzt-Patienten-Beziehung als Dialektik von Demokratisierungs- und Ökonomisierungsprozessen dargestellt. Drittens beschäftigt sich der Beitrag mit Entwicklung einer neuen Gesundheitskultur, die die gesundheitliche Eigenverantwortung des Einzelnen betont, zugleich jedoch neuen Ausgrenzungs- und Stigmatisierungsprozessen den Weg zu ebnen droht. Abschließend wird ein in groben Zügen ein Forschungsprogramm umschrieben, welches Ökonomisierungs- und Kommerzialisierungsprozesse auf diesen drei Forschungsfeldern analytisch und bewertend unter die Lupe zu nehmen versucht.
Mit umfassenden rechtlichen Regelungen zur Zulassung und Anwendung von chemischen Pflanzenschutzmitteln wurde in Deutschland schon früh versucht, diesen Risiken zu begegnen. Nicht zuletzt in den aktuellen Debatten um Pestizidrückstände in Obst und Gemüse wurde aber auch immer wieder deutlich, dass sich der Zielkonflikt zwischen Anwendungsinteressen und Schutzanforderungen rechtlich nicht vollständig lösen lässt. Im Zentrum des vom Bundesministerium für Bildung und Forschung geförderten, transdisziplinären Projekts start2 stand daher die Frage: Wie können ergänzend zu rechtlichen Maßnahmen bei der Zulassung Risiken als Folge der bestimmungsgemäßen Anwendung von Pflanzenschutzmitteln weiter und nachhaltig vermindert werden?
Die vorliegende Handreichung gibt konkrete Antworten auf diese Frage. Im Zentrum steht dabei der Ansatz, Risikominderung mehr als bisher in gemeinsamer Verantwortung aller beteiligten gesellschaftlichen Akteure zu betreiben. Damit dies gelingt, muss den einzelnen Akteuren nicht nur aufgezeigt werden, welche Möglichkeiten sie haben, durch ihr Handeln einen wirksamen Beitrag zu dieser Aufgabe zu leisten. Die Handlungsmöglichkeiten der verschiedenen Akteure sollten sich überdies zu einer wirksamen Gesamtstrategie verbinden lassen. start2 hat zu diesem Zweck drei Handlungsfelder untersucht, deren Zuschnitt sich am Lebenszyklus eines Pflanzenschutzmittels ausrichtet: „Entwicklung von Pflanzenschutzmittelwirkstoffen“, "Landwirtschaftliche Pflanzenschutzpraxis“ und „Gewässer und Trinkwasserschutz“.
Die Handreichung richtet sich an Entscheidungsträgerinnen und Entscheidungsträger in Betrieben, Organisationen, Verwaltung und Politik (siehe auch den Lesehinweis auf der folgenden Seite). Sie gibt Informationen und konkrete Empfehlungen, wo neue Handlungsmöglichkeiten ansetzen und wo in der Praxis bereits umgesetzte Maßnahmen weiterentwickelt werden können. In einzelnen Fällen sind die vorgeschlagenen Handlungsmöglichkeiten zur Risikominderung auf den besseren Umgang mit besonders gefährlichen Stoffen zugeschnitten. Im Fokus des Projekts standen dabei Pflanzenschutzmittel, die möglicherweise Gesundheitsschäden auslösen können, indem sie auf das Hormonsystem wirken...
Auf der großen Konferenz der SGIR (Standing Group on International Relations) vom 9.-11. September 2010 in Stockholm, Schweden, organisierten wir eine eigene Sektion zum Thema Sicherheitskultur im Wandel. In sieben panels wurden viele Aspekte dieses Oberthemas diskutiert und erläutert, wie im ausführlichen Konferenzbericht nachzulesen ist
All of the papers in the volume except one (Kaji) take up some aspect of relative clause construction in some Bantu language. Kaji’s paper aims to account for how Tooro (J12; western Uganda) lost phonological tone through a comparative study of the tone systems of other western Uganda Bantu languages. The other papers examine a range of ways of forming relative clauses, often including non-restrictive relatives and clefts, in a wide range of languages representing a variety of prosodic systems.
In den Jahren 2006-2007 wurde die epiphytische Flechtenflora im Nordbezirk Moskaus erneut untersucht, um sie mit den Ergebnissen aus den Untersuchungen der Jahre 1988-1991 zu vergleichen. Statt 18 konnten nun 55 Flechtenarten nachgewiesen werden. Als Hauptursache für diese Zunahme wird die erhöhte Eutrophierung der Standorte angenommen.