Informatik
Refine
Year of publication
- 2023 (183)
- 2019 (159)
- 2016 (133)
- 2021 (130)
- 2020 (116)
- 2022 (115)
- 2015 (96)
- 2017 (91)
- 2018 (82)
- 2009 (38)
- 2024 (36)
- 2012 (34)
- 2011 (31)
- 2013 (31)
- 2010 (30)
- 2014 (30)
- 2004 (24)
- 2006 (23)
- 2001 (22)
- 2002 (22)
- 2007 (21)
- 2008 (21)
- 1999 (20)
- 2003 (19)
- 1998 (14)
- 2005 (14)
- 1994 (13)
- 1996 (13)
- 2000 (13)
- 1997 (12)
- 1995 (8)
- 1993 (4)
- 1991 (2)
- 1972 (1)
- 1978 (1)
- 1987 (1)
- 1989 (1)
- 1990 (1)
- 1992 (1)
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)
We present a higher-order call-by-need lambda calculus enriched with constructors, case-expressions, recursive letrec-expressions, a seq-operator for sequential evaluation and a non-deterministic operator amb, which is locally bottom-avoiding. We use a small-step operational semantics in form of a normal order reduction. As equational theory we use contextual equivalence, i.e. terms are equal if plugged into an arbitrary program context their termination behaviour is the same. We use a combination of may- as well as must-convergence, which is appropriate for non-deterministic computations. We evolve different proof tools for proving correctness of program transformations. We provide a context lemma for may- as well as must- convergence which restricts the number of contexts that need to be examined for proving contextual equivalence. In combination with so-called complete sets of commuting and forking diagrams we show that all the deterministic reduction rules and also some additional transformations keep contextual equivalence. In contrast to other approaches our syntax as well as semantics does not make use of a heap for sharing expressions. Instead we represent these expressions explicitely via letrec-bindings.
Static analysis of different non-strict functional programming languages makes use of set constants like Top, Inf, and Bot denoting all expressions, all lists without a last Nil as tail, and all non-terminating programs, respectively. We use a set language that permits union, constructors and recursive definition of set constants with a greatest fixpoint semantics. This paper proves decidability, in particular EXPTIMEcompleteness, of subset relationship of co-inductively defined sets by using algorithms and results from tree automata. This shows decidability of the test for set inclusion, which is required by certain strictness analysis algorithms in lazy functional programming languages.
Extending the method of Howe, we establish a large class of untyped higher-order calculi, in particular such with call-by-need evaluation, where similarity, also called applicative simulation, can be used as a proof tool for showing contextual preorder. The paper also demonstrates that Mann’s approach using an intermediate “approximation” calculus scales up well from a basic call-by-need non-deterministic lambdacalculus to more expressive lambda calculi. I.e., it is demonstrated, that after transferring the contextual preorder of a non-deterministic call-byneed lambda calculus to its corresponding approximation calculus, it is possible to apply Howe’s method to show that similarity is a precongruence. The transfer is not treated in this paper. The paper also proposes an optimization of the similarity-test by cutting off redundant computations. Our results also applies to deterministic or non-deterministic call-by-value lambda-calculi, and improves upon previous work insofar as it is proved that only closed values are required as arguments for similaritytesting instead of all closed expressions.
Die Implementation der Striktheits-Analyse, die im Zuge dieser Arbeit vorgenommen wurde, stellt eine effiziente Approximation der abstrakten Reduktion mit Pfadanalyse dar. Durch die G#-Maschine, ein neues, auf der G-Maschine basierendes Maschinenmodell, wurde die verwendete Methode systematisch dargelegt. Die große Ähnlichkeit mit der G-Maschin, die in unserer Implementation beibehalten werden konnte, zeigt, wie natürlich die verwendete Methode der Reduktion in funktionalen Programmiersprachen entspricht. Obwohl die Umsetzung mehr Wert auf Nachvollziehbarkeit, als auf Effizienz legt, zeigt sie, daß die Methode der abstrakten Reduktion mit Pfadanalyse auch in einer funktionalen Implementierung durchaus alltagstauglich ist und Striktheits-Information findet, die Umsetzungen anderer Methoden nicht finden. Es bestehen Möglichkeiten zur Optimierung u. a. von Programmteilen, die für jede simulierte G#-Maschinen-Anweisung ausgeführt werden. Bei vorsichtiger Einschätzung erscheint eine Halbierung der Laufzeit mit vertretbarem Aufwand erreichbar.
Gegenstand der Arbeit ist ein Gleichheitskalkül für den Kern einer nicht-strikten funktionalen Programmiersprache. Funktionale Programmiersprachen unterstützen bestens die Prinzipien Abstraktion, Einkapselung, Hierarchiesierung und Modularisierung, die gemeinhin als Grundelemente des Software-Engineering betrachtet werden. Darüber hinaus bieten funktionale Programmiersprachen aufgrund ihrer Entwicklung aus dem Lambda-Kalkül eine große Nähe zu mathematischen Modellen. Daher besitzen sie im Bereich der Programmverifikation ausgeprägte Vorteile gegenüber imperativen oder objekt-orientierten Programmiersprachen. In der Arbeit wird nun ein Gleichheitsbegriff für Ausdrücke in funktionalen Programmiersprachen entwickelt und dessen Praktikabilität durch die Implementierung eines Beweisers untermauert. Dieser Gleichheitsbegriff ist die kontextuelle Gleichheit, die Ausdrücke aufgrund ihres Terminierungsverhaltens als Unterprogramme in allen möglichen Kontexten einordnet. Kontextuelle Gleichheit wird in Kapitel 2 vorgestellt, nachdem der klassische und der sogenannte "lazy" Lambda-Kalkül eingeführt wurden. Kapitel 3 enthält einen Überblick über die funktionale Programmierung, da auch die Implementierung des o.g. Beweisers in einer funktionalen Programmiersprache, nämlich Haskell, durchgeführt wird. In Kapitel 4 wird die funktionale Kernsprache, die Gegenstand der Untersuchung sein wird, beschrieben. Sie enthält alle wesentlichen Elemente wie z.B. Funktionsdefinition und -anwendung sowie Datentypen. Im selben Kapitel wird auch der Gleichheitsbegriff für diese Kernsprache definiert. Kapitel 5 schließlich entwickelt auf Basis der zuvor erfolgten Definitionen einen Kalkül für den Gleichheitsbeweis. Außerdem wird in diesem Kapitel auch die Umsetzung dieses Gleichheitskalküls präsentiert. Aus der Dissertation von Marko Schütz werden hierbei Erkenntnisse über die Kontextanalyse verwendet, um erfüllende Belegungen von freien Variablen zu berechnen. Die Arbeit schließt mit Beispielanalysen und Meßwerten sowie einer Diskussion der Ergebnisse und möglicher Erweiterungen.
Die moderne Biochemie ist eine Wissenschaft, die sich im Wandel befindet. Während die bisherige Forschung sehr stark experimentell geprägt ist, existiert eine theoretische Biologie, analog zur theoretischen Chemie, nur in Ansätzen. Trotzdem wandelt sich auch diese Wissenschaft hin zu einer stärkeren Einbindung theoretischer Ansätze. Der Grund hierfür liegt in der Betrachtung von zunehmend komplexeren Systemen. So beschäftigt man sich in der Systembiologie, einem Teilbereich der Biochemie, unter anderem mit der Aufklärung komplexer Reaktionsnetzwerke. Während Ausschnitte dieser Netzwerke weiterhin experimentell aufgeklärt und verstanden werden, lässt sich das zusammenhängende Bild zunehmend nur noch durch eine theoretisch geprägte Modellbildung fassen. Darüber hinaus zeigen neuere Forschungsergebnisse die Bedeutung der Tatsache, dass Moleküle, Zellen und Zellhaufen, also wichtige Forschungsubjekte der Biochmie, dreidimensionale Gebilde sind – eine Tatsache, die bei der Modellbildung berücksichtigt werden muss. Eine Antwort auf die genannten Herausforderungen ist der konzertierte Einsatz von Simulation und Visualisierung als Mittel des Erkenntnisgewinns. Damit ist die Informatik gefordert entsprechende dedizierte Werkzeuge zu entwickeln, die Simulation, Visualisierung und Interaktion im Kontext des von der Anwendungsdisziplin gesetzten räumlich-zeitlichen Problemkreises miteinander verbinden. In dieser Arbeit wird ein integriertes Konzept zu Simulation, Interaktivität und Visualisierung vorgelegt, das auf einer Anforderungsanalyse in Bezug auf Anforderungen an die Simulation und Anforderungen an die Interaktivität und Visualisierung basiert. Zur Lösung der aufgeworfenen Probleme wird ein „Baukastensystem“ auf Basis von Multi-Agenten-Systemen vorgeschlagen. Die Auswahl des geeigneten Simulationsverfahrens, z. B. die Auswahl eines stochastischen Verfahrens gegenüber einem deterministischen Verfahrens, wird so zur Auswahl eines Bausteins, wobei gezeigt wird, wie z. B. mit Hilfe von Regeln die Auswahl auch automatisiert werden kann. Ebenso wird gezeigt, wie man „Baussteine“ auch im räumlichen Sinne verstehen kann, als Dinge, die in einem dreidimensionalen Kontext einen bestimmten Raum einnehmen und die, in ihrer Gesamtheit betrachtet, den Beobachtungsraum der Simulation ausfüllen. Diese Bausteine finden sich entsprechend ebenfalls im Kontext der Interaktion wieder. Ein wichtiger Aspekt in diesem Baukastenkonzept ist die Frage der Kommunikationsstruktur und des Kommunikationsprotokolls, für den ein Vorschlag erarbeitet wird. Das entwickelte Gesamtkonzept besteht aus zwei Teilen: Einem Konzept für Ein- und Ausgabegeräte mit einer gemeinsamen Metapher, die die Geräte logisch in den Anwendungskontext einbettet und einem Simulations- und Visualisierungskonzept auf der Basis der Kopplung heterogener intelligenter Agenten in eine gemeinsame Simulationsumgebung. Hierfür wurde ein spezieller Dialekt einer Agentenkommunikationssprache entwickelt, der dabei insbesondere den Aspekt der dreidimensionalen Visualierung einer solchen Simulation berücksichtigt.
In Abschnitt 4.1 wurden Algebren auf Mengen und Relationen vorgestellt. Desweitern wurde in Abschnitt 4.2 eine zu ALC erweiterte terminologische Wissensrepräsentationssprache ALCX definiert und gezeigt, daß die in Abschnitt 4.1 vorgestellten Algebren zur Festlegung der odell-theoretischen Semantik der Sprache ALCX benutzt werden können. Als Ergebnis einer derartigen Festlegung kann jeder terminologische Ausdruck direkt mit einem algebraischen Term assoziiert werden. Desweitern können alle in den Algebren aufgeführten universellen Identitäten in semantisch äquivalente terminologische Identitäten überführt werden. Eine mittels ALCX repräsentierte Wissensbasis ist in meinem Programm mit Hilfe der in der funktionalen Programmiersprache Gofer (Version 2.28) gegebenen Möglichkeiten formuliert. Mein Programm bietet durch Simplifizierung von Anfrageausdrücken eine optimierte Lösung des aus dem Bereich der Wissensrepräsentation bekannten Retrieval-Problems. Die Simplifizierung von Anfrageausdrücken wird in meinem Programm erzielt, indem in den oben genannten Algebren erfüllte universelle Identitäten als Simplifikationshilfsmittel benutzt werden. Die in den Algebren aufgeführten universellen Identitäten bestehen stets aus zwei äquivalenten Termen, für die eine unterschiedliche Anzahl von Reduktionsschritten zur Evaluierung benötigt werden. Es existieren universelle Identitäten, bei denen unabhängig von den Instanzen der Argumentterme ein Term gegenüber einem anderen Term effizienter auswertbar ist. Bei diesen universellen Identitäten kann eine Simplifikation von einem Term zu einem anderen Term immer unproblematisch realisiert werden. Es gibt jedoch auch universelle Identitäten, bei denen die Unabhängigkeit von den Instanzen der Argumentterme nicht gegeben ist. In diesen Fällen wird ein von der Wissensbasis abhängiges Komplexitätsabschätzungsverfahren eingesetzt, um den effizienter auswertbaren Term von zwei an einer universellen Identität beteiligten Termen zu ermitteln. Daß die Simplifikation eines Anfrageausdrucks große Einsparungen bei dessen Auswertung nach sich ziehen kann, wurde an verschiedenen Beispielen in Abschnitt 5.4.4 gezeigt. Über eine weitere Möglichkeit, die zum Simplifizieren von Anfrageausdrucken verwendet werden kann, wurde in Abschnitt 5.4.5 berichtet. Die Genauigkeit der Komplexitätsabschätzung kann erhöht werden, indem das Komplexitätsabschätzungsverfahren erweitert wird. So kann beispielsweise die Komplexität der Funktion "oder" genauer abgeschätzt werden, indem für zu vereinigende Mengen überprüft wird, ob Teilmengenbeziehungen vorhanden sind. Durch eine genauere Abschätzung der Mächtigkeit entstehender Vereinigungsmengen wird die Komplexitätsabschätzung insgesamt in ihrer Genauigkeit gesteigert. Eine Änderung der Instanzen meiner terminologischen Datenbank erfordert eine Änderung des Skripts meines Programms. Indem die Instanzen-Daten in einer veränderlichen Datenbank festgehalten würden, könnte hier Abhilfe geschaffen werden. Dies könnte im Rahmen der Erstellung einer benutzterfreundlichen Ein- und Ausgabe-Schnittstelle realisiert werden.
In this dissertation a non-deterministic lambda-calculus with call-by-need evaluation is treated. Call-by-need means that subexpressions are evaluated at most once and only if their value must be known to compute the overall result. Also called "sharing", this technique is inevitable for an efficient implementation. In the lambda-ND calculus of chapter 3 sharing is represented explicitely by a let-construct. Above, the calculus has function application, lambda abstractions, sequential evaluation and pick for non-deterministic choice. Non-deterministic lambda calculi play a major role as a theoretical foundation for concurrent processes or side-effected input/output. In this work, non-determinism additionally makes visible when sharing is broken. Based on the bisimulation method this work develops a notion of equality which respects sharing. Using bisimulation to establish contextual equivalence requires substitutivity within contexts, i.e., the ability to "replace equals by equals" within every program or term. This property is called congruence or precongruence if it applies to a preorder. The open similarity of chapter 4 represents a new concept, insofar that the usual definition of a bisimulation is impossible in the lambda-ND calculus. So in section 3.2 a further calculus lambda-Approx has to be defined. Section 3.3 contains the proof of the so-called Approximation Theorem which states that the evaluation in lambda-ND and lambda-Approx agrees. The foundation for the non-trivial precongruence proof is set out in chapter 2 where the trailblazing method of Howe is extended to be capable with sharing. By the use of this (extended) method, the Precongruence Theorem proves open similarity to be a precongruence, involving the so-called precongruence candidate relation. Joining with the Approximation Theorem we obtain the Main Theorem which says that open similarity of the lambda-Approx calculus is contained within the contextual preorder of the lambda-ND calculus. However, this inclusion is strict, a property whose non-trivial proof involves the notion of syntactic continuity. Finally, chapter 6 discusses possible extensions of the base calculus such as recursive bindings or case and constructors. As a fundamental study the calculus lambda-ND provides neither of these concepts, since it was intentionally designed to keep the proofs as simple as possible. Section 6.1 illustrates that the addition case and constructors could be accomplished without big hurdles. However, recursive bindings cannot be represented simply by a fixed point combinator like Y, thus further investigations are necessary.
Ziel dieser Arbeit war es, ein System zu entwickeln, mit dem Sätze von Reduktionsdiagrammen auf ihre Vollständigkeit überprüft werden können. Das System sollte in der puren, funktionalen Programmiersprache Haskell realisiert werden und speziell auf einen nichtdeterministischen Kalkül mit Konstruktoren, einem case-Konstrukt und einem rekursiven let- Ausdruck (letrec) ausgerichtet sein. Dazu wurde in Kapitel 2 der lambda-Kalkül und funktionale Programmiersprachen eingeführt, um die Entwicklung der Kalküle lambda-nd und lambda-nd,rec zu motivieren. Die Basis-Kalküle lambda-nd und lamda-nd,rec wurden in Kapitel 3 bezüglich ihrer Sprachdefinition und Reduktionsregeln vorgestellt. Die Implementierung der beiden Kalküle und der Parser für die verwendete Kernsprache wurden ebenso angegeben wie die Mechanismen zur Markierung und Reduktion der Terme. Die Unterscheidung eines reduzierbaren Terms in NO- und internen Redex, sowie deren Erkennung wurde in diesem Kapitel besonders herausgestellt, da sie die Grundlage für die zu validierenden Reduktionsdiagramme darstellt. Damit ist der Grundstock für diese Arbeit gelegt worden. In Kapitel 4 haben wir kurz Methoden vorgestellt, die lamda-Kalkülen und deren Derivate eine Bedeutung zuzumessen versuchen, um Programme oder Terme miteinander vergleichen zu können. Also nicht nur ihre Termstruktur, sondern ihr Verhalten zu vergleichen. Dabei ist festgestellt worden, daß für nichtdeterministische Kalküle nur eine Methode verfügbar ist, und zwar die der kontextuellen Äquivalenz. Da wir gängige Programmtransformationen dahingehend überprüfen wollten, ob sie der kontextuellen Äquivalenz genügen, also nicht die Auswertung oder das Ergebnis derselben verändern, haben wir ein Kontext-Lemma vorgestellt. Mit Hilfe des Kontext-Lemmas ist es uns möglich gewesen, die Gültigkeit von Beweisen in Reduktionskontexten auf beliebige Kontexte auszudehnen. Für die eigentlichen Beweise werden Reduktionsdiagramme benötigt, die Reduktionsfolgen in verschiedener Weise umstellen. Wir haben die Reduktionsdiagramme ebenfalls in Kapitel 4 definiert. Die Reduktionsdiagramme müssen an jeder Stelle einer Reduktionsfolge anwendbar sein, da sonst die Äquivalenz-Beweise nicht möglich sind. D. h. es müßte bewiesen werden, daß mindestens ein Reduktionsdiagramm einer definierten Menge von Reduktionsdiagrammen für jeden Term und jede seiner Reduktionsfolgen anwendbar ist. Der naive Weg wäre, alle Terme und seine Reduktionsfolgen dahingehend zu überprüfen. Da dies jedoch nicht möglich ist, haben wir uns dazu entschlossen so viele Terme wie möglich zu untersuchen, nicht um die Vollständigkeit der Diagramme zu beweisen, sondern um zu zeigen, daß auf viele verschiedenartige Terme Reduktionsdiagramme erfolgreich angewendet werden können. Die Generierung der Terme haben wir in Kapitel 5 ausführlich dargestellt. In Kapitel 6 haben wir die Sprache zur Darstellung von Reduktionsdiagrammen und die Implementierung der Diagramm-Validierung beschrieben. Weiterhin haben wir ein Verfahren vorgestellt, mit dem wir fehlende Diagramme für Terme suchen und meist auch finden können. Das gesamte System haben wir so aufgebaut, daß eine große Menge an Termen generiert wird, für die Diagramme anwendbar sein müssen. Wenn keines der Diagramme auf einen Term anwendbar ist, also nicht validiert werden kann, dann wird ein passendes Diagramm gesucht. Mit Hilfe des entwickelten Systems Jonah sind in Kapitel 7 verschiedene Programmtransformationen dahingehend überprüft worden, ob die angegebenen Reduktionsdiagramme für große Mengen von Termen gültig sind. Dabei ist als Ergebnis herausgekommen, daß ein vollständiger Satz an Reduktionsdiagrammen für die (cp)-Reduktion nur sehr schwer zu finden ist. Selbst neu hinzugefügte Transformationen, die dabei helfen sollten, die Schwierigkeiten zu umgehen, konnten nicht verwendet werden, da es uns ebenfalls nicht möglich gewesen ist, für sie vollständige Diagrammsätze zu finden. Daraufhin haben wir den Basis-Kalkül zweimal erweitert, um die Schwierigkeiten der (cp)-Diagramme in den Griff zu bekommen. Aber auch diese Ansätze haben kein zufriedenstellendes Ergebnis geliefert. Als positives Ergebnis dieser Arbeit kann aber festgestellt werden, daß das System Jonah bei der Entwicklung nichtdeterministischer Kalküle auf Basis von lambda-Kalkülen eine sehr gute Hilfestellung sein kann, auch wenn es nicht zum vollständigen Beweis der Gültigkeit von Reduktionsdiagrammen dienen kann.
In dieser Diplomarbeit wurde zunächst eine Einführung in das Gebiet der Unifikationstheorie gegeben, um dann zum Teilgebiet des Kontextmatchings zu kommen. Dieses wurde in das Gesamtgebiet der Unifikation eingeordnet. In Anlehnung an [Schm2003] wurde die Komplexität einiger Einschränkungen des Kontextmatchings betrachtet. Insbesondere wurde ein Algorithmus zur Lösung linearer Kontextmatchingprobleme in polynomieller Zeit vorgestellt. Es folgte die Einführung des Transformationsalgorithmus aus [Schm2003] zur Lösung allgemeiner Kontextmatchingprobleme, wobei nach und nach verbesserte Transformationsregeln für einzelne spezielle Problemsituationen vorgestellt wurden. Über [Schm2003] hinausgehend wurden die Regeln Split: Korrespondierende Lochpfade und Konstantenelimination vorgestellt. Im Rahmen der Diplomarbeit wurden die genannten Algorithmen in der funktionalen Programmiersprache Haskell implementiert, wobei auf eine einfache Erweiterbarkeit um neue Transformationsregeln sowie alternative Heuristiken zur Auswahl der in einem Schritt anzuwendenden Transformationsregel geachtet wurde. Die Implementierung (und damit auch die in ihr implementierten Algorithmen) wurde mit Hilfe von zufällig erzeugten Termen auf ihre Leistungsfähigkeit getestet. Hauptaugenmerk lag dabei darauf, inwiefern sich Regeln, die über die Basisregeln aus Tabelle 3.4.1 hinausgehen, positiv auf die Anzahl der Transformationsschritte auswirken. Das Ergebnis ist beeindruckend: durch die Einführung komplexerer Transformationsregeln ließen sich in unseren Testfällen bis zu 87% der Transformationsschritte einsparen, im Durchschnitt immerhin noch 83%. Speziell komplexere Kontextmatchingprobleme mit einer größeren Anzahl an Kontextvariablen profitieren hiervon. Insbesondere die Erkennung korrespondierender Positionen in Verbindung mit der Regel Split führte zu erheblichen Verbesserungen. Die implementierten Algorithmen zur Erkennung korrespondierender Positionen stellen teilweise nur ein notwendiges Kriterium für die Existenz korrespondierender Löcher dar. Dies kann zu fehlerhaften Erkennungen solcher Positionen führen. Wie sich in unseren Tests zeigte, scheint das jedoch kein gravierendes Problem zu sein, da die entsprechenden Split- Transformationen ohnehin äußerst sparsam eingesetzt werden.
Wir haben ein Softwaresystem entwickelt, das in der Lage ist, Beschreibungen von Termersetzungssystemen höherer Ordnung, deren Reduktionsregeln auf einer strukturellen operationalen Semantik basieren, einzulesen und zu interpretieren. Das System ist dabei fähig, Reduktionskontexte für die Redexsuche zu benutzen, die entweder vom Benutzer definiert werden können oder automatisch anhand der strikten Positionen berechnet werden. Außerdem dürfen Kontexte und spezielle Definitionen für Term-Mengen, die wir Domains nennen, in den Reduktionsregeln verwendet werden. Mit dem resultierenden Reduktionssystem-Format können wir somit nicht nur den „lazy“ Lambda-Kalkül, den Call-by-Value Lambda-Kalkül und verwandte, um Konstruktoren und Fallunterscheidungen erweiterte Kalküle, wie die in Kapitel 4 vorgestellten Kernsprachen KFP und PCF, darstellen, sondern auch den (in Abschnitt 4.3 vorgestellten) Call-by-Need Lambda-Kalkül, welcher sich durch die Verwendung von Kontexten innerhalb der Regeln deutlich von den anderen Kalkülen abhebt. Allerdings hält sich der Call-by-Need Lambda-Kalkül damit nicht an das in Kapitel 5 vorgestellte GDSOS-Format, das u.a. sicherstellt, dass Bisimulation eine Kongruenz ist. Wir haben dabei in Abschnitt 5.3.3 bewiesen, dass sich ein GDSOS-Reduktionssystem in ein äquivalentes strukturiertes Auswertungssystem nach Howe übersetzen lässt. Unser System ist in der Lage, die GDSOS-Bedingungen zu prüfen und gibt eine Warnung aus, falls eine der nötigen Bedingungen nicht erfüllt ist (wobei aus dieser auch gleich der Grund des Verstoßes hervorgeht). Wie wir gesehen haben, ist unser System nicht nur befähigt, die einzelnen Reduktionsschritte für kleinere Bespiele ordnungsgemäß auszuführen, sondern es ist durchaus in der Lage, auch aufwendigere KFP-Ausdrücke, wie in unserem Quicksort- Beispiel, auszuwerten.
A new approach to optimize multilevel logic circuits is introduced. Given a multilevel circuit, the synthesis method optimizes its area while simultaneously enhancing its random pattern testability. The method is based on structural transformations at the gate level. New transformations involving EX-OR gates as well as Reed–Muller expansions have been introduced in the synthesis of multilevel circuits. This method is augmented with transformations that specifically enhance random-pattern testability while reducing the area. Testability enhancement is an integral part of our synthesis methodology. Experimental results show that the proposed methodology not only can achieve lower area than other similar tools, but that it achieves better testability compared to available testability enhancement tools such as tstfx. Specifically for ISCAS-85 benchmark circuits, it was observed that EX-OR gate-based transformations successfully contributed toward generating smaller circuits compared to other state-of-the-art logic optimization tools.
Retiming is a widely investigated technique for performance optimization. It performs powerful modifications on a circuit netlist. However, often it is not clear, whether the predicted performance improvement will still be valid after placement has been performed. This paper presents a new retiming algorithm using a highly accurate timing model taking into account the effect of retiming on capacitive loads of single wires as well as fanout systems. We propose the integration of retiming into a timing-driven standard cell placement environment based on simulated annealing. Retiming is used as an optimization technique throughout the whole placement process. The experimental results show the benefit of the proposed approach. In comparison with the conventional design flow based on standard FEAS our approach achieved an improvement in cycle time of up to 34% and 17% on the average.
Retiming is a widely investigated technique for performance optimization. In general, it performs extensive modifications on a circuit netlist, leaving it unclear, whether the achieved performance improvement will still be valid after placement has been performed. This paper presents an approach for integrating retiming into a timing-driven placement environment. The experimental results show the benefit of the proposed approach on circuit performance in comparison with design flows using retiming only as a pre- or postplacement optimization method.
Channel routing is an NP-complete problem. Therefore, it is likely that there is no efficient algorithm solving this problem exactly.In this paper, we show that channel routing is a fixed-parameter tractable problem and that we can find a solution in linear time for a fixed channel width.We implemented our approach for the restricted layer model. The algorithm finds an optimal route for channels with up to 13 tracks within minutes or up to 11 tracks within seconds.Such narrow channels occur for example as a leaf problem of hierarchical routers or within standard cell generators.
We present a theoretical analysis of structural FSM traversal, which is the basis for the sequential equivalence checking algorithm Record & Play presented earlier. We compare the convergence behaviour of exact and approximative structural FSM traversal with that of standard BDD-based FSM traversal. We show that for most circuits encountered in practice exact structural FSM traversal reaches the fixed point as fast as symbolic FSM traversal, while approximation can significantly reduce in the number of iterations needed. Our experiments confirm these results.
We present the FPGA implementation of an algorithm [4] that computes implications between signal values in a boolean network. The research was performed as a masterrsquos thesis [5] at the University of Frankfurt. The recursive algorithm is rather complex for a hardware realization and therefore the FPGA implementation is an interesting example for the potential of reconfigurable computing beyond systolic algorithms. A circuit generator was written that transforms a boolean network into a network of small processing elements and a global control logic which together implement the algorithm. The resulting circuit performs the computation two orders of magnitudes faster than a software implementation run by a conventional workstation.
This paper presents a new timing driven approach for cell replication tailored to the practical needs of standard cell layout design. Cell replication methods have been studied extensively in the context of generic partitioning problems. However, until now it has remained unclear what practical benefit can be obtained from this concept in a realistic environment for timing driven layout synthesis. Therefore, this paper presents a timing driven cell replication procedure, demonstrates its incorporation into a standard cell placement and routing tool and examines its benefit on the final circuit performance in comparison with conventional gate or transistor sizing techniques. Furthermore, we demonstrate that cell replication can deteriorate the stuck-at fault testability of circuits and show that stuck-at redundancy elimination must be integrated into the placement procedure. Experimental results demonstrate the usefulness of the proposed methodology and suggest that cell replication should be an integral part of the physical design flow complementing traditional gate sizing techniques.
One of the most severe short-comings of currently available equivalence checkers is their inability to verify integer multipliers. In this paper, we present a bit level reverse-engineering technique that can be integrated into standard equivalence checking flows. We propose a Boolean mapping algorithm that extracts a network of half adders from the gate netlist of an addition circuit. Once the arithmetic bit level representation of the circuit is obtained, equivalence checking can be performed using simple arithmetic operations. Experimental results show the promise of our approach.