Lîm Tsú-thuàn Posts Notes Projects Talks Site Roll

Person. Lîm Tsú-thuàn [dannypsnl]

I study programming language theory and system software. I have interests include fiction, history, and math.

Mail me: inbox@dannypsnl.me

Backlinks

Theorem. Left/right adjoints preserve (co)/limits [0IGM]

Proposition. Integer with arithmetic progression topology is not locally compact [1OV1]

Programming 生涯回顧 [2020]

2025 年 [2025]

2026 - Week 4 [2026-W4]

2026 - Week 5 [2026-W5]

presheaves exponential 同構的推導 [21ME]

視Profunctor為Hom functor的generalization [2323]

Definition. Boundary and interior of $\Delta^n$ [23BZ]

Definition. Finite type and finite $\Delta$ -complex [2A0Q]

Proposition. Natural transformations pair of adjunctions [31KN]

語法作為一種檢視方式 [32PV]

How to install hut (CLI tool for sr.ht) [4V6X]

以 effect 為合約：用 effect system 解耦遍歷演算法與存取點 [4Z05]

Example. Limit與colimit [50LK]

Definition. Hopf bundle [5A3M]

Definition. Dimension of a $\Delta$ -complex [5MJV]

選舉演算法 [5X6Y]

Example. 程式作為natural transformation [631K]

Example. frame 的 oppsite 不必是 frame [6CPF]

Log Replication [6PAS]

Proposition. For any sieve $R$ in $J$ , bigger sieve $S \supseteq R$ also in $J$ [7R33]

Definition. Category的另類定義 [7U86]

Definition. $n$ -th homology [7XRX]

Definition. Site [84R3]

部落格作為一個fediverse帳號 [8664]

Definition. Skeleta [8CBL]

Lexical scoping與dynamic scoping的對偶 [958P]

用Adjunction構造Monad [9XIR]

在 guix 上用 patchelf 設定正確的連結器 [A05P]

Non-linear spine [A17O]

Types on Scott's graph model [A3Q8]

To CPS or not to CPS：編譯理論之爭 [ASEH]

Definition. Riemann curvature tensor [B2D1]

安裝 Guix [B4OI]

Property. Maximality axiom [BEIE]

善與善的對抗 [BF9W]

Proposition. natural transformation可以視為end [C07X]

模擬選舉演算法 [C6J7]

Brid.gy cross-post 的使用方法 [CIEP]

violet literate programming 支援 [D1AX]

Definition. $n$ -th simplicial homology [DDAF]

記錄一下 zoxide 在 fish 裡要怎麼設定 [E891]

Basic Subtoposes of the Effective Topos：Proposition 1.2 [ECDG]

Definition. Boundary homomorphism (also known as differential) [EFJB]

從公理系統到natural deduction [EGRZ]

RSS in emacs：elfeed [EHWW]

Proposition. 微分方程式 $x' = ax$ 解形式一定是 $ke^{at}$ [EMGT]

Pattern Unification演算法理論部分 [F6C1]

Definition. Sieve [FG8Y]

Theorem. Computably (recursively) inseparable sets [FW2E]

Property. Pullback stability [FXZI]

Structural Interface 的設計限制 [G9M2]

Functor與Natural transformation [GC75]

Rakka 使用初體驗 [GMYW]

Core concepts in Simplicial Homology [GYD9]

Counterexample. 關於sieve的組合封閉 [HZSP]

Normalization 問題 [I3KA]

什麼是CPS？ [IAVH]

Definition. Maximal sieve [IGSL]

violet 的一點新進展 [ILIG]

3-sphere $S^3$ (群 $SU(2)$ ) 跟 $\mathbb{R}P^3$ [JRT2]

Osiris: replicated logs [K4RQ]

Definition. $n$ -simplex of a $\Delta$ -complex [K5BK]

Theorem. Vaughan (1977) [L3M8]

Lemma. First homology of a short chain complex over a PID [LNMK]

J-sheaf 的直覺 [LPLF]

Property. Transitivity [MACB]

部落格問題挑戰 [MNIW]

Definition. Chain complex [O7WN]

常見的組合子 [OQKM]

