Search

Reversible computing is motivated by both pragmatic and foundational considerations arising from a variety of disciplines. We take a particular path through the development of reversible computation, emphasizing compositional reversible computation. We start from a historical perspective, by reviewing those approaches that developed reversible extensions of lambda-calculi, Turing machines, and communicating process calculi. These approaches share a common challenge: computations made reversible in this way do not naturally compose locally. We then turn our attention to computational models that eschew the detour via existing irreversible models. Building on an original analysis by Landauer, the insights of Bennett, Fredkin, and Toffoli introduced a fresh approach to reversible computing in which reversibility is elevated to the status of the main design principle. These initial models are expressed using low-level bit manipulations, however. Abstracting from the low-level of the Bennett-Fredkin-Toffoli models and pursuing more intrinsic, typed, and algebraic models, naturally leads to rig categories as the canonical model for compositional reversible programming. The categorical model reveals connections to type isomorphisms, symmetries, permutations, groups, and univalent universes. This, in turn, paves the way for extensions to reversible programming based on monads and arrows. These extensions are shown to recover conventional irreversible programming, a variety of reversible computational effects, and more interestingly both pure (measurement-free) and measurement-based quantum programming., Comment: 18 pages

We selected 29 medical imaging projects from 48 candidates, assessed 10 software qualities by answering 108 questions for each software project, and interviewed 8 of the 29 development teams. Based on the quantitative data, we ranked the MI software with the Analytic Hierarchy Process (AHP). The four top-ranked software products are 3D Slicer, ImageJ, Fiji, and OHIF Viewer. Generally, MI software is in a healthy state as shown by the following: we observed 88% of the documentation artifacts recommended by research software development guidelines, 100% of MI projects use version control tools, and developers appear to use the common quasi-agile research software development process. However, the current state of the practice deviates from the existing guidelines because of the rarity of some recommended artifacts, low usage of continuous integration (17% of the projects), low use of unit testing (about 50% of projects), and room for improvement with documentation (six of nine developers felt their documentation was not clear enough). From interviewing the developers, we identified five pain points and two qualities of potential concern: lack of development time, lack of funding, technology hurdles, ensuring correctness, usability, maintainability, and reproducibility. The interviewees proposed strategies to improve the state of the practice, to address the identified pain points, and to improve software quality. Combining their ideas with ours, we have the following list of recommendations: increase documentation, increase testing by enriching datasets, increase continuous integration usage, move to web applications, employ linters, use peer reviews, design for change, add assurance cases, and incorporate a "Generate All Things" approach., Comment: 73 pages, 14 figures, 12 tables

Rig groupoids provide a semantic model of \PiLang, a universal classical reversible programming language over finite types. We prove that extending rig groupoids with just two maps and three equations about them results in a model of quantum computing that is computationally universal and equationally sound and complete for a variety of gate sets. The first map corresponds to an $8^{\text{th}}$ root of the identity morphism on the unit $1$. The second map corresponds to a square root of the symmetry on $1+1$. As square roots are generally not unique and can sometimes even be trivial, the maps are constrained to satisfy a nondegeneracy axiom, which we relate to the Euler decomposition of the Hadamard gate. The semantic construction is turned into an extension of \PiLang, called \SPiLang, that is a computationally universal quantum programming language equipped with an equational theory that is sound and complete with respect to the Clifford gate set, the standard gate set of Clifford+T restricted to $\le 2$ qubits, and the computationally universal Gaussian Clifford+T gate set.

Free categorical constructions characterise quantum computing as the combination of two copies of a reversible classical model, glued by the complementarity equations of classical structures. This recipe effectively constructs a computationally universal quantum programming language from two copies of Pi, the internal language of rig groupoids. The construction consists of Hughes' arrows. Thus answer positively the question whether a computational effect exists that turns reversible classical computation into quantum computation: the quantum effect. Measurements can be added by layering a further effect on top. Our construction also enables some reasoning about quantum programs (with or without measurement) through a combination of classical reasoning and reasoning about complementarity., Comment: This version: fix some strange characters and missing 'inv' in two of the Frobenius laws

