100 results on '"Robert Glück"'
Search Results
2. From reversible programming languages to reversible metalanguages
- Author
-
Robert Glück, Robin Kaarsgaard, and Tetsuo Yokoyama
- Subjects
General Computer Science ,Theoretical Computer Science - Published
- 2022
- Full Text
- View/download PDF
3. An Inversion Tool for Conditional Term Rewriting Systems - A Case Study of Ackermann Inversion
- Author
-
Maja Hanne Kirkeby, Maria Bendix Mikkelsen, and Robert Glück
- Subjects
FOS: Computer and information sciences ,Class (set theory) ,Computer Science - Programming Languages ,Computer science ,Program transformation ,Inverse ,Inversion (meteorology) ,Term (logic) ,Ackermann function ,Set (abstract data type) ,TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ,Computer Science::Logic in Computer Science ,Computer Science::Programming Languages ,Computer Science::Symbolic Computation ,Rewriting ,Algorithm ,Programming Languages (cs.PL) - Abstract
We report on an inversion tool for a class of oriented conditional constructor term rewriting systems. Four well-behaved rule inverters ranging from trivial to full, partial and semi-inverters are included. Conditional term rewriting systems are theoretically well founded and can model functional and non-functional rewrite relations. We illustrate the inversion by experiments with full and partial inversions of the Ackermann function. The case study demonstrates, among others, that polyvariant inversion and input-output set propagation can reduce the search space of the generated inverse systems., Comment: In Proceedings VPT 2021, arXiv:2109.02001
- Published
- 2021
- Full Text
- View/download PDF
4. Constructing a binary tree from its traversals by reversible recursion and iteration
- Author
-
Robert Glück and Tetsuo Yokoyama
- Subjects
Binary tree ,Computer science ,Preorder ,Recursion (computer science) ,Inverse ,Context (language use) ,0102 computer and information sciences ,02 engineering and technology ,01 natural sciences ,Inversion (discrete mathematics) ,Computer Science Applications ,Theoretical Computer Science ,010201 computation theory & mathematics ,Signal Processing ,0202 electrical engineering, electronic engineering, information engineering ,Reversible computing ,020201 artificial intelligence & image processing ,Algorithm ,Time complexity ,Information Systems - Abstract
We cast two algorithms to generate the inorder and preorder of the labels of a binary tree in the context of reversible computing nearly three decades after they were first examined in the light of program inversion. The reversible traversals directly define the inverse algorithms that reconstruct the binary tree and have the same linear time and space requirements as the traversals. A reversible while-language is extended with reversible recursion.
- Published
- 2019
- Full Text
- View/download PDF
5. Towards a Unified Language Architecture for Reversible Object-Oriented Programming
- Author
-
Lasse Hay-Schmidt, Robert Glück, Tue Haulund, and Martin Holm Cservenka
- Subjects
Object-oriented programming ,Parsing ,Interface (Java) ,Computer science ,Programming language ,Inverter ,Compiler ,Architecture ,computer.software_genre ,computer ,Interpreter - Abstract
A unified language architecture for an advanced reversible object-oriented language is described. The design and implementation choices made for a tree-walking interpreter and source-language inverter are discussed, as well as the integration with an existing monadic parser, type checker and PISA compiler backend. A demonstration of the web interface and the interactions required to interpret, compile and invert reversible object-oriented programs is given. Our aim is that this platform will make reversible programming approachable to a wider community.
- Published
- 2021
- Full Text
- View/download PDF
6. Inversion Framework: Reasoning about Inversion by Conditional Term Rewriting Systems
- Author
-
Maja Hanne Kirkeby and Robert Glück
- Subjects
Class (computer programming) ,Functional programming ,Correctness ,Theoretical computer science ,Orthogonality (programming) ,Computer science ,Property (programming) ,010102 general mathematics ,Program transformation ,0102 computer and information sciences ,01 natural sciences ,Inversion (linguistics) ,010201 computation theory & mathematics ,Rewriting ,0101 mathematics - Abstract
We introduce a language-independent framework for reasoning about program inverters by conditional term rewriting systems. These systems can model the three fundamental forms of inversion, i.e., full, partial and semi-inversion, in declarative languages. The correctness of the generic inversion algorithm introduced in this contribution is proven for all well-behaved rule inverters, and we demonstrate that this class of inverters encompasses several of the inversion algorithms published throughout the past years. This new generic approach enables us to establish fundamental properties, e.g., orthogonality, for entire classes of well-behaved full inverters, partial inverters and semi-inverters regardless of their particular local rule inverters. We study known inverters as well as classes of inverters that yield left-to-right deterministic systems; left-to-right determinism is a desirable property, e.g., for functional programs; however, at the same time it is not generally a property of inverted systems. This generic approach enables a more systematic design of program inverters and fills a gap in our knowledge of program inversion.
- Published
- 2020
- Full Text
- View/download PDF
7. Reversible Programs Have Reversible Semantics
- Author
-
Robin Kaarsgaard, Robert Glück, and Tetsuo Yokoyama
- Subjects
Inversion (linguistics) ,Development (topology) ,Recursion ,Programming language ,Computer science ,Semantics (computer science) ,Metalanguage ,Category of sets ,computer.software_genre ,Semantics ,computer ,Injective function - Abstract
During the past decade, reversible programming languages have been formalized using various established semantic frameworks. However, these semantics fail to effectively specify the distinct properties of reversible languages at the metalevel, and even neglect the central question of whether the defined language is reversible. In this paper, we build on a metalanguage foundation for reversible languages based on the category of sets and partial injective functions. We exemplify our approach through step-by-step development of the full semantics of an r-Turing complete reversible while-language with recursive procedures. This yields a formalization of the semantics in which the reversibility of the language and its inverse semantics are immediate, as well as the inversion of programs written in the language. We further discuss applications and future research directions for reversible semantics.
- Published
- 2020
- Full Text
- View/download PDF
8. Reversible Languages and Incremental State Saving in Optimistic Parallel Discrete Event Simulation
- Author
-
Robert Glück, Markus Schordan, Michael Kirkedal Thomsen, and Tomas Oppelstrup
- Subjects
Basis (linear algebra) ,Computer science ,Benchmark (computing) ,Node (circuits) ,Parallel computing ,State (computer science) ,Benchmarking ,Discrete event simulation ,Massively parallel ,Rollback - Abstract
Optimistic parallel discrete event simulation (PDES) requires to do a distributed rollback if conflicts are detected during a simulation due to the massively parallel optimistic execution approach. When a rollback of a simulation is performed each node that is determined to be in a wrong state must be restored to one of its previous states. This can be achieved through reverse computation or by restoring a previous checkpoint. In this paper we investigate and compare both approaches, reverse computation and a variant of checkpointing, incremental state saving (also called incremental checkpointing), to restore a previous program state as part of an optimistic parallel discrete event simulation. We present a benchmark model that is specifically designed for evaluating the performance of approaches to reversibility in PDES. Our benchmarking model has mathematical properties that allow to tune the amount of arithmetic operations relative to the amount of memory operations. These tuning opportunities are the basis for our systematic performance evaluation.
- Published
- 2020
- Full Text
- View/download PDF
9. An Experiment Combining Specialization with Abstract Interpretation
- Author
-
John P. Gallagher and Robert Glück
- Subjects
Computer Science - Symbolic Computation ,FOS: Computer and information sciences ,Computer Science - Logic in Computer Science ,Computer Science - Programming Languages ,Computer science ,Programming language ,business.industry ,Modular design ,Symbolic Computation (cs.SC) ,Abstract interpretation ,computer.software_genre ,Partial evaluation ,Domain (software engineering) ,Logic in Computer Science (cs.LO) ,Specialization (logic) ,Feature (machine learning) ,business ,computer ,Interpreter ,Abstraction (linguistics) ,Programming Languages (cs.PL) - Abstract
It was previously shown that control-flow refinement can be achieved by a program specializer incorporating property-based abstraction, to improve termination and complexity analysis tools. We now show that this purpose-built specializer can be reconstructed in a more modular way, and that the previous results can be achieved using an off-the-shelf partial evaluation tool, applied to an abstract interpreter. The key feature of the abstract interpreter is the abstract domain, which is the product of the property-based abstract domain with the concrete domain. This language-independent framework provides a practical approach to implementing a variety of powerful specializers, and contributes to a stream of research on using interpreters and specialization to achieve program transformations., Comment: In Proceedings VPT/HCVS 2020, arXiv:2008.02483
- Published
- 2020
- Full Text
- View/download PDF
10. Foundations of Reversible Computation
- Author
-
Iain Phillips, Martin Kutrib, Claudio Antares Mezzina, Lukasz Mikulski, Germán Vidal, Bogdan Aman, Robin Kaarsgaard, Jarkko Kari, R. Nagarajan, Gabriel Ciobanu, Ivan Lanese, G. M. Pinna, Irek Ulidowski, Luca Prigioniero, Robert Glück, Ulidowski, I, Lanese, I, Schultz, UP, Ferreira, C, Romanian Academy, Alexandru Ioan Cuza University of Iași [Romania], University of Copenhagen = Københavns Universitet (UCPH), University of Turku, Justus-Liebig-Universität Gießen = Justus Liebig University (JLU), Foundations of Component-based Ubiquitous Systems (FOCUS), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Dipartimento di Informatica - Scienza e Ingegneria [Bologna] (DISI), Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO)-Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO), Alma Mater Studiorum University of Bologna (UNIBO), Università degli Studi di Urbino 'Carlo Bo', Nicolaus Copernicus University [Toruń], Middlesex University [London], Imperial College London, Università degli Studi di Cagliari = University of Cagliari (UniCa), Università degli Studi di Milano = University of Milan (UNIMI), University of Leicester, Universitat Politècnica de València (UPV), European Project: COST Action IC1405,COST - European Cooperation in Science and Technology,IC1405(2015), University of Copenhagen = Københavns Universitet (KU), Justus-Liebig-Universität Gießen (JLU), Universita degli Studi di Cagliari [Cagliari], Università degli Studi di Milano [Milano] (UNIMI), Irek Ulidowski, Ivan Lanese, Ulrik Pagh Schultz, Carla Ferreira, Aman B., Ciobanu G., Gluck R., Kaarsgaard R., Kari J., Kutrib M., Lanese I., Mezzina C.A., Mikulski L., Nagarajan R., Phillips I., Pinna G.M., Prigioniero L., Ulidowski I., and Vidal G.
- Subjects
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] ,Theoretical computer science ,Computer science ,business.industry ,Computation ,media_common.quotation_subject ,Computability ,Multiple applications ,020207 software engineering ,Robotics ,0102 computer and information sciences ,02 engineering and technology ,Formal methods ,01 natural sciences ,Reversible computing, Foundations, Formal methods ,[INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL] ,Debugging ,010201 computation theory & mathematics ,0202 electrical engineering, electronic engineering, information engineering ,Reversible computing ,Artificial Intelligence & Image Processing ,Cost action ,Artificial intelligence ,business ,media_common - Abstract
International audience; Reversible computation allows computation to proceed not only in the standard, forward direction, but also backward, recovering past states. While reversible computation has attracted interest for its multiple applications, covering areas as different as low-power computing , simulation, robotics and debugging, such applications need to be supported by a clear understanding of the foundations of reversible computation. We report below on many threads of research in the area of foundations of reversible computing, giving particular emphasis to the results obtained in the framework of the European COST Action IC1405, entitled "Reversible Computation-Extending Horizons of Computing", which took place in the years 2015-2019.
- Published
- 2020
- Full Text
- View/download PDF
11. Semi-inversion of Conditional Constructor Term Rewriting Systems
- Author
-
Robert Glück and Maja Hanne Kirkeby
- Subjects
050101 languages & linguistics ,Functional programming ,Computer science ,Programming language ,Heuristic ,05 social sciences ,Program transformation ,02 engineering and technology ,Term (logic) ,computer.software_genre ,Prolog ,Inversion (linguistics) ,0202 electrical engineering, electronic engineering, information engineering ,Programming paradigm ,Computer Science::Programming Languages ,020201 artificial intelligence & image processing ,0501 psychology and cognitive sciences ,Rewriting ,computer ,computer.programming_language - Abstract
Inversion is an important and useful program transformation and has been studied in various programming language paradigms. Semi-inversion is more general than just swapping the input and output of a program; instead, parts of the input and output can be freely swapped. In this paper, we present a polyvariant semi-inversion algorithm for conditional constructor term rewriting systems. These systems can model logic and functional languages, which have the advantage that semi-inversion, as well as partial and full inversion, can be studied across different programming paradigms. The semi-inverter makes use of local inversion and a simple but effective heuristic and is proven to be correct. A Prolog implementation is applied to several problems, including inversion of a simple encrypter and of a program inverter for a reversible language.
- Published
- 2020
- Full Text
- View/download PDF
12. An Efficient Composition of Bidirectional Programs by Memoization and Lazy Update
- Author
-
Zhenjiang Hu, Robert Glück, Bach Nguyen Trong, and Kanae Tsushima
- Subjects
Correctness ,Memoization ,Semantics (computer science) ,Computer science ,020207 software engineering ,02 engineering and technology ,Parallel computing ,Reuse ,0202 electrical engineering, electronic engineering, information engineering ,Overhead (computing) ,Table (database) ,020201 artificial intelligence & image processing ,Lazy evaluation ,Associative property - Abstract
Bidirectional transformations (BX) are a solution to the view update problem and widely used for synchronizing data. The semantics and correctness of bidirectional programs have been investigated intensively during the past years, but their efficiency and optimization are not yet fully understood. In this paper, as a first step, we study different evaluation methods to optimize their evaluation. We focus on the interpretive evaluation of BX compositions because we found that these compositions are an important cause of redundant computations if the compositions are not right associative. For evaluating BX compositions efficiently, we investigate two memoization methods. The first method, minBiGUL\(_m\), uses memoization, which improves the runtime of many BX programs by keeping intermediate results for later reuse. A disadvantage is the familiar tradeoff for keeping and searching values in a table. When inputs become large, the overhead increases and the effectiveness decreases. To deal with large inputs, we introduce the second method, xpg, that uses tupling, lazy update and lazy evaluation as optimizations. Lazy updates delay updates in closures and enables them to use them later. Both evaluation methods were fully implemented for minBiGUL. The experimental results show that our methods are faster than the original method of BiGUL for the non-right associative compositions.
- Published
- 2020
- Full Text
- View/download PDF
13. An Experiment in Ping-Pong Protocol Verification by Nondeterministic Pushdown Automata
- Author
-
Robert Glück
- Subjects
FOS: Computer and information sciences ,Computer Science - Logic in Computer Science ,TheoryofComputation_COMPUTATIONBYABSTRACTDEVICES ,Theoretical computer science ,Formal Languages and Automata Theory (cs.FL) ,Computer science ,Computer Science - Formal Languages and Automata Theory ,Dyck language ,lcsh:QA75.5-76.95 ,Regular language ,Computer Science::Logic in Computer Science ,D.1 ,D.3.4 ,F.1.1 ,F.1.2 ,Protocol (object-oriented programming) ,Computer Science::Cryptography and Security ,Computer Science - Programming Languages ,Intersection (set theory) ,lcsh:Mathematics ,Pushdown automaton ,Cryptographic protocol ,lcsh:QA1-939 ,Logic in Computer Science (cs.LO) ,Nondeterministic algorithm ,TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ,Automata theory ,lcsh:Electronic computers. Computer science ,Computer Science::Formal Languages and Automata Theory ,Programming Languages (cs.PL) - Abstract
An experiment is described that confirms the security of a well-studied class of cryptographic protocols (Dolev-Yao intruder model) can be verified by two-way nondeterministic pushdown automata (2NPDA). A nondeterministic pushdown program checks whether the intersection of a regular language (the protocol to verify) and a given Dyck language containing all canceling words is empty. If it is not, an intruder can reveal secret messages sent between trusted users. The verification is guaranteed to terminate in cubic time at most on a 2NPDA-simulator. The interpretive approach used in this experiment simplifies the verification, by separating the nondeterministic pushdown logic and program control, and makes it more predictable. We describe the interpretive approach and the known transformational solutions, and show they share interesting features. Also noteworthy is how abstract results from automata theory can solve practical problems by programming language means., In Proceedings MARS/VPT 2018, arXiv:1803.08668
- Published
- 2018
- Full Text
- View/download PDF
14. Join inverse categories and reversible recursion
- Author
-
Robert Glück, Holger Bock Axelsen, and Robin Kaarsgaard
- Subjects
Discrete mathematics ,Functional programming ,Recursion ,Logic ,010102 general mathematics ,Structure (category theory) ,0102 computer and information sciences ,01 natural sciences ,Mutual recursion ,Theoretical Computer Science ,Algebra ,Morphism ,Computational Theory and Mathematics ,010201 computation theory & mathematics ,Countable set ,Reversible computing ,0101 mathematics ,Categorical variable ,Software ,Mathematics - Abstract
Recently, a number of reversible functional programming languages have been proposed. Common to several of these is the assumption of totality, a property that is not necessarily desirable, and certainly not required in order to guarantee reversibility. In a categorical setting, however, faithfully capturing partiality requires handling it as additional structure. Recently, Giles studied inverse categories as a model of partial reversible (functional) programming. In this paper, we show how additionally assuming the existence of countable joins on such inverse categories leads to a number of properties that are desirable when modeling reversible functional programming, notably morphism schemes for reversible recursion, a †-trace, and algebraic ω -compactness. This gives a categorical account of reversible recursion, and, for the latter, provides an answer to the problem posed by Giles regarding the formulation of recursive data types at the inverse category level.
- Published
- 2017
- Full Text
- View/download PDF
15. A Minimalist's Reversible While Language
- Author
-
Tetsuo Yokoyama and Robert Glück
- Subjects
Programming language ,Computer science ,020207 software engineering ,0102 computer and information sciences ,02 engineering and technology ,computer.software_genre ,01 natural sciences ,010201 computation theory & mathematics ,Artificial Intelligence ,Hardware and Architecture ,0202 electrical engineering, electronic engineering, information engineering ,Computer Vision and Pattern Recognition ,Electrical and Electronic Engineering ,computer ,Software - Published
- 2017
- Full Text
- View/download PDF
16. Fundamentals of reversible flowchart languages
- Author
-
Holger Bock Axelsen, Tetsuo Yokoyama, and Robert Glück
- Subjects
Theoretical computer science ,General Computer Science ,Semantics (computer science) ,Computer science ,0102 computer and information sciences ,02 engineering and technology ,computer.software_genre ,01 natural sciences ,Theoretical Computer Science ,law.invention ,Turing machine ,symbols.namesake ,Control flow ,Computable function ,law ,0202 electrical engineering, electronic engineering, information engineering ,Reversible computing ,Flowchart ,Syntax (programming languages) ,Programming language ,020207 software engineering ,Structured programming ,TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ,010201 computation theory & mathematics ,symbols ,computer - Abstract
This paper presents the fundamentals of reversible flowcharts. Reversible flowcharts are intended to naturally represent the structure and control flow of reversible (imperative) programming languages in a simple computation model in the same way classical flowcharts do for conventional languages. Although reversible flowcharts are superficially similar to classical flowcharts, there are crucial differences: atomic steps are limited to locally invertible operations, and join points require an explicit orthogonalizing conditional expression.Despite these constraints, we show that reversible flowcharts are both expressive and robust: reversible flowcharts can simulate irreversible ones by adapting reversibilization techniques to the flowchart model. Thus, reversible flowcharts are r-Turing-complete, meaning that they can compute exactly all injective computable functions. Furthermore, structured reversible flowcharts are as expressive as unstructured ones, as shown by a reversible version of the classic Structured Program Theorem.We illustrate how reversible flowcharts can be concretized with two example programming languages, complete with syntax and semantics: a low-level unstructured language and a high-level structured language. We introduce concrete tools such as program inverters and translators for both languages, which follow the structure suggested by the flowchart model. To further illustrate the different concepts and tools brought together in this paper, we present two major worked examples: a reversible permutation-to-code algorithm attributed to Dijkstra, and a simulation scheme for reversible Turing machines. By exhibiting a wide range of uses, we hope that the proposed reversible flowcharts can serve as a springboard for further theoretical research in reversible computing. Structured and unstructured reversible flowcharts are introduced and explored.They are shown to be equivalent and as expressive as reversible Turing machines (RTMs).Programming languages modeled on the flowchart variants are designed and formalized.Program inversion and translation between these languages is given in full.The results are demonstrated on Dijkstra's permutation encoding and RTM simulation.
- Published
- 2016
- Full Text
- View/download PDF
17. Data Structures and Dynamic Memory Management in Reversible Languages
- Author
-
Martin Holm Cservenka, Robert Glück, Torben Ægidius Mogensen, and Tue Haulund
- Subjects
Assembly language ,Computer science ,Programming language ,020207 software engineering ,02 engineering and technology ,computer.software_genre ,Data structure ,Dynamic memory management ,020204 information systems ,0202 electrical engineering, electronic engineering, information engineering ,Compiler ,computer ,Queue ,Heap (data structure) ,computer.programming_language - Abstract
We present a method for reversible dynamic memory management based on a reversible version of the Buddy Memory system. This method supports decoupled allocation and deallocation of variable-sized records and can be applied to any reversible language with heap storage. We demonstrate how these new capabilities allow for the direct realization of commonplace data structures such as trees, heaps and queues which until now has not been practical in a reversible language. Finally, we provide a definition of our method in the high-level reversible language Janus as well as a description of its fragmentation and garbage-generation characteristics. The reversible memory management system has been fully implemented and tested in a compiler for a reversible object-oriented programming language targeting the reversible assembly language PISA.
- Published
- 2018
- Full Text
- View/download PDF
18. Implementing Reversible Object-Oriented Language Features on Reversible Machines
- Author
-
Torben Ægidius Mogensen, Tue Haulund, and Robert Glück
- Subjects
060201 languages & linguistics ,Class (computer programming) ,Object-oriented programming ,Assembly language ,Computer science ,Programming language ,Dynamic dispatch ,06 humanities and the arts ,02 engineering and technology ,computer.software_genre ,Inheritance (object-oriented programming) ,0602 languages and literature ,0202 electrical engineering, electronic engineering, information engineering ,020201 artificial intelligence & image processing ,Virtual function ,Janus ,Compiler ,computer ,computer.programming_language - Abstract
We extend the reversible language Janus with support for class-based object-oriented programming, class inheritance and subtype-polymorphism. We describe how to implement these features on reversible hardware - with emphasis on the implementation of reversible dynamic dispatch using virtual method tables. Our translation is effective (i.e. garbage-free) and we demonstrate its practicality by implementation of a fully-featured compiler targeting the reversible assembly language PISA.
- Published
- 2017
- Full Text
- View/download PDF
19. Designing Garbage-Free Reversible Implementations of the Integer Cosine Transform
- Author
-
Tetsuo Yokoyama, Michael Kirkedal Thomsen, Torben Ægidius Mogensen, Eva Rotenberg, Alexis De Vos, Holger Bock Axelsen, Robert Glück, and Stéphane Burignat
- Subjects
Linear map ,Discrete mathematics ,Discrete sine transform ,Integer ,Hardware and Architecture ,Computer science ,Prime factor ,Discrete cosine transform ,Electrical and Electronic Engineering ,Software ,Injective function ,Prime (order theory) ,Fractional Fourier transform - Abstract
Discrete linear transformations are important tools in information processing. Many such transforms are injective and therefore prime candidates for a physically reversible implementation into hardware. We present here reversible integer cosine transformations on n input integers. The resulting reversible circuit is able to perform both the forward transform and the inverse transform. The detailed structure of such a reversible design strongly depends on the odd prime factors of the determinant of the transform: whether those are of the form 2 k ± 1 or of the form 2 k ± 2 l ± 1 or neither of these forms.
- Published
- 2014
- Full Text
- View/download PDF
20. Reversible Computing: Foundations and Software
- Author
-
Robert Glück and Tetsuo Yokoyama
- Subjects
Computer Networks and Communications ,Computer science ,business.industry ,02 engineering and technology ,Theoretical Computer Science ,Software ,Hardware and Architecture ,020204 information systems ,0202 electrical engineering, electronic engineering, information engineering ,Reversible computing ,020201 artificial intelligence & image processing ,Software engineering ,business - Published
- 2018
- Full Text
- View/download PDF
21. A Classical Propositional Logic for Reasoning About Reversible Logic Circuits
- Author
-
Robin Kaarsgaard, Holger Bock Axelsen, and Robert Glück
- Subjects
010302 applied physics ,Discrete mathematics ,Zeroth-order logic ,Well-formed formula ,Toffoli gate ,0102 computer and information sciences ,Intuitionistic logic ,Intermediate logic ,01 natural sciences ,Algebra ,Computer Science::Hardware Architecture ,TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ,Computer Science::Emerging Technologies ,010201 computation theory & mathematics ,Computer Science::Logic in Computer Science ,0103 physical sciences ,Reversible computing ,Dynamic logic (modal logic) ,Autoepistemic logic ,Hardware_LOGICDESIGN ,Mathematics - Abstract
We propose a syntactic representation of reversible logic circuits in their entirety, based on Feynman's control interpretation of Toffoli's reversible gate set. A pair of interacting proof calculi for reasoning about these circuits is presented, based on classical propositional logic and monoidal structure, and a natural order-theoretic structure is developed, demonstrated equivalent to Boolean algebras, and extended categorically to form a sound and complete semantics for this system. We show that all strong equivalences of reversible logic circuits are provable in the system, derive an equivalent equational theory, and describe its main applications in the verification of both reversible circuits and template-based reversible circuit rewriting systems.
- Published
- 2016
- Full Text
- View/download PDF
22. A Practical Simulation Result for Two-Way Pushdown Automata
- Author
-
Robert Glück
- Subjects
TheoryofComputation_COMPUTATIONBYABSTRACTDEVICES ,Theoretical computer science ,Nested word ,Deterministic context-free grammar ,Pushdown automaton ,020207 software engineering ,0102 computer and information sciences ,02 engineering and technology ,01 natural sciences ,Embedded pushdown automaton ,Automaton ,Deterministic pushdown automaton ,Nondeterministic algorithm ,TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ,010201 computation theory & mathematics ,Computer Science::Logic in Computer Science ,0202 electrical engineering, electronic engineering, information engineering ,Time complexity ,Algorithm ,Computer Science::Formal Languages and Automata Theory ,Mathematics - Abstract
The simulation of two-way deterministic and nondeterministic pushdown automata is revisited. A uniform algorithm presented herein decides on a random-access machine in linear time resp. cubic time whether a given pushdown automaton accepts a word, while the actual run of the automaton may take exponential time. The algorithm is practical since it only explores reachable configurations, simulates a class of quasi-deterministic decision problems in linear time even if the pushdown automaton is nondeterministic, and iterates over a simple work list. This is an improvement over previous simulation algorithms.
- Published
- 2016
- Full Text
- View/download PDF
23. Maximally-Polyvariant Partial Evaluation in Polynomial Time
- Author
-
Robert Glück
- Subjects
Polynomial ,Computer science ,String (computer science) ,020206 networking & telecommunications ,020207 software engineering ,02 engineering and technology ,Partial evaluation ,Matrix polynomial ,Stable polynomial ,Minimal polynomial (linear algebra) ,TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS ,Specialization (functional) ,0202 electrical engineering, electronic engineering, information engineering ,Computer Science::Programming Languages ,Time complexity ,Algorithm - Abstract
Maximally-polyvariant partial evaluation is a strategy for program specialization that propagates static values as accurate as possible. The online partial evaluator presented here achieves this precision in time polynomial in the number of partial-evaluation configurations. This is a significant improvement because a conventional partial evaluator can take exponential time, and no fast algorithm was known for maximally-polyvariant specialization. For an important class of quasi-deterministic specialization problems, our algorithm performs in linear time, even for linear-time specialization of a naive string matcher into a linear-time matcher, which was Futamura’s long-standing open challenge. Our results are presented using a recursive flowchart language.
- Published
- 2016
- Full Text
- View/download PDF
24. A self-applicable online partial evaluator for recursive flowchart languages
- Author
-
Robert Glück
- Subjects
Flowchart ,Meta-circular evaluator ,Recursion ,Theoretical computer science ,Computer science ,Programming language ,computer.software_genre ,Partial evaluation ,law.invention ,law ,Specialization (logic) ,Compiler ,computer ,Software ,Generator (mathematics) - Abstract
This paper describes a self-applicable online partial evaluator for a flowchart language with recursive calls. Self-application of the partial evaluator yields generating extensions that are as efficient as those reported in the literature for offline partial evaluation. This result is remarkable because it has been assumed that online partial evaluation techniques unavoidably lead to inefficient and overgeneralized generating extensions. The purpose of this paper is not to determine which kind of partial evaluation is better, but to show how the problem can be solved by recursive polyvariant specialization. The design of the self-applicable online partial evaluator is based on a number of known techniques, but by combining them in a new way this result can be produced. The partial evaluator, its techniques, and its implementation are presented in full. Self-application according to all three Futamura projections is demonstrated. The complete bootstrap of a compiler generator from a partial evaluator is also reported. Copyright © 2011 John Wiley & Sons, Ltd.
- Published
- 2011
- Full Text
- View/download PDF
25. Self-generating program specializers
- Author
-
Robert Glück
- Subjects
Computer science ,Programming language ,Bootstrapping ,Information processing ,computer.software_genre ,Partial evaluation ,Computer Science Applications ,Theoretical Computer Science ,Set (abstract data type) ,Signal Processing ,Projection (set theory) ,Algorithm ,computer ,Interpreter ,Information Systems - Abstract
This paper demonstrates the existence of self-generating program specializers and uses a language-independent projection to obtain them. The projection is considered from the viewpoint of the interpretive approach and a bootstrapping technique is identified by which a specializer can optimize its own implementation. A theorem is presented that equates the set of self-generating specializers and the set of specializers produced by the new projection. A practical consequence of the theorem is that an implementation of a specializer must contain an error if it is not possible to observe self-generation, which requires only a textual program comparison. Self-generation may thus provide a method for testing specializers and self-interpreters while they are under development.
- Published
- 2010
- Full Text
- View/download PDF
26. An investigation of Jones optimality and BTI-universal specializers
- Author
-
Robert Glück
- Subjects
Programming language ,business.industry ,Bootstrapping ,Computer science ,Computational intelligence ,computer.software_genre ,Symbolic computation ,Partial evaluation ,Computer Science Applications ,Specialization (logic) ,Artificial intelligence ,business ,computer ,Software - Abstract
Jones optimality implies that a program specializer is strong enough to remove an entire level of self-interpretation. This paper argues that Jones optimality, which was originally devised as a criterion for self-applicable specializers, plays a fundamental role in the use of a binding-time improvement prepass prior to specialization. We establish that, regardless of the binding-time improvements applied to a subject program (no matter how extensively), a specializer that is not Jones-optimal is strictly weaker than a specializer that is Jones-optimal. We describe the main approaches that increase the strength of a specializer without requiring its modification, namely incremental specialization and the interpretive approach, and show that they are equally powerful when the specializer is bti-universal. Since this includes the generation of program specializers from interpreters, the theoretical possibility of bootstrapping powerful specializers is established.
- Published
- 2008
- Full Text
- View/download PDF
27. Offline partial evaluation can be as accurate as online partial evaluation
- Author
-
Robert Glück and Niels H. Christensen
- Subjects
Flowchart ,Computer science ,Generalization ,business.industry ,Program specialization ,Machine learning ,computer.software_genre ,Partial evaluation ,law.invention ,Constant (computer programming) ,law ,TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS ,Binding time analysis ,Point (geometry) ,Artificial intelligence ,business ,computer ,Software - Abstract
We show that the accuracy of online partial evaluation, or polyvariant specialization based on constant propagation, can be simulated by offline partial evaluation using a maximally polyvariant binding-time analysis. We point out that, while their accuracy is the same, online partial evaluation offers better opportunities for powerful generalization strategies. Our results are presented using a flowchart language with recursive procedures.
- Published
- 2004
- Full Text
- View/download PDF
28. The universal resolving algorithm and its correctness: inverse computation in a functional language
- Author
-
Sergei M. Abramov and Robert Glück
- Subjects
Functional programming ,Correctness ,Theoretical computer science ,Computer science ,Pattern matcher ,Computation ,Process (computing) ,Inverse ,computer.software_genre ,Tree (data structure) ,Computer Science::Programming Languages ,Algorithm ,computer ,Software ,Interpreter - Abstract
We present an algorithm for inverse computation in a first-order functional language based on the notion of a perfect process tree. The Universal Resolving Algorithm introduced in this paper is sound and complete, and computes each solution for which the given program terminates, in finite time. The algorithm has been implemented for TSG, a typed dialect of S-Graph, and shows some remarkable results for the inverse computation of functional programs such as a pattern matcher and an interpreter for imperative programs.
- Published
- 2002
- Full Text
- View/download PDF
29. Program transformation system based on generalized partial computation
- Author
-
Yoshihiko Futamura, Robert Glück, and Zenjiro Konishi
- Subjects
Theoretical computer science ,Computer Networks and Communications ,Computer science ,Astrophysics::High Energy Astrophysical Phenomena ,Computation ,Program transformation ,Astrophysics::Cosmology and Extragalactic Astrophysics ,Auxiliary function ,Program optimization ,Abstract data type ,Partial evaluation ,Theoretical Computer Science ,Automated theorem proving ,Hardware and Architecture ,Inference engine ,Algorithm ,Software - Abstract
Generalized Partial Computation (GPC) is a program transformation method utilizing partial information about input data, abstract data types of auxiliary functions and the logical structure of a source program. GPC uses both an inference engine such as a theorem prover and a classical partial evaluator to optimize programs. Therefore, GPC is more powerful than classical partial evaluators but harder to implement and control. We have implemented an experimental GPC system called WSDFU (Waseda Simplify-Distribute-Fold-Unfold). This paper demonstrates the power of the program transformation system as well as its theorem prover and discusses some future works.
- Published
- 2002
- Full Text
- View/download PDF
30. FROM STANDARD TO NON-STANDARD SEMANTICS BY SEMANTICS MODIFIERS
- Author
-
Robert Glück and Sergei M. Abramov
- Subjects
Computer science ,business.industry ,Programming language ,Program transformation ,computer.software_genre ,Type erasure ,Operational semantics ,Action semantics ,Denotational semantics ,Well-founded semantics ,Computational semantics ,Computer Science (miscellaneous) ,Artificial intelligence ,business ,computer ,Natural language processing ,Programming language theory - Abstract
An approach for systematically modifying the semantics of programming languages by semantics modifiers is described. Semantics modifiers are a class of programs that allow the development of general and reusable "semantics components". Language independence is achieved through the interpretive approach: an interpreter serves as a mediator between the new language and the language for which the non-standard semantics was implemented. Inverse computation, equivalence transformation and neighborhood analysis are shown to be semantics modifiers. Experiments with these modifiers show the computational feasibility of this approach. Seven modifier projections are given which allow the efficient implementation of non-standard interpreters and non-standard compilers by program specialization or other powerful program transformation methods.
- Published
- 2001
- Full Text
- View/download PDF
31. Inverse computation and the Universal Resolving Algorithm
- Author
-
Sergei M. Abramov and Robert Glück
- Subjects
Tree (data structure) ,Functional programming ,Multidisciplinary ,Theoretical computer science ,Computation ,Programming paradigm ,Reactive programming ,Inverse ,Fifth-generation programming language ,Programming domain ,Algorithm ,Mathematics - Abstract
We survey fundamental concepts for inverse programming and then present the Universal Resolving Algorithm, an algorithm for inverse computation in a first-order, functional programming language. We discuss the key concepts of the algorithm, including a three-step approach based on the notion of a perfect process tree, and demonstrate our implementation with several examples of inverse computation.
- Published
- 2001
- Full Text
- View/download PDF
32. Abstraction from constructors and functional constructors and their applications
- Author
-
Yoshihiko Futamura, Robert Glück, and Kazuhiko Kakehi
- Subjects
Functional programming ,Multidisciplinary ,Transformation (function) ,Programming language ,TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS ,Program transformation ,computer.software_genre ,Data structure ,computer ,Type constructor ,Associative property ,Abstraction (linguistics) ,Mathematics - Abstract
Structures using constructors are of ordinary use in functional programming to represent data structures of unbound size. Lack of associativity of constructors, however, hinders program analyses or efficient executions. This paper describes ideas of abstraction toward constructors, and similarly abstraction from constructing functions, which we call functional constructors. We demonstrate our ideas making program analyses easier and enable transformation to efficient execution.
- Published
- 2001
- Full Text
- View/download PDF
33. Automatic generation of very efficient programs by Generalized Partial Computation
- Author
-
Zen jiro Konishi, Yoshihiko Futamura, and Robert Glück
- Subjects
Multidisciplinary ,Theoretical computer science ,Astrophysics::High Energy Astrophysical Phenomena ,Computation ,Program transformation ,Astrophysics::Cosmology and Extragalactic Astrophysics ,Auxiliary function ,Program optimization ,Partial evaluation ,Power (physics) ,Automated theorem proving ,Inference engine ,Algorithm ,Mathematics - Abstract
Generalized Partial Computation (GPC) is a program transformation method utilizing partial information about input data, properties of auxiliary functions and the logical structure of a source program. GPC uses both an inference engine such as a theorem prover and a classical partial evaluator to optimize programs. Therefore, GPC is more powerful than classical partial evaluators but harder to implement and control. We have implemented an experimental GPC system called WSDFU (Waseda Simplify-Distribute-Fold-Unfold). This paper discusses the power of the program transformation system, its theorem prover and future works.
- Published
- 2001
- Full Text
- View/download PDF
34. Loop peeling based on quasi-invariance/induction variables
- Author
-
Yoshihiko Futamura, Robert Glück, and Litong Song
- Subjects
Loop fission ,Loop splitting ,Multidisciplinary ,Loop inversion ,Loop fusion ,Loop nest optimization ,Loop interchange ,Loop tiling ,Algorithm ,Loop dependence analysis ,Mathematics - Abstract
Loop optimization plays an important role in compiler optimization and program transformation. Many sophisticated techniques such as loop-invariance code motion have been developed. Loop peeling is a technique to assist parallelization of loops by unfolding loops a few times. This paper introduces a novel technique called loop peeling based on quasi-invariance/induction variables. It aims at finding a general and automatic method to derive how many times a given loop should be peeled. Our technique allows for a number of iterations before some variables assigned inside a given loop become invariance or induction variables. In this paper we define the notion of quasi-invariance/induction variables, present an algorithm for statically computing the optimal peeling length of a given loop. Our technique can increase the accuracy of program analyses, improve the effectiveness of loop peeling and is well-suited as supporting other optimization techniques in the context of supercomputers.
- Published
- 2001
- Full Text
- View/download PDF
35. Conjunctive partial deduction: foundations, control, algorithms, and experiments
- Author
-
Jesper Tranekjær Jørgensen, Danny De Schreye, Michael Leuschel, Morten Heine Sørensen, Robert Glück, and Bern Martens
- Subjects
supercompilation ,Theoretical computer science ,Correctness ,Partial evaluation ,Logic ,Semantics (computer science) ,Program specialisation and transformation ,interpreters ,Well-quasi orders ,computer.software_genre ,Logic programming ,unfold/fold ,Set (abstract data type) ,Prolog ,logic programming ,well-quasi orders ,partial evaluation ,Failure semantics ,partial deduction ,Mathematics ,computer.programming_language ,Supercompilation ,Programming language ,trees ,Extension (predicate logic) ,Unfold/fold ,program specialisation and transformation ,logic programs ,Partial deduction ,unfold fold transformation ,computer - Abstract
Partial deduction in the Lloyd-Shepherdson framework cannot achieve certain optimisations which are possible by unfold/fold transformations. We introduce conjunctive partial deduction, an extension of partial deduction accommodating such optimisations, e.g., tupling and deforestation, We first present a framework for conjunctive partial deduction, extending the Lloyd-Shepherdson framework by considering conjunctions of atoms (instead of individual atoms) for specialisation and renaming. Correctness results are given for the framework with respect to computed answer semantics, least Herbrand model semantics, and finite failure semantics, Maintaining the well-known distinction between local and global control, we describe a basic algorithm for conjunctive partial deduction, and refine it into a concrete algorithm for which we prove termination, The problem of finding suitable renamings which remove redundant arguments turns out to be important, so we give an independent technique for this. A fully automatic implementation has been undertaken, which always terminates, Differences between the abstract semantics and Prolog's left-to-right execution motivate deviations from the abstract technique in the actual implementation, which we discuss. The implementation has been tested on an extensive set of benchmarks which demonstrate that conjunctive partial deduction indeed pays off, surpassing conventional partial deduction on a range of small to medium-size programs, while remaining manageable in an automatic and terminating system. (C) 1999 Elsevier Science Inc. All rights reserved. ispartof: Journal of logic programming vol:41 issue:2 pages:231-277 status: published
- Published
- 1999
- Full Text
- View/download PDF
36. Ed and the Movies
- Author
-
Robert Glück
- Subjects
Cultural Studies ,Literature and Literary Theory - Abstract
(1999). Ed and the Movies. Harrington Gay Men's Fiction Quarterly: Vol. 1, No. 1, pp. 85-90.
- Published
- 1999
- Full Text
- View/download PDF
37. 1998 symposium on partial evaluation
- Author
-
Peter Thiemann, Robert Glück, and Olivier Danvy
- Subjects
Engineering drawing ,General Computer Science ,Computer science ,Partial evaluation ,Theoretical Computer Science - Published
- 1998
- Full Text
- View/download PDF
38. On the degeneration of program generators by program composition
- Author
-
Robert Glück and Andrei Klimov
- Subjects
Class (computer programming) ,Computer Networks and Communications ,Program specialization ,Programming language ,Computer science ,Program transformation ,Extension (predicate logic) ,computer.software_genre ,Partial evaluation ,Theoretical Computer Science ,Dual (category theory) ,Development (topology) ,Hardware and Architecture ,Composition (language) ,computer ,Software - Abstract
One of the main discoveries in the seventies was that the concept of a generating extension covers a very wide class of apparently different program generators. Program specialization, or partial evaluation, is powerful because it provides uniform techniques for the automatic implementation of generating extensions from ordinary programs. The Futamura projections stand as the cornerstone of the development of program specialization. This paper takes the idea of the Futamura projections further. Threedegeneration projections are formulated which tell us how to achieve the reverse goal by program composition, namely turning a generating extension into an ordinary program. The fact that program composition can invert the effect of program specialization shows that these projections are dual in a sense. The degeneration projections complete a missing link between programs and generating extensions and allow for novel applications of program transformation.
- Published
- 1998
- Full Text
- View/download PDF
39. A regeneration scheme for generating extensions
- Author
-
Andrei Klimov and Robert Glück
- Subjects
Scheme (programming language) ,Theoretical computer science ,business.industry ,Programming language ,Computer science ,Computation ,Dimension (graph theory) ,Computer programming ,Program transformation ,Extension (predicate logic) ,computer.software_genre ,Partial evaluation ,Computer Science Applications ,Theoretical Computer Science ,Transformation (function) ,Signal Processing ,business ,computer ,Information Systems ,computer.programming_language - Abstract
A regeneration scheme is presented which shows how to change the computation staging of a generating extension by a two-level metasystem structure using program specialization and program composition. From the results described in this paper we can see that program generation and program degeneration are two extremes of the same transformation dimension; this relates several well-known program transformations under a general scheme.
- Published
- 1997
- Full Text
- View/download PDF
40. [Untitled]
- Author
-
Robert Glück and Jesper Tranekjær Jørgensen
- Subjects
Scheme (programming language) ,Functional programming ,General Computer Science ,Computer science ,Programming language ,Computation ,Program transformation ,Computational intelligence ,computer.software_genre ,Partial evaluation ,Computer engineering ,Specialization (functional) ,computer ,computer.programming_language ,Generator (mathematics) - Abstract
Program specialization can divide a computation into several computation stages. This paper investigates the theoretical limitations and practical problems of standard specialization tools, presents multi-level specialization, and demonstrates that, in combination with the cogen approach, it is far more practical than previously supposed. The program generator which we designed and implemented for a higher-order functional language converts programs into very compact multi-level generating extensions that guarantee fast successive specialization. Experimental results show a remarkable reduction of generation time and generator size compared to previous attempts of multi-level specialization by self-application. Our approach to multi-level specialization seems well-suited for applications where generation time and program size are critical.
- Published
- 1997
- Full Text
- View/download PDF
41. Reversible Representation and Manipulation of Constructor Terms in the Heap
- Author
-
Holger Bock Axelsen and Robert Glück
- Subjects
Functional programming ,Binary tree ,Theoretical computer science ,Simple (abstract algebra) ,Computer science ,Programming language ,Algebraic data type ,Representation (mathematics) ,Data structure ,computer.software_genre ,Machine code ,computer ,Heap (data structure) - Abstract
We currently have limited understanding of how complex data (e.g. algebraic data types) can be represented and manipulated in reversible machine code, in particular without generating garbage. In this paper we present methods for representing and manipulating binary trees (constructor terms) in the heap of a reversible machine. We also give methods for enforcing the so-called first-match policy for a simplified version of the recent reversible functional language RFUN by Yokoyama et al., and simple methods to support let-calls via stack environments.
- Published
- 2013
- Full Text
- View/download PDF
42. Simulation of Two-Way Pushdown Automata Revisited
- Author
-
Robert Glück
- Subjects
FOS: Computer and information sciences ,TheoryofComputation_COMPUTATIONBYABSTRACTDEVICES ,Semantics (computer science) ,Memoization ,Computer science ,Formal Languages and Automata Theory (cs.FL) ,Computer Science - Formal Languages and Automata Theory ,computer.software_genre ,lcsh:QA75.5-76.95 ,Deterministic pushdown automaton ,D.3.4 ,F.1.1 ,Computer Science - Programming Languages ,Programming language ,lcsh:Mathematics ,Pushdown automaton ,lcsh:QA1-939 ,Automaton ,Nondeterministic algorithm ,TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ,Key (cryptography) ,Computer Science::Programming Languages ,lcsh:Electronic computers. Computer science ,computer ,Interpreter ,Computer Science::Formal Languages and Automata Theory ,Programming Languages (cs.PL) - Abstract
The linear-time simulation of 2-way deterministic pushdown automata (2DPDA) by the Cook and Jones constructions is revisited. Following the semantics-based approach by Jones, an interpreter is given which, when extended with random-access memory, performs a linear-time simulation of 2DPDA. The recursive interpreter works without the dump list of the original constructions, which makes Cook's insight into linear-time simulation of exponential-time automata more intuitive and the complexity argument clearer. The simulation is then extended to 2-way nondeterministic pushdown automata (2NPDA) to provide for a cubic-time recognition of context-free languages. The time required to run the final construction depends on the degree of nondeterminism. The key mechanism that enables the polynomial-time simulations is the sharing of computations by memoization., Comment: In Proceedings Festschrift for Dave Schmidt, arXiv:1309.4557
- Published
- 2013
- Full Text
- View/download PDF
43. A positive supercompiler
- Author
-
Robert Glück, Neil D. Jones, and Morten Heine Sørensen
- Subjects
Transformation (function) ,Computer science ,Generalization ,Computation ,Factor (programming language) ,Folding (DSP implementation) ,Deforestation (computer science) ,Rewriting ,computer ,Algorithm ,Software ,Partial evaluation ,computer.programming_language - Abstract
We introduce apositive supercompiler, a version of Turchin's supercompiler maintaining only positive information during transformation, and using folding without generalization. The positive supercompiler can also be regarded as a variant of Wadler's deforestation maintaining an increased amount of information. We compare our algorithm to deforestation and, in less detail, to partial evaluation, Turchin's supercompiler, Generalized Partial Computation (GPC), and partial deduction by classifying these transformers by the amount of information they maintain during transformation. This factor is significant, as a differentiating example reveals: positive supercompilation, Turchin's supercompiler, GPC and partial deduction can specialize a general pattern matcher with respect to a fixed pattern to obtain an efficient matcher very similar to the Knuth–Morris–Pratt algorithm. Deforestation and traditional partial evaluation achieve this effect only after a non-trivial hand rewriting of the general matcher.
- Published
- 1996
- Full Text
- View/download PDF
44. Metasystem transition schemes in computer science and mathematics
- Author
-
Robert Glück and Andrei Klimov
- Subjects
Philosophy ,Automated theorem proving ,Theoretical computer science ,Computer science ,Program specialization ,business.industry ,Computation ,Transition (fiction) ,Metasystem transition ,Artificial intelligence ,Special case ,business - Abstract
We analyze metasystem transitions which may be observed, or are intentionally used, in computer science and mathematics. Various metasystem structures are present in their activities of executing, creating and manipulating formal linguistic models. The crucial role in automating the creation and manipulation of linguistic models is played by metacomputation, that is, computation over formal models. The manipulation of languages is one of the most essential problems of linguistic modeling. In this paper we analyze different schemes for transforming language definitions by metasystem transition and metacomputation, and present an example of ultra‐metasystem transition. We show that self‐application of metacomputation, a special case of metasystem transition, plays a central role in linguistic modeling. These techniques may also be utilized for reducing hierarchies of mathematical definitions and for manipulating mathematical texts effectively. Finally, we discuss a direct approach to theorem proving using a...
- Published
- 1995
- Full Text
- View/download PDF
45. Fortran program specialization
- Author
-
Robert Zöchling, Paul Kleinrubatscher, Albert Kriegshaber, and Robert Glück
- Subjects
Computer science ,Fortran ,Program specialization ,Programming language ,Specialization (functional) ,Program transformation ,Parallel computing ,computer.software_genre ,Computer Graphics and Computer-Aided Design ,computer ,Software ,Partial evaluation ,computer.programming_language - Abstract
We have developed and implemented a partial evaluator for a subset of Fortran 77. A partial evaluator is a tool for program transformation which takes as input a general program and a part of its input, and produces as output a specialized program. The goal is efficiency: a specialized program often runs an order of magnitude faster than the general program. The partial evaluator is based on the off-line approach and uses a binding-time analysis prior to the specialization phase. The source language includes multi-dimensional arrays, procedures and functions, as well as global storage. The system is presented and experimental results are given.
- Published
- 1995
- Full Text
- View/download PDF
46. Cleaning Up: Garbage-Free Reversible Circuits by Design Languages
- Author
-
Holger Bock Axelsen, Michael Kirkedal Thomsen, and Robert Glück
- Subjects
Theoretical computer science ,Computer science ,Functional logic programming ,Programming language ,Hardware description language ,Second-generation programming language ,Ontology language ,computer.software_genre ,Formal language ,Reversible computing ,Fifth-generation programming language ,computer ,computer.programming_language ,Declarative programming - Abstract
Reversible logic is a computational model that ensure that no values are discarded or duplicated. This gives the connection to Landauer's principle if and only if the underlying circuits are garbage-free. This paper shows how to describe and implement garbage-free reversible logic circuits in an easy and concise way. We use two domain-specific languages that are designed to describe reversible logic at different levels and garbage-free methods to translate between these. This approach relies heavily on programming language technology that is known and used for conventional functional languages. Though the languages ensure reversibility of the logic descriptions, they are not guaranteed to be garbage-free. It is still an important task for the designer to find the correct embeddings.
- Published
- 2012
- Full Text
- View/download PDF
47. Minimizing Garbage Size by Generating Reversible Simulations
- Author
-
Tetsuo Yokoyama, Holger Bock Axelsen, and Robert Glück
- Subjects
Turing machine ,symbols.namesake ,Sorting algorithm ,Semantics (computer science) ,Computer science ,Computation ,Encoding (memory) ,symbols ,Sorting ,Garbage output ,Garbage ,Algorithm - Abstract
Reversible simulations can realize any irreversible computation on any r-Turing complete reversible computation model at the expense of additional garbage output. The problem of minimizing the garbage size is an important issue in reversible simulations. We discuss the notion of the minimal garbage size of reversible simulations. Then, we propose a three-stage reversible simulation for minimizing garbage size, the first stage generates specialized irreversible programs, the second translates them into reversible simulations, and the third performs reversible simulation using the generated reversible programs. Two case studies on sorting algorithms suggest that the proposed method generates solutions with minimal garbage size.
- Published
- 2012
- Full Text
- View/download PDF
48. Towards a Reversible Functional Language
- Author
-
Holger Bock Axelsen, Robert Glück, and Tetsuo Yokoyama
- Subjects
Functional programming ,Interpretation (logic) ,Theoretical computer science ,Computer science ,Programming language ,Semantics (computer science) ,Recursive descent parser ,computer.software_genre ,Inversion (linguistics) ,Operator (computer programming) ,Computer Science::Programming Languages ,Inverse function ,computer ,Interpreter - Abstract
We identify concepts of reversibility for a functional language by means of a set of semantic rules with specific properties. These properties include injectivity along with local backward determinism, an important operational property for an efficient reversible language. We define a concise reversible first-order functional language in which access to the backward semantics is provided to the programmer by inverse function calls. Reversibility guarantees that in this language a backward run (inverse interpretation) is as fast as the corresponding forward run itself. By adopting a symmetric first-match policy for case expressions, we can write overlapping patterns in case branches, as is customary in ordinary functional languages, and also in leaf expressions, unlike existing inverse interpreter methods, which enables concise programs. In patterns, the use of a duplication/equality operator also simplifies inverse computation and program inversion. We discuss the advantages of a reversible functional language using example programs, including run-length encoding. Program inversion is seen to be as lightweight as for imperative reversible languages and realized by recursive descent. Finally, we show that the proposed language is r-Turing complete.
- Published
- 2012
- Full Text
- View/download PDF
49. A Reversible Processor Architecture and Its Reversible Logic Design
- Author
-
Holger Bock Axelsen, Michael Kirkedal Thomsen, and Robert Glück
- Subjects
Instruction set ,Logic synthesis ,Gate count ,Computer architecture ,Computer science ,Reversible computing ,Compiler ,computer.software_genre ,Control logic ,computer ,Program counter ,Microarchitecture - Abstract
We describe the design of a purely reversible computing architecture, Bob, and its instruction set, BobISA. The special features of the design include a simple, yet expressive, locally-invertible instruction set, and fully reversible control logic and address calculation. We have designed an architecture with an ISA that is expressive enough to serve as the target for a compiler from a high-level structured reversible programming language. All-in-all, this paper demonstrates that the design of a complete reversible computing architecture is possible and can serve as the core of a programmable reversible computing system.
- Published
- 2012
- Full Text
- View/download PDF
50. On the generation of specializers
- Author
-
Robert Glück
- Subjects
Programming language ,Computer science ,computer.software_genre ,computer ,Software - Abstract
Self-applicable specializers have been used successfully to automate the generation of compilers. Specializers are often rather sophisticated, for which reason one would like to adapt and transform them with the aid of the computer. But how to automate this process? The answer to this question is given by three specializer projections. While the Futamura projections define the generation of compilers from interpreters, the specializer projections define the generation of specializers from interpreters. We discuss the potential applications of the specializer projections, and argue that their realization is a real touchstone for the effectiveness of the specialization principle. In particular, we discuss generic specializers, bootstrapping of subject languages and the generation of optimizing specializers from interpretive specifications. The Futamura projections are regarded as a special case of the specializer projections. Recent results confirm that the specializer projections can be performed in practice using partial evaluators.
- Published
- 1994
- Full Text
- View/download PDF
Catalog
Discovery Service for Jio Institute Digital Library
For full access to our library's resources, please sign in.