Remote
Cass Alexandru
@cxandru@types.pl
mastodon 4.8.0-alpha.2+glitchPhD student with Ralf Hinze, Jurriaan Rot & Niels van der Weide in Category Theory for the design of Proven Correct, Total Algorithms
#categorytheory #agda #haskell #nix #emacs Recursion Schemes/Structured Recursion Generic Programming Language Acquisition New Masculinities #vegan #sustainable #skeptic Friend Boulderer #meditation Yin #maker 🇪🇺an
236 Followers
189 Following
18 Posts
Joined November 27, 2022
Pronouns:
they/them
Personal Site:
Slides for my talk at #TYPES tomorrow are now up on my website (https://cxandru.ee/)
> be me
> idea: Restaurant w board games, when you order you get a recommended game to play based on expected time to have your order ready
> business is booming
> one day manager comes to me says boss there's a problem
> me: what, is the concept not working?
> no, it is, but ... most recommended board game is Risk
#shitpost
Replying to
The key idea is that, for a d&c algorithm to terminate, the divide step should make inputs "smaller". As such, we work in the setting 𝒞^I for some well ordered set (I, <). We introduce the novel concept of a well founded (endo)-functor on 𝒞^I, describing a functor whose output is pointwise determined by smaller inputs. 4/8
vermeil: gold-covered silver
verdant: green, as in plants
vermillion: bright red
🤪
Replying to
A a coalgebra is called recursive, if for every F-algebra a, the equation h = c; Fh; a admits a unique solution, i.e. can act as a definition. Our contribution is a novel sufficient criterion for all coalgebras for some functor to be recursive. 3/8
Replying to
Next to PLDI, I will be giving a talk about this work at TYPES, and Henning Urbat will give one at CMCS, so keep your eyes peeled 👀. 8/8
Replying to
@jonmsterling Nix: same exact versions of your dependencies on everyone's machines and CI and possible docker image artefacts. Given previous posts I've seen on here of people not having the same latex environments as their coauthors, I don't understand the aversion to learning a genuinely useful technology, especially since, if properly set up, only one person on the team needs to deeply understand it
Replying to
Divide-and-conquer algorithms are described by the notion of coalgebra-to-algebra morphism for some functor F.
The "divide" step is given by an F-coalgebra c, the "combine" step by an F-algebra a, and the whole algorithm h
satisfies the functional equation h = c; Fh; a. 2/8
Replying to
The Agda implementation of the main theorem of our paper, as well as a library we wrote for writing recursive algorithms based on coalgebras for well founded functors, can be found at https://git8.cs.fau.de/software/intrinsically-recursive/ .
In our paper we show how one can also use our technique for proving recursivity of coalgebras in a non-indexed setting, as well as providing case studies of QuickSort, CYK parsing, and the Euclidean algorithm. 7/8
Replying to
A functor G: 𝒞I → 𝒞I is well founded if for every i ∈ I there exists a functor $G_{
Replying to
What does this buy us? Well, we can make dual use of an indexed setting already present for intrinsic verification of partial correctness
to also prove total correctness, by combining the index with a suitable relation such that it corresponds to a ranking argument. And all this is done at the level of the functor, allowing the separation of recursion behaviour from nonrecursive business logic, in the spirit of structured recursion. 6/8
Replying to
@Taneb@hacksrus.xyz Only reason really is bc one of the applications is sorting with the Finite Multiset QIT as Index. The translation to stdlib of IntrinsicallyRecursiveCoalgs is entirely straightforward, I'm considering releasing a version that works for stdlib though idk what best practices are if one wanta to avoid code duplication …