Informatik
Refine
Year of publication
- 2009 (38) (remove)
Document Type
- Working Paper (9)
- Article (6)
- Diploma Thesis (6)
- Doctoral Thesis (6)
- Bachelor Thesis (5)
- Book (4)
- Conference Proceeding (2)
Has Fulltext
- yes (38) (remove)
Is part of the Bibliography
- no (38) (remove)
Keywords
- Lambda-Kalkül (6)
- Nebenläufigkeit (3)
- Funktionale Programmiersprache (2)
- Operationale Semantik (2)
- Programmiersprache (2)
- Pufferspeicher (2)
- Affymetrix (1)
- Algorithmus (1)
- Bioinformatics (1)
- Bioinformatik (1)
Institute
- Informatik (38)
- Medizin (3)
- Präsidium (3)
- Psychologie (3)
- Biochemie und Chemie (2)
- Biowissenschaften (2)
- Geographie (2)
- Geowissenschaften (2)
- Mathematik (2)
- Pharmazie (2)
- Physik (2)
- Sportwissenschaften (2)
- Frankfurt Institute for Advanced Studies (FIAS) (1)
- Zentrum für Weiterbildung (1)
Motivated by the question of correctness of a specific implementation of concurrent buffers in the lambda calculus with futures underlying Alice ML, we prove that concurrent buffers and handled futures can correctly encode each other. Correctness means that our encodings preserve and reflect the observations of may- and must-convergence, and as a consequence also yields soundness of the encodings with respect to a contextually defined notion of program equivalence. While these translations encode blocking into queuing and waiting, we also describe an adequate encoding of buffers in a calculus without handles, which is more low-level and uses busy-waiting instead of blocking. Furthermore we demonstrate that our correctness concept applies to the whole compilation process from high-level to low-level concurrent languages, by translating the calculus with buffers, handled futures and data constructors into a small core language without those constructs.
We investigate methods and tools for analyzing translations between programming languages with respect to observational semantics. The behavior of programs is observed in terms of may- and mustconvergence in arbitrary contexts, and adequacy of translations, i.e., the reflection of program equivalence, is taken to be the fundamental correctness condition. For compositional translations we propose a notion of convergence equivalence as a means for proving adequacy. This technique avoids explicit reasoning about contexts, and is able to deal with the subtle role of typing in implementations of language extensions.
The paper proposes a variation of simulation for checking and proving contextual equivalence in a non-deterministic call-by-need lambda-calculus with constructors, case, seq, and a letrec with cyclic dependencies. It also proposes a novel method to prove its correctness. The calculus’ semantics is based on a small-step rewrite semantics and on may-convergence. The cyclic nature of letrec bindings, as well as nondeterminism, makes known approaches to prove that simulation implies contextual equivalence, such as Howe’s proof technique, inapplicable in this setting. The basic technique for the simulation as well as the correctness proof is called pre-evaluation, which computes a set of answers for every closed expression. If simulation succeeds in finite computation depth, then it is guaranteed to show contextual preorder of expressions.
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.
An der Universität Frankfurt entwickelte Online-Self-Assessment-Verfahren für die Studiengänge Psychologie und Informatik sollen Studieninteressierten noch vor Studienbeginn auf der Basis von Selbsterkundungsmaßnahmen und Tests eine Rückmeldung über ihre eigenen Fähigkeiten, Motive, personalen Kompetenzen und Interessen mit Blick auf den jeweiligen Studiengang geben. Sowohl die Befunde zur psychometrischen Güte der Verfahren als auch jene zur prognostischen Validität lassen ihren Einsatz zur Feststellung studienrelevanter Kompetenzen als geeignet erscheinen. Da die erfassten Kompetenzen und Merkmale substanzielle Beziehun-gen zu Studienleistungen aufweisen, könnten die Informationen über individuelle Stärken zur Wahl eines geeigneten Studienganges genutzt werden; Schwächen hingegen könnten frühzeitig Hinweise für geeignete Fördermaßnahmen liefern.
The Symposium on Theoretical Aspects of Computer Science (STACS) is held alternately in France and in Germany. The conference of February 26-28, 2009, held in Freiburg, is the 26th in this series. Previous meetings took place in Paris (1984), Saarbr¨ucken (1985), Orsay (1986), Passau (1987), Bordeaux (1988), Paderborn (1989), Rouen (1990), Hamburg (1991), Cachan (1992), W¨urzburg (1993), Caen (1994), M¨unchen (1995), Grenoble (1996), L¨ubeck (1997), Paris (1998), Trier (1999), Lille (2000), Dresden (2001), Antibes (2002), Berlin (2003), Montpellier (2004), Stuttgart (2005), Marseille (2006), Aachen (2007), and Bordeaux (2008). ...
Understanding the dynamics of recurrent neural networks is crucial for explaining how the brain processes information. In the neocortex, a range of different plasticity mechanisms are shaping recurrent networks into effective information processing circuits that learn appropriate representations for time-varying sensory stimuli. However, it has been difficult to mimic these abilities in artificial neural models. In the present thesis, we introduce several recurrent network models of threshold units that combine spike timing dependent plasticity with homeostatic plasticity mechanisms like intrinsic plasticity or synaptic normalization. We investigate how these different forms of plasticity shape the dynamics and computational properties of recurrent networks. The networks receive input sequences composed of different symbols and learn the structure embedded in these sequences in an unsupervised manner. Information is encoded in the form of trajectories through a high-dimensional state space reminiscent of recent biological findings on cortical coding. We find that these self-organizing plastic networks are able to represent and "understand" the spatio-temporal patterns in their inputs while maintaining their dynamics in a healthy regime suitable for learning. The emergent properties are not easily predictable on the basis of the individual plasticity mechanisms at work. Our results underscore the importance of studying the interaction of different forms of plasticity on network behavior.
A framework for the analysis and visualization of multielectrode spike trains / von Ovidiu F. Jurjut
(2009)
The brain is a highly distributed system of constantly interacting neurons. Understanding how it gives rise to our subjective experiences and perceptions depends largely on understanding the neuronal mechanisms of information processing. These mechanisms are still poorly understood and a matter of ongoing debate remains the timescale on which the coding process evolves. Recently, multielectrode recordings of neuronal activity have begun to contribute substantially to elucidating how information coding is implemented in brain circuits. Unfortunately, analysis and interpretation of multielectrode data is often difficult because of their complexity and large volume. Here we propose a framework that enables the efficient analysis and visualization of multielectrode spiking data. First, using self-organizing maps, we identified reoccurring multi-neuronal spike patterns that evolve on various timescales. Second, we developed a color-based visualization technique for these patterns. They were mapped onto a three-dimensional color space based on their reciprocal similarities, i.e., similar patterns were assigned similar colors. This innovative representation enables a quick and comprehensive inspection of spiking data and provides a qualitative description of pattern distribution across entire datasets. Third, we quantified the observed pattern expression motifs and we investigated their contribution to the encoding of stimulus-related information. An emphasis was on the timescale on which patterns evolve, covering the temporal scales from synchrony up to mean firing rate. Using our multi-neuronal analysis framework, we investigated data recorded from the primary visual cortex of anesthetized cats. We found that cortical responses to dynamic stimuli are best described as successions of multi-neuronal activation patterns, i.e., trajectories in a multidimensional pattern space. Patterns that encode stimulus-specific information are not confined to a single timescale but can span a broad range of timescales, which are tightly related to the temporal dynamics of the stimuli. Therefore, the strict separation between synchrony and mean firing rate is somewhat artificial as these two represent only extreme cases of a continuum of timescales that are expressed in cortical dynamics. Results also indicate that timescales consistent with the time constants of neuronal membranes and fast synaptic transmission (~10-20 ms) appear to play a particularly salient role in coding, as patterns evolving on these timescales seem to be involved in the representation of stimuli with both slow and fast temporal dynamics.
The selection of features for classification, clustering and approximation is an important task in pattern recognition, data mining and soft computing. For real-valued features, this contribution shows how feature selection for a high number of features can be implemented using mutual in-formation. Especially, the common problem for mutual information computation of computing joint probabilities for many dimensions using only a few samples is treated by using the Rènyi mutual information of order two as computational base. For this, the Grassberger-Takens corre-lation integral is used which was developed for estimating probability densities in chaos theory. Additionally, an adaptive procedure for computing the hypercube size is introduced and for real world applications, the treatment of missing values is included. The computation procedure is accelerated by exploiting the ranking of the set of real feature values especially for the example of time series. As example, a small blackbox-glassbox example shows how the relevant features and their time lags are determined in the time series even if the input feature time series determine nonlinearly the output. A more realistic example from chemical industry shows that this enables a better ap-proximation of the input-output mapping than the best neural network approach developed for an international contest. By the computationally efficient implementation, mutual information becomes an attractive tool for feature selection even for a high number of real-valued features.
This note shows that in non-deterministic extended lambda calculi with letrec, the tool of applicative (bi)simulation is in general not usable for contextual equivalence, by giving a counterexample adapted from data flow analysis. It also shown that there is a flaw in a lemma and a theorem concerning finite simulation in a conference paper by the first two authors.
Zur genomweiten Genexpressionsanalyse werden Microarray-Experimente verwendet. Ziel dieser Arbeit ist es, Methoden zur Präprozessierung von Microarrays der Firma Affymetrix zu evaluieren und die VSN-Methode für Experimente mit weniger als 1000 Zellen zu verbessern. Bei dieser Technologie wird die Expression jedes Gens durch mehrere Probessets gemessen. Jedes Probeset besteht aus einem Perfect-Match (PM) und einem dazugehörigen Mismatch (MM). Der Expressionswert pro Gen wird durch ein vierstufiges Verfahren aus den einzelnen Probe-Werten berechnet: Hintergrundkorrektur, Normalisierung, PM-Adjustierung und Aggregation. Für jeden dieser Schritte existieren mehrere Algorithmen. Dazu dienten die im affy-Paket des Bioconductor implementierten Methoden MAS5, RMA, VSN und die Methode sRMA von Cope et al. [Cope et al., 2006] in Kombination mit der Methode VSN von Huber et al. [Huber et al., 2002]. Den ersten Teil dieser Arbeit bildet die Reanalyse der Datensätze von Küppers et al. [Küppers et al., 2003] und Piccaluga et al. [Piccaluga et al., 2007] mit der VSN-Methode. Dabei konnte gezeigt werden, dass die VSN-Methode gegenüber Klein et al. [Klein et al., 2001] Vorteile zeigt. Bei beiden Datensätzen wurden zusätzliche Gene gefunden, die für die Pathogenese der jeweiligen Tumorarten wichtig sein können. Einige der zusätzlich gefunden Gene wurden durch andere wissenschaftliche Arbeiten bestätigt. Die Gene, die bisher in keinem Zusammenhang mit der untersuchten Tumorart stehen, sind eine Möglichkeit für die weitere Forschung. Vor allem der Zytokine/Zytokine Signalweg wurde bei beiden Reanalysen als überrepräsentiert erkannt. Da für einige Microarray-Experimente die Anzahl der Zellen und damit die Menge an mRNA nur begrenzt zur Verfügung stehen, müssen die Laborarbeit und die statistischen Analysen angepasst werden. Hierzu werden fünf Methoden für die Präprozessierung untersucht, um zu evaluieren, welche Methode geeignet ist, derartige Expressionsdaten zu verrechnen. Auf Basis eines Testdatensatzes der bereits zur Etablierung des Laborprozesses diente werden Expressionswerte durch empirische Verteilung, Gammaverteilung und ein linear gemischtes Modell simuliert. Die Simulation lässt sich in vier Schritte einteilen: Wahl der Verteilung, Simulation der Expressionsmatrix, Simulation der differentiellen Expression, Sortierung der Probes innerhalb des Probesets. Anschließend werden die fünf Präprozessierungsmethoden mit diesen simulierten Expressionsdaten auf ihre Sensitivität und Spezifität untersucht. Während sich bei den empirisch und gammaverteilt simulierten Expressionsdaten kein eindeutiges Ergebnis abzeichnet, hat sVSN bei den Daten aus dem linear gemischten Modell die größte Sensitivität und die größte Spezifität. Der in dieser Arbeit entwickelte sVSN-Algorithmus wurde zum ersten Mal angewendet und bewertet. Abschließend wird ein Teildatensatz von Brune et al. verwendet und hinsichtlich der fünf Präprozessierungsmethoden untersucht. Die Ergebnisse der sVSN-Methode wird im Detail weiter verfolgt. Die zusätzlich gefunden Gene können durch bereits veröffentlichte Arbeiten bestätigt werden. Letztendlich zeigt sich, dass neuere statistische Methoden (wie das im Rahmen dieser Arbeit entwickelte sVSN) bei der Analyse von Affymetrix Microarrays einen Vorteil bringen. Die sVSN und sRMA Methoden zeigen Vorteile, da die Probes nach der Normalisierung gewichtet werden, bevor diese aggregiert werden. Die MAS5-Methode schneidet am schlechtesten ab und sollte bei geringen Zellmengen nicht eingesetzt werden. Für die Analyse mit geringer Menge an mRNA müssen weitere Untersuchungen vorgenommen werden, um eine geeignete statistische Methode für die Analyse der Expressionsdaten zu finden.
Ambiguity and communication
(2009)
The ambiguity of a nondeterministic finite automaton (NFA) N for input size n is the maximal number of accepting computations of N for an input of size n. For all k, r 2 N we construct languages Lr,k which can be recognized by NFA's with size k poly(r) and ambiguity O(nk), but Lr,k has only NFA's with exponential size, if ambiguity o(nk) is required. In particular, a hierarchy for polynomial ambiguity is obtained, solving a long standing open problem (Ravikumar and Ibarra, 1989, Leung, 1998).
Bayessche Methoden zur Schätzung von Stammbäumen mit Verzweigungszeitpunkten aus molekularen Daten
(2009)
Ein großes Ziel der Evolutionsbiologie ist es, die Stammesgeschichte der Arten zu rekonstruieren. Historisch verwendeten Systematiker hierfür morphologische und anatomische Merkmale. Mit dem stetigen Zuwachs an verfügbaren Sequenzdaten werden heute verstärkt Methoden entwickelt und eingesetzt, welche die Rekonstruktion auf Basis von molekularen Daten ermöglichen. Im Fokus der aktuellen Forschung steht die Anwendung und Weiterentwicklung Bayesscher Methoden. Diese Methoden besitzen große Popularität, da sie in Verbindung mit Markov-Ketten-Monte-Carlo-Verfahren eingesetzt werden können, um einen Stammbaum zu vorgegebenen Spezies zu schätzen und dessen Variabilität zu bestimmen. Im Rahmen dieser Dissertation wurde die erweiterbare Software TreeTime entwickelt. TreeTime bietet Schnittstellen für die Einbindung von molekularen Evolutions- und Ratenänderungsmodellen und stellt neu entwickelte Methoden bereit, um Stammbäume mit Verzweigungszeitpunkten zu rekonstruieren. In TreeTime werden die molekularen Daten und die zeitlichen Informationen, wie z.B. Fossilfunde, in einem Bayes-Verfahren simultan berücksichtigt, um die Zeitpunkte der Artaufspaltungen genauer zu datieren. Für die Anwendung Bayesscher Methoden in der Rekonstruktion von Stammbäumen wird ein stochastisches Modell benötigt, das die Evolution der molekularen Sequenzen entlang den Kanten eines Stammbaums beschreibt. Der Mutationsprozess der Sequenzen wird durch ein molekulares Evolutionsmodell definiert. Die Verwendung der klassischen molekularen Evolutionsmodelle impliziert die Annahme einer konstanten Evolutionsgeschwindigkeit der Sequenzen im Stammbaum. Diese Annahme wird als Hypothese der molekularen Uhr bezeichnet und bildet die Grundlage zum Schätzen der Verzweigungszeiten des Stammbaums. Der Verzweigungszeitpunkt, an dem sich zwei Spezies im Stammbaum aufspalten, spiegelt sich in der Ähnlichkeit der zugehörigen molekularen Sequenzen. Je älter dieser Verzweigungszeitpunkt ist, desto größer ist die Anzahl der unterschiedlichen Positionen in den Sequenzen. Häufig ist jedoch die Annahme der molekularen Uhr verletzt, so dass in gewissen Teilbereichen eines Stammbaums eine erhöhte Evolutionsgeschwindigkeit nachweisbar ist. Falls die Verletzung konstanter Evolutionsgeschwindigkeiten nicht ausgeschlossen werden kann, sollten schwankende Mutationsraten in der Modellierung explizit berücksichtigt werden. Hierfür wurden verschiedene Ratenänderungsmodelle vorgeschlagen. Bisher sind nur wenige dieser Ratenänderungsmodelle in Softwarepaketen verfügbar und ihre Eigenschaften sind nicht ausreichend erforscht. Das Ziel dieser Arbeit ist die Entwicklung und Bereitstellung von Bayesschen Modellen und Methoden zum Schätzen von Stammbäumen mit Verzweigungszeitpunkten. Die Methoden sollten auch bei unterschiedlichen Evolutionsgeschwindigkeiten im Stammbaum anwendbar sein. Vorgestellt wird ein neues Ratenänderungsmodell, eine neue Möglichkeit der Angabe von flexiblen Beschränkungen für die Topologie des Stammbaums sowie die Nutzung dieser Beschränkungen für die zeitliche Kalibrierung. Das neue Raten Änderungsmodell sowie die topologischen und zeitlichen Beschränkungen werden in einen modularen Softwareentwurf eingebettet. Durch den erweiterbaren Entwurf können bestehende und zukünftige molekulare Evolutionsmodelle und Ratenänderungsmodelle in die Software eingebunden und verwendet werden. Die vorgestellten Modelle und Methoden werden gemäß dem Softwareentwurf in das neu entwickelte Programm TreeTime aufgenommen und effzient implementiert. Zusätzlich werden bereits vorhandene Modelle programmiert und eingebunden, die nicht in anderen Softwarepaketen verfügbar sind. Des Weiteren wird eine neue Methode entwickelt und angewendet, um die Passgenauigkeit eines Modells für die Apriori-Verteilung auf der Menge der Baumtopologien zu beurteilen. Diese Methode wird zur Auswahl geeigneter Modelle benutzt, indem eine Auswertung der beobachteten Baumtopologien der Datenbank TreeBASE durchgeführt wird. Anschließend wird die Software TreeTime in einer Simulationsstudie eingesetzt, um die Eigenschaften der implementierten Ratenänderungsmodelle zu vergleichen. Die Software wird für die Rekonstruktion des Stammbaums zu 38 Spezies aus der Familie der Eidechsen (Lacertidae) verwendet. Da die zugehörigen molekularen Daten von der Hypothese der molekularen Uhr abweichen, werden unterschiedliche Ratenänderungsmodelle bei der Rekonstruktion verwendet und abschließend bewertet. ........
Algorithms and data structures constitute the theoretical foundations of computer science and are an integral part of any classical computer science curriculum. Due to their high level of abstraction, the understanding of algorithms is of crucial concern to the vast majority of novice students. To facilitate the understanding and teaching of algorithms, a new research field termed "algorithm visualisation" evolved in the early 1980's. This field is concerned with innovating techniques and concepts for the development of effective algorithm visualisations for teaching, study, and research purposes. Due to the large number of requirements that high-quality algorithm visualisations need to meet, developing and deploying effective algorithm visualisations from scratch is often deemed to be an arduous, time-consuming task, which necessitates high-level skills in didactics, design, programming and evaluation. A substantial part of this thesis is devoted to the problems and solutions related to the automation of three-dimensional visual simulation of algorithms. The scientific contribution of the research presented in this work lies in addressing three concerns: - Identifying and investigating the issues related to the full automation of visual simulations. - Developing an automation-based approach to minimising the effort required for creating effective visual simulations. - Designing and implementing a rich environment for the visualisation of arbitrary algorithms and data structures in 3D. The presented research in this thesis is of considerable interest to (1) researchers anxious to facilitate the development process of algorithm visualisations, (2) educators concerned with adopting algorithm visualisations as a teaching aid and (3) students interested in developing their own algorithm animations.
Various concurrency primitives had been added to functional programming languages in different ways. In Haskell such a primitive is a MVar, joins are described in JoCaml and AliceML uses futures to provide a concurrent behaviour. Despite these concurrency libraries seem to behave well, their equivalence between each other has not been proven yet. An expressive formal system is needed. In their paper "On proving the equivalence of concurrency primitives", Jan Schwinghammer, David Sabel, Joachim Niehren, and Manfred Schmidt-Schauß define a universal calculus for concurrency primitives known as the typed lambda calculus with futures. There, equivalence of processes had been proved. An encoding of simple one-place buffers had been worked out. This bachelor’s thesis is about encoding more complex concurrency abstractions in the lambda calculus with futures and proving correctness of its operational semantics. Given the new abstractions, we will discuss program equivalence between them. Finally, we present a library written in Haskell that exposes futures and our concurrency abstractions as a proof of concept.
This paper gives a brief overview of computation models for data stream processing, and it introduces a new model for multi-pass processing of multiple streams, the so-called mp2s-automata. Two algorithms for solving the set disjointness problem with these automata are presented. The main technical contribution of this paper is the proof of a lower bound on the size of memory and the number of heads that are required for solving the set disjointness problem with mp2s-automata.
We propose a variation of online paging in two-level memory systems where pages in the fast cache get modified and therefore have to be explicitly written back to the slow memory upon evictions. For increased performance, up to alpha arbitrary pages can be moved from the cache to the slow memory within a single joint eviction, whereas fetching pages from the slow memory is still performed on a one-by-one basis. The main objective in this new alpha-paging scenario is to bound the number of evictions. After providing experimental evidence that alpha-paging can adequately model flash-memory devices in the context of translation layers we turn to the theoretical connections between alpha-paging and standard paging. We give lower bounds for deterministic and randomized alpha-paging algorithms. For deterministic algorithms, we show that an adaptation of LRU is strongly competitive, while for the randomized case we show that by adapting the classical Mark algorithm we get an algorithm with a competitive ratio larger than the lower bound by a multiplicative factor of approximately 1.7.