Current software development is often quite code-centric and aimed at short-term deliverables, due to various contextual forces (such as the need for new revenue streams from many individual buyers). We're interested in software where different forces drive the development. \textbf{Well understood domains} and \textbf{long-lived software} provide one such context. A crucial observation is that software artifacts that are currently handwritten contain considerable duplication. By using domain-specific languages and generative techniques, we can capture the contents of many of the artifacts of such software. Assuming an appropriate codification of domain knowledge, we find that the resulting de-duplicated sources are shorter and closer to the domain. Our prototype, Drasil, indicates improvements to traceability and change management. We're also hopeful that this could lead to long-term productivity improvements for software where these forces are at play., Comment: 12 pages, paper accepted at EVCS 2023

Quantum models of computation are widely believed to be more powerful than classical ones. Efforts center on proving that, for a given problem, quantum algorithms are more resource efficient than any classical one. All this, however, assumes a standard predictive paradigm of reasoning where, given initial conditions, the future holds the answer. How about bringing information from the future to the present and exploit it to one's advantage? This is a radical new approach for reasoning, so-called Retrodictive Computation, that benefits from the specific form of the computed functions. We demonstrate how to use tools of symbolic computation to realize retrodictive quantum computing at scale and exploit it to efficiently, and classically, solve instances of the quantum Deutsch-Jozsa, Bernstein-Vazirani, Simon, Grover, and Shor's algorithms.

This position paper argues that decisions on processes, tools, techniques and software artifacts (such as user manuals, unit tests, design documents and code) for scientific software development should be driven by science, not by personal preference. Decisions should not be based on anecdotal evidence, gut instinct or the path of least resistance. Moreover, decisions should vary depending on the users and the context. In most cases of interest, this means that a longer term view should be adopted. We need to use a scientific approach based on unambiguous definitions, empirical evidence, hypothesis testing and rigorous processes. By developing an understanding of where input hours are spent, what most contributes to user satisfaction, and how to leverage knowledge produced, we can determine what interventions have the greatest value relative to the invested effort. We will be able to recommend software production processes that justify their value because the long-term output benefits are high compared to the required input resources. A preliminary definition of productivity is presented, along with ideas on how to potentially measure this quality. We briefly explore the idea of improving productivity via an approach where all artifacts are generated from codified knowledge., Comment: 2 pages

To improve software development methods and tools for research software, we first need to understand the current state of the practice. Therefore, we have developed a methodology for assessing the state of the software development practices for a given research software domain. For each domain we wish to answer questions such as: i) What artifacts (documents, code, test cases, etc.) are present? ii) What tools are used? iii) What principles, process and methodologies are used? iv) What are the pain points for developers? v) What actions are used to improve qualities like maintainability and reproducibility? To answer these questions, our methodology prescribes the following steps: i) Identify the domain; ii) Identify a list of candidate software packages; iii) Filter the list to a length of about 30 packages; iv) Gather source code and documentation for each package; v) Collect repository related data on each software package, like number of stars, number of open issues, number of lines of code; vi) Fill in the measurement template (the template consists of 108 questions to assess 9 qualities (including the qualities of installability, usability and visibility)); vii) Interview developers (the interview consists of 20 questions and takes about an hour); viii) Rank the software using the Analytic Hierarchy Process (AHP); and, ix) Analyze the data to answer the questions posed above. A domain expert should be engaged throughout the process, to ensure that implicit information about the domain is properly represented and to assist with conducting an analysis of the commonalities and variabilities between the 30 selected packages. Using our methodology, spreadsheet templates and AHP tool, we estimate (based on our experience with using the process) the time to complete an assessment for a given domain at 173 person hours., Comment: 35 pages, 3 figures

The Agda Universal Algebra Library (agda-algebras) is a library of types and programs (theorems and proofs) we developed to formalize the foundations of universal algebra in dependent type theory using the Agda programming language and proof assistant. In this paper we draw on and explain many components of the agda-algebras library, which we extract into a single Agda module in order to present a self-contained formal and constructive proof of Birkhoff's HSP theorem in Martin-L\"of dependent type theory. In the course of our presentation, we highlight some of the more challenging aspects of formalizing the basic definitions and theorems of universal algebra in type theory. Nonetheless, we hope this paper and the agda-algebras library serve as further evidence in support of the claim that dependent type theory and the Agda language, despite the technical demands they place on the user, are accessible to working mathematicians (such as ourselves) who possess sufficient patience and resolve to formally verify their results with a proof assistant. Indeed, the agda-algebras library now includes a substantial collection of definitions, theorems, and proofs from universal algebra, illustrating the expressive power of inductive and dependent types for representing and reasoning about general algebraic and relational structures., Comment: This is the long (35 page) version of a paper submitted to TYPES 2021; the previous draft, [v2], was a comprehensive description of an old version of the Agda Universal Algebra Library (called UALib; ver. 1.0.0); the library was rewritten and renamed agda-algebras (ver. 2.0.0); this paper describes only a subset of the agda-algebras library that we used to prove Birkhoff's HSP theorem in Agda

