音乐是生命的哈希
分类: 音乐 / 标签: 思考 / 字数: 2727
在开始说明为什么音乐是生命的哈希之前，请允许我啰嗦一些类型系统的事情，虽然这可能和标题毫无关系。
类型系统
lean4是一个有意思的语言，其中的mathlib完成了很大一部分undergraduate的数学论述。但是使用的不是集合论语言，而是类型论。lean4所使用的类型系统背后的类型论是对以集合论为主要语言的现有数学的一次挑战。集合论中大部分的定理可以用类型论描述，而类似于罗素悖论的问题被类型系统巧妙避开。这也是计算机可以用于实现辅助证明的原因。虽然Algol60之后许多语言也都内涵类型系统的设计概念，但lean4确实是头一个以彻底描述现有数学体系为目的而设计的语言。
类型系统如何正确构造
类型系统的正确性是由柯里-霍华德同构保证的。简而言之，类型=命题，程序=证明。当你在用程序定义一个个类型的时候，就等价于在证明一个个命题。也就是说如果我们想从逻辑上证明一个命题，就只需要在类型系统中用程序构造出一个类型的实例。而这个实例将成为类型本身的证明。（可能我的表述有循环的嫌疑，但目前来说可以忽略正确性这件事，让我们关注类型系统的类型如何定义才是正确的）
类型直接通过规则来定义：（引用自香蕉空间）
- 规定什么样的表达式对应某类型的实例, 相当于给出类型的生成元, 这对应构造规则;
- 规定什么样的表达式能使用某类型的实例, 相当于给出它满足的万有性质, 这对应消去规则.
为什么音乐是生命的哈希
现在我们终于可以开始讨论为什么我觉得音乐是生命的哈希这件事情。
- 规定：该语境下，人类活动->音乐对应人类情感活动的示例，给出了人类情感活动的生成元。
- 规定：该语境下，音乐×音乐->mixed音乐可以使用人类情感活动的示例，给出了消去元。
音乐的混合形成了人类情感的混合，事实上，一段好的音乐也往往是多个人的情感混合。即使是一个的音乐作品也是一个人在不同状态下的情感混合。古典乐中的乐章，现代音乐中的段落结构都揭示了这一点。
而一段伟大的音乐，则必然源于一个使用了消去元的音乐，即不同情感的混合。
lean4（抱歉我又提及）中每一个类型都有一个唯一的数字编号。其实生命最不需要的就是编号（这几乎在说明你是和其他人一样但独一无二的废话）。一个人要认可自己的定位和编号，至少需要一个可以运算的方式来实现自我探索。虽然他们可能会收敛，但每个人收敛前的路径是独一无二的（真是悲喜交加的描述）。
我认为以音乐作为类型的根本不同在于，这是一种序列化的数字，而且人体直接参与运算而依赖于计算机。不是对每个类型仅仅用一个数字标识。虽然类型直接可以通过运算来互相转换，但如果我是一个为了设计用来描述个人类型的系统，更有意义的表达是一串数字，而不是一个数字。 一个数字，每个人都不同。一串数字。几乎每个人都有共同点。音乐，提供了稀疏空间下的个人独特标识数的运算，（可以认为是大质数的某种算法）。
身份证已经做到了给每一个人一个编号，方便了行政事务的开展和管理。定义了亲属和户籍体系。 而well-develop的社会，应该提供除唯一标识外丰富的运算空间，就像比特应该应该在内存中组成软件应用。人类的协作才能迸发出魔法般的力量。可惜的是，我看到的多数还是仅仅重复的编号，而没有一种真正的运算贯彻始终，这样的实体终究会因为编号的消亡而同步消失，因为几乎只以为人编号而生。可能金钱是这些运算的产物。但是金钱的分配，显然对某些计算是有偏好加成的。虽然音乐也是如此。但人类的货币系统多次重置，我们几乎无法理解前货币系统的情形，但还好我们依然对古代的音乐也有某种统一的认同。音乐，比金钱更加忠实地记录了一个生命的当下状态，并且是本质上不可简单消去，只能继续混合。
一些其他的比喻
如果是两个人贡献两袋钱，混在一起后几乎没法分辨。如果把两个乐谱相互混合，甚至乐段，甚至乐句。从开始的清晰分辨到最后的浑然一体，带来的欣快感显然是截然不同的。这内涵了一个高尚的主题（人类是可以通过努力打开自己而互相理解的）
或许这是一种比区块链（实体间默认相互不信任而设立的信用体系）更加高明的算法。音乐让相互的认证成为乐趣，而非单纯的成本。
后记
深度思考的产出和随意表达的区别 就像gpto1和gpt3.5 的差别
以上内容使用iPhone在深夜使用termius/nano竖屏编辑。这是我满意的文本。 以下的内容使用Y9000X在头脑混乱时在vscode上编辑。 我其实不满意这样的文字。 纯文本的魅力就在于强迫用符号来思考强化了整体感，连续感。 追求打字速度WPM前更应该强调的是深刻的思考。 从容不迫很重要，这几乎是一切深刻思考的前提条件。 而我此刻应该知道为什么有些创业是昙花一现，因为焦虑深深藏在人们心底。愿世界没有负债，狡诈和欺瞒。
这些是真的弃用内容
音乐是更大语境下的类型系统，不精确，但时空跨度更大。毕竟在身份证没有出现的时候，那些渴望交流的人们就在使用音乐。 应用的范围不限于伤痛，回忆，欢聚等一系列社会活动，内涵地理，历史，文化等信息。所有人聚在一起计算了一个不会碰撞的哈希。
主观角度讲，人类恨不得把所有东西都分类个遍，用语言传承所有经验。但如果是一个人，能深入的命题是少数的，能做出的证明也往往以生命为笔墨，岁月为纸张。一个有限的人生，选取有限的命题，做出有限的证明。千古寸心事，欧高黎嘉陈。
人以类聚，物以群分。对于很难逐个了解的个体，聚类是为数不多的方式去理解他们。假如有些事情对我们很重要却难以了解，聚类是必要的手段。比如人们想数一数星星的个数。如果时机不对太阳高悬头顶，寥若晨星，应是在夜半三更，才见得到浩如星河，大珠小珠落玉盘。
如果生命充满阳光，方向是明确的自是可以嬉戏，若要在黑暗中踱步，则要看各自本命星的指引。听萨满度天意，看诸葛夜观星，族群以一种奇怪的方式围绕在智者的周围。人们燃起火堆，借用太阳千万年前的光，在黑暗中思索同样千万年以前来自星星的光（也可能是引力波）。
以上只想说明，聚类只有在丰富的内涵和主题有待进一步探讨前才有必要。聚类是音乐本身的意义，因为他是一些碰撞了的哈希。如果人们不再因为音乐而碰撞，那么人们在旷野，或者人们在远离，或者运算本身就在减慢，人们开始重新思考过往的哈希函数是不是碰撞太多而淹没了太多的个人声音。什么时候可以构造一个全新的哈希函数，用音乐吧。这是社会结构合理的最好的证明。
预言一则
闻风动，闻鸡舞。优秀的听觉和伟大的直觉是一个乐者的素养。当金丝雀停止唱歌，是因为它知道这个时候用心听更重要。 黑夜来临了。危机像黑夜，让人们从耀眼的日光中重拾过往的星图，重新思考千万年前来时的路。不论有没有光，声音还是可以让彼此靠近，然后生命延续。
证人自证，清者自清。至于命题和类型本身，生命自有解答，命中自定也。