Search

In constructive set theory, an ordinal is a hereditarily transitive set. In homotopy type theory (HoTT), an ordinal is a type with a transitive, wellfounded, and extensional binary relation. We show that the two definitions are equivalent if we use (the HoTT refinement of) Aczel's interpretation of constructive set theory into type theory. Following this, we generalize the notion of a type-theoretic ordinal to capture all sets in Aczel's interpretation rather than only the ordinals. This leads to a natural class of ordered structures which contains the type-theoretic ordinals and realizes the higher inductive interpretation of set theory. All our results are formalized in Agda., Comment: v2: Minor changes. To appear at LICS'23. v3: Acknowledgments updated

Region-based type systems are a powerful tool for various kinds of program analysis. We introduce a new inference algorithm for region types based on an abstract notion of environment transformation. It analyzes the code of a method only once, even when there are multiple invocations of the method of different region types in the program. Elements of such an abstract transformation are essentially constraints for equality and subtyping that capture flow information of the program. In particular, we work with access graphs in the definition of abstract transformations to guarantee the termination of the inference algorithm, because they provide a finite representation of field access paths., Comment: To appear at APLAS'22; arXiv version contains appendices on the construction of concatenation and join for abstract transformations and an example of type inference

In a constructive setting, no concrete formulation of ordinal numbers can simultaneously have all the properties one might be interested in; for example, being able to calculate limits of sequences is constructively incompatible with deciding extensional equality. Using homotopy type theory as the foundational setting, we develop an abstract framework for ordinal theory and establish a collection of desirable properties and constructions. We then study and compare three concrete implementations of ordinals in homotopy type theory: first, a notation system based on Cantor normal forms (binary trees); second, a refined version of Brouwer trees (infinitely-branching trees); and third, extensional well-founded orders. Each of our three formulations has the central properties expected of ordinals, such as being equipped with an extensional and well-founded ordering as well as allowing basic arithmetic operations, but they differ with respect to what they make possible in addition. For example, for finite collections of ordinals, Cantor normal forms have decidable properties, but suprema of infinite collections cannot be computed. In contrast, extensional well-founded orders work well with infinite collections, but almost all properties are undecidable. Brouwer trees take the sweet spot in the middle by combining a restricted form of decidability with the ability to work with infinite increasing sequences. Our three approaches are connected by canonical order-preserving functions from the "more decidable" to the "less decidable" notions. We have formalised the results on Cantor normal forms and Brouwer trees in cubical Agda, while extensional well-founded orders have been studied and formalised thoroughly by Escardo and his collaborators. Finally, we compare the computational efficiency of our implementations with the results reported by Berger., Comment: Improves, expands on, and reuses material from our previous short conference paper "Connecting Constructive Notions of Ordinals in Homotopy Type Theory", arXiv:2104.02549. v3: Thm 73 and Rem 74 corrected

The Talbot like effect of symmetric Pearcey beams (SPBs) is presented numerically and experimentally in the free space. Owing to the Talbot like effect, the SPBs have the property of periodic and multiple autofocusing. Meanwhile, the focal positions and focal times of SPBs are controlled by the beam shift factor and the distribution factors. What is more, the beam shift factor can also affect the Talbot-like effect and the Talbot period. Therefore, several tiny optical bottles can be generated under the appropriate parameter setting. It is believed that the results can diversify the application of the Talbot effect., Comment: 11 pages, 6 figures

A common approach to improve software quality is to use programming guidelines to avoid common kinds of errors. In this paper, we consider the problem of enforcing guidelines for Featherweight Java (FJ). We formalize guidelines as sets of finite or infinite execution traces and develop a region-based type and effect system for FJ that can enforce such guidelines. We build on the work by Erbatur, Hofmann and Z\u{a}linescu, who presented a type system for verifying the finite event traces of terminating FJ programs. We refine this type system, separating region typing from FJ typing, and use ideas of Hofmann and Chen to extend it to capture also infinite traces produced by non-terminating programs. Our type and effect system can express properties of both finite and infinite traces and can compute information about the possible infinite traces of FJ programs. Specifically, the set of infinite traces of a method is constructed as the greatest fixed point of the operator which calculates the possible traces of method bodies. Our type inference algorithm is realized by working with the finitary abstraction of the system based on B\"uchi automata., Comment: main part (14 pages) published at PPDP'21; arXiv version contains an appendix on the FJ operational semantics and the extension to support exception handling (15 pages total)

