Forwarded from Sergey Kucherenko
The Functional Essence of Imperative Binary Search Trees
Algorithms on restructuring binary search trees are typically presented in imperative pseudocode. Understandably so, as their performance relies on in-place execution, rather than the repeated allocation of fresh nodes in memory. Unfortunately, these imperative algorithms are notoriously difficult to verify as their loop invariants must relate the unfinished tree fragments being rebalanced. This paper presents several novel functional algorithms for accessing and inserting elements in a restructuring binary search tree that are as fast as their imperative counterparts; yet the correctness of these functional algorithms is established using a simple inductive argument. For each data structure, move-to-root, splay, and zip trees, this paper describes both a bottom-up algorithm using zippers and a top-down algorithm using a novel first-class constructor context primitive. The functional and imperative algorithms are equivalent: we mechanise the proofs establishing this in the Coq proof assistant using the Iris framework. This yields a first fully verified implementation of well known algorithms on binary search trees with performance on par with the fastest implementations in C.
https://www.microsoft.com/en-us/research/uploads/prod/2023/07/fiptree-tr-v4.pdf
Algorithms on restructuring binary search trees are typically presented in imperative pseudocode. Understandably so, as their performance relies on in-place execution, rather than the repeated allocation of fresh nodes in memory. Unfortunately, these imperative algorithms are notoriously difficult to verify as their loop invariants must relate the unfinished tree fragments being rebalanced. This paper presents several novel functional algorithms for accessing and inserting elements in a restructuring binary search tree that are as fast as their imperative counterparts; yet the correctness of these functional algorithms is established using a simple inductive argument. For each data structure, move-to-root, splay, and zip trees, this paper describes both a bottom-up algorithm using zippers and a top-down algorithm using a novel first-class constructor context primitive. The functional and imperative algorithms are equivalent: we mechanise the proofs establishing this in the Coq proof assistant using the Iris framework. This yields a first fully verified implementation of well known algorithms on binary search trees with performance on par with the fastest implementations in C.
https://www.microsoft.com/en-us/research/uploads/prod/2023/07/fiptree-tr-v4.pdf
The Structure of Meaning in Language: Parallel Narratives in Linear Algebra and Category Theory
https://www.ams.org/journals/notices/202402/rnoti-p174.pdf
https://www.ams.org/journals/notices/202402/rnoti-p174.pdf
https://www.cs.ru.nl/B.Jacobs/PAPERS/ProbabilisticReasoning.pdf Jacobs, [2023] "Structured Probabilistic Reasoning"
https://link.springer.com/chapter/10.1007/978-3-031-16912-0_3 Hinze, Swierstra, [2022] "Calculating Datastructures"
SpringerLink
Calculating Datastructures
Where do datastructures come from? This paper explores how to systematically derive implementations of one-sided flexible arrays from a simple reference implementation. Using the dependently typed programming language Agda, each calculation constructs an...
STRANGE NEW UNIVERSES: PROOF ASSISTANTS AND SYNTHETIC FOUNDATIONS
MICHAEL SHULMAN
Existing computer programs called proof assistants can verify the correctness of mathematical proofs but their specialized proof languages present a barrier to entry for many mathematicians. Large language models have the potential to lower this barrier, enabling mathematicians to interact with proof assistants in a more familiar vernacular. Among other advantages, this may allow mathematicians to explore radically new kinds of mathematics using an LLM-powered proof assistant to train their intuitions as well as ensure their arguments are correct. Existing proof assistants have already played this role for fields such as homotopy type theory
https://www.ams.org/journals/bull/0000-000-00/S0273-0979-2024-01830-8/S0273-0979-2024-01830-8.pdf
MICHAEL SHULMAN
Existing computer programs called proof assistants can verify the correctness of mathematical proofs but their specialized proof languages present a barrier to entry for many mathematicians. Large language models have the potential to lower this barrier, enabling mathematicians to interact with proof assistants in a more familiar vernacular. Among other advantages, this may allow mathematicians to explore radically new kinds of mathematics using an LLM-powered proof assistant to train their intuitions as well as ensure their arguments are correct. Existing proof assistants have already played this role for fields such as homotopy type theory
https://www.ams.org/journals/bull/0000-000-00/S0273-0979-2024-01830-8/S0273-0979-2024-01830-8.pdf
ABSTRACTION BOUNDARIES AND SPEC DRIVEN DEVELOPMENT IN PURE MATHEMATICS
JOHAN COMMELIN AND ADAM TOPAZ
In this article we discuss how abstraction boundaries can help tame complexity in mathematical research with the help of an interactive theorem prover. While many of the ideas we present here have been used implicitly by mathematicians for some time, we argue that the use of an interactive theorem prover introduces additional qualitative benefits in the implementation of these ideas.
https://www.ams.org/journals/bull/0000-000-00/S0273-0979-2024-01831-X/S0273-0979-2024-01831-X.pdf
JOHAN COMMELIN AND ADAM TOPAZ
In this article we discuss how abstraction boundaries can help tame complexity in mathematical research with the help of an interactive theorem prover. While many of the ideas we present here have been used implicitly by mathematicians for some time, we argue that the use of an interactive theorem prover introduces additional qualitative benefits in the implementation of these ideas.
https://www.ams.org/journals/bull/0000-000-00/S0273-0979-2024-01831-X/S0273-0979-2024-01831-X.pdf
https://okmij.org/ftp/tagless-final/datatypes.html
Many examples of tagless-final DSL embedding center on languages with numbers and functions. Occasionally, arrays and lists make an ad hoc appearance. One may, however, want to embed a language with tuples, sums (such as option a.k.a Maybe), as well as various trees. Rather than designing the embedding for each particular data type from scratch, one would ideally apply a general method, almost mechanically. Such general and convenient embedding recipe has been lacking so far.
Examples of ADT embedding in tagless-final style are rare because ADT invariably evoke pattern-matching -- the biggest attraction of ADT -- and pattern-matching in tagless-final style is known to be awkward. Or so I thought.
This article demonstrates a systematic embedding of a language with ADTs, and their recursive processing (constructing, transforming, consuming) using pattern-matching.
Many examples of tagless-final DSL embedding center on languages with numbers and functions. Occasionally, arrays and lists make an ad hoc appearance. One may, however, want to embed a language with tuples, sums (such as option a.k.a Maybe), as well as various trees. Rather than designing the embedding for each particular data type from scratch, one would ideally apply a general method, almost mechanically. Such general and convenient embedding recipe has been lacking so far.
Examples of ADT embedding in tagless-final style are rare because ADT invariably evoke pattern-matching -- the biggest attraction of ADT -- and pattern-matching in tagless-final style is known to be awkward. Or so I thought.
This article demonstrates a systematic embedding of a language with ADTs, and their recursive processing (constructing, transforming, consuming) using pattern-matching.
okmij.org
Algebraic Data Types and Pattern-Matching
Tagless-final embedding of DSLs with data types and representing pattern-matching
Bruno Gavranović has finally published his thesis 🎉
Fundamental Components of Deep Learning
A category-theoretic approach
https://www.brunogavranovic.com/assets/FundamentalComponentsOfDeepLearning.pdf
A summary is available at: https://www.brunogavranovic.com/posts/2024-03-13-my-thesis-is-out.html
Fundamental Components of Deep Learning
A category-theoretic approach
https://www.brunogavranovic.com/assets/FundamentalComponentsOfDeepLearning.pdf
A summary is available at: https://www.brunogavranovic.com/posts/2024-03-13-my-thesis-is-out.html
Oxidizing OCaml with Modal Memory Management
A. Lorenzen, L. White, S. Dolan, R. Eisenberg, S. Lindley
https://homepages.inf.ed.ac.uk/slindley/papers/mode-inference-draft-feb2024.pdf
A. Lorenzen, L. White, S. Dolan, R. Eisenberg, S. Lindley
https://homepages.inf.ed.ac.uk/slindley/papers/mode-inference-draft-feb2024.pdf
Asymptotic speedup via effect handlers
D. Hillerström, S. Lindley, J. Longley
https://www.cambridge.org/core/journals/journal-of-functional-programming/article/asymptotic-speedup-via-effect-handlers/296879DE2FD96FB6CF388F27978C76E4
D. Hillerström, S. Lindley, J. Longley
https://www.cambridge.org/core/journals/journal-of-functional-programming/article/asymptotic-speedup-via-effect-handlers/296879DE2FD96FB6CF388F27978C76E4
Cambridge Core
Asymptotic speedup via effect handlers | Journal of Functional Programming | Cambridge Core
Asymptotic speedup via effect handlers - Volume 34
From Batch to Stream: Automatic Generation of Online Algorithms
We propose a new technique that converts batch processing programs (i.e., offline algorithms) to their online streaming version that takes one element at a time.
As a cool example, given the standard variance computation for a list of elements (left), our method can automatically generate Welford’s algorithm for online variance computation (right):
https://pbs.twimg.com/media/GMBpnclXcAEh9B9?format=jpg&name=4096x4096
Paper: https://arxiv.org/abs/2404.04743
Code: https://github.com/utopia-group/opera
We propose a new technique that converts batch processing programs (i.e., offline algorithms) to their online streaming version that takes one element at a time.
As a cool example, given the standard variance computation for a list of elements (left), our method can automatically generate Welford’s algorithm for online variance computation (right):
https://pbs.twimg.com/media/GMBpnclXcAEh9B9?format=jpg&name=4096x4096
Paper: https://arxiv.org/abs/2404.04743
Code: https://github.com/utopia-group/opera