Recently, I have been working on Abstract Algebra which has derived category theory and exposes its strong relation with computer science.
其实就是范畴论的…… 看到 Log 我第一时间想到的是对数(logarithm)……

难怪，代数的抽象
为了确认 title 里 Log 的含义其实我还是忍不住打开看了，那就顺便翻译一下。

Abstract Algebra Learning Log - Preliminaries by Harry Yin
《抽象代数》学习笔记 — 预章
—
Recently, I have been working on Abstract Algebra which has derived category theory and exposes its strong relation with computer science.
最近我在学习抽象代数，自它派生出了范畴论，它与计算机科学有很大联系。
—
Brief Introduction
简要引言
—
All these learning logs will be based on one online and free textbook (2019 Version), naming Abstract Algebra which is licensed under the GNU FDL.
This learning log is basically in two parts, one is my own understandings or complementions to some of the parts, another part is my own answers to part of the Exercises section in the end of the chapter. And succeeding learning logs will mainly based on this form too.
First part may contain works in the textbook itself, therefore, this series of posts is licensed under the GNU FDL either.
这些笔记都是基于一个免费的网上教材(2019版)，它以 GNU FDL 开源，名字叫《抽象代数》Abstract Algebra。
我把笔记大致分成了两部分，一部分是我自己的理解和补充，另一部分则是我对书中节末练习的解答。
后继的学习笔记也会基本保持这个形式。
第一部分可能包含教材里既有的内容，所以，这一系列文章也以 GNU FDL 许可证发布。
—
Understandings and complementions to textbook
部分一，对教材内容的理解和补充
—
Page 6, Proof of De Mogran's Laws
P6，De Mogran 定律的证明
—
1. $(A\cup{B})' = (A'\cap{B'})$
We define two statements, $p$ and $q$, representing $x\in{A}$ and $x\in{B}$ respectively.
statement $x\in{(A\cup{B})}'
\Leftrightarrow{\neg{ (p\lor{q}) }}
\Leftrightarrow{ (\neg{p}\land{\neg{q}}) }
\Leftrightarrow{x\in{ (A'\cup{B'}) }}.
$ (The relation between $\neg{ (p\lor{q}) }$ and $(\neg{p}\land{\neg{q}})$ can be deduced by simply enumerating through all the possible values of $p$ and $q$, e.g. $true$ or $false$ for statements).

Thus, $\forall{x}\in{(A\cup{B})'} \rArr{ x\in{ (A'\cap{B'}) } }
\rArr{ (A\cup{B})' } \supset{ A'\cap{B'} }$. Conversely, we can prove $(A\cup{B})'\subset{A'\cap{B'}}$.
{— 注：原文使用 Emacs org mode 排版，这里 TeX 上稍有修改，原文采用 GNU FDL 许可证 —}

…… 算了这么多数学公式，我干脆用 TeX 排版了发吧

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

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

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

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 断言