Symmetries in reversible programming: from symmetric rig groupoids to reversible programming languages

The Pi family of reversible programming languages for boolean circuits is presented as a syntax of combinators witnessing type isomorphisms of algebraic data types. In this paper, we give a denotational semantics for this language, using weak groupoids à la Homotopy Type Theory, and show how to derive an equational theory for it, presented by 2-combinators witnessing equivalences of type isomorphisms. We establish a correspondence between the syntactic groupoid of the language and a formally presented univalent subuniverse of finite types. The correspondence relates 1-combinators to 1-paths, and 2-combinators to 2-paths in the universe, which is shown to be sound and complete for both levels, forming an equivalence of groupoids. We use this to establish a Curry-Howard-Lambek correspondence between Reversible Logic, Reversible Programming Languages, and Symmetric Rig Groupoids, by showing that the syntax of Pi is presented by the free symmetric rig groupoid, given by finite sets and bijections. Using the formalisation of our results, we perform normalisation-by-evaluation, verification and synthesis of reversible logic gates, motivated by examples from quantum computing. We also show how to reason about and transfer theorems between different representations of reversible circuits.

Several results on compact metrizable spaces in $$\mathbf {ZF}$$

In the absence of the axiom of choice, the set-theoretic status of many natural statements about metrizable compact spaces is investigated. Some of the statements are provable in $$\mathbf {ZF}$$ ZF , some are shown to be independent of $$\mathbf {ZF}$$ ZF . For independence results, distinct models of $$\mathbf {ZF}$$ ZF and permutation models of $$\mathbf {ZFA}$$ ZFA with transfer theorems of Pincus are applied. New symmetric models of $$\mathbf {ZF}$$ ZF are constructed in each of which the power set of $$\mathbb {R}$$ R is well-orderable, the Continuum Hypothesis is satisfied but a denumerable family of non-empty finite sets can fail to have a choice function, and a compact metrizable space need not be embeddable into the Tychonoff cube $$[0, 1]^{\mathbb {R}}$$ [ 0 , 1 ] R .

Asymptotic Rational Approximation To Pi: Solution of an "Unsolved Problem'' Posed By Herbert Wilf

International audience The webpage of Herbert Wilf describes eight Unsolved Problems. Here, we completely resolve the third of these eight problems. The task seems innocent: find the first term of the asymptotic behavior of the coefficients of an ordinary generating function, whose coefficients naturally yield rational approximations to $\pi$. Upon closer examination, however, the analysis is fraught with difficulties. For instance, the function is the composition of three functions, but the innermost function has a non-zero constant term, so many standard techniques for analyzing function compositions will completely fail. Additionally, the signs of the coefficients are neither all positive, nor alternating in a regular manner. The generating function involves both a square root and an arctangent. The complex-valued square root and arctangent functions each rely on complex logarithms, which are multivalued and fundamentally depend on branch cuts. These multiple values and branch cuts make the function extremely tedious to visualize using Maple. We provide a complete asymptotic analysis of the coefficients of Wilf's generating function. The asymptotic expansion is naturally additive (not multiplicative); each term of the expansion contains oscillations, which we precisely characterize. The proofs rely on complex analysis, in particular, singularity analysis (which, in turn, rely on a Hankel contour and transfer theorems).