唉，难怪别人说我进步慢。

我算是彻底见识了数学的『严谨』了，排除英文表达外我都无法好好地说明啥是啥了，虽然是严谨但是为什么不直接用工具来验证表达是严谨的？

技术性翻译是最难的，因为好一点的翻译都要维护名词表…… 我懒得弄了
而且我觉得我弄这些东西好没意义啊

1. 自反性 Reflectivity\\
由于 $\forall{x \in X}$，$x$ 皆在 $x_i$，所以它是易证的。 \\
2. 对称性 Symmetry\\
$x \eql y \Leftrightarrow x\ and\ y\ are\ in\ the\ same\ part\ x_i\ of\ partition\ \mathcal{P} \Leftrightarrow y \eql x$，由于不考虑顺序。 \\

这到底是什么意思，抽象都可以抽象，抽象全都不应该抽象

真应该让那些数学家好好把使用到的记法和基本模型列出来，我都没见过好好列过的

教集合论的时候就应该把逻辑连在一起对比着学，尤其是要把所有逻辑operator列成表给example

否则用讲故事、比喻的方法教也可以，数学家觉得直接套抽象问题好嘛，其实抽象问题比计算机随机生成的输入好多少？难道使用实际问题的益处不够明显？

写不下去了，XeTeX。

#math PDF 排版 postscript 打印后的版本(我也不清楚是不是，反正我不是TeX的开发者)

虽然这本书《AATA(Abstract Algebra — Theory and Application)》看起来对计算机科学比较友好（我非常吃惊地发现里面的数学都是魔改过的…… 虽然数学本身就毫无规范可言）

（说起来，虽然数学本身毫无规范可言，nm, ij, xy, abc, fgh 还是很通用的？）

但是，我觉得要想好好理解一本外语书的内容，首先我得翻译它……

而且，逻辑、范畴论、偏序理论什么的东西，难道你编程、算法都不会去讨论这些哲学的东西能有什么好效果？它们可不是一般的抽象
就像喝茶一样，不到那个年月悟不出其中的内容，实际上悟出来了又怎么样…… 还是数学证明 我还是愿意先继续写点 for (c1 in up) if (up[c1] == c) up[c1] = up[b]; 那样别的东西，现在时间很紧，很多函数库待写，真的抽不出时间去学哲学，学机器学习都比学哲学好啊

范畴论装X指南 Monad 的那个 eta :: a -> t a、mu :: t t a -> t a 开始看起来很高大上，其实就是 (_ :: List a -> List a) = mu . ((fmap eta) :: List a -> List (List a))，居然就是一个 wrap 一个 flatten
可是即便是这样又有什么用？我还才疏学浅，实在领略不出其中奥妙，大概它们被造出来就是为了解决它们存在的时候可以提出的问题吧，emmm。

连《范畴论装逼指南》都没有讲得很好，然后某JS讲的就太偏差了

总之就是工程界（即便是程序表述这种领域，编译器后端）很少使用，而使用到则更多是逻辑证明的问题，虽然这类问题也很重要（并且有自动化的解决方案）但一般来说用于程序变换优化效果其实不咋样（可想而知我们编程的时候能做多大程度的[程序员弱手动优化的]串行计算呢？经常是存储和控制流上面的问题）

我真不知道那些数学证明应该怎么解析了，怎么越看数学越感觉它不够规范…… {C} 都只能以 { x: x is complex } 的形式定义，可是 { a| a > 1 } 里的 mid 又去哪了，这个 (:) 是 where 的意思可是 where 又是什么意思，|又又是什么意思…… 头疼数学啊

所以我觉得先造一门语言更加重要，而目前我还是有很多程序需要写的……

TeX的开发者是算法大佬文学编程大佬Donald Knuth

我来讲一个笑话：

typealias Predicate<T> = (T) -> Boolean
interface Set<in T> {
  operator fun contains(elem: T): Boolean
  fun union(other: Set<T>): Set<T> = object: Set<T> {
    override fun contains(elem: T) = elem in this@union || elem in other
  }
  fun insect(other: Set<T>): Set<T> = object: Set<T> {
    override fun contains(elem: T) = elem in this@union && elem in other
  }
}

class LogicalSet<in T>(private val predicate: Predicate<T>): Set<T> {
override fun contains(elem: T) = predicate(elem)
override fun union(other: Set<T>) = (other as? LogicalSet<T>)?.let { LogicalSet(predicate orStmt other.predicate) } ?: super.union(other)
override fun insect(other: Set<T>) = (other as? LogicalSet<T>)?.let { LogicalSet(predicate andStmt other.predicate) } ?: super.insect(other)
}

不一定能编译，所以说是『笑话』


提示两点：

