Refine
Year of publication
Document Type
- Preprint (759)
- Article (402)
- Working Paper (119)
- Doctoral Thesis (93)
- Diploma Thesis (47)
- Conference Proceeding (41)
- Book (37)
- Bachelor Thesis (36)
- diplomthesis (28)
- Report (25)
Has Fulltext
- yes (1619)
Is part of the Bibliography
- no (1619)
Keywords
Institute
- Informatik (1619) (remove)
The goal of this report is to prove correctness of a considerable subset of transformations w.r.t. contextual equivalence in an extended lambda-calculus LS with case, constructors, seq, let, and choice, with a simple set of reduction rules; and to argue that an approximation calculus LA is equivalent to LS w.r.t. the contextual preorder, which enables the proof tool of simulation. Unfortunately, a direct proof appears to be impossible.
The correctness proof is by defining another calculus L comprising the complex variants of copy, case-reduction and seq-reductions that use variable-binding chains. This complex calculus has well-behaved diagrams and allows a proof of correctness of transformations, and that the simple calculus LS, the calculus L, and the calculus LA all have an equivalent contextual preorder.
The calculus CHF models Concurrent Haskell extended by concurrent, implicit futures. It is a process calculus with concurrent threads, monadic concurrent evaluation, and includes a pure functional lambda-calculus which comprises data constructors, case-expressions, letrec-expressions, and Haskell’s seq. Futures can be implemented in Concurrent Haskell using the primitive unsafeInterleaveIO, which is available in most implementations of Haskell. Our main result is conservativity of CHF, that is, all equivalences of pure functional expressions are also valid in CHF. This implies that compiler optimizations and transformations from pure Haskell remain valid in Concurrent Haskell even if it is extended by futures. We also show that this is no longer valid if Concurrent Haskell is extended by the arbitrary use of unsafeInterleaveIO.
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.
Frankfurt, an einem gewöhnlichen Morgen gegen 8:00 Uhr: Von Osten strömen zahlreiche Pendler über die A 66 in Richtung Innenstadt. Spätestens »Am Erlenbruch« kommt es zu Staus und zäh fließendem Verkehr. Frankfurter Informatiker können diese Staus mithilfe eines Simulationssystems vorhersagen. Mehr noch: Sie berechnen den Ausstoß von Schadstoffen und deren Verteilung über das Stadtgebiet. Ziel ist die Optimierung von Verkehrsleitstrategien.
Aging of biological systems is controlled by various processes which have a potential impact on gene expression. Here we report a genome-wide transcriptome analysis of the fungal aging model Podospora anserina. Total RNA of three individuals of defined age were pooled and analyzed by SuperSAGE (serial analysis of gene expression). A bioinformatics analysis identified different molecular pathways to be affected during aging. While the abundance of transcripts linked to ribosomes and to the proteasome quality control system were found to decrease during aging, those associated with autophagy increase, suggesting that autophagy may act as a compensatory quality control pathway. Transcript profiles associated with the energy metabolism including mitochondrial functions were identified to fluctuate during aging. Comparison of wild-type transcripts, which are continuously down-regulated during aging, with those down-regulated in the long-lived, copper-uptake mutant grisea, validated the relevance of age-related changes in cellular copper metabolism. Overall, we (i) present a unique age-related data set of a longitudinal study of the experimental aging model P. anserina which represents a reference resource for future investigations in a variety of organisms, (ii) suggest autophagy to be a key quality control pathway that becomes active once other pathways fail, and (iii) present testable predictions for subsequent experimental investigations.
Time-critical applications process a continuous stream of input data and have to meet specific timing constraints. A common approach to ensure that such an application satisfies its constraints is over-provisioning: The application is deployed in a dedicated cluster environment with enough processing power to achieve the target performance for every specified data input rate. This approach comes with a drawback: At times of decreased data input rates, the cluster resources are not fully utilized. A typical use case is the HLT-Chain application that processes physics data at runtime of the ALICE experiment at CERN. From a perspective of cost and efficiency it is desirable to exploit temporarily unused cluster resources. Existing approaches aim for that goal by running additional applications. These approaches, however, a) lack in flexibility to dynamically grant the time-critical application the resources it needs, b) are insufficient for isolating the time-critical application from harmful side-effects introduced by additional applications or c) are not general because application-specific interfaces are used. In this thesis, a software framework is presented that allows to exploit unused resources in a dedicated cluster without harming a time-critical application. Additional applications are hosted in Virtual Machines (VMs) and unused cluster resources are allocated to these VMs at runtime. In order to avoid resource bottlenecks, the resource usage of VMs is dynamically modified according to the needs of the time-critical application. For this purpose, a number of previously not combined methods is used. On a global level, appropriate VM manipulations like hot migration, suspend/resume and start/stop are determined by an informed search heuristic and applied at runtime. Locally on cluster nodes, a feedback-controlled adaption of VM resource usage is carried out in a decentralized manner. The employment of this framework allows to increase a cluster’s usage by running additional applications, while at the same time preventing negative impact towards a time-critical application. This capability of the framework is shown for the HLT-Chain application: In an empirical evaluation the cluster CPU usage is increased from 49% to 79%, additional results are computed and no negative effect towards the HLT-Chain application are observed.
G-CSC Report 2010
(2011)
The present report gives a short summary of the research of the Goethe Center for Scientific Computing (G-CSC) of the Goethe University Frankfurt. G-CSC aims at developing and applying methods and tools for modelling and numerical simulation of problems from empirical science and technology. In particular, fast solvers for partial differential equations (i.e. pde) such as robust, parallel, and adaptive multigrid methods and numerical methods for stochastic differential equations are developed. These methods are highly adanvced and allow to solve complex problems..
The G-CSC is organised in departments and interdisciplinary research groups. Departments are localised directly at the G-CSC, while the task of interdisciplinary research groups is to bridge disciplines and to bring scientists form different departments together. Currently, G-CSC consists of the department Simulation and Modelling and the interdisciplinary research group Computational Finance.
The economic success of the World Wide Web makes it a highly competitive environment for web businesses. For this reason, it is crucial for web business owners to learn what their customers want. This thesis provides a conceptual framework and an implementation of a system that helps to better understand the behavior and potential interests of web site visitors by accounting for both explicit and implicit feedback. This thesis is divided into two parts.
The first part is rooted in computer science and information systems and uses graph theory and an extended click-stream analysis to define a framework and a system tool that is useful for analyzing web user behavior by calculating the interests of the users.
The second part is rooted in behavioral economics, mathematics, and psychology and is investigating influencing factors on different types of web user choices. In detail, a model for the cognitive process of rating products on the Web is defined and an importance hierarchy of the influencing factors is discovered.
Both parts make use of techniques from a variety of research fields and, therefore, contribute to the area of Web Science.