Definition. $n$ -th simplicial chain module and $n$ -chains [Q5M5]

Proxmox與Intel I-219v [RKU5]

When a map is an equivalence? [RNNM]

正確處理單位的算術系統 [S20M]

Colimit作為Coend [S2W7]

用 effect system 實現直釋器 [SW6P]

Frames與complete Heyting algebras不同之處 [TJ21]

Adjunction [U27X]

現代 - 商業、科技與政治交織的空間 [U5YI]

JIT: Write XOR Execute policy [UIC7]

Lemma. We have $\partial_{n-1} \circ \partial_n = 0$ [URFG]

具體的 Sheaf 以及如何得到 ringed 與 locally ringed space 的定義 [UXEP]

Status of the smooth rectangular Peg problem [VEYQ]

induction principle 的生成 [VGOA]

Lie 群的意義 [VQ6V]

用 effect handler 實作 parser combinator [VSMS]

日本北陸之旅 2025/10 能登 [VW5V]

Definition. Delta complex [WBTD]

代數幾何：視 base ring 的元素為函數 [WYCP]

轉移控制權作為 effect：coroutine 與排程器 [Y7OR]

關於漫畫epub [YSRC]

MacOS網路雜記 [YUFB]

色彩繽紛的範疇論 [Z00L]

Interchange Law [ZB1T]

Definition. Grothendieck topology [ZD97]

Definition. J-sheaf [ZUQN]

Dependent Pattern Matching [ag-0001]

Intrinsically typed term [ag-0002]

Dependent equality in dependent type theory [ag-000C]

Streams and finite observations [ag-000D]

旋轉矩陣的 product 是給定角度的相加 [ag-000E]

W-type (the type of well-founded, labelled trees) [ag-000I]

M-type (the type of non-well-founded, labelled trees) [ag-000J]

Eliminator [ag-000K]

NOTE: Explicit Weakening [ag-000S]

SOGAT of type theory with $\Pi$ -types, a Tarski universe, and natural numbers [ag-000W]

FIXME. SOGAT of type theory with erasure with $\Pi$ -types, a Tarski universe, and natural numbers [ag-000X]

Model mapping TT to untyped LC [ag-000Y]

單位乘法通用化 [ag-4AP1]

Polymorphic types [ag-8LAS]

Regular type的導數是它的one-hole context [ag-93PB]

Example. CwF 標準案例 [ag-A3OG]

PER as types: dependent product & sum [ag-BQXB]

用函數表示 [ag-FKSF]

PER: 正確處理 exponentiation [ag-KA1U]

邏輯公理系統 [ag-L7FN]

natural deduction [ag-M036]

PER as types: sum [ag-MM24]

PER as types: product [ag-NN5N]

從構造就拒絕錯誤 [ag-SPBG]

Partial Equivalences as Types: First attempts [ag-U75Z]

為什麼UIP跟univalence不能並存 [ag-WN45]

Local operator 與 Nucleus [ag-X72H]

對 List 取 quotient [ag-YGG9]

Tool. agda 的開發工具 [agda-0001]

Contribution. agda-mode-vscode [agda-mode-vscode]

agda-tree [agda-tree]

Algebraic Graph [algebraicgraph]

bib2tr [bib2tr]

部落格遷移 [blog-0000]

Reference. clojure isn't lisp enough [clojure-isnt-lisp-enough]

Reference. closure conversion [closure-conversion]

polymorphism 的執行期設計 [cs-0000]

什麼是啟動編譯器？ (bootstrap compiler) [cs-0001]

運作原理 [cs-0002]

用普通的可執行檔可能不是一個好主意 [cs-0003]

何謂 elaboration？ [cs-0004]

Macro system [cs-0005]

什麼是 subroutine？ [cs-0006]

作業系統的行程排程 [cs-0007]

Algorithm. Mark sweep GC [cs-0008]

Parser combinator：文法規則就是組合子的運用 [cs-0009]

Definition. 左遞迴 [cs-000A]

Definition. Parser combinator [cs-000B]

消除左遞迴的方法 [cs-000C]

擴展到 operator 優先序問題 [cs-000D]

處理優先度相同的運算子 [cs-000E]

Appendix. 其他 expression combinator [cs-000F]