In classical set theory, there are many equivalent ways to introduce ordinals. In a constructive setting, however, the different notions split apart, with different advantages and disadvantages for each. We consider three different notions of ordinals in homotopy type theory, and show how they relate to each other: A notation system based on Cantor normal forms, a refined notion of Brouwer trees (inductively generated by zero, successor and countable limits), and wellfounded extensional orders. For Cantor normal forms, most properties are decidable, whereas for wellfounded extensional transitive orders, most are undecidable. Formulations for Brouwer trees are usually partially decidable. We demonstrate that all three notions have properties expected of ordinals: their order relations, although defined differently in each case, are all extensional and wellfounded, and the usual arithmetic operations can be defined in each case. We connect these notions by constructing structure preserving embeddings of Cantor normal forms into Brouwer trees, and of these in turn into wellfounded extensional orders. We have formalised most of our results in cubical Agda., Comment: main part (16 pages) published at MFCS'21; arXiv version contains an appendix with proofs (27 pages total)

In this letter, we introduce a new class of light beam, the circular symmetric Airy beam (CSAB), which arises from the extensions of the one dimensional (1D) spectrum of Airy beam from rectangular coordinates to cylindrical ones. The CSAB propagates at initial stages with a single central lobe that autofocuses and then defocuses into the multi-rings structure. Then, these multi-rings perform the outward accelerations during the propagation. That means the CSAB has the inverse propagation of the abruptly autofocusing Airy beam. Besides, the propagation features of the circular symmetric Airy vortex beam (CSAVB) also have been investigated in detail. Our results offer a complementary tool with respect to the abruptly autofocusing Airy beam for practical applications., Comment: 4pages,8figures

We show that the types of the witnesses in the Herbrand functional interpretation can be simplified, avoiding the use of "sets of functionals" in the interpretation of implication and universal quantification. This is done by presenting an alternative formulation of the Herbrand functional interpretation, which we show to be equivalent to the original presentation. As a result of this investigation we also strengthen the monotonicity property of the original presentation, and prove a monotonicity property for our alternative definition., Comment: 9 pages

We introduce a syntactic translation of Goedel's System T parametrized by a weak notion of a monad, and prove a corresponding fundamental theorem of logical relation. Our translation structurally corresponds to Gentzen's negative translation of classical logic. By instantiating the monad and the logical relation, we reveal the well-known properties and structures of T-definable functionals including majorizability, continuity and bar recursion. Our development has been formalized in the Agda proof assistant., Comment: 17 pages. Changes: (1) remove the restriction of satisfying the monad laws in the definition of nuclei, (2) add a unified theorem of logical relation. This paper will appear in FSCD 2020

We present three ordinal notation systems representing ordinals below $\varepsilon_0$ in type theory, using recent type-theoretical innovations such as mutual inductive-inductive definitions and higher inductive types. We show how ordinal arithmetic can be developed for these systems, and how they admit a transfinite induction principle. We prove that all three notation systems are equivalent, so that we can transport results between them using the univalence principle. All our constructions have been implemented in cubical Agda., Comment: 14 pages, to appear at CPP 2020

We give a new proof of the well-known fact that all functions $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$ which are definable in G\"odel's System T are continuous via a syntactic approach. Differing from the usual syntactic method, we firstly perform a translation of System T into itself in which natural numbers are translated to functions $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$. Then we inductively define a continuity predicate on the translated elements and show that the translation of any term in System T satisfies the continuity predicate. We obtain the desired result by relating terms and their translations via a parametrized logical relation. Our constructions and proofs have been formalized in the Agda proof assistant. Because Agda is also a programming language, we can execute our proof to compute moduli of continuity of T-definable functions.