这里的条目一般都是不适合成文的小段证明或者算法，其中有些和我的研究方向有关，有些则纯粹是兴趣。因为我个人不喜欢TeX，所以都是HTML页面。视具体情况，可能会用英文。顺便说一句，虽然标题写的是「算法与证明」，但这两者其实是一回事。
下面是一个简要的目录，我尝试着在标题中把证明或者算法的内容简短地表达出来，但看上去这是一件相当困难的任务。
线性代数
形式语言与自动机
- MFA(memory finite automata)变体与拓展正规语言(regex)的性质
- AFA(alternating finite automata)与DFA等价
- variable-star-free regex相交的非空性判定算法
- 带regex约束的straight line word equation至少是PS的
- 用2FT(two-way finite transducer)编码带捕获与引用的replaceAll(半成品)
- 用NSST(nondeterministic streaming string transducer)编码带捕获与引用的replaceAll
- NFA在NSST作用下的原象(pre-image)的构造算法
- NSST约束总结
- NFA在FT作用下的象(post-image)的构造算法
- 正规语言在NSST/PSST作用下的post-image不是正规的
- 构造确定型Büchi自动机的补
- 任何非空的Büchi自动机的语言中总存在一个lasso形的无穷字