艹，才想起来很多脚本语言里数值类型混乱不堪；Ruby 曾经还分过 Fixnum 和 Bignum，肯定是这些在诬陷正直的 JVM。

只好解析成 AST 的形式由我自己来鉴定真伪了……

这个时候就需要鼓吹我们正直的 JVM、CLR、C++，不与一些辣鸡脚本语言同流合污、随手胡乱对待数值类型。
明明写着看着是 1，其实是 1.0 的这种语言和辣鸡 JavaScript 是没有灵魂上的区别的。

……可惜正直的语言还不如 Python3、PHP 火，可惜啊可惜

typealias Atom = Int

这时候就体现你用 Typealias 的一个好处，就是想用用、不想用随时换，不会找不到该改哪

算法请参照：
https://github.com/duangsuse-valid-projects/three-kt-files/blob/master/src/commonMain/kotlin/Calc.kt#L103

跑分实现在：
https://github.com/duangsuse-valid-projects/three-kt-files/blob/master/src/jvmMain/kotlin/BasicBench.kt (lib)
https://github.com/duangsuse-valid-projects/three-kt-files/blob/master/src/jvmMain/kotlin/CalcBench.kt

#Telegram #dev 挺好啊，比那些不用框架的强多了

其实啥时候 Harray Ying 为什么不去学学范畴论呢…… 最近偏工程的事情很多，没时间看这篇文章了……

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) 有啥区别
一般对称是指逻辑运算符上的、交换律是指所有运算符上的……