racket 中的有界續延如何實作 effect system 的功能？ [cs-000G]

實現 resume [cs-000H]

Algorithm. 君主選舉 [cs-000I]

How to parse expression with the parser combinator [cs-2IWA]

Definition. Computational adequacy (of semantics) [cs-H4U2]

closure conversion [cs-N1SG]

魔物獵人荒野充能斧操作筆記 [game-0000]

Reference. General Recursion [general-recursion]

第一日（飛機/住宿） [hokuriku-day1]

第二日（能登第一日） [hokuriku-day2]

第三日（能登第二日） [hokuriku-day3]

html2scrbl [html2scrbl]

html2tree [html2tree]

Lîm Tsú-thuàn [index]

Contribution. llir/llvm [llir]

Reference. macro as type [macro-as-type]

Contribution. magic-racket [magic-racket]

MaJu [maju]

Soundness and completeness [math-0000]

無外部空間下如何考慮幾何空間的測量？ [math-0001]

Gödel incompleteness theorem 到底證明了什麼？ [math-0002]

Theorem. Gödel incompleteness [math-0003]

Definition. substitution [math-0004]

Lawvere's fixed point theorem 的陳述與應用 [math-0005]

Theorem. Lawvere's fixed point [math-0006]

Example. 應用到 lambda calculus [math-0007]

Example. 應用到 Cantor's theorem [math-0008]

Lemma. no point-surjective morphism [math-0009]

Definition. point-surjective [math-000A]

Theorem. A space is Hausdorff iff its diagonal map is closed [math-000B]

Transformation induced dual basis [math-000D]

understanding $F$ -algebra [math-000E]

Definition. $F$ -algebra (algebra for an endofunctor) [math-000F]

Definition. category of $F$ -algebras [math-000G]

Theorem. Lambek's [math-000H]

catamorphism [math-000I]

anamorphism [math-000J]

Theorem. Borsuk–Ulam [math-000L]

Lemma. [math-000M]

Definition. Natural Transformation [math-000N]

Definition. Homotopy extension property (HEP) [math-000O]

Definition. Pfaffian [math-000P]

Determinant 的意義 [math-000Q]

Definition. exterior algebra [math-000R]

Naturality cannot be given by a family of isomorphisms [math-000S]

My exploring Borsuk-Ulam Theorem [math-000U]

Determinant of Skew-Symmetric Matrices [math-000V]

Proof. Using the properties of matrix column operations [math-000W]

Counterexample. $p$ no need to be identity when $p \gg f = f$ [math-000X]

Proposition. Right adjoint fully faithful <=> counit is isomorphism [math-000Y]

Definition. Immersion, embedding, and submanifold [math-000Z]

Definition. Generalized element [math-0010]

Internal language 之用 [math-0011]

Definition. prime ideal [math-0012]

Definition. maximal ideal [math-0013]

Definition. Jacobian matrix [math-0014]

$\R P^1$ is diffeomorphic to $S^1$ [math-0015]

The Basel problem with trigonometric Fourier series [math-0016]

測地線方程組推導 [math-0017]

Definition. 切向量場沿曲線平行 (parallel) [math-0018]

Definition. 流形上的微分式 [math-0019]

Presheaves, Yoneda embedding, and Yoneda lemma [math-001A]

Lemma. Presheaves are colimits of representables [math-001B]

Definition. The category of elements [math-001C]

Definition. Diffeological space [math-001D]

Formal Topology in UF [math-001G]

沒有內接矩形的平面曲線 [math-001H]

Simplex category 與 face maps [math-001I]

具體的 simplicial set: Torus [math-001J]

Definition. Gödel encoding [math-030A]

Proposition. If two computability models are equivalent, then decidable equality exists for one iff another has one [math-0L0G]

為什麼需要 domain theory？遞迴的數學表示 [math-28UX]

基本的約束 [math-2C9J]

Theorem. The field of fractions is a torsion-free module [math-3E35]

Definition. Models of Turing machine [math-3XVQ]

Example. Every discrete poset is a DCPO [math-4J1T]

Proposition. $U_3$ is open [math-4M36]

Definition. Total computability model [math-6G74]