We present a new conceptual definition of 'productivity' for sustainably developing research software. Existing definitions are flawed as they are short-term biased, thus devaluing long-term impact, which we consider to be the principal goal. Taking a long-term view of productivity helps fix that problem. We view the outputs of the development process as knowledge and user satisfaction. User satisfaction is used as a proxy for effective quality. The explicit emphasis on all knowledge produced, rather than just the operationalizable knowledge (code) implies that human-reusable knowledge, i.e. documentation, should also be greatly valued when producing research software., Comment: 9 pages, Collegeville Workshop on Scientific Software Whitepaper, 2020

A theorem prover without an extensive library is much less useful to its potential users. Algebra, the study of algebraic structures, is a core component of such libraries. Algebraic theories also are themselves structured, the study of which was started as Universal Algebra. Various constructions (homomorphism, term algebras, products, etc) and their properties are both universal and constructive. Thus they are ripe for being automated. Unfortunately, current practice still requires library builders to write these by hand. We first highlight specific redundancies in libraries of existing systems. Then we describe a framework for generating these derived concepts from theory definitions. We demonstrate the usefulness of this framework on a test library of 227 theories., Comment: Accepted at: Conference on Intelligent Computer Mathematics (CICM 2020)

The generality and pervasiness of category theory in modern mathematics makes it a frequent and useful target of formalization. It is however quite challenging to formalize, for a variety of reasons. Agda currently (i.e. in 2020) does not have a standard, working formalization of category theory. We document our work on solving this dilemma. The formalization revealed a number of potential design choices, and we present, motivate and explain the ones we picked. In particular, we find that alternative definitions or alternative proofs from those found in standard textbooks can be advantageous, as well as "fit" Agda's type theory more smoothly. Some definitions regarded as equivalent in standard textbooks turn out to make different "universe level" assumptions, with some being more polymorphic than others. We also pay close attention to engineering issues so that the library integrates well with Agda's own standard library, as well as being compatible with as many of supported type theories in Agda as possible.

In reversible computing, the management of space is subject to two broad classes of constraints. First, as with general-purpose computation, every allocation must be paired with a matching de-allocation. Second, space can only be safely de-allocated if its contents are restored to their initial value from allocation time. Generally speaking, the state of the art provides limited partial solutions that address the first constraint by imposing a stack discipline and by leaving the second constraint to programmers' assertions. We propose a novel approach based on the idea of fractional types. As a simple intuitive example, allocation of a new boolean value initialized to $\texttt{false}$ also creates a value $1/{\texttt{false}}$ that can be thought of as a garbage collection (GC) process specialized to reclaim, and only reclaim, storage containing the value $\texttt{false}$. This GC process is a first-class entity that can be manipulated, decomposed into smaller processes and combined with other GC processes. We formalize this idea in the context of a reversible language founded on type isomorphisms, prove its fundamental correctness properties, and illustrate its expressiveness using a wide variety of examples. The development is backed by a fully-formalized Agda implementation., Comment: For the agda formalization, see https://github.com/DreamLinuxer/FracAncilla

Mathematical software systems are becoming more and more important in pure and applied mathematics in order to deal with the complexity and scalability issues inherent in mathematics. In the last decades we have seen a cambric explosion of increasingly powerful but also diverging systems. To give researchers a guide to this space of systems, we devise a novel conceptualization of mathematical software that focuses on five aspects: inference covers formal logic and reasoning about mathematical statements via proofs and models, typically with strong emphasis on correctness; computation covers algorithms and software libraries for representing and manipulating mathematical objects, typically with strong emphasis on efficiency; concretization covers generating and maintaining collections of mathematical objects conforming to a certain pattern, typically with strong emphasis on complete enumeration; narration covers describing mathematical contexts and relations, typically with strong emphasis on human readability; finally, organization covers representing mathematical contexts and objects in machine-actionable formal languages, typically with strong emphasis on expressivity and system interoperability. Despite broad agreement that an ideal system would seamlessly integrate all these aspects, research has diversified into families of highly specialized systems focusing on a single aspect and possibly partially integrating others, each with their own communities, challenges, and successes. In this survey, we focus on the commonalities and differences of these systems from the perspective of a future multi-aspect system.

