Zhixuan Yang

interested in algebraic and logical methods in computer science, Lecturer at the University of Exeter

Homepage: https://yangzhixuan.github.io/
Pronouns: He/him

Public Key

npub1v6afl9hlcsdeqcw06j3lqtv48xjqpmfyp2nc5e6k829vlp5ekg3qjac7s4

NIP-05 Address

zyang_at_mathstodon.xyz@momostr.pink

Profile Code

nprofile1qqsxdw5ljmlugxusv88afgls9k2nnfqqa5jq4fu2vatr4zk0s6vmygsprpmhxue69uhhyetvv9ujumt0d4hhxarj9ecxjmntwglvar

Publishing to

relay.momostr.pink

Author Public Key

npub1v6afl9hlcsdeqcw06j3lqtv48xjqpmfyp2nc5e6k829vlp5ekg3qjac7s4

Show more details

Last Notes

2026-05-16 12:35:42 UTC

- reply

You are right! I didn't wanted inf to be the top but accidentally made it the top. My mistake!

2026-05-16 11:29:15 UTC

- reply

∞ needs to be above everything; otherwise it wouldn't be the least solution of the equation `inf = succ inf`. Alternatively we could write ∞ as "Succ (Succ (Succ ...))" so that n ⊑ ∞ is subsumed by the other condition.
> By changing "one" to "some" this includes the case n = m and supports data type with more than one recursion, like binary trees.
Yes exactly.

2026-05-16 10:50:03 UTC

- reply