Proposition. nilpotent maps form a prime ideal [math-6W2V]

Leibniz product rule [math-7EIK]

Definition. Scott open [math-7H66]

Definition. Scott topology and continuous [math-8KRP]

Definition. Directed subset [math-980H]

Definition. Ringed space [math-9M06]

Theorem. lambda 通過 K1 再編碼 lambda 不能從 lambda 的 identity 得出 [math-A9X1]

Theorem. Kleene's s-m-n [math-ADUE]

Definition. Locally Ringed space [math-AYGI]

Lemma. Partial combinatory algebra沒有decidable equality [math-BF7A]

Theorem. $\text{Frac}(A/x) = \mathbb{F}_2$ [math-C8CK]

Theorem. Adequacy (充分性定理) [math-CFN7]

Definition. Computability model [math-DO60]

Definition. Computability model of lambda terms [math-FJTC]

Definition. Partial applicative structure [math-FNBV]

Definition. Track [math-GM4F]

Definition. Covariant Derivative (Linear Connection) [math-HCIJ]

Corollary. About Boolean ring [math-HS0H]

Definition. Continuous (topological) [math-HSXV]

Theorem. Kleene's first model 與 Closed lambda terms 不等價 [math-I098]

Definition. The category of assemblies over a pca [math-I7R9]

Definition. $\mu$ 的解釋結果 [math-IG9K]

Definition. Holonomy [math-L2W1]

Definition. Partial equivalence relation [math-L43K]

Theorem. Prime ideals of $A$ are also maximal [math-LRSC]

Proposition. (cpo)-continuous function space is a cpo [math-LVSY]

Lawvere-Tierney topology [math-MRL4]

Definition. Partial combinatory algebra (pca) [math-NYGO]

Definition. Preorder [math-O6C8]

Definition. Weak product [math-O7B4]

Definition. Higher-order structures and (computability) models [math-ONFA]

Definition. Category of DCPOs [math-P5X4]

Definition. Sheaf [math-PPAW]

Definition. Simulation of computability models [math-QAL6]

Theorem. Generalized fixed point [math-QQ3Y]

Definition. $\mathcal{C}\llbracket e \rrbracket$ 的解釋 [math-SSSU]

Definition. Kleene's first model [math-SVXS]

Definition. Weil algebra [math-T4B2]

Theorem. Premanifold 為 Hausdorff 的等價條件 [math-T4B3]

Proposition. Hom-functors preserve limits [math-TGEI]

Definition. Rules of $\mu$ [math-TMY9]

Theorem. Cantor's [math-U27C]

Definition. Real Projective $n$ -space as quotient of $S^n$ [math-UGKQ]

Definition. Partial order [math-VRM5]

Theorem. Bijection between hom-set $\text{Hom}(A, \mathbb{F}_2)$ and $\operatorname{Spec} A$ [math-W5KY]

Definition. The category of partial equivalence relations [math-W6F9]

Programming in pcas [math-WE2N]

代數幾何：非常基本的部分 [math-XGSJ]

Definition. Directed-complete partial order (DCPO) [math-XL3D]

Definition. Parallel transport [math-XU4I]

Definition. Pointed poset [math-XV49]

Definition. Typed partial combinatory algebra (TPCA) [math-Y5YD]

Definition. Assembly over pca [math-YOTV]

戴德金分割與1為何等於0.9...(無限循環) [math-YTJO]

常青筆記的困難 [note-0001]

Reference. Can this program stop? [program-termination]

Error is Value [programming-0000]

Reflection in Go: create a stack[T] [programming-0001]

fun networking: tcp close [programming-0002]

sauron supports find references in project [programming-0003]

Integrating Mathlive into editor.js and Thoughts on Note-Taking Systems [programming-0004]

Rhombus 用標記運算自動排序資料 [programming-0005]

Soufflé 入門 [programming-0TXN]

Magic in redux-go v2.1: package rematch [programming-10WZ]

How trait with lifetime can be a trouble and how to fix it [programming-B70A]

Design of Redux-go v2 [programming-BDGQ]

DPDK usertools: devbind [programming-IYOG]

Kubernetes Networking: concept and overview from underlying perspective [programming-RML7]