We present GOOL, a Generic Object-Oriented Language. It demonstrates that a language, with the right abstractions, can capture the essence of object-oriented programs. We show how GOOL programs can be used to generate human-readable, documented and idiomatic source code in multiple languages. Moreover, in GOOL, it is possible to express common programming idioms and patterns, from simple library-level functions, to simple tasks (command-line arguments, list processing, printing), to more complex patterns, such as methods with a mixture of input, output and in-out parameters, and finally Design Patterns (such as Observer, State and Strategy). GOOL is an embedded DSL in Haskell that can generate code in Python, Java, C# and C++., Comment: Long version of paper at PEPM 2020

Over the last decades, a class of important mathematical results have required an ever increasing amount of human effort to carry out. For some, the help of computers is now indispensable. We analyze the implications of this trend towards "big mathematics", its relation to human cognition, and how machine support for big math can be organized. The central contribution of this position paper is an information model for "doing mathematics", which posits that humans very efficiently integrate four aspects: inference, computation, tabulation, and narration around a well-organized core of mathematical knowledge. The challenge for mathematical software systems is that these four aspects need to be integrated as well. We briefly survey the state of the art.

Many interesting and useful symbolic computation algorithms manipulate mathematical expressions in mathematically meaningful ways. Although these algorithms are commonplace in computer algebra systems, they can be surprisingly difficult to specify in a formal logic since they involve an interplay of syntax and semantics. In this paper we discuss several examples of syntax-based mathematical algorithms, and we show how to specify them in a formal logic with undefinedness, quotation, and evaluation., Comment: 16 pages

To build a large library of mathematics, it seems more efficient to take advantage of the inherent structure of mathematical theories. Various theory presentation combinators have been proposed, and some have been implemented, in both legacy and current systems. Surprisingly, the ``standard library'' of most systems do not make pervasive use of these combinators. We present a set of combinators optimized for reuse, via the tiny theories approach. Our combinators draw their power from the inherent structure already present in the \emph{category of contexts} associated to a dependently typed language. The current work builds on ideas originating in CLEAR and Specware and their descendents (both direct and intellectual). Driven by some design criteria for user-centric library design, our library-building experience via the systematic use of combinators has fed back into the semantics of these combinators, and later into an updated syntax for them., Comment: Extended version of paper with a similar title at CICM 2012, also listed as arXiv:1204.0053. Submitted to a journal. Almost the entire article has been rewritten

Our main models of computation (the Turing Machine and the RAM) make fundamental assumptions about which primitive operations are realizable. The consensus is that these include logical operations like conjunction, disjunction and negation, as well as reading and writing to memory locations. This perspective conforms to a macro-level view of physics and indeed these operations are realizable using macro-level devices involving thousands of electrons. This point of view is however incompatible with quantum mechanics, or even elementary thermodynamics, as both imply that information is a conserved quantity of physical processes, and hence of primitive computational operations. Our aim is to re-develop foundational computational models that embraces the principle of conservation of information. We first define what conservation of information means in a computational setting. We emphasize that computations must be reversible transformations on data. One can think of data as modeled using topological spaces and programs as modeled by reversible deformations. We illustrate this idea using three notions of data. The first assumes unstructured finite data, i.e., discrete topological spaces. The corresponding notion of reversible computation is that of permutations. We then consider a structured notion of data based on the Curry-Howard correspondence; here reversible deformations, as a programming language for witnessing type isomorphisms, comes from proof terms for commutative semirings. We then "move up a level" to treat programs as data. The corresponding notion of reversible programs equivalences comes from the "higher dimensional" analog to commutative semirings: symmetric rig groupoids. The coherence laws for these are exactly the program equivalences we seek. We conclude with some generalizations inspired by homotopy type theory and survey directions for further research.

