-
Human Perception-Inspired Grain Segmentation Refinement Using Conditional Random Fields
Authors:
Doruk Aksoy,
Huolin L. Xin,
Timothy J. Rupert,
William J. Bowman
Abstract:
Accurate segmentation of interconnected line networks, such as grain boundaries in polycrystalline material microstructures, poses a significant challenge due to the fragmented masks produced by conventional computer vision algorithms, including convolutional neural networks. These algorithms struggle with thin masks, often necessitating intricate post-processing for effective contour closure and…
▽ More
Accurate segmentation of interconnected line networks, such as grain boundaries in polycrystalline material microstructures, poses a significant challenge due to the fragmented masks produced by conventional computer vision algorithms, including convolutional neural networks. These algorithms struggle with thin masks, often necessitating intricate post-processing for effective contour closure and continuity. Addressing this issue, this paper introduces a fast, high-fidelity post-processing technique, leveraging domain knowledge about grain boundary connectivity and employing conditional random fields and perceptual grou** rules. This approach significantly enhances segmentation mask accuracy, achieving a 79% segment identification accuracy in validation with a U-Net model on electron microscopy images of a polycrystalline oxide. Additionally, a novel grain alignment metric is introduced, showing a 51% improvement in grain alignment, providing a more detailed assessment of segmentation performance for complex microstructures. This method not only enables rapid and accurate segmentation but also facilitates an unprecedented level of data analysis, significantly improving the statistical representation of grain boundary networks, making it suitable for a range of disciplines where precise segmentation of interconnected line networks is essential.
△ Less
Submitted 15 December, 2023;
originally announced December 2023.
-
Schur Decomposition for Stiff Differential Equations
Authors:
Thoma Zoto,
John C. Bowman
Abstract:
A quantitative definition of numerical stiffness for initial value problems is proposed. Exponential integrators can effectively integrate linearly stiff systems, but they become expensive when the linear coefficient is a matrix, especially when the time step is adapted to maintain a prescribed local error. Schur decomposition is shown to avoid the need for computing matrix exponentials in such si…
▽ More
A quantitative definition of numerical stiffness for initial value problems is proposed. Exponential integrators can effectively integrate linearly stiff systems, but they become expensive when the linear coefficient is a matrix, especially when the time step is adapted to maintain a prescribed local error. Schur decomposition is shown to avoid the need for computing matrix exponentials in such simulations, while still circumventing linear stiffness.
△ Less
Submitted 21 May, 2023;
originally announced May 2023.
-
Elasticity Solver in Minecraft for Learning Mechanics of Materials by Gaming
Authors:
Zachariah P. Beck,
Brandon Alpert,
Alexander J. Bowman,
William R. Watson,
Adrian Buganza Tepole
Abstract:
Video games have emerged as a medium for learning by creating engaging environments, encouraging creative and deep thinking, and exposing learners to complex problems. Unfortunately, even though there are increasing examples of video games for many basic science and engineering concepts, similar efforts for higher level engineering concepts such as mechanics of materials are still lacking. Here we…
▽ More
Video games have emerged as a medium for learning by creating engaging environments, encouraging creative and deep thinking, and exposing learners to complex problems. Unfortunately, even though there are increasing examples of video games for many basic science and engineering concepts, similar efforts for higher level engineering concepts such as mechanics of materials are still lacking. Here we present a mesh-free elasticity solver implementation in the popular video game Minecraft, a sandbox game where players can build any structure they can imagine. Modifications to the game, called mods in the Minecraft community, are a common feature of this platform. Our elasticity mod computes the stress and deformation of arbitrary structures and colors the blocks with a heat-map to visualize the result of the analysis. We used this mod in the Honors section of two courses taught at Purdue University: Basic Mechanics I Statics, Mechanics of Materials. This articles describes our experience develo** and deploying this tool to encourage its use in biomedical engineering classrooms. A future goal is to engage the broader audience Minecraft players that already interact regularly with Minecraft mods.
△ Less
Submitted 14 December, 2022;
originally announced December 2022.
-
Mid-Air Helicopter Delivery at Mars Using a Jetpack
Authors:
Jeff Delaune,
Jacob Izraelevitz,
Samuel Sirlin,
David Sternberg,
Louis Giersch,
L. Phillipe Tosi,
Evgeniy Skliyanskiy,
Larry Young,
Michael Mischna,
Shannah Withrow-Maser,
Juergen Mueller,
Joshua Bowman,
Mark S Wallace,
Havard F. Grip,
Larry Matthies,
Wayne Johnson,
Matthew Keennon,
Benjamin Pipenberg,
Harsh Patel,
Christopher Lim,
Aaron Schutte,
Marcel Veismann,
Haley Cummings,
Sarah Conley,
Jonathan Bapst
, et al. (10 additional authors not shown)
Abstract:
Mid-Air Helicopter Delivery (MAHD) is a new Entry, Descent and Landing (EDL) architecture to enable in situ mobility for Mars science at lower cost than previous missions. It uses a jetpack to slow down a Mars Science Helicopter (MSH) after separation from the backshell, and reach aerodynamic conditions suitable for helicopter take-off in mid air. For given aeroshell dimensions, only MAHD's lander…
▽ More
Mid-Air Helicopter Delivery (MAHD) is a new Entry, Descent and Landing (EDL) architecture to enable in situ mobility for Mars science at lower cost than previous missions. It uses a jetpack to slow down a Mars Science Helicopter (MSH) after separation from the backshell, and reach aerodynamic conditions suitable for helicopter take-off in mid air. For given aeroshell dimensions, only MAHD's lander-free approach leaves enough room in the aeroshell to accommodate the largest rotor option for MSH. This drastically improves flight performance, notably allowing +150\% increased science payload mass. Compared to heritage EDL approaches, the simpler MAHD architecture is also likely to reduce cost, and enables access to more hazardous and higher-elevation terrains on Mars. This paper introduces a design for the MAHD system architecture and operations. We present a mechanical configuration that fits both MSH and the jetpack within the 2.65-m Mars heritage aeroshell, and a jetpack control architecture which fully leverages the available helicopter avionics. We discuss preliminary numerical models of the flow dynamics resulting from the interaction between the jets, the rotors and the side winds. We define a force-torque sensing architecture capable of handling the wind and trimming the rotors to prepare for safe take-off. Finally, we analyze the dynamic environment and closed-loop control simulation results to demonstrate the preliminary feasibility of MAHD.
△ Less
Submitted 7 March, 2022;
originally announced March 2022.
-
Dependent Type Systems as Macros
Authors:
Stephen Chang,
Michael Ballantyne,
Milo Turner,
William J. Bowman
Abstract:
We present Turnstile+, a high-level, macros-based metaDSL for building dependently typed languages. With it, programmers may rapidly prototype and iterate on the design of new dependently typed features and extensions. Or they may create entirely new DSLs whose dependent type "power" is tailored to a specific domain. Our framework's support of language-oriented programming also makes it suitable f…
▽ More
We present Turnstile+, a high-level, macros-based metaDSL for building dependently typed languages. With it, programmers may rapidly prototype and iterate on the design of new dependently typed features and extensions. Or they may create entirely new DSLs whose dependent type "power" is tailored to a specific domain. Our framework's support of language-oriented programming also makes it suitable for experimenting with systems of interacting components, e.g., a proof assistant and its companion DSLs. This paper explains the implementation details of Turnstile+, as well as how it may be used to create a wide-variety of dependently typed languages, from a lightweight one with indexed types, to a full spectrum proof assistant, complete with a tactic system and extensions for features like sized types and SMT interaction.
△ Less
Submitted 2 July, 2021;
originally announced July 2021.
-
Is Sized Ty** for Coq Practical?
Authors:
Jonathan Chan,
Yufeng Li,
William J. Bowman
Abstract:
Contemporary proof assistants such as Coq require that recursive functions be terminating and corecursive functions be productive to maintain logical consistency of their type theories, and some ensure these properties using syntactic checks. However, being syntactic, they are inherently delicate and restrictive, preventing users from easily writing obviously terminating or productive functions at…
▽ More
Contemporary proof assistants such as Coq require that recursive functions be terminating and corecursive functions be productive to maintain logical consistency of their type theories, and some ensure these properties using syntactic checks. However, being syntactic, they are inherently delicate and restrictive, preventing users from easily writing obviously terminating or productive functions at their whim.
Meanwhile, there exist many sized type theories that perform type-based termination and productivity checking, including theories based on the Calculus of (Co)Inductive Constructions (CIC), the core calculus underlying Coq. These theories are more robust and compositional in comparison. So why haven't they been adapted to Coq?
In this paper, we venture to answer this question with CIC$\widehat{*}$, a sized type theory based on CIC. It extends past work on sized types in CIC with additional Coq features such as global and local definitions. We also present a corresponding size inference algorithm and implement it within Coq's kernel; for maximal backward compatibility with existing Coq developments, it requires no additional annotations from the user.
In our evaluation of the implementation, we find a severe performance degradation when compiling parts of the Coq standard library, inherent to the algorithm itself. We conclude that if we wish to maintain backward compatibility, using size inference as a replacement for syntactic checking is wildly impractical in terms of performance.
△ Less
Submitted 13 December, 2021; v1 submitted 11 December, 2019;
originally announced December 2019.
-
Typed Closure Conversion for the Calculus of Constructions
Authors:
William J. Bowman,
Amal Ahmed
Abstract:
Dependently typed languages such as Coq are used to specify and verify the full functional correctness of source programs. Type-preserving compilation can be used to preserve these specifications and proofs of correctness through compilation into the generated target-language programs. Unfortunately, type-preserving compilation of dependent types is hard. In essence, the problem is that dependent…
▽ More
Dependently typed languages such as Coq are used to specify and verify the full functional correctness of source programs. Type-preserving compilation can be used to preserve these specifications and proofs of correctness through compilation into the generated target-language programs. Unfortunately, type-preserving compilation of dependent types is hard. In essence, the problem is that dependent type systems are designed around high-level compositional abstractions to decide type checking, but compilation interferes with the type-system rules for reasoning about run-time terms.
We develop a type-preserving closure-conversion translation from the Calculus of Constructions (CC) with strong dependent pairs ($Σ$ types)---a subset of the core language of Coq---to a type-safe, dependently typed compiler intermediate language named CC-CC. The central challenge in this work is how to translate the source type-system rules for reasoning about functions into target type-system rules for reasoning about closures. To justify these rules, we prove soundness of CC-CC by giving a model in CC. In addition to type preservation, we prove correctness of separate compilation.
△ Less
Submitted 12 August, 2018;
originally announced August 2018.
-
The Murchison Widefield Array Correlator
Authors:
S. M. Ord,
B. Crosse,
D. Emrich,
D. Pallot,
R. B. Wayth,
M. A. Clark,
S. E. Tremblay,
W. Arcus,
D. Barnes,
M. Bell,
G. Bernardi,
N. D. R. Bhat,
J. D. Bowman,
F. Briggs,
J. D. Bunton,
R. J. Cappallo,
B. E. Corey,
A. A. Deshpande,
L. deSouza,
A. Ewell-Wice,
L. Feng,
R. Goeke,
L. J. Greenhill,
B. J. Hazelton,
D. Herne
, et al. (42 additional authors not shown)
Abstract:
The Murchison Widefield Array (MWA) is a Square Kilometre Array (SKA) Precursor. The telescope is located at the Murchison Radio--astronomy Observatory (MRO) in Western Australia (WA). The MWA consists of 4096 dipoles arranged into 128 dual polarisation aperture arrays forming a connected element interferometer that cross-correlates signals from all 256 inputs. A hybrid approach to the correlation…
▽ More
The Murchison Widefield Array (MWA) is a Square Kilometre Array (SKA) Precursor. The telescope is located at the Murchison Radio--astronomy Observatory (MRO) in Western Australia (WA). The MWA consists of 4096 dipoles arranged into 128 dual polarisation aperture arrays forming a connected element interferometer that cross-correlates signals from all 256 inputs. A hybrid approach to the correlation task is employed, with some processing stages being performed by bespoke hardware, based on Field Programmable Gate Arrays (FPGAs), and others by Graphics Processing Units (GPUs) housed in general purpose rack mounted servers. The correlation capability required is approximately 8 TFLOPS (Tera FLoating point Operations Per Second). The MWA has commenced operations and the correlator is generating 8.3 TB/day of correlation products, that are subsequently transferred 700 km from the MRO to Perth (WA) in real-time for storage and offline processing. In this paper we outline the correlator design, signal path, and processing elements and present the data format for the internal and external interfaces.
△ Less
Submitted 23 January, 2015;
originally announced January 2015.
-
Efficient Dealiased Convolutions without Padding
Authors:
John C. Bowman,
Malcolm Roberts
Abstract:
Algorithms are developed for calculating dealiased linear convolution sums without the expense of conventional zero-padding or phase-shift techniques. For one-dimensional in-place convolutions, the memory requirements are identical with the zero-padding technique, with the important distinction that the additional work memory need not be contiguous with the input data. This decoupling of data and…
▽ More
Algorithms are developed for calculating dealiased linear convolution sums without the expense of conventional zero-padding or phase-shift techniques. For one-dimensional in-place convolutions, the memory requirements are identical with the zero-padding technique, with the important distinction that the additional work memory need not be contiguous with the input data. This decoupling of data and work arrays dramatically reduces the memory and computation time required to evaluate higher-dimensional in-place convolutions. The technique also allows one to dealias the higher-order convolutions that arise from Fourier transforming cubic and higher powers. Implicitly dealiased convolutions can be built on top of state-of-the-art fast Fourier transform libraries: vectorized multidimensional implementations for the complex and centered Hermitian (pseudospectral) cases have been implemented in the open-source software FFTW++.
△ Less
Submitted 10 February, 2011; v1 submitted 7 August, 2010;
originally announced August 2010.
-
Surface Parametrization of Nonsimply Connected Planar Bézier Regions
Authors:
Orest Shardt,
John C. Bowman
Abstract:
A technique is described for constructing three-dimensional vector graphics representations of planar regions bounded by cubic Bézier curves, such as smooth glyphs. It relies on a novel algorithm for compactly partitioning planar Bézier regions into nondegenerate Coons patches. New optimizations are also described for Bézier inside-outside tests and the computation of global bounds of directionall…
▽ More
A technique is described for constructing three-dimensional vector graphics representations of planar regions bounded by cubic Bézier curves, such as smooth glyphs. It relies on a novel algorithm for compactly partitioning planar Bézier regions into nondegenerate Coons patches. New optimizations are also described for Bézier inside-outside tests and the computation of global bounds of directionally monotonic functions over a Bézier surface (such as its bounding box or optimal field-of-view angle). These algorithms underlie the three-dimensional illustration and typography features of the TeX-aware vector graphics language Asymptote.
△ Less
Submitted 7 August, 2010; v1 submitted 17 May, 2010;
originally announced May 2010.
