Cass Alexandru

PhD 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

Last Notes

2026-06-05 07:18:16 GMT

I scored 10 / 12 on "Extension Or Imitation"
https://doscienceto.it/extension-or-imitation
Try it out?
via @nprofile…mx55
#Haskell #HaskellLanguageExtensionOrImitation

2026-01-30 16:32:41 GMT

- reply

@nprofile…t6k2
writes:
Usually, see e.g. [1], the termination of the Ackermann function is proved using the lexicographic order on ℕ × ℕ, but it is well known that this has order type ω².
My question is, how would a definition using ω²-recursion (?) directly look like, as opposed to indirectly via the equivalence of this to lexicographic order on ℕ × ℕ. I'm also happy for pointers to literature on the topic.
@nprofile…4hp5 @nprofile…s7d2

2026-01-30 13:15:52 GMT

Question (feel free to boost): The way the Ackermann function can be proven to terminate in type theory is by making use of primitive recursion to define higher-order functions (the Dialectica interpretation iiuc) (c.f.The identification of propositions and types in Martin-Löf's type theory: A programming example). What I want to know is, can we define it with transfinite recursion instead? Recursion to which ordinal? What would the definition look like?
I found the below quote in a post by @nprofile…4hp5 :
Here’s a puzzle for you (for me too): glance at the definition of the Ackermann function. Say the two-place version. As the Wikipedia article notes, the value for A(m, n) depends values of A(m*, n*) with (m*, n*) preceding (m, n) in the lexicographic ordering—looks like a job for transfinite induction up to ω2! Yet the Ackermann function outpaces every primitive recursive function, and as we’ve read, PRA handles induction up to any ordinal less than ωω! - Non-Standard Models of Arithmetic 10 | Diagonal Argument.
There is also the paper Elimination of Higher type Levels in Definitions of Primitive Recursive Functionals by Means of Transfinite Recursion which seems to be about how you do sth like this in a general way, but I don't understand enough about this topic yet to try to understand and try to apply it.
Pinging @nprofile…s7d2 , I feel like you might be interested or have insights

2025-04-11 17:02:33 GMT

- reply

@nprofile…6kk0 do you know www.radioswissclassic.ch ?

2024-12-07 19:24:53 GMT

- reply

@nprofile…fa4k I also watched the whole video and do agree that the one point she does seem to miss is that where he comes across as the smart guy he explains how it is often by coincidence and not bc he's claiming to be super smart, and this is an experience I've also had – sometimes one has some particular bit of in-depth knowledge on a topic from which others falsely conclude that one knows the whole topic to that level of depth, whereas this depth is quite narrowly confined.

2024-11-25 22:02:23 GMT

- reply

@nprofile…klk6 adding to this (for future reference): the number that will be generated for the column may be some digit which may not necessarily correspond to the column number one sees visually, so it's best to first see what number gets generated, and then copy that number back over to the source

2024-11-25 21:16:02 GMT

- reply

@nprofile…klk6 ok, I saw that mentioned in the manual as well, I guess the only issue is that that isn't valid Haskell code anymore, so ghci doesn't load it (at least when inside of a `code` environment, idk if bird ticks are different?)

2024-11-25 16:03:58 GMT

@nprofile…klk6 quick lhs2tex question: Do you know how I would go about aligning the closing paren with the word boundary of y in the line below?
( a -> b ) -> a -> c
bar x -> biz y
(also, I have another more obscure question of less importance, but when I try to use \aligncolumn{2}{c}\aligncolumn{4}{c} I get the error \mathit allowed only in math mode. (this is with the default style, which is "poly", iirc))