Informatik
Refine
Year of publication
Document Type
- Preprint (748)
- Article (401)
- Working Paper (119)
- Doctoral Thesis (93)
- Diploma Thesis (46)
- Conference Proceeding (41)
- Book (37)
- Bachelor Thesis (36)
- diplomthesis (29)
- Report (25)
Has Fulltext
- yes (1607)
Is part of the Bibliography
- no (1607)
Keywords
Institute
- Informatik (1607)
- Frankfurt Institute for Advanced Studies (FIAS) (1002)
- Physik (982)
- Mathematik (55)
- Präsidium (41)
- Medizin (25)
- Biowissenschaften (21)
- Exzellenzcluster Makromolekulare Komplexe (8)
- Psychologie (8)
- Deutsches Institut für Internationale Pädagogische Forschung (DIPF) (5)
- Geowissenschaften (5)
- Senckenbergische Naturforschende Gesellschaft (5)
- Geographie (4)
- Hochschulrechenzentrum (4)
- Pharmazie (4)
- Biochemie und Chemie (3)
- Goethe-Zentrum für Wissenschaftliches Rechnen (G-CSC) (3)
- Universitätsbibliothek (3)
- Biodiversität und Klima Forschungszentrum (BiK-F) (2)
- Center for Membrane Proteomics (CMP) (2)
- Institut für Ökologie, Evolution und Diversität (2)
- Sportwissenschaften (2)
- Wirtschaftswissenschaften (2)
- Center for Scientific Computing (CSC) (1)
- E-Finance Lab e.V. (1)
- Erziehungswissenschaften (1)
- Geschichtswissenschaften (1)
- Gesellschaftswissenschaften (1)
- Informatik und Mathematik (1)
- Institut für Bienenkunde (1)
- Kulturwissenschaften (1)
- Neuere Philologien (1)
- Zentrum für Arzneimittelforschung, Entwicklung und Sicherheit (ZAFES) (1)
- Zentrum für Weiterbildung (1)
This paper shows equivalence of applicative similarity and contextual approximation, and hence also of bisimilarity and contextual equivalence, in LR, the deterministic call-by-need lambda calculus with letrec extended by data constructors, case-expressions and Haskell's seqoperator. LR models an untyped version of the core language of Haskell. Bisimilarity simplifies equivalence proofs in the calculus and opens a way for more convenient correctness proofs for program transformations.
The proof is by a fully abstract and surjective transfer of the contextual approximation into a call-by-name calculus, which is an extension of Abramsky's lazy lambda calculus. In the latter calculus equivalence of similarity and contextual approximation can be shown by Howe's method. Using an equivalent but inductive definition of behavioral preorder we then transfer similarity back to the calculus LR.
The translation from the call-by-need letrec calculus into the extended call-by-name lambda calculus is the composition of two translations. The first translation replaces the call-by-need strategy by a call-by-name strategy and its correctness is shown by exploiting infinite tress, which emerge by unfolding the letrec expressions. The second translation encodes letrec-expressions by using multi-fixpoint combinators and its correctness is shown syntactically by comparing reductions of both calculi. A further result of this paper is an isomorphism between the mentioned calculi, and also with a call-by-need letrec calculus with a less complex definition of reduction than LR.
Motivated by the question whether sound and expressive applicative similarities for program calculi with should-convergence exist, this paper investigates expressive applicative similarities for the untyped call-by-value lambda-calculus extended with McCarthy's ambiguous choice operator amb. Soundness of the applicative similarities w.r.t. contextual equivalence based on may-and should-convergence is proved by adapting Howe's method to should-convergence. As usual for nondeterministic calculi, similarity is not complete w.r.t. contextual equivalence which requires a rather complex counter example as a witness. Also the call-by-value lambda-calculus with the weaker nondeterministic construct erratic choice is analyzed and sound applicative similarities are provided. This justifies the expectation that also for more expressive and call-by-need higher-order calculi there are sound and powerful similarities for should-convergence.
The pi-calculus is a well-analyzed model for mobile processes and mobile computations.
While a lot of other process and lambda calculi that are core languages of higher-order concurrent and/or functional programming languages use a contextual semantics observing the termination behavior of programs in all program contexts, traditional program equivalences in the pi-calculus are bisimulations and barbed testing equivalences, which observe the communication capabilities of processes under reduction and in contexts.
There is a distance between these two approaches to program equivalence which makes it hard to compare the pi-calculus with other languages. In this paper we contribute to bridging this gap by investigating a contextual semantics of the synchronous pi-calculus with replication and without sums.
To transfer contextual equivalence to the pi-calculus we add a process Stop as constant which indicates success and is used as the base to define and analyze the contextual equivalence which observes may- and should-convergence of processes.
We show as a main result that contextual equivalence in the pi-calculus with Stop conservatively extends barbed testing equivalence in the (Stop-free) pi-calculus. This implies that results on contextual equivalence can be directly transferred to the (Stop-free) pi-calculus with barbed testing equivalence.
We analyze the contextual ordering, prove some nontrivial process equivalences, and provide proof tools for showing contextual equivalences. Among them are a context lemma, and new notions of sound applicative similarities for may- and should-convergence.
Motivated by our experience in analyzing properties of translations between programming languages with observational semantics, this paper clarifies the notions, the relevant questions, and the methods, constructs a general framework, and provides several tools for proving various correctness properties of translations like adequacy and full abstractness. The presented framework can directly be applied to the observational equivalences derived from the operational semantics of programming calculi, and also to other situations, and thus has a wide range of applications.
Our motivation is the question whether the lazy lambda calculus, a pure lambda calculus with the leftmost outermost rewriting strategy, considered under observational semantics, or extensions thereof, are an adequate model for semantic equivalences in real-world purely functional programming languages, in particular for a pure core language of Haskell. We explore several extensions of the lazy lambda calculus: addition of a seq-operator, addition of data constructors and case-expressions, and their combination, focusing on conservativity of these extensions. In addition to untyped calculi, we study their monomorphically and polymorphically typed versions. For most of the extensions we obtain non-conservativity which we prove by providing counterexamples. However, we prove conservativity of the extension by data constructors and case in the monomorphically typed scenario.
Our motivation is the question whether the lazy lambda calculus, a pure lambda calculus with the leftmost outermost rewriting strategy, considered under observational semantics, or extensions thereof, are an adequate model for semantic equivalences in real-world purely functional programming languages, in particular for a pure core language of Haskell. We explore several extensions of the lazy lambda calculus: addition of a seq-operator, addition of data constructors and case-expressions, and their combination, focusing on conservativity of these extensions. In addition to untyped calculi, we study their monomorphically and polymorphically typed versions. For most of the extensions we obtain non-conservativity which we prove by providing counterexamples. However, we prove conservativity of the extension by data constructors and case in the monomorphically typed scenario.
Diese Diplomarbeit beschäftigt sich mit dem Entwurf und der Implementierung der Auslesefirmware für den GET4 Chip im Rahmen des CBM (Compressed Baryonic Matter) Experiments.
Physikalische Experimente mit Teilchenbeschleunigern, wie das geplante CBM Experiment, erzeugen große Mengen an Sensordaten, die aufbereitet, gespeichert und ausgewertet werden müssen. Der GET4 Chip ist ein möglicher TDC (Time to Digital Converter) Chip mit 4 Kanälen für den TOF (Time of Flight) Detektor des CBM Experiments. Der GET4 Chip erzeugt einen Zeitstempel für die Treffer der TOF RPC (Resistive Plate Chambers) Sensoren.
Die Auslese der GET4 Daten wird von einem ROC (Readout Controller Board) übernommen, das mit einem FPGA (Field Programmable Gate Array) ausgestattet ist. Das ROC Board lässt sich über die ROC Firmware für verschiedene Einsatzzwecke flexibel konfigurieren, so dass damit auch andere Frontend Elektronik, wie z.B. der n-XYTER Chip, ausgelesen werden kann. Während dieser Diplomarbeit wurde das SysCore2 mit einem Virtex-4 FX20 als ROC verwendet. Inzwischen ist das SysCore3 verfügbar, das einen deutlich leistungsfähigeren FPGA besitzt. Die bisher verfügbare Firmware für den GET4 war für den Betrieb im 24 Bit Modus konzipiert.
Der bevorzugte Auslesemodus für den GET4 ist der 32 Bit Modus, da der 24 Bit Modus einige Beschränkungen aufweist und die volle Funktionalität des GET4s nur im 32 Bit Modus zur Verfügung steht. Im Rahmen dieser Diplomarbeit wurde die vorhandene 24 Bit Firmware für den 32 Bit Modus erweitert, so dass der zweite Datenkanal des GET4s, sowie der DDR (Double Data Rate) Modus für die Datenübertragung zur Verfügung steht. Neben der Erhöhung der Datenübertragungsraten stand die mögliche Skalierbarkeit der Firmware für die Auslese möglichst vieler GET4 Chips im Fokus. Dazu musste die Firmware umgestaltet werden, um die begrenzten BRAM Ressourcen des FPGAs nicht unnötig zu belegen.
Eine weitere wichtige Neuerung der 32 Bit Firmware ist die automatische Synchronisation der Epochen zwischen ROC und GET4. Dazu werden die Epochennachrichten der GET4s mit der Epoche des ROCs verglichen und bei Bedarf Synchronisationsnachrichten mit der korrekten Epoche an die GET4s gesendet.
Visualisierung von E-Mail-Traffic mit Schwerpunkt auf eine inhaltliche Analyse von Wortmustern
(2010)
E-Mail hat sich zu einem sehr wichtigen Kommunikationsmittel entwickelt, leidet aber aktuell unter einer massiven Verbreitung unerwünschter und unverlangter Inhalte. Diese können für einen Anwender nicht nur lästig sein, sondern auch die vorhandene Netz- und Speicher-Infrastruktur enorm belasten.
Die Notwendigkeit einer Filterung des E-Mail-Traffic hat zu einer Reihe recht unterschiedlicher Methoden geführt, die computergesteuert eine E-Mail auf ihren Spam-Gehalt untersuchen.
Die Motivation hinter dieser Arbeit ist zu prüfen, ob die besonderen Eigenschaften der visuellen Wahrnehmung eines Menschen als unterstützendes Mittel eingesetzt werden können, um E-Mail-Inhalte zu überprüfen und eventuell vorhandene Wort-Muster, die auf Spam deuten, sichtbar zu machen.
Um dieses Ziel zu erreichen musste zuerst eine geeignete Auswahl spamspezifischer Merkmale getroffen werden. Danach wurden Methoden des Text Minings angewendet, um aus dem Inhalt einer E-Mail strukturierte Daten zu gewinnen, die sich zur Repräsentation einer Nachricht eignen und als Grundlage für eine Visualisierung herangezogen werden können. Basierend auf den vorab ausgewählten Spam-Charakteristika wurdenWorteigenschaften mit Hilfe extern angebundener Wortlisten, regulärer Ausdrücke und unter Einsatz eines Wörterbuches überprüft, und die erhaltenen Ergebnisse flossen neben einer einfachen Gewichtung von Worthäufigkeiten in Form einer anwendungsspezifischen Gewichtung mit ein.
Es wurden anschließend zwei verschiedene Sichten konzipiert, um einem Anwender einen Einblick in die extrahierten Daten zu ermöglichen. Es hat sich herausgestellt, dass besonders Treemaps geeignet sind um die anfallenden Datenmengen kompakt abzubilden, aber gleichzeitig einen notwendigen Detailgrad auf einzelne Worteigenschaften gewährleisten.
Das Konzept wurde prototypisch unter Verwendung des Mailservers Mercury/32 sowie einer MySQL-Datenbank implementiert und konnte teilweise aufzeigen, dass es anhand der von der Engine generierten Strukturen möglich ist, spamspezifische Merkmale einer E-Mail unter Verwendung der gewählten Visualisierungstechniken auf eine Weise sichtbar zu machen, die einem Anwender eine Mustererkennung erlauben.
Die Diplomarbeit wurde als Gemeinschaftsarbeit angefertigt und konnte sinnvoll in zwei Bereiche aufgeteilt werden: Die Engine und die Visualisierung. Die konzeptuellen Überlegungen für das Thema sind größtenteils gemeinsam erfolgt, jedoch liegt der Schwerpunkt von Pouneh Khayat Pour im Bereich der Analyse und der von Yvonne Neidert in der Visualisierung.
The human brain is an unparalleled system: Through millions of years of evolution and during a lifespan of learning, our brains have developed remarkable abilities for dealing with incoming sensory data, extracting structure and useful information, and finally drawing the conclusions that result in the actions we take. Understanding the principles behind this machinery and building artificial systems that mimic at least some of these capabilities is a long standing goal in both the scientific and the engineering communities. While this goal still seems unreachable, we have seen tremendous progress when it comes to training data-driven algorithms on vast amounts of training data, e.g. to learn an optimal data model and its parameters in order to accomplish some task. Such algorithms are now omnipresent: they are part of recommender systems, they perform speech recognition and generally build the foundation for many semi-autonomous systems. They start to be integral part of many technical systems modern technical societies rely on for their everyday functioning. Many of these algorithms were originally inspired by biological systems or act as models for sensory data processing in mammalian brains. The response properties of a certain population of neurons in the first stages of the mammalian visual pathway, for example, can be modeled by algorithms such as Sparse Coding (SC), Independent Component Analysis (ICA) or Factor Analysis (FA). These well established learning algorithms typically assume linear interactions between the variables of the model. Most often these relationships are expressed in the form of a matrix-vector products between a matrix with learned dictionary-elements (basis vectors as column vectors) and the latent variables of these models. While on the one hand this linear interaction can sometimes be justified by the physical process for which the machine learning model is proposed, it is on the other hand often chosen just because of its mathematical and practical convenience. From an optimal coding point of view though, one would generally expect that the ideal model closely reflect the core interactions of the system it is modeling. In vision for example, one of the dominant processes giving rise to our sensory percepts are occlusions. Occluding objects are omnipresent in visual scenes and it would not be surprising if the mammalian visual system would be optimized to process occluding structures in the visual data stream. Yet, the established mathematical models of the first stages of the visual processing path (like, e.g., SC, ICA or FA) all assume linear interactions between the active image components. In this thesis we will discuss new models that aim to approximate the effects of occluding components by assuming nonlinear interactions between their activated dictionary elements. We will present learning algorithms that infer optimal parameters for these models given data. In the experiments, we will validate the algorithms on artificial ground truth data and demonstrate their ability to recover the correct model parameters. We will show that the predictions made by these nonlinear models correspond better to the experimental data measured in-vivo than the predictions made by the established linear models. Furthermore, we systematically explore and compare a large space of plausible combinations of hyperparameters and preprocessing schemes in order to eliminate any effects of artefacts on the observed results. Training nonlinear sparse coding models is computationally more demanding than training linear models. In order to perform the numerical experiments described in this thesis we developed a software framework that facilitates the implementation of massive parallel expectation maximization (EM) based learning algorithms. This infrastructure was used for all experiments described in here, as well as by collaborators in projects we will not discuss. Some of the experiments required more than 1017 floating point operations and were run on a computer cluster running on up to 5000 CPU Cores in parallel. Our parallel framework enabled these experiments to be performed.