Informatik
Refine
Year of publication
Document Type
- Preprint (747)
- Article (400)
- Working Paper (119)
- Doctoral Thesis (92)
- Diploma Thesis (46)
- Conference Proceeding (41)
- Book (37)
- Bachelor Thesis (35)
- diplomthesis (29)
- Report (25)
- Part of a Book (13)
- Contribution to a Periodical (10)
- Master's Thesis (6)
- Habilitation (1)
- Lecture (1)
- Review (1)
Has Fulltext
- yes (1603)
Is part of the Bibliography
- no (1603)
Keywords
Institute
- Informatik (1603)
- Frankfurt Institute for Advanced Studies (FIAS) (1001)
- 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)
Raytracing und Szenengraphen
(2006)
Raytracing ist ein bekanntes Verfahren zur Erzeugung fotorealistischer Bilder. Globale Beleuchtungseffekte einer 3D-Szene werden durch das Raytracing-Verfahren physikalisch korrekt dargestellt. Erst aktuelle Forschungsarbeiten ermöglichen es, das sehr rechenintensive Verfahren bei interaktiven Bildraten in Echtzeit zu berechnen. Komplexe 3D-Szenen, wie sie beispielsweise in 3D-Spielen oder Simulationen vorkommen, können durch einen Szenengraphen modelliert und animiert werden. Damit die Rendering-Ergebnisse eines Szenengraphen näher an einem realen Bild liegen, ist es erforderlich das Raytracing-Verfahren in einen Szenengraphen einzugliedern. In dieser Arbeit werden die Möglichkeiten zur Integration eines Echtzeit-Raytracers in eine Szenengraph-API untersucht. Ziel dieser Diplomarbeit ist die Darstellung dynamischer Szenen bei interaktiven Bildraten unter Verwendung des Raytracing-Verfahrens auf einem herkömmlichen PC. Zunächst müssen bestehende Open Source Szenengraph-APIs und aktuelle Echtzeit-Raytracer auf ihre Eignung zur Integration hin überprüft werden. Bei der Verarbeitung dynamischer Szenen spielt die verwendete Beschleunigungsdatenstruktur des Raytracers eine entscheidende Rolle. Da eine komplette Neuerstellung der Datenstruktur in jedem Bild zuviel Zeit in Anspruch nimmt, ist eine schnelle und kostengünstige Aktualisierung erforderlich. Die in [LAM01] vorgestellte Lösung, eine Hüllkörperhierarchie (BVH) als Beschleunigungsdatenstruktur zu verwenden, fügt sich sehr gut in das Konzept eines Szenengraphen ein. Dadurch wird eine einfache Aktualisierung ermöglicht. Um das Ziel dieser Arbeit zu erreichen, ist es notwendig, die Parallelisierbarkeit des Raytracing-Verfahrens auszunutzen. Purcell zeigt in [Pur04], dass Grafikprozessoren (GPUs) neben ihrer eigentlichen Aufgabe auch für allgemeine, parallele Berechnungen wie das Raytracing verwendet werden können. Die in bisherigen Arbeiten über GPU-basiertes Raytracing entwickelten Systeme können dynamische Szenen nicht bei interaktiven Bildraten darstellen. Aus diesem Grund wird in dieser Diplomarbeit ein neues System konzipiert und implementiert, das den in [TS05] entwickelten Raytracer erweitert und in die Open Source Szenengraph-API OGRE 3D integriert. Das implementierte System ermöglicht die Darstellung statischer und dynamischer Szenen unter Verwendung einer Consumer-Grafikkarte bei interaktiven Bildraten. Durch seine Erweiterbarkeit bildet das System das Grundgerüst für ein Realtime-High-Quality-Rendering-System.
We model sequential synchronous circuits on the logical level by signal-processing programs in an extended lambda calculus Lpor with letrec, constructors, case and parallel or (por) employing contextual equivalence. The model describes gates as (parallel) boolean operators, memory using a delay, which in turn is modeled as a shift of the list of signals, and permits also constructive cycles due to the parallel or. It opens the possibility of a large set of program transformations that correctly transform the expressions and thus the represented circuits and provides basic tools for equivalence testing and optimizing circuits. A further application is the correct manipulation by transformations of software components combined with circuits. The main part of our work are proof methods for correct transformations of expressions in the lambda calculus Lpor, and to propose the appropriate program transformations.
This paper extends the internal frank report 28 as follows: It is shown that for a call-by-need lambda calculus LRCCP-Lambda extending the calculus LRCC-Lambda by por, i.e in a lambda-calculus with letrec, case, constructors, seq and por, copying can be done without restrictions, and also that call-by-need and call-by-name strategies are equivalent w.r.t. contextual equivalence.
Call-by-need lambda calculi with letrec provide a rewritingbased operational semantics for (lazy) call-by-name functional languages. These calculi model the sharing behavior during evaluation more closely than let-based calculi that use a fixpoint combinator. In a previous paper we showed that the copy-transformation is correct for the small calculus LR-Lambda. In this paper we demonstrate that the proof method based on a calculus on infinite trees for showing correctness of instantiation operations can be extended to the calculus LRCC-Lambda with case and constructors, and show that copying at compile-time can be done without restrictions. We also show that the call-by-need and call-by-name strategies are equivalent w.r.t. contextual equivalence. A consequence is correctness of all the transformations like instantiation, inlining, specialization and common subexpression elimination in LRCC-Lambda. We are confident that the method scales up for proving correctness of copy-related transformations in non-deterministic lambda calculi if restricted to "deterministic" subterms.
This paper proves several generic variants of context lemmas and thus contributes to improving the tools to develop observational semantics that is based on a reduction semantics for a language. The context lemmas are provided for may- as well as two variants of mustconvergence and a wide class of extended lambda calculi, which satisfy certain abstract conditions. The calculi must have a form of node sharing, e.g. plain beta reduction is not permitted. There are two variants, weakly sharing calculi, where the beta-reduction is only permitted for arguments that are variables, and strongly sharing calculi, which roughly correspond to call-by-need calculi, where beta-reduction is completely replaced by a sharing variant. The calculi must obey three abstract assumptions, which are in general easily recognizable given the syntax and the reduction rules. The generic context lemmas have as instances several context lemmas already proved in the literature for specific lambda calculi with sharing. The scope of the generic context lemmas comprises not only call-by-need calculi, but also call-by-value calculi with a form of built-in sharing. Investigations in other, new variants of extended lambda-calculi with sharing, where the language or the reduction rules and/or strategy varies, will be simplified by our result, since specific context lemmas are immediately derivable from the generic context lemma, provided our abstract conditions are met.
Fraktale Planetengenerierung
(2006)
Wie die Diplomarbeit gezeigt hat, lassen sich zwar ganze Planeten ohne größere Verzerrungen mit Hilfe fraktaler Methoden modellieren. Allerdings stößt die Darstellungsqualität an ihre Grenzen, da sich gängige Level-of-Detail-Algorithmen, wie ROAM bzw. Röttger, nicht einfach an die durch das Surface-Refinement gegebenen Bedingungen anpassen. Insbesondere die Triangulierung durch gleichseitige Dreiecke hat sich als problematisch erwiesen. Ohne diese LOD-Techniken kann aber nur eine relativ geringe Auflösung berechnet werden. Der vorgestellte Level-of-Detail-Algorithmus stellt zwar keinen Ersatz für die obengenannten Verfahren dar. Er bietet aber eine sehr gute Grundlage, denn er schränkt einfach und dadurch sehr schnell den Bereich ein, in dem sich der Betrachter bzw. die virtuelle Kamera befindet. Dies ist vorallem auch deshalb wichtig, weil die bisher entwickelten LOD-Algorithmen nur mit vergleichsweise kleinen Flächen wirklich effizient funktionieren. Eine Kombination aus dem in der Diplomarbeit entwickelten Verfahren und einem ROAM/Röttger-ähnlichen Algorithmus würde deren jeweiligen Schwächen beheben. Die eigentliche Modellierung der Landschaft bzw. der Gebirgszüge lässt sich dagegen problemlos auch auf sphärische Körper übertragen, zumindest wenn man dafür den Plasma-Algorithmus verwendet.
Reasoning about the correctness of program transformations requires a notion of program equivalence. We present an observational semantics for the concurrent lambda calculus with futures Lambda(fut), which formalizes the operational semantics of the programming language Alice ML. We show that natural program optimizations, as well as partial evaluation with respect to deterministic rules, are correct for Lambda(fut). This relies on a number of fundamental properties that we establish for our observational semantics.
Wiki-Systeme im eLearning
(2006)
Wiki-Systeme lassen sich in den verschiedensten Anwendungsgebieten auf angenehme Weise, aufgrund ihrer Open-Source Lizenz, durch die Anreicherung entsprechender Zusatzmodule anpassen. An dieser Stelle muss jedoch bedacht werden, dass durch die Integration vermehrter Funktionen, das charakteristische Merkmal der Wiki-Systeme 'Einfachheit' an Präsenz verlieren kann. Dieses, für Wikis typische Charakteristikum ist eine nicht zu unterschätzende Stärke, da sowohl die Expansion der Enzyklopädie Wikipedia, als auch die zunehmende Anzahl bestehender Wikis im Internet geradezu Beweis dafür sind, dass keine anderen Anwendungen in diesem Verhältnis existiert haben. Würde somit das Wiki, aufgrund der Anpassung an ein vorliegendes Konzept an Einfachheit verlieren, so müssten die Beweggründe des Wiki-Einsatzes noch mal überdacht werden. Ebenso könnte in den Bereichen, in denen die Stärken von Wikis unbrauchbar sind, ein anderes System womöglich bessere Ergebnisse liefern als ein Wiki. Aus diesen Gründen sollte vor einem Wiki-Einsatz überprüft werden, ob die vorhandenen Merkmale und Funktionen eines Wikis mit den eigenen Anforderungen übereinstimmen. Die im Rahmen dieser Arbeit durchgeführte Befragung hat gezeigt, das Wikis größtenteils als Präsentationsmedium, zur gemeinsamen Texterstellung und als Informationsplattform genutzt werden. Es ist deutlich geworden, dass die Integration von Wikis im Lehrbereich geeignete Anwendung findet. Auffallend war, dass zwar bei (fast) allen Befragten Schwierigkeiten aufgetreten sind und sogar erhoffte Erwartungen teilweise nicht erfüllt wurden, dennoch war der größte Teil der Befragten mit dem Wiki-Einsatz zufrieden und bewertete diesen als positiv. Die Art der aufgetretenen Schwierigkeiten und Schwachstellen zeigt, dass den Lehrenden gewisse Anleitungen und Richtlinien für einen erfolgreichen Wiki-Einsatz fehlten. Denn Informationen zum didaktischen Rahmen - in denen Wikis eingesetzt werden können - und wie Wikis eingesetzt werden sollen, waren nicht vorhanden. Somit sollen die - in dieser Arbeit - erarbeiteten Empfehlungen und Kriterien, Lehrende zu einem optimierten Wiki-Einsatz in Lehrveranstaltungen verhelfen. Außerdem sind in dieser Arbeit Vorgaben enthalten, wie Wiki-Einsätze von Lehrenden gestaltet werden können, so dass die häufig auftretenden Probleme vermieden werden können. Die erarbeiteten Empfehlungen und Kriterien sind gleichermaßen aus den positiven, wie auch aus den negativen Erfahrungen der Befragten entstanden. Insbesondere sollen die Empfehlungen und Kriterien, die von den Befragten permanent beklagten auftretenden Schwierigkeiten und Probleme verhindern. Eine Garantie jedoch, dass die Einhaltung dieser Empfehlungen und Kriterien zu einem erfolgreichen Wiki-Einsatz führen und ob keine relevanten Kriterien unbeachtet gelassen sind, kann an dieser Stelle nicht gegeben werden. Ob sich nun die Probleme, die sich mit Wiki-Einsätzen wiederholt ergeben haben, durch die Befolgung dieser Kriterien und Empfehlungen vermeiden lassen, könnte im Rahmen einer nachfolgenden Diplomarbeit untersucht werden, in der Wiki- Einsätze, begleitet werden. Weiterhin sollte im Rahmen einer weiteren Arbeit die Situation der Lernenden und die Auswirkung auf das Lernverhalten in Verbindung mit Wiki-Systemen evaluiert werden, so dass einige Thesen dieser Arbeit belegt oder gar widerlegt werden können.
ALPHA ist die Architektur einer lokationssensitiven Puppe für hydropneumatische Animation. Es ist ein Animations-Eingabegerät. Die Puppe soll ein Objekt repräsentieren, welches animiert werden soll. Ihre Gliedmaßen, welche aus Knochen und Gelenken bestehen, sind beweglich. Sie wird an einen Computer angeschlossen und die gegenwärtige Stellung ihrer Gelenke kann mittels eines ebenfalls entwickelten Treibers von diesem Computer eingelesen werden. Des Weiteren wird erklärt was eine hydropneumatische Animation ist. Die Diplomarbeit weist die folgende Gliederung auf: • Motivation • Technische Grundlagen und State-Of-The-Art-Analyse • Anforderungsanalyse • Das eigene Konzept, die lokationssensitive Puppe (ALPHA) • Evaluation • Ausblick Die Motivation beschäftigt sich mit der Entwicklung der Filmanimation und einiger Errungenschaften in der Laufbahn der Animationstechnologischen Entwicklung. Die technischen Grundlagen beschränken sich auf die Funktionsweise von Messapparaturen, welche als Gelenkstellungssensoren fungieren können. Im Einzelnen sind das der optische Resolver, der Optoencoder und die Kombination von einem Drehpotentiometer und einem Analog/Digital-Wandler. Zur State-Of-The-Art-Analyse gehört die Erläuterung bereits entwickelter Stellungs- und Bewegungsmessender Technologien, wie das Stop-Motion-Verfahren, das Motion-Capturing, das Dinosaur-Input-Device und der Datenhandschuh. Eine Zusammenstellung der Defizite dieser Verfahren schließt dieses Kapitel ab. Die Analyse der Anforderungen an ein zu entwickelndes System ist im Kapitel Anforderungsanalyse zu finden. Zum eigenen Konzept gehört die gesamte Entwicklung einer lokationssensitiven Puppe. Die Puppe ist das Ebenbild des Skeletts eines zu animierendes Objekts. Sie besteht aus mehreren Gliedmaßen, welche an ihren Gelenken beweglich sind. Die Gelenkstellung wird von Potentiometern gemessen, dessen Signal ein A/D-Wandler empfängt. Die Umschaltung der einzelnen Messwerte erfolgt über Analog-Multiplexer. Die gesamte Steuerung der Bauteile und das Auslesen des A/D-Wandler werden durch einen Treiber über den Parallelport eines PCs gesteuert. Die Funktionsweise des Treibers und seine Implementierung werden ebenfalls in diesem Kapitel erläutert. Im Kapitel Evaluation befindet sich eine Bewertung des Konzepts und der Erfüllung der Anforderungsanalyse. Schließlich zeigt der Ausblick die Möglichkeiten der Anwendungen der Puppe und einen Blick in zukünftige Technologien.
We develop a proof method to show that in a (deterministic) lambda calculus with letrec and equipped with contextual equivalence the call-by-name and the call-by-need evaluation are equivalent, and also that the unrestricted copy-operation is correct. Given a let-binding x = t, the copy-operation replaces an occurrence of the variable x by the expression t, regardless of the form of t. This gives an answer to unresolved problems in several papers, it adds a strong method to the tool set for reasoning about contextual equivalence in higher-order calculi with letrec, and it enables a class of transformations that can be used as optimizations. The method can be used in different kind of lambda calculi with cyclic sharing. Probably it can also be used in non-deterministic lambda calculi if the variable x is "deterministic", i.e., has no interference with non-deterministic executions. The main technical idea is to use a restricted variant of the infinitary lambda-calculus, whose objects are the expressions that are unrolled w.r.t. let, to define the infinite developments as a reduction calculus on the infinite trees and showing a standardization theorem.