Yes, in a strict language I would view "data Nat = Zero | Succ Nat" as an equation "N ~= 1 + N" in DCPO, giving us just the discrete dcpo Nat. (This is the semantics of _values_ of Nat, so it doesn't need to support recursion. Computations of Nat have semantics F N and admit recurison.)
PS: I increasingly like strict functional languages (say ML or GHC with the Strict extension). Laziness occasionally improves asymptotic complexity but more often slows down the constant factor, and more importantly, making reasoning a lot harder.

2026-05-16 10:22:41 UTC

- reply

> Sometimes Haskell solves the fixpoint equation `inf = Succ inf` to infinity, instead of the least solution, which should be infinite loops.
There might be a misunderstanding here. If Nat is defined as `data Nat = Zero | Succ Nat`. This datatype in Haskell has as elements: (1) a bottom, (2) Zero, and (3) `Succ n` for an existing `n`. Modulo the usual boring statement "Haskell doesn't have a formal semantics!", we can view Nat as an equation N ~= F (1 + U N) in the category DCPPO of dcppos and non-strict continuous functions, where F : DCPO -> DCPPO freely adds a bottom element, + of dcpos is just taking their disjoint union, and U : DCPPO -> DCPO forgets the bottom. The least solution of N has the following elements:
* ⊥
* Zero
* Succ ⊥
* Succ Zero
* Succ (Succ ⊥)
* Succ (Succ Zero)
...
* ∞
with the order n ⊑ m if m = ∞ or m can be obtained by replacing a ⊥ in n with another element. In this dcppo N, the least solution 'inf = Succ inf' is already ∞, rather than ⊥.

2026-05-08 22:55:55 UTC

- reply

This must not be surprising to physicists at all, but I only knew very recently: if I play some music using my phone near the pickup of my electric guitar, the pickup can actually pick up the sound!

2026-04-22 22:24:41 UTC

Today one of my colleague reminded me a few years ago some people were saying things like "we use dependent types instead of HOL because they are the right language to formalise maths beautifully". Now suddenly they don't care about beauty 😆

2026-01-20 22:21:15 UTC

- reply

Now I think my code works: my effect handler library runs with O(1) running-time overhead. O(1)-time for installing a handler. O(1)-time for calling an operation. And with the optional staging support it can run faster than hand-rolled programs.

2026-01-20 22:13:13 UTC

I have been very sad during the last two hours because my code is so slow while its ghc core looks reasonably fast after my careful examination. It turns out I was running the wrong test 🤣

2025-10-08 17:36:29 UTC

- reply

I hate all kinds of zoos, but surely letting the belugas live in a theme park in a country that you might dislike is better than just killing them?

2025-10-08 17:32:53 UTC

https://www.theguardian.com/environment/2025/oct/06/canada-marineland-beluga-whales

2025-08-26 09:27:45 UTC

Future technology!
https://media.mathstodon.xyz/media_attachments/files/115/094/349/983/778/049/original/bc5eccb263e46612.png

2025-08-22 15:49:20 UTC

Finally I can close the jobs.ac.uk tab that I've been checking everyday for nearly a year... Now it comes to the decision:
* staying in academia (which I've been trained for for almost a decade but I am getting a bit tired of in the recent one or two years),
* or going to industry (which I am less familiar with but seems interesting and satisfying in a different way)...

2025-07-25 18:37:48 UTC

- reply

I hope it doesn't take you an hour to brew and then tell you "no result!"

2025-04-27 17:44:48 UTC

- reply

(As usual in the discussion of problems of this kind, it's better to talk about mathematically specific programming languages/type theories instead of Haskell/OCaml/Agda.)
In call-by-value languages, for every type τ, we actually have two different things in the language: (1) values of type τ and (2) computations of type τ. Only values can substitute variables of type τ, and if the language has recursion (or some computational effects), only computations support recursion/effects. Now coming back to inductive data types, because general recursion is not allowed on values, so we don't have to (and shouldn't) include infinite values as _values_ of inductive types. General recursion only forces us to include infinite/divergent computations as _computations_ of inductive types. We can of course separately have coinductive types, whose _values_ have infinite values.
Paul Levy's work on call-by-push-value answers questions like this extremely clearly. I highly recommend checking out the first chapters of this CBPV book. (A while ago I think I saw on mastodon that someone said CBPV isn't about computational effects. I was quite surprised because CBPV is totally about computational effects...)

2025-03-20 16:26:30 UTC

- reply

Skimming over the definition of NKA on page 6 of your link, I think it's the same idea (replacing sets with nominal sets)

2025-03-20 12:31:58 UTC

Deterministic automata ≅[𝔹, Set]: 🤩
Effectful automata≅[𝔹, Set_R]: 🤮
(Set_R is the Kleisli category for an accessible monad R : Set -> Set. For example, R may be the finite powerset monad; in this case the automata are nondeterministic automata)
Throwing in a bit of effects seems to immediately destroy my topos-theoretic understanding of automata...

2025-03-15 13:07:13 UTC

- reply

❤️ thanks!

2025-03-15 12:29:55 UTC

- reply

Sounds interesting! I'd like to learn more about Conway theory. Could you please give me some pointers? Conway's too famous to search... (or maybe it's google being trashy nowadays) 🙈

2025-03-15 00:12:18 UTC

- reply

Conversely, given a presheaf \(F : \mathbb{B} \to Set\), we can construct a deterministic LTS with states \( \{(b, s) \mid b \in \mathbb{B}, s \in F(b)\}\). The coalgebra map for every state \((b,s)\) can be defined using the information in \(b\) and \(F\).

2025-03-15 00:12:11 UTC

- reply

For a fixed set \(\Sigma\), let \(C : Set \to Set\) be the functor \(2 \times ({-})^\Sigma\). A \(C\)-coalgebra \(S, c : S \to C S\) is exactly a deterministic transition system: every element \(s \in S\) is a state, \(\pi_1(c(s))\) tells us whether \(s\) is an accepting state, \(\pi_2(c(s)) : \Sigma \to S\) tells us the new state for each input \(\in\Sigma\).
Let \(C_*\) be the cofree comonad over \(C\). An element of \(C_*1\) is an infinite \(\Sigma\)-branching tree with every node labelled by 2. Such a tree should be thought of as a "behaviour" of a state s in a deterministic transition system — it tells you starting from this state s, after making a series of transitions, whether you are still in an accepting state. For every coalgebra \((S, c)\), there is a map \(\mathit{unfold} : S \to C_* 1\) that "unrolls" every state to its behaviour.
Define category \(\mathbb{B}\) to have objects \(C_*1\) and morphisms \(\mathbb{B}(b_1, b_2) := \{ p \in \Sigma^* \mid b_1 ! p = b_2\}\), where \(b_1 ! p = b2\) means that \(b_2\) is the subtree of \(b_1\) after descending along the path \(p\).
Then I claim the category of coalgebras of \(C\), i.e. deterministic LTSs, is equivalent to the functor category \([\mathbb{B}, Set]\). A coalgebra \(S, c : S \to C S\) corresponds to the functor \(F : \mathbb{B} \to Set\) sending every \(b \in \mathbb{B}\) to the set \(\{s \in S \mid \mathit{unfold}(s) = b\}\). And the action of \(F\) on every morphism \(p \in \mathbb{B}(b_1, b_2)\) sends every \(s \in F b_1\) to the state obtained by running \(p\) from \(s\).

2025-03-15 00:11:49 UTC

Wait, deterministic labelled transition systems form a presheaf category? 🤔 This sounds like a very useful fact but I haven't seen it before

2025-03-03 01:08:55 UTC

- reply

yes... She seemed to be a very firm believer in capitalism to the extent that anything that is not directly and completely controlled by private companies is bad

2025-03-02 17:46:59 UTC

- reply

I was very surprised someone who worked in academia before could think the current system is communist. Maybe she just uses the word capitalism to mean whatever she likes and the word communism to mean whatever she dislikes.

2025-03-01 00:21:21 UTC

- reply

Oh I didn't mean in a few years, and I didn't expect most Americans would change. I am patiently waiting for something much bigger (if I can see it)

2025-03-01 00:14:11 UTC

- reply

After the hypocrisy's exposed, there will be a bigger chance for a real change!

2025-02-24 14:36:03 UTC

Lovely website for our local student-organised seminar https://lapras-imperial.github.io/ on programming languages. I'm glad to see that logic/PL research at Imperial is slowly being revived. When it comes to bringing people together to *actually talk about interesting research*, sometimes a passionate student @npub19kf…3032 can be much more effective than multi-grant professors

2025-02-19 21:49:42 UTC

"Accelerating scientific breakthroughs with an AI co-scientist"
aptly named!

2025-01-21 00:50:00 UTC

The wall looks great with the light from the shiny big house behind it!
https://media.mathstodon.xyz/media_attachments/files/113/863/588/038/480/679/original/154d07f43e9db692.jpeg

2025-01-15 14:46:41 UTC

- reply

🎉 🥳

2024-12-24 04:13:48 UTC

Today I learnt: Impact Factors of journals are computed simply by the number of total citations divided by the number articles within a year. What a great metric to measure impact of journals!

2024-12-11 20:14:51 UTC

So there is not just the University of Bath, but also Bath Spa University. What's next? Bath Spa Skin-care University?

2024-11-04 17:41:06 UTC

Hard to believe more than 1000 people holding a PhD are going to compete for 10 positions (https://jrf.chu.cam.ac.uk/rf_2025/home/further_particulars/) with a starting salary as low as £23K (annual, pre-tax). 😅 And I'm going to be one of these 1000 poor people

2024-10-23 02:12:18 UTC

There must have been a person who wished to the monkey's paw "let there be only one USB port shape and make it symmetric!"
Now I have tens of USB Type-C cables that are visually indistinguishable but have different functionalities 💀 Some are faster, some can transfer video signals, some support fast charging...

2024-10-08 22:28:56 UTC

I can't wait until the day that I create the most beautiful book font and win a nobel literature prize😆

2024-09-28 01:03:11 UTC

I just put online the draft of my phd thesis [Structure and Language of Higher-Order Algebraic Effects](https://yangzhixuan.github.io/pdf/yang-thesis-draft-28-sep.pdf)
I might write a short introduction here someday, but for today let me just thank the amazing PLT online community here (and previously on twitter). I've learnt so much about type theory and category theory by just reading your toots/tweets and talking to you. Without this friendly online community, I'm sure this thesis will be much much weaker.
After 7 months of writing, my soul has been drained out by the thesis, but it has also been a very formative experience. After being liberated from the 25-page acmart template, for the first time I felt I was freely exploring my ideas without worrying about the page limit, without worrying about how to sell things to the busy reviewers. In this process many good ideas flowed out of my fingers, although they technically all could have been written two years ago! But I didn't explore them two years ago because they wouldn't fit into a conference submission! After this experience, I don't think I will be making conference submissions very often in the future.

2024-08-21 14:38:11 UTC

Haven't had some proper tea for years!
https://media.mathstodon.xyz/media_attachments/files/113/000/514/779/334/338/original/8b8c07032bab2e23.jpeg

2024-08-18 12:56:18 UTC

- reply

For me, the deal-breaker of non-Apple laptops is the unreliability of Windows and Linux desktop environments. My experience using Arch Linux (with a btrfs filesystem!!) circa 2010 is still my biggest nightmare with computers. It was like my OS could go brick after EVERY rebooting/updating. Seeing the many times that my colleagues using Linux can't connect to wifi, microphone, etc, I'm unsure the usability of Linux desktop environments has improved over the years...
Sadly it seems Apple's OS and laptops are becoming increasingly unreliable too. My top-spec M2 Macbook crashes on a daily basis unless I turn off sleeping, whereas my 2014 macbook air is still as reliable as a brick except that its hjkl keys have been completely dead and it can't upgrade to newer OSs.