Probabilistic programming languages are valuable because they allow domain experts to express probabilistic models and inference algorithms without worrying about irrelevant details. However, for decades there remained an important and popular class of probabilistic inference algorithms whose efficient implementation required manual low-level coding that is tedious and error-prone. They are algorithms whose idiomatic expression requires random array variables that are latent or whose likelihood is conjugate. Although that is how practitioners communicate and compose these algorithms on paper, executing such expressions requires eliminating the latent variables and recognizing the conjugacy by symbolic mathematics. Moreover, matching the performance of handwritten code requires speeding up loops by more than a constant factor. We show how probabilistic programs that directly and concisely express these desired inference algorithms can be compiled while maintaining efficiency. We introduce new transformations that turn high-level probabilistic programs with arrays into pure loop code. We then make great use of domain-specific invariants and norms to optimize the code, and to specialize and JIT-compile the code per execution. The resulting performance is competitive with manual implementations., Comment: Final version

A biform theory is a combination of an axiomatic theory and an algorithmic theory that supports the integration of reasoning and computation. These are ideal for specifying and reasoning about algorithms that manipulate mathematical expressions. However, formalizing biform theories is challenging since it requires the means to express statements about the interplay of what these algorithms do and what their actions mean mathematically. This paper describes a project to develop a methodology for expressing, manipulating, managing, and generating mathematical knowledge as a network of biform theories. It is a subproject of MathScheme, a long-term project at McMaster University to produce a framework for integrating formal deduction and symbolic computation., Comment: 11 pages

Different communities rely heavily on software, but use quite different software development practices. {\bf Objective}: We wanted to measure the state of the practice in the area of statistical software for psychology to understand how it compares to best practices. {\bf Method}: We compared and ranked 30 software tools with respect to adherence to best software engineering practices on items that could be measured by end-users. {\bf Results} We found that R packages use quite good practices, that while commercial packages were quite usable, many aspects of their development is too opaque to be measures, and that research projects vary a lot in their practices. {\bf Conclusion} We recommend that more organizations adopt practices similar to those used by CRAN to facilitate success, even for small teams. We also recommend close coupling of source code and documentation, to improve verifiability., Comment: 23 pages + 10 pages of appendices, 11 figures

We present a reproducible method to analyze the state of software development practices in a given scientific domain and apply this method to Geographic Information Systems (GIS). The analysis is based on grading a set of 30 GIS products using a template of 56 questions based on 13 software qualities. The products range in scope and purpose from a complete desktop GIS systems, to stand-alone tools, to programming libraries/packages. The final ranking of the products is determined using the Analytic Hierarchy Process (AHP), a multicriteria decision making method that focuses on relative comparisons between products, rather than directly measuring qualities. The results reveal concerns regarding the correctness, maintainability, transparency and reproducibility of some GIS software. Three recommendations are presented as feedback to the GIS community: 1) Ensure each project has a requirements specification document, 2) Provide a wealth of support methods, such as an IRC (Internet Relay Chat) channel, a Stack Exchange tag for new questions, or opening the issue tracker for support requests, as well as the more traditional email-based methods, and, 3) Design product websites for maximum transparency (of the development process), for open source projects, provide a developer's guide.

We are interested in algorithms that manipulate mathematical expressions in mathematically meaningful ways. Expressions are syntactic, but most logics do not allow one to discuss syntax. ${\rm CTT}_{\rm qe}$ is a version of Church's type theory that includes quotation and evaluation operators, akin to quote and eval in the Lisp programming language. Since the HOL logic is also a version of Church's type theory, we decided to add quotation and evaluation to HOL Light to demonstrate the implementability of ${\rm CTT}_{\rm qe}$ and the benefits of having quotation and evaluation in a proof assistant. The resulting system is called HOL Light QE. Here we document the design of HOL Light QE and the challenges that needed to be overcome. The resulting implementation is freely available., Comment: 20 pages. arXiv admin note: text overlap with arXiv:1612.02785

We establish a close connection between a reversible programming language based on type isomorphisms and a formally presented univalent universe. The correspondence relates combinators witnessing type isomorphisms in the programming language to paths in the univalent universe; and combinator optimizations in the programming language to 2-paths in the univalent universe. The result suggests a simple computational interpretation of paths and of univalence in terms of familiar programming constructs whenever the universe in question is computable.

