CHAD for expressive total languages

DOI10.1017/S096012952300018XOpenAlexW3203610362MaRDI QIDQ6149934FDOQ6149934

Authors Fernando Lucatelli Nunes, Matthijs Vákár 

Publication date 5 March 2024

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2110.00446

zbMATH Keywords

scientific computingprogramming languagesCartesian closed categoriesdenotational semanticstype systemscoalgebraslogical relationspolynomial functorsprogram transformationsautomatic differentiationGrothendieck constructioncomma categoriesinductive typesexponentiabilitylinear typesfibered categoriessoftware correctnessinitial algebra semanticsextensive categoriesvariant typesArtin gluingcoinductive types(co)monadicitycreation of initial algebrasdependently typed languagesextensive indexed categoriesfree cocompletion under coproducts

Mathematics Subject Classification ID

Computer science (68-XX)

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 $Sigma$-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.

Cites work

• scientific article; zbMATH DE number 193320 (Why is no real title available?)
• scientific article; zbMATH DE number 3522182 (Why is no real title available?)
• scientific article; zbMATH DE number 575948 (Why is no real title available?)
• scientific article; zbMATH DE number 2068087 (Why is no real title available?)
• scientific article; zbMATH DE number 6982909 (Why is no real title available?)
• scientific article; zbMATH DE number 2172008 (Why is no real title available?)
• scientific article; zbMATH DE number 1840601 (Why is no real title available?)
• scientific article; zbMATH DE number 7566054 (Why is no real title available?)
• scientific article; zbMATH DE number 3305157 (Why is no real title available?)
• scientific article; zbMATH DE number 3367095 (Why is no real title available?)
• scientific article; zbMATH DE number 2222246 (Why is no real title available?)
• scientific article; zbMATH DE number 7650831 (Why is no real title available?)
• μ-Bicomplete Categories and Parity Games
• A simple automatic derivative evaluation program
• Accessible Categories: The Foundations of Categorical Model Theory
• Adjoint triangles
• Basic Category Theory
• Categorical logic and type theory
• Categories for Types
• Correctness of automatic differentiation via diffeologies and categorical gluing
• Dependent types and fibred computational effects
• Dialectica models of type theory
• Diffeology
• Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen
• Evaluating Derivatives
• Galois theories
• Higher-order containers
• Introduction to Smooth Manifolds
• Introduction to extensive and distributive categories
• Kan extensions in enriched category theory
• Least fixed point of a functor
• Lokal präsentierbare Kategorien. (Locally presentable categories)
• Non-canonical isomorphisms
• On lifting of biadjoints and lax algebras
• On the versatility of open logical relations. Continuity, automatic differentiation, and a containment theorem
• Proof theory in the abstract
• Pseudoalgebras and non-canonical isomorphisms
• Reverse AD at higher types: pure, principled and denotationally correct
• Semantic factorization and descent
• Terminal coalgebras in well-founded set theory
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES

Cited in

(1)

• Lax comma categories: Cartesian closedness, extensivity, topologicity, and descent

This page was built for publication: CHAD for expressive total languages

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6149934)