CHAD for expressive total languages

DOI10.1017/S096012952300018XarXiv2110.00446OpenAlexW3203610362MaRDI 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)

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.

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)

Cites Work

• Introduction to Smooth Manifolds
• Diffeology
• Evaluating Derivatives
• Categorical logic and type theory
• Lokal präsentierbare Kategorien. (Locally presentable categories)
• Galois theories
• Accessible Categories: The Foundations of Categorical Model Theory
• Title not available (Why is that?)
• Non-canonical isomorphisms
• Title not available (Why is that?)
• Categories for Types
• Title not available (Why is that?)
• Title not available (Why is that?)
• Introduction to extensive and distributive categories
• Title not available (Why is that?)
• Terminal coalgebras in well-founded set theory
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Kan extensions in enriched category theory
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Title not available (Why is that?)
• Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen
• Adjoint triangles
• A simple automatic derivative evaluation program
• Basic Category Theory
• Title not available (Why is that?)
• Least fixed point of a functor
• μ-Bicomplete Categories and Parity Games
• Title not available (Why is that?)
• Proof theory in the abstract
• Pseudoalgebras and non-canonical isomorphisms
• On lifting of biadjoints and lax algebras
• Semantic factorization and descent
• Title not available (Why is that?)
• Dialectica models of type theory
• Correctness of automatic differentiation via diffeologies and categorical gluing
• On the Versatility of Open Logical Relations
• Reverse AD at higher types: pure, principled and denotationally correct
• Dependent Types and Fibred Computational Effects
• Higher-order containers

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)