HugePages on Kubernetes [programming-RR5A]

The Go concurrency bug I made [programming-S0L5]

cgo can be a trouble [programming-S4P0]

DPDK -- EAL Input/output error [programming-S807]

利用參考等價性質的技巧 [racket-0000]

Contribution. racket-langserver [racket-langserver]

racket-llvm [racket-llvm]

架一個自用的Rama叢集 [rama-cluster]

redux [redux]

call/prompt [rkt-0000]

abort/cc [rkt-0001]

Continuation prompt tag 的產生方式 [rkt-0002]

call/cc [rkt-0003]

rocket [rocket]

sauron [sauron]

NixOS 需要定期清除 generations [software-0000]

XDP [software-0001]

Mastodon 私訊相比於一般通訊軟體 e.g. LINE, Telegram [software-0003]

git send-email 的設定 [software-0004]

let Racket GC manage your FFI object [software-0005]

git send-email setup with Protonmail [software-0006]

已完成的軟體 [software-0007]

TeXmacs [software-0008]

Mastodon 私訊加密 [software-3UST]

The little prover shrubbery 版本 [the-little-prover]

使用 TLA+ 的第一步 [tla-0000]

使用 PlusCal 語言 [tla-0001]

增加不變量 [tla-0002]

tr [tr-0000]

生成 embed 與 index HTML [tr-0001]

raco tr next 與使用方式 [tr-0002]

地址唯一性 [tr-0003]

數學支援 [tr-0004]

RSS 與 searching [tr-0005]

LaTeX 工作的獨立標籤 [tr-0006]

tr-notes transclude 的發展 [tr-0007]

tr/card [tr-0008]

用CSS計算nesting [tr-01YZ]

基於檔案內容判斷是否進行建置的必要性 [tr-1XYR]

Idea. Generate HTMLs for local cards? [tr-47YA]

private cards [tr-490U]

從有限元素中隨機取未使用的元素 [tr-D6VS]

Tufte風格的margin note [tr-P10S]

資料庫其實很快 [tr-QE7I]

自訂Header [tr-VGBX]

Config as code [tr-XH91]

是否發佈由設定檔控制 [tr-YGRJ]

Algorithm. Strictly positive check [tt-0000]

Why? [tt-0001]

原理 [tt-0002]

實作 [tt-0003]

Example. Not Bad [tt-0004]

Example. Loop [tt-0005]

Algorithm. Elaboration zoo 中的合一演算法與隱式參數 [tt-0006]

Algorithm. 合一演算法的過程 [tt-0007]

安插隱式參數的方法 [tt-0008]

什麼是 contextual variables？為什麼 contextual variables 是 B 與 x？ [tt-0009]

什麼是 rigid form？ [tt-000A]

Invert [tt-000B]

Rename [tt-000C]

Lambda 化 [tt-000D]

型別有多大？ [tt-000E]

型別的大小 [tt-000F]

遞迴 [tt-000G]

應用 slice category [tt-000H]

Example. 從 $1$ 出發 [tt-000I]

inductive data type [tt-000J]

分形遞迴（Tree Recursion） [tt-000K]

子類型與多型（泛型） [tt-000L]

Go 的 interface [tt-000M]

Java 的 interface 與 bounded polymorphism (bounded quantification) [tt-000N]

問題所在 [tt-000O]

Definition. Injectivity [tt-000Q]

Definition. Predicative [tt-000R]

Type system 的 Soundness 與 Completeness [tt-000S]

隱式編程：coherence 與 stability 屬性 [tt-000T]

Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics [tt-000U]

Display map category 捕捉了類型論的什麼面向？ [tt-BBGG]

NOTE: Substitution Without Copy and Paste [tt-IHCF]

Hindley-Milner type system: Incrementally build way & Make new [tt-NSSH]

Reference. types cross languages [type-cross-language]

effect system in typed/racket [typed-racket-eff]

verse calculus (redex model) [verse-calculus-redex]

violet [violet]

Example. 初步實驗的效果 [violet-0000]

Lemma. HoTT 2.1.4 [violet-EVW3]

The concept of webmention [webmention-0000]

sender view [webmention-0001]

receiver view [webmention-0002]