2022/10/16 by Fernando Lucatelli Nunes, Matthijs Vákár, Nunes, Fernando Lucatelli +1
Computer Science · #18A25 #18D20 #68N15 #68N18 #68Q55 #68W30 #Category Theory (math.CT) #D.3 #D.3.1 #F.3.1 #F.3.2 #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Natural Language Processing Techniques #Programming Languages (cs.PL) #Semantic Web and Ontologies
paper · pdf · doi:10.48550/arxiv.2210.08530
openalex publication_date 2022/10/16 · openalex created_date 2022/10/20 · openalex updated_date 2026/07/28
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.