arXiv subjects
Publications and source records attributed to David Richter.
We find explicit ridge unfoldings of the three exceptional 4D polytopes (24-cell, 120-cell, 600-cell) that result in overlaps of their facets. These failures bring an end to the full classification of regular polytopes with the all-net property.
With growing complexity, distributed software systems become increasingly challenging to maintain and reason about. When implementing a distributed protocol, developers must ensure manually that the different components fit together. Choreographic programming addresses this challenge by specifying global protocols in a single program and projecting them into communicating processes, so-called endpoints. Recent choreographic approaches are designed as programming libraries that embed this paradigm into a host language like Haskell or Rust. In these designs, we observe common cases of partiality: unreachable branches in endpoint projection (EPP) and located-value access can trigger runtime errors or undefined behavior, relying on manual discipline of library maintainers rather than being statically type-checked. Also, some programs require users to write down dummy branches that should not be reachable, for example when branching on sum types. To close this gap, we use the dependently typed Lean programming language to implement a similar choreographic library. We show how we are able to move from a partial EPP to a total EPP function, and also eliminate cases of partiality in user-written code with pattern matching on sum types. ChorLean ensures total EPP and safe value access via proof-carrying located values, passing Lean's totality checker without undefined cases, while supporting the same feature set as libraries like MultiChor.
Choreographic programming is a programming model for developing distributed applications where an entire communication protocol is written as a single program, which a compiler then projects to one process per participant. Choreographic programming abstracts over low-level network communication primitives such as sockets, and provides a high degree of safety guarantees with deadlock freedom ensured by construction. Mechanizing choreographies necessarily deals with both operations specific to distributed programming and standard (local) operations that also occur in non-distributed programs, as well as the typical issues of binding and substitution. We aim to sidestep the latter issues, thereby obtaining a more concise mechanization that focuses on the essential distributed aspects of choreographies. To this end, we use a method recently proposed by Thiemann to elegantly model deadlock-free processes in a dependently typed language: Using state transformers to represent the computations performed by each process. We bring the state transformer model to choreographies, allowing us to reduce the usual mechanization effort around binding and substitution, and to abstract over the details of the "local" aspects of the language. We mechanize in Lean a choreographic language that supports point-to-point communication, broadcasting, recursive procedures, and local stateful methods, allowing each participant to be assigned a different set of methods. We prove soundness and completeness of endpoint projection, establish deadlock freedom for the projected processes, prove confluence, and verify a Hoare logic for choreographies.
We revisit the role of higher-order unification in dependently typed languages and identify a fundamental limitation of existing pattern-based fragments: their inability to synthesize functions defined by case analysis. Even simple and ubiquitous constraints arising from type inference, particularly from use of induction principles, fall outside the expressive power of Miller patterns and their modern extensions. We observe that such constraints naturally correspond to definitions by dependent pattern matching. Motivated by this correspondence, we propose integrating dependent pattern matching into the unification process. We present a prototype implementation of a small dependently typed language that collects delayed unification constraints and resolves them via a pattern matching compiler. Our approach successfully infers solutions that are rejected by current systems such as Rocq and Lean, suggesting a new direction for unification that unifies type inference and pattern matching compilation.
The energetic response of inertial particles to turbulent flow motions is important for both a fundamental understanding of the multi-phase dynamics at play, and for applications such as reduced-order models of particle dispersion processes, and their two-way coupled effects onto the flow phase. Numerous studies focus on the energetics of ensembles of particles in homogeneous isotropic turbulence, where the influence of flow anisotropy (such as that provided by boundary conditions, or other external forcing) is not considered a priori. In this work, we investigate the role of flow anisotropy on the Eulerian scale-wise particle phase energetics in a turbulent wall bounded flow for settling inertial Lagrangian particles. By using coupled Eulerian-Lagrangian direct numerical simulations at moderate Reynolds number, we aim to unravel the complex dependency of the scale-wise particle energetics on the turbulence intensity, particle inertia, and particle settling. In particular, we focus on how the developing anisotropy of the underlying turbulent flow (derived from the presence of the wall) is donated to the particle phase, and how particle inertia and settling preserve this large scale anisotropy into the formally isotropic scale range of the flow. We derive an exact (but unclosed) conservation law for the particle phase energetics at arbitrary scale, and use an asymptotic argument to help elucidate our DNS data. We discuss the relative changes to the quasi-streamwise and vertical components of the fluctuating particle field, and finish by discussing the implications of anisotropic non-local effects for more general flows, and the implications for continuum models of inertial settling Lagrangian particles.
Incrementalization speeds up computations by avoiding unnecessary recomputations and by efficiently reusing previous results. While domain-specific techniques achieve impressive speedups, e.g., in the context of database queries, they are difficult to generalize. Meanwhile, general approaches offer little support for incrementalizing domain-specific operations. In this work, we present DeCo, a novel core calculus for incremental functional programming with support for a wide range of user-defined data types. Despite its generic nature, our approach statically incrementalizes domain-specific operations on user-defined data types. It is, hence, more fine-grained than other generic techniques which resort to treating domain-specific operations as black boxes. We mechanized our work in Lean and proved it sound, meaning incrementalized execution computes the same result as full reevaluation. We also provide an executable implementation with case studies featuring examples from linear algebra, relational algebra, dictionaries, trees, and conflict-free replicated data types, plus a brief performance evaluation on linear and relational algebra and on trees.
Changes in aerosol concentrations can modify cloud brightness, producing a strong but poorly constrained influence on Earth's energy balance. Because cloud reflectivity depends on the size distribution of cloud droplets, and aerosol size strongly governs activation into droplets, one might expect cloud properties to be sensitive to aerosol size distributions. Here we show, through a combination of cloud chamber experiments and high-resolution simulations, that cloud microphysical and optical properties are often insensitive to aerosol size. Detectable impacts on cloud optical properties occur only under weak convective forcing and high aerosol concentrations. These results indicate that, in most conditions, cloud reflectivity can be predicted from aerosol number alone without detailed knowledge of aerosol size distributions, providing new constraints on how aerosol perturbations affect climate.
Neural-guided equation discovery systems use a data set as prompt and predict an equation that describes the data set without extensive search. However, if the equation does not meet the user's expectations, there are few options for getting other equation suggestions without intensive work with the system. To fill this gap, we propose Residuals for Equation Discovery (RED), a post-processing method that improves a given equation in a targeted manner, based on its residuals. By parsing the initial equation to a syntax tree, we can use node-based calculation rules to compute the residual for each subequation of the initial equation. It is then possible to use this residual as new target variable in the original data set and generate a new prompt. If, with the new prompt, the equation discovery system suggests a subequation better than the old subequation on a validation set, we replace the latter by the former. RED is usable with any equation discovery system, is fast to calculate, and is easy to extend for new mathematical operations. In experiments on 53 equations from the Feynman benchmark, we show that it not only helps to improve all tested neural-guided systems, but also all tested classical genetic programming systems.
Deep learning approaches are becoming increasingly attractive for equation discovery. We show the advantages and disadvantages of using neural-guided equation discovery by giving an overview of recent papers and the results of experiments using our modular equation discovery system MGMT ($\textbf{M}$ulti-Task $\textbf{G}$rammar-Guided $\textbf{M}$onte-Carlo $\textbf{T}$ree Search for Equation Discovery). The system uses neural-guided Monte-Carlo Tree Search (MCTS) and supports both supervised and reinforcement learning, with a search space defined by a context-free grammar. We summarize seven desirable properties of equation discovery systems, emphasizing the importance of embedding tabular data sets for such learning approaches. Using the modular structure of MGMT, we compare seven architectures (among them, RNNs, CNNs, and Transformers) for embedding tabular datasets on the auxiliary task of contrastive learning for tabular data sets on an equation discovery task. For almost all combinations of modules, supervised learning outperforms reinforcement learning. Moreover, our experiments indicate an advantage of using grammar rules as action space instead of tokens. Two adaptations of MCTS -- risk-seeking MCTS and AmEx-MCTS -- can improve equation discovery with that kind of search.
Developing reduced order models for the transport of solid particles in turbulence typically requires a statistical description of the particle-turbulence interactions. In this work, we utilize a statistical framework to derive continuum equations for the moments of the slip velocity of inertial settling Lagrangian particles in a turbulent boundary layer. Using coupled Eulerian-Lagrangian direct numerical simulations, we then identify the dominant mechanisms controlling the slip velocity variance, and find that for a range of St+, Sv+, and Re, the slip variance is primarily controlled by local differences between the "seen" variance and the particle velocity variance, while terms appearing due to the inhomogeneity of the turbulence are sub-leading until Sv+ becomes large. We also consider several comparative metrics to assess the relative magnitudes of the fluctuating slip velocity and the mean slip velocity, and we find that the vertical mean slip increases rapidly with Sv+, rendering the variance relatively small -- an effect found to be most substantial for Sv+>1. Finally, we compare the results to a model of the acceleration variance Berk and Coletti (2021) based the concept of a response function described in Csanady (1963), highlighting the role of the crossing trajectories mechanism. We find that while there is good agreement for low Sv+, systematic errors remain, possibly due to implicit non-local effects arising from rapid particle settling and inhomogeneous turbulence. We conclude with a discussion of the implications of this work for modeling the transport of coarse dust grains in the atmospheric surface layer.
Linear algebra computations are foundational for neural networks and machine learning, often handled through arrays. While many functional programming languages feature lists and recursion, arrays in linear algebra demand constant-time access and bulk operations. To bridge this gap, some languages represent arrays as (eager) functions instead of lists. In this paper, we connect this idea to a formal logical foundation by interpreting functions as the usual negative types from polarized type theory, and arrays as the corresponding dual positive version of the function type. Positive types are defined to have a single elimination form whose computational interpretation is pattern matching. Just like (positive) product types bind two variables during pattern matching, (positive) array types bind variables with multiplicity during pattern matching. We follow a similar approach for Booleans by introducing conditionally-defined variables. The positive formulation for the array type enables us to combine typed partial evaluation and common subexpression elimination into an elegant algorithm whose result enjoys a property we call maximal fission, which we argue can be beneficial for further optimizations. For this purpose, we present the novel intermediate representation indexed administrative normal form (AiNF), which relies on the formal logical foundation of the positive formulation for the array type to facilitate maximal loop fission and subsequent optimizations. AiNF is normal with regard to commuting conversion for both let-bindings and for-loops, leading to flat and maximally fissioned terms. We mechanize the translation and normalization from a simple surface language to AiNF, establishing that the process terminates, preserves types, and produces maximally fissioned terms.
A generic orthotope is an orthogonal polytope whose tangent cones are described by read-once Boolean functions. The purpose of this note is to develop a theory ofEhrhart polynomials for integral generic orthotopes. The most remarkable part of this theory is a relation between the number of lattice points in an integral generic orthotope $P$ and the number of unit cubes in $P$ of various floral types. This formula is facilitated through the introduction of a set of "local polynomials" defined for every read-once Boolean function.
Automatic Differentiation (AD) has become a dominant technique in ML. AD frameworks have first been implemented for imperative languages using tapes. Meanwhile, functional implementations of AD have been developed, often based on dual numbers, which are close to the formal specification of differentiation and hence easier to prove correct. But these papers have focussed on correctness not efficiency. Recently, it was shown how an approach using dual numbers could be made efficient through the right optimizations. Optimizations are highly dependent on order, as one optimization can enable another. It can therefore be useful to have fine-grained control over the scheduling of optimizations. One method expresses compiler optimizations as rewrite rules, whose application can be combined and controlled using strategy languages. Previous work describes the use of term rewriting and strategies to generate high-performance code in a compiler for a functional language. In this work, we implement dual numbers AD in a functional array programming language using rewrite rules and strategy combinators for optimization. We aim to combine the elegance of differentiation using dual numbers with a succinct expression of the optimization schedule using a strategy language. We give preliminary evidence suggesting the viability of the approach on a micro-benchmark.
Modeling sequential and parallel composition of effectful computations has been investigated in a variety of languages for a long time. In particular, the popular do-notation provides a lightweight effect embedding for any instance of a monad. Idiom bracket notation, on the other hand, provides an embedding for applicatives. First, while monads force effects to be executed sequentially, ignoring potential for parallelism, applicatives do not support sequential effects. Composing sequential with parallel effects remains an open problem. This is even more of an issue as real programs consist of a combination of both sequential and parallel segments. Second, common notations do not support invoking effects in direct-style, instead forcing a rigid structure upon the code. In this paper, we propose a mixed applicative/monadic notation that retains parallelism where possible, but allows sequentiality where necessary. We leverage a direct-style notation where sequentiality or parallelism is derived from the structure of the code. We provide a mechanisation of our effectful language in Coq and prove that our compilation approach retains the parallelism of the source program.
This article studies a large, general class of orthogonal polytopes which we may call "generic orthotopes". These objects emerged from a desire to represent a Coxeter complex by an orthogonal polytope that is particularly nice with respect to traditional topological, structural, or combinatorial considerations. Generic orthotopes have a pleasant "homogeneity" property, somewhat like a smoothly bounded compact subset of Euclidean space. Thus, as soon as we demand that every vertex of an orthogonal polytope be a floral arrangement, as defined here, many derivative structures such as faces and cross-sections are also described by floral arrangements. We also give formulas for the volume and Euler characteristic of a generic orthotope using a couple of statistics that are defined naturally for floral arrangements.
Decentralized applications (dApps) consist of smart contracts that run on blockchains and clients that model collaborating parties. dApps are used to model financial and legal business functionality. Today, contracts and clients are written as separate programs -- in different programming languages -- communicating via send and receive operations. This makes distributed program flow awkward to express and reason about, increasing the potential for mismatches in the client-contract interface, which can be exploited by malicious clients, potentially leading to huge financial losses. In this paper, we present Prisma, a language for tierless decentralized applications, where the contract and its clients are defined in one unit and pairs of send and receive actions that "belong together" are encapsulated into a single direct-style operation, which is executed differently by sending and receiving parties. This enables expressing distributed program flow via standard control flow and renders mismatching communication impossible. We prove formally that our compiler preserves program behavior in presence of an attacker controlling the client code. We systematically compare Prisma with mainstream and advanced programming models for dApps and provide empirical evidence for its expressiveness and performance.
Direct numerical simulations two-way coupled with inertial particles are used to investigate the particle distribution and two-way coupling effect of low-inertia ($St_{LSM}=0.0625$, $St_{VLSM}=0.009$) and high-inertia ($St_{LSM}=0.475$, $St_{VLSM}=0.069$) particles associated with the large-scale motions (LSMs) and very-large-scale motions (VLSMs) in an open channel flow at a Reynolds number of $Re_τ= 550$. One method of filtering the VLSMs from the flow is via artificial domain truncation, which alters the mean particle concentration profile and particle clustering due to the removal of VLSMs from a large domain simulation. In order to exclude possible correlation of the turbulence introduced by a small domain size with periodic boundary conditions, low- and high-pass filtering is performed during the simulation to isolate the particle interaction with different spatial scales. The results show that particle accumulation and turbophoresis are under-predicted without VLSMs, whereas the particle clustering and two-way coupling effects are mainly determined by particle coupling with LSMs. In the inner layer, the elongated streamwise anisotropic particle clustering can be reproduced by particles coupling solely with LSMs for low Stokes number ($St_{LSM}=0.0625$) particles. However, we do not observe similar particle clustering behavior in the outer layer as seen in the full simulation by coupling particles with either LSMs or VLSMs for high Stokes number ($St_{VLSM}=0.069$) particles. This indicates that the organized particle structures are formed by the joint action of LSMs and VLSMs, especially for high Stokes number particles in the outer layer.
Very large-scale motions (VLSMs) and large-scale motions (LSMs) coexist at moderate Reynolds numbers in a very long open channel flow. Direct numerical simulations two-way coupled with inertial particles are analysed using spectral information to investigate the modulation of VLSMs. In the wall-normal direction, particle distributions (mean/preferential concentration) exhibit two distinct behaviors in the inner flow and outer flow, corresponding to two highly anisotropic turbulent structures, LSMs and VLSMs. This results in particle inertia's non-monotonic effects on the VLSMs: low inertia (based on the inner scale) and high inertia (based on the outer scale) both strengthen the VLSMs whereas moderate and very high inertia have little influence. Through conditional tests, low and high inertia particles enhance VLSMs following two distinct routes. Low inertia particles promote VLSMs indirectly through the enhancement of the regeneration cycle (the self-sustaining mechanism of LSMs) in the inner region whereas high inertia particles enhance the VLSM directly through contribution to the Reynolds shear stress at similar temporal scales in the outer region. This understanding also provides more general insight into inner-outer interaction in high Reynolds number, wall-bounded flows.