(1) 为什么 not (p or q) 能够推出 (not p) and (not q)
真值表！
不过也可以这么理解： p, q elementof (true, true),..., (false, false) and nexists true. {p, q} => (p, q) = (false, false) => (not p) and (not q)
说白了还是真值表……
就是说 exists true. {p, q} 的逆命题 nexists true. {p, q}，我们知道 p, q 不是 true 就是 false（所以非true的case我们知道肯定是false）
排除集合 {true} 的集合 {true, false} 就是梭 all false. {p, q}

(2) 对称性(symmetric) 和交换律(commuative) 有啥区别
一般对称是指逻辑运算符上的、交换律是指所有运算符上的……

那个 ADT Stack 版本的算法的错误找出来了；是左右结合性没弄好的问题，也就是说递归没有仿造完全

事实证明，ADT 版本可以做到更高的健壮性，不会随便 Stack OOM，可是正确性……

systemStack: 20 reports
of: 12.580254ms, 529.422micros, ...
min=129.954micros, max=12.580254ms, mean=824.48265micros, std=2.6990074188995345ms
ascending: 129.954micros, 132.066micros, ...
25%=135.936micros, 50%(median)=154.33micros, 75%=217.637micros

AdtStack: 20 reports
of: 2.592621ms, 694.436micros, ...
min=194.401micros, max=4.149009ms, mean=625.55215micros, std=958.3029449019385micros
ascending: 194.401micros, 194.551micros, ...
25%=218.736micros, 50%(median)=291.062micros, 75%=440.197micros

Nashorn JS: 20 reports
of: 71.968035ms, 4.155004ms, 3.591066ms, ...
min=2.019314ms, max=71.968035ms, mean=6.260406349999999ms, std=15.103676630348096ms
ascending: 2.019314ms, 2.074786ms, 2.077331ms, ...
25%=2.128427ms, 50%(median)=2.39595ms, 75%=3.076965ms

—
『高性能』实锤了 😂
本来我还打算骂它一通的呢
其实『高性能』的是比 Nashorn，哈哈，这么比有点太过分了……

我花了断续两天时间，结果在输入纯中缀链达到 7KB 的程度上，不考虑构造集合对象的时间，也只是比 use system stack 的极端情况快那么一点点而已 😂
太过分了。
我多写了10行代码，回头我就给它删掉算了

#Kotlin 这是属于比较逗逼的情况 utf16Size*(16/8)/1024

这个方差是属于比较感性的情况，虽然看完数学公式我根本无法把 Sigma 1/N 和 sumBy /size 对应起来，即便代换一下就是我也不知道1还有如此妙用，因为我无法分清它是Real(R, rational)呢还是Integer(Z)呢……都一样吧呵呵

emmm
\sqrt{\frac{1}{N} \sum_i^N{(A_i-mean(A))^2}}
where N = card(A)

这是开始写错但始乱不终弃的case，多亏我看不顺眼逻辑不通畅函数写一半的东西，虽然还是很不顺畅，以至于我以为我连逻辑基础都没有了。

真想早点睡…… 不得不先带头谈谈学校里打算谈的事，虽然
改天我要不要回顾一下之前的历史？

我果然还是进步得太慢…… 最近也才开始看得懂《编译原理实践教程》（指USTC资料，虽然我不是很看得上）和《深入分析GCC》

一般来说， #school 里我记录的笔记（很多是比较逗逼的，比如上面的修错，虽然修久了我会发现我连逻辑推导都做不到了）都会讲一遍
没做笔记的不会讲。

首先当然是 #book 好书（文）推荐
—
《她是龙》小狱
|Telegraph
注：使用 online OCR 字符识别，哦不，没找到多好的工具。
https://ocr.wdku.net/#
技术还是 Google,MS 家强
排版还要花时间，暂时出不来

他不知道，这个世界没有人有名字，所有人都只有印着一大堆标签的别称。他更不知道的是，其实故事以外的人也是这样的，即便是每个人都有着属于自己的名字，可还是得在脑门上贴上无数的标签过活，他们看别人的时候离开这些纸条就会失去判断力，却埋怨别人不肯了解自己的内心。
—

自动粘滞(sticky)Regex 有点牛逼啊，我之前的都是那些一匹配啥都匹配的，也不可能用 ?! negative lookahead 断言

虽然我连 GAWK 都不会用
UPDATE: 上面的 "(.*)" 应改成 "(.*?)"、<*?> 和 <*> 的意思不一样，它表示『最小匹配』…… 也就是说 takeUntil 到下一项 '"'; 以上 Regex 会把 <abc><123> 弄错，没注意到是因为 <.> 不匹配换行符，感谢细心观众 https://t.iss.one/bystartw_tw. refs

/(.*)。$/ [$1。\n]
/^(.*)：『(.*)』$/ [$1：『$2』\n]

/regex/ [replacement]
替换一下再修改处理出来的Markdown版本