-
Unraveling the iterative CHAD
Authors:
Fernando Lucatelli Nunes,
Gordon Plotkin,
Matthijs Vákár
Abstract:
Combinatory Homomorphic Automatic Differentiation (CHAD) was originally formulated as a semantics-driven source transformation for reverse-mode AD in total programming languages. We extend this framework to partial languages with features such as potentially non-terminating operations, real-valued conditionals, and iteration constructs like while-loops, while preserving CHAD's structure-preserving…
▽ More
Combinatory Homomorphic Automatic Differentiation (CHAD) was originally formulated as a semantics-driven source transformation for reverse-mode AD in total programming languages. We extend this framework to partial languages with features such as potentially non-terminating operations, real-valued conditionals, and iteration constructs like while-loops, while preserving CHAD's structure-preserving semantics principle. A key contribution is the introduction of iteration-extensive indexed categories, which allow iteration in the base category to lift to parameterized initial algebras in the indexed category. This enables iteration to be interpreted in the Grothendieck construction of the target language in a principled way. The resulting fibred iterative structure cleanly models iteration in the categorical semantics. Consequently, the extended CHAD transformation remains the unique structure-preserving functor (an iterative Freyd category morphism) from the freely generated iterative Freyd category of the source language to the Grothendieck construction of the target's syntactic semantics, mapping each primitive operation to its derivative. We prove the correctness of this transformation using the universal property of the source language's syntax, showing that the transformed programs compute correct reverse-mode derivatives. Our development also contributes to understanding iteration constructs within dependently typed languages and categories of containers. As our primary motivation and application, we generalize CHAD to languages with data types, partial features, and iteration, providing the first rigorous categorical semantics for reverse-mode CHAD in such settings and formally guaranteeing the correctness of the source-to-source CHAD technique.
△ Less
Submitted 20 May, 2025;
originally announced May 2025.
-
Monoidal closure of Grothendieck constructions via $Σ$-tractable monoidal structures and Dialectica formulas
Authors:
Fernando Lucatelli Nunes,
Matthijs Vákár
Abstract:
We study the categorical structure of the Grothendieck construction of an indexed category $\mathcal{L}:\mathcal{C}^{op}\to\mathbf{CAT}$ and characterise fibred limits, colimits, and monoidal structures. Next, we give sufficient conditions for the monoidal closure of the total category $Σ_\mathcal{C} \mathcal{L}$ of a Grothendieck construction of an indexed category…
▽ More
We study the categorical structure of the Grothendieck construction of an indexed category $\mathcal{L}:\mathcal{C}^{op}\to\mathbf{CAT}$ and characterise fibred limits, colimits, and monoidal structures. Next, we give sufficient conditions for the monoidal closure of the total category $Σ_\mathcal{C} \mathcal{L}$ of a Grothendieck construction of an indexed category $\mathcal{L}:\mathcal{C}^{op}\to\mathbf{CAT}$. Our analysis is a generalization of Gödel's Dialectica interpretation, and it relies on a novel notion of $Σ$-tractable monoidal structure. As we will see, $Σ$-tractable coproducts simultaneously generalize cocartesian coclosed structures, biproducts and extensive coproducts. We analyse when the closed structure is fibred -- usually it is not.
△ Less
Submitted 21 May, 2024; v1 submitted 13 May, 2024;
originally announced May 2024.
-
Free Doubly-Infinitary Distributive Categories are Cartesian Closed
Authors:
Fernando Lucatelli Nunes,
Matthijs Vákár
Abstract:
We investigate categories in which products distribute over coproducts, a structure we call doubly-infinitary distributive categories. Through a range of examples, we explore how this notion relates to established concepts such as extensivity, infinitary distributivity, and cartesian closedness. We show that doubly-infinitary distributivity strictly strengthens the classical notion of infinitary d…
▽ More
We investigate categories in which products distribute over coproducts, a structure we call doubly-infinitary distributive categories. Through a range of examples, we explore how this notion relates to established concepts such as extensivity, infinitary distributivity, and cartesian closedness. We show that doubly-infinitary distributivity strictly strengthens the classical notion of infinitary distributivity. Moreover, we prove that free doubly-infinitary distributive categories are cartesian closed, unlike free distributive categories. The paper concludes with observations on non-canonical isomorphisms, alongside open questions and directions for future research.
△ Less
Submitted 24 June, 2025; v1 submitted 15 March, 2024;
originally announced March 2024.
-
Logical Relations for Partial Features and Automatic Differentiation Correctness
Authors:
Fernando Lucatelli Nunes,
Matthijs Vákár
Abstract:
We present a simple technique for semantic, open logical relations arguments about languages with recursive types, which, as we show, follows from a principled foundation in categorical semantics. We demonstrate how it can be used to give a very straightforward proof of correctness of practical forward- and reverse-mode dual numbers style automatic differentiation (AD) on ML-family languages. The…
▽ More
We present a simple technique for semantic, open logical relations arguments about languages with recursive types, which, as we show, follows from a principled foundation in categorical semantics. We demonstrate how it can be used to give a very straightforward proof of correctness of practical forward- and reverse-mode dual numbers style automatic differentiation (AD) on ML-family languages. The key idea is to combine it with a suitable open logical relations technique for reasoning about differentiable partial functions (a suitable lifting of the partiality monad to logical relations), which we introduce.
△ Less
Submitted 23 October, 2022; v1 submitted 16 October, 2022;
originally announced October 2022.
-
Automatic Differentiation for ML-family languages: correctness via logical relations
Authors:
Fernando Lucatelli Nunes,
Matthijs Vákár
Abstract:
We give a simple, direct and reusable logical relations technique for languages with term and type recursion and partially defined differentiable functions. We demonstrate it by working out the case of Automatic Differentiation (AD) correctness: namely, we present a correctness proof of a dual numbers style AD code transformation for realistic functional languages in the ML-family. We also show ho…
▽ More
We give a simple, direct and reusable logical relations technique for languages with term and type recursion and partially defined differentiable functions. We demonstrate it by working out the case of Automatic Differentiation (AD) correctness: namely, we present a correctness proof of a dual numbers style AD code transformation for realistic functional languages in the ML-family. We also show how this code transformation provides us with correct forward- and reverse-mode AD.
The starting point is to interpret a functional programming language as a suitable freely generated categorical structure. In this setting, by the universal property of the syntactic categorical structure, the dual numbers AD code transformation and the basic $ω$-cpo semantics arise as structure preserving functors. The proof follows, then, by a novel logical relations argument.
The key to much of our contribution is a powerful monadic logical relations technique for term recursion and recursive types. It provides us with a semantic correctness proof based on a simple approach for denotational semantics, making use only of the very basic concrete model of $ω$-cpos.
△ Less
Submitted 14 June, 2024; v1 submitted 14 October, 2022;
originally announced October 2022.
-
CHAD for Expressive Total Languages
Authors:
Fernando Lucatelli Nunes,
Matthijs Vákár
Abstract:
We show how to apply forward and reverse mode Combinatory Homomorphic Automatic Differentiation (CHAD) to total functional programming languages with expressive type systems featuring the combination of - tuple types; - sum types; - inductive types; - coinductive types; - function types. We achieve this by analysing the categorical semantics of such types in $Σ$-types (Grothendieck constructions)…
▽ More
We show how to apply forward and reverse mode Combinatory Homomorphic Automatic Differentiation (CHAD) to total functional programming languages with expressive type systems featuring the combination of - tuple types; - sum types; - inductive types; - coinductive types; - function types. We achieve this by analysing the categorical semantics of such types in $Σ$-types (Grothendieck constructions) of suitable categories. Using a novel categorical logical relations technique for such expressive type systems, we give a correctness proof of CHAD in this setting by showing that it computes the usual mathematical derivative of the function that the original program implements. The result is a principled, purely functional and provably correct method for performing forward and reverse mode automatic differentiation (AD) on total functional programming languages with expressive type systems.
△ Less
Submitted 3 April, 2023; v1 submitted 1 October, 2021;
originally announced October 2021.
-
Towards the Systematic Testing of Virtual Reality Programs (extended version)
Authors:
Stevao A. Andrade,
Fatima L. S. Nunes,
Marcio E. Delamaro
Abstract:
Software testing is a critical activity to ensure that software complies with its specification. However, current software testing activities tend not to be completely effective when applied in specific software domains in Virtual Reality (VR) that has several new types of features such as images, sounds, videos, and differentiated interaction, which can become sources of new kinds of faults. This…
▽ More
Software testing is a critical activity to ensure that software complies with its specification. However, current software testing activities tend not to be completely effective when applied in specific software domains in Virtual Reality (VR) that has several new types of features such as images, sounds, videos, and differentiated interaction, which can become sources of new kinds of faults. This paper presents an overview of the main VR characteristics that can have an impact on verification, validation, and testing (VV&T). Furthermore, it analyzes some of the most successful VR open-source projects to draw a picture concerning the danger of the lack of software testing activities. We compared the current state of software testing practice in open-source VR projects and evaluate how the lack of testing can be damaging to the development of a product. We assessed the incidence of code smells and verified how such projects behave concerning the tendency to present faults. The results showed that the practice of software testing is not yet widespread in the development of VR applications. It was also found that there is a high incidence of code smells in VR projects. Regarding fault-proneness the results showed that about 12.2% of the classes analyzed in VR projects are fault-prone. Regarding the application of software testing techniques on VR projects, it was observed that only a small number of projects are concerned about developing test cases for VR projects, perhaps because we still do not have the necessary tools to help in this direction. Concerning smells, we concluded that there is a high incidence in VR projects, especially regarding implementing smells and this high incidence can have a significant influence on faults. Finally, the study related to fault proneness pointed out that the lack of software testing activity is a significant risk to the success of the projects.
△ Less
Submitted 18 September, 2020;
originally announced September 2020.