A biform theory is a combination of an axiomatic theory and an algorithmic theory that supports the integration of reasoning and computation. These are ideal for formalizing algorithms that manipulate mathematical expressions. A theory graph is a network of theories connected by meaning-preserving theory morphisms that map the formulas of one theory to the formulas of another theory. Theory graphs are in turn well suited for formalizing mathematical knowledge at the most convenient level of abstraction using the most convenient vocabulary. We are interested in the problem of whether a body of mathematical knowledge can be effectively formalized as a theory graph of biform theories. As a test case, we look at the graph of theories encoding natural number arithmetic. We used two different formalisms to do this, which we describe and compare. The first is realized in ${\rm CTT}_{\rm uqe}$, a version of Church's type theory with quotation and evaluation, and the second is realized in Agda, a dependently typed programming language., Comment: 43 pages; published without appendices in: H. Geuvers et al., eds, Intelligent Computer Mathematics (CICM 2017), Lecture Notes in Computer Science, Vol. 10383, pp. 9-24, Springer, 2017

Since there are different ways of axiomatizing and developing a mathematical theory, knowledge about a such a theory may reside in many places and in many forms within a library of formalized mathematics. We introduce the notion of a realm as a structure for consolidating knowledge about a mathematical theory. A realm contains several axiomatizations of a theory that are separately developed. Views interconnect these developments and establish that the axiomatizations are equivalent in the sense of being mutually interpretable. A realm also contains an external interface that is convenient for users of the library who want to apply the concepts and facts of the theory without delving into the details of how the concepts and facts were developed. We illustrate the utility of realms through a series of examples. We also give an outline of the mechanisms that are needed to create and maintain realms., Comment: As accepted for CICM 2014

We motivate and give semantics to theory presentation combinators as the foundational building blocks for a scalable library of theories. The key observation is that the category of contexts and fibered categories are the ideal theoretical tools for this purpose., Comment: Extended version of paper to appear in proceedings of CICM 2012

Video game development is currently a very labour-intensive endeavour. Furthermore it involves multi-disciplinary teams of artistic content creators and programmers, whose typical working patterns are not easily meshed. SAGA is our first effort at augmenting the productivity of such teams. Already convinced of the benefits of DSLs, we set out to analyze the domains present in games in order to find out which would be most amenable to the DSL approach. Based on previous work, we thus sought those sub-parts that already had a partially established vocabulary and at the same time could be well modeled using classical computer science structures. We settled on the 'story' aspect of video games as the best candidate domain, which can be modeled using state transition systems. As we are working with a specific company as the ultimate customer for this work, an additional requirement was that our DSL should produce code that can be used within a pre-existing framework. We developed a full system (SAGA) comprised of a parser for a human-friendly language for 'story events', an internal representation of design patterns for implementing object-oriented state-transitions systems, an instantiator for these patterns for a specific 'story', and three renderers (for C++, C# and Java) for the instantiated abstract code., Comment: In Proceedings DSL 2011, arXiv:1109.0323

We present some of the experiments we have performed to best test our design for a library for MathScheme, the mechanized mathematics software system we are building. We wish for our library design to use and reflect, as much as possible, the mathematical structure present in the objects which populate the library., Comment: Accepted as a work-in-progress paper at CICM 2011

Decomposing the domain of a function into parts has many uses in mathematics. A domain may naturally be a union of pieces, a function may be defined by cases, or different boundary conditions may hold on different regions. For any particular problem the domain can be given explicitly, but when dealing with a family of problems given in terms of symbolic parameters, matters become more difficult. This article shows how hybrid sets, that is multisets allowing negative multiplicity, may be used to express symbolic domain decompositions in an efficient, elegant and uniform way, simplifying both computation and reasoning. We apply this theory to the arithmetic of piecewise functions and symbolic matrices and show how certain operations may be reduced from exponential to linear complexity., Comment: Calculemus 2010 (17th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning), part of Conferences on Intelligent Computer Mathematics 2010. 17 pages.

We observe that the vocabulary used to construct the "answer" to problems in computer algebra can have a dramatic effect on the computational complexity of solving that problem. We recall a formalization of this observation and explain the classic example of sparse polynomial arithmetic. For this case, we show that it is possible to extend the vocabulary so as reap the benefits of conciseness whilst avoiding the obvious pitfall of repeating the problem statement as the "solution". It is possible to extend the vocabulary either by irreducible cyclotomics or by $x^n-1$: we look at the options and suggest that the pragmatist might opt for both., Comment: 7 pages. Submitted to ISSAC 2010

We define a canonical form for piecewise defined functions. We show that this has a wider range of application as well as better complexity properties than previous work., Comment: submitted to ISSAC 2007