arXiv subjects

Chuangjie Xu

Publications and source records attributed to Chuangjie Xu.

13 recordsLinked to original sources

arXiv2026

Information Propagation and Contraction in Functional Interpretations

This paper separates two components of functional interpretations: affine information propagation and contraction. We introduce information nuclei as an algebraic interface to capture the affine component. An information nucleus specifies what information is associated with finite-type objects, how exact objects are compatible with such information, and how information is propagated through functions. From any information nucleus we obtain a formula translation and a soundness theorem for affine finite-type arithmetic. Extending soundness to finite-type arithmetic with contraction requires one additional ingredient: a formula-indexed contraction structure reducing the challenges generated by duplicated assumptions to a single challenge. Finite collections of candidates with union yield a Herbrand-style interpretation, while exact information with challenge selection yields the usual Dialectica interpretation over an arithmetic system restricted to decidable primitive formulas. The resulting framework provides a uniform method for specifying the information carried by extracted realizers, allowing existing functional interpretations to be systematically enriched with auxiliary data, such as continuity information.

cs.LO↗

arXiv2025

Constructive Ordinal Exponentiation

Cantor's ordinal numbers, a powerful extension of the natural numbers, are a cornerstone of set theory. They can be used to reason about the termination of processes, prove the consistency of logical systems, and justify some of the core principles of modern programming language theory such as recursion. In classical mathematics, ordinal arithmetic is well-studied; constructively, where ordinals are taken to be transitive, extensional, and wellfounded orders on sets, addition and multiplication are well-known. We present a negative result showing that general constructive ordinal exponentiation is impossible, but we suggest two definitions that come close. The first definition is abstract and solely motivated by the expected equations; this works as long as the base of the exponential is positive. The second definition is based on decreasing lists and can be seen as a constructive version of Sierpiński's definition via functions with finite support; this requires the base to have a trichotomous least element. Whenever it makes sense to ask the question, the two constructions are equivalent, allowing us to prove algebraic laws, cancellation properties, and preservation of decidability of the exponential. The core ideas do not depend on any specific constructive set theory or type theory, but a concrete computer-checked mechanization using the Agda proof assistant is given in homotopy type theory.

cs.LO↗

arXiv2023

Set-Theoretic and Type-Theoretic Ordinals Coincide

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.

cs.LO↗

arXiv2023

Type-Theoretic Approaches to Ordinals

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.

cs.LO↗

arXiv2022

Inferring Region Types via an Abstract Notion of Environment Transformation

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.

cs.PL↗

arXiv2021

Autofocusing Self-Imaging: The Symmetric Pearcey Talbot-like Effect

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.

physics.optics↗

arXiv2021

Type-based Enforcement of Infinitary Trace Properties for Java

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ă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üchi automata.

cs.LO↗

arXiv2021

Connecting Constructive Notions of Ordinals in Homotopy Type Theory

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.

cs.LO↗

arXiv2020

A Gentzen-style monadic translation of Gödel's System T

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.

cs.LO↗

arXiv2020

A syntactic approach to continuity of T-definable functionals

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ödel'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.

math.LO↗

arXiv2020

Circular symmetric Airy beam with the inverse propagation of the abruptly autofocusing Airy beam

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.

physics.optics↗

arXiv2020

Three Equivalent Ordinal Notation Systems in Cubical Agda

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.

math.LO↗

arXiv2019

On the Herbrand Functional Interpretation

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.

cs.LO↗