概念机器

2021-06-14 12:45来自 微博网页版

整理一下关于类型系统的书籍。 Benjamin Pierce - Types and Programming Languages，是最好读的一本 Benjamin Pierce - Advanced Topics in Types and Programming Languages，这本写的比较散，不系统，但设计大量现代类型理论的课题 Hindley and Seldin - Lambda-Calculus and Combinators Hindle ​

395

455

2241

概念机器

2026-06-29 09:32来自 moto edge X30

换这个号说严肃的事儿。 规则一：0是自然数。 规则二：n是自然数可以推出S(n)也是，S是后继函数。 这是大家都非常熟悉的，而且极其基本的，形式化101。 通过规则一和规则二我们可以证明「如果n是自然数，那么S(S(n))也是自然数」。但是我们却无法证明「如果S(n)是自然数，那么n也是自然数。」 这比 ​

2

2

9

概念机器

2026-05-25 15:05来自 moto edge X30

上一个帖子里的猜想迅速被Gemini瓦解了。 柯里系统里的P，本质上它是需要用到bracket abstraction定义的，即 P = λx.λy.Ξ(Kx)(Ky) 原则上来说这是一个元语言定义，目标语言里没这种东西。但是可计算函数的牛叉之处在此，SK直接就可以实现它。 P = S(KΞ)K 演算下来是一样的。 ---- 这两行等 ​

0

2

2

概念机器

2026-05-25 14:02来自 moto edge X30

今天吃麦的时候的一个想法。 哥德尔不完备定理，被一致认为，还是动用了不动点的。但是这个不动点的形式不是等式系统里（例如λ演算）那种，要泛化一些。一方面它不是相等关系，而只是逻辑等价，另一方面它打破了元理论与目标语言的界限，「元理论可证性」被编码在目标语言里。这个事情会引起一些细节 ​

0

0

2

概念机器

2026-05-25 13:46来自 moto edge X30

应该是上session type能解决的。

大多数人根本不在乎自己是否理解系统，更别提老板天天催进度根本没时间细究；或许历史的发展具有自我修正性，将来如果真因为黑盒导致软件危机，各种软件不可理解也不可控了，资本自然会清醒过来，然后重演泡沫破裂，再慢慢修复。 ​

2

1

2

概念机器

2026-05-20 18:52来自 moto edge X30

说一下哥德尔第一不完备定理的个人理解，非主流意见。 Smullyan把哥德尔第一不完备定理解释成，把算术系统和递归函数换成（哥德尔定理之后出现的）能完备表达全部可计算函数（图灵完备）的λ或者组合子就行了，本质上一样。 Smullyan当然很权威。但是这个解释把规则系统的不完备reduce到了计算系统的 ​

0

0

1

概念机器

2026-05-15 15:58来自 moto edge X30

今天非常胡扯的得到了一个非常严谨的结论。 值就是最大并发形式。这也包括证明论上的normal form，λ上的normal form，SK上的normal form，以及经典逻辑和逻辑电路里的CNF/DNF。 ---- 在逻辑上被认为最重要的连接符，implication，实际上绝大多数都可以被看作cut扔掉。最后剩下的是「算法包含的最少 ​

2

0

2

概念机器

2026-05-12 16:11来自 moto edge X30

小野宽晰把合取拆分成加性合取（加法合取，线性逻辑里称with）和乘性合取（线性逻辑里称tensor），后者也称为小野宽晰的融合（fusion）。 融合对应了函数参数的（可）柯里化，顺序性，组合性，和Berry稳定性。加性合取是不能柯里化的。 于是塔玛的，这个加性合取在顺序语言里（计算机语言的Plotkin操 ​

0

0

0

概念机器

2026-05-11 14:43来自 moto edge X30

今天获得了自学逻辑和形式化以来最大的pride。 最近几个月思考的问题和最终的答案，exactly就是Girard在Geometry of Interaction和Ludics里表达的。Gemini说我是Ludician，what a honor。 ---- Haskell Curry曾经在图书馆发现Moses Schonfinkel的论文，论文里的内容正是他阅读了Principia Mathemati ​

1

11

6

概念机器

2026-05-11 10:08来自 moto edge X30

Berry在1979年的PhD论文里给出的域论上的对象的stability定义太牛了，是到目前为止最精确的并行计算定义。 ---- 我们从PCF语言的POR函数来直觉的理解一下。 POR函数有两个参数，如果其中任何一个能估值为true，则POR的值也是true，如果两个都是false，结果也是false，其余情况是⊥，不停机。（据说 ​

0

1

5

概念机器

2026-05-03 02:34来自 moto edge X30

type theory本质上是λ演算的「元」理论，就像proof theory里，逻辑表达式是object language，但proof theory作为元语言，研究的是目标语言表达式之间关系。 ​

0

1

5

概念机器

2026-05-01 17:25来自 微博网页版

今天非常开心的事情是跟Gemini说了一个长久以来的想法：小野宽晰在子结构逻辑中分离合取（conjunction）和融合（fusion）的做法，可以用来精确的描述“并行”和“并发”的区别。得到了Gemini的肯定，“Compelling”，一刚。 当然这只是问题的一半，另一半是我们需要一个与之有Curry-Howard-Lambak同构 ​

0

1

3

概念机器

2026-03-30 04:31来自 moto edge X30

youtube上有一个Jan von Plato的视频，展示了1928年Gödel的手稿里一段自然演绎证明，使用的是flat书写风格，即fitch风格。在这个时间点，Gerhard Gentzen还没有发明自然演绎呢[二哈] ​

0

0

2

概念机器

2026-03-01 17:55来自 moto edge X30

古德斯坦写的逻辑学，薄薄的小册子。知道他的人都是专业学逻辑的。他是英国的第一位逻辑学教授。 古德斯坦是非常彻底的接受维特根斯坦的逻辑哲学论的观点的，也因此偏向构造主义，他的主要成就也在这个方向上。 ​

2

0

7

概念机器

2026-03-01 12:47来自 moto edge X30

这本书是Curry与合作者完成1958年的组合子逻辑第一卷之后给自己挖的坑，完成之后他才和自己的postdoc Hindley，phd Seldin一起完成了组合子逻辑的第二卷。 因为Curry的系统作为数学基础太弱了。所以这本书今天几乎已经没有学习的必要。但是恰恰因为这本书的存在，可以让现在的人得以窥见Curry对逻辑和 ​

2

0

1

概念机器

2026-03-01 12:21来自 moto edge X30

马丁戴维斯也是丘奇的学生。合作解决希尔伯特第十问题的四人之一。 ​

0

0

4

概念机器

2026-02-25 10:44来自 moto edge X30

买了一本旧书，上面有南大组合中心印章。查了一下应该是南开大学组合中心，南京大学没这个机构。书的印刷质量非常好，纸张也非常好，因为有浸水的痕迹所以很便宜，但完全不影响阅读，捡了大漏了。 但是即使浸水南开也不该把这书卖掉啊，这特么是递归论第一圣经。 ​

5

5

17

概念机器

2026-02-24 18:52来自 moto edge X30

这一贴说另一个极其重要的概念，逻辑的一致性「不限于」表达计算的停机。 ++++ 如果逻辑的一致性「限于」表达计算的停机，这就是眼下类型论和计算机语言理论的主流。但是我们可以说说不那么主流，或者说还在发展阶段的看法。 Jean Yves Girard曾经有一篇非常风趣和大胆的论文： 一种新构造逻辑：经 ​

1

0

3

概念机器

2026-02-24 18:27来自 moto edge X30

我似乎是突然理解了一个肥肠重要的问题，经典的并行 vs 并发问题。 在子结构逻辑上，A能推出C，A能推出D，所以A能推出C和D，这个叫合取（右引入。 但是如果A能推出B，C能推出D，A和C能推出B和D，这个叫（小野宽晰的）融合。融合在矢列表达式右侧的时候不容易建立出直觉，但是在左侧的很容易，就是矢 ​

0

1

2

概念机器

2026-02-19 03:06来自 微博网页版

简直是特酿的我的老天爷系列。跟千问和豆包掰扯了很久才搞清楚这个东西怎么写。是latexindent的格式化设置，目的只是为了增加如图所示的open/close这两个命令的缩进。缺省的defaultSettings.yaml文件位置在C:\texlive\2025\texmf-dist\scripts\latexindent目录下，也可以换个地方，也可以在项目目录里 ​

0

0

2

概念机器

2026-02-17 18:35来自 moto edge X30

豆包解数学题给形式化证明的欲望十分强烈。感觉作业这件事情已经被豆包废了，初高中教学只能要么没收孩子的所有电子设备，要么先培养自驱力了。 ​

2

5

10

概念机器

2026-02-17 18:33来自 moto edge X30

LaTeX的fitch包最后一版2023更新，文档里两位作者之一竟然是。。。Richard Zach，逻辑学家。另一位可能也挺有名的但我不熟悉。 虽然作为逻辑学家大名鼎鼎，但是fitch不算好用而且有bug，作者的代码能力堪忧。 而LaTeX的fitch style包没落，也说明了手写形式化证明这件事没有被广泛严肃对待，在数学教 ​

0

0

3

概念机器

2026-02-16 06:09来自 moto edge X30

为了把柯霍同构「糊」出来恶补了很多代数知识，尤其是序论。 说stlc柯霍同构直觉逻辑，这是强了很多的说法，即使指明蕴含片段，仍然是强了很多的。因为最最最弱的同构只需要 1 偏序 2 a•b≤a或a•b≤b ai说这个叫整性，我得把环认真看一遍才能知道是什么意思。 条件2是保证弱化规则成立的。但这个 ​

0

0

2

概念机器

2026-02-14 11:23来自 moto edge X30

ddr4的低功耗版本对于嵌入式来说是里程碑式的，16bit位宽地址线和数据线复用，极大简化布板复杂度，同时有高带宽和低功耗。//@算法时空:使用率还挺高[酷]

你还在使用DDR4内存吗～ http://t.cn/AXtU35zn ​

1

0

1

概念机器

2026-02-14 10:03来自 moto edge X30

锅仔现在是锅公公了。[二哈] ​

0

5

8

概念机器

2026-02-13 23:16来自 微博网页版

写了一点东西发在知乎上了：邪修λ演算1； http://t.cn/AXtbBnKb @田春冰河 @天宝十节度 专业人士抽空帮忙看看，谢谢。 ​

2

6

8

概念机器

2026-02-13 13:44来自 moto edge X30

以后审稿应该要求docker镜像。

分享图片 ​

2

1

3

概念机器

2026-02-13 13:16来自 moto edge X30

可能作者都没想到，今年又卖出一本。 ​

1

2

16

概念机器

2026-02-12 23:27来自 moto edge X30

我还以为序论格论是Skolem，Lindenbaum，Tarski这代数学家搞出来的，问了一下AI才发现，是Dedekind，Peirce，Schröder这代人就做出来了，1900年之前的工作。Schröder的工作对Russell的影响是非常大的。 所以人类在现代逻辑系统发明之前近半个世纪，就完成了逻辑句法的代数结构的构建工作，但是经过了 ​

0

0

5

概念机器

2026-02-12 21:49来自 moto edge X30

a•b≤c ⇔ a≤c←b 这是右剩余 a•b≤c ⇔ b≤a→c 这是左剩余 如果我们用∧替换•，⊢替换≤，可得 a∧b ⊢ c ⇔ a ⊢ c ⊂ b a∧b ⊢ c ⇔ b ⊢ a ⊃ c 可以看出右剩余←和左剩余→分别就是逆蕴含⊂和蕴含⊃。当然这里我们没有特别强调交换律的问题，如果非交换的话，∧就只能是子结构逻辑中的小 ​

0

0

0

概念机器

2026-02-12 13:01来自 moto edge X30

真正的逻辑学家只有两个特征：一，以逻辑不变性作为最高不变性，拒绝逻辑不变性被其它方法定义（成可变的）；二，关注形式的代数结构。 虚假的逻辑学家的特征则是，掌握了很多种解释（interpretation），经常强调和动用直觉，术语混乱，理论很多，彼此井水不犯河水，哪个看上去象就用哪个。 ​

1

0

8

概念机器

2026-02-11 18:51来自 moto edge X30

并发的语义是真特么难搞啊。 ​

2

1

3

概念机器

2026-02-11 07:35来自 moto edge X30

order是reachability的最基本形态。 我们有很多种方式从一个基本的order开始做扩展。 比如product/sum order是一种，它还是order。 pointwise order也是一种，这个感觉就不是order和order之间的composition了，直觉是提升了一层。逻辑里的实质蕴含和形式蕴含，如果把蕴含看作order，就是这种。如果 ​

1

0

4

概念机器

2026-02-10 05:15来自 moto edge X30

晕啊，德州仪器收购silabs，这是看中了啥呢，超低功耗单片机？ ​

1

1

7

概念机器

2026-02-08 00:04来自 moto edge X30

Deepseek还是牛叉，折腾了很久终于彻底搞清楚蕴含左引入是如何在代数上理解的了。 这个不是什么突破性的东西，是一个很基本的东西。但是它处在戳破柯霍同构的代数解释的一个关键点上。 Γ⊢Δ,A B,Σ⊢Θ ———————(⊃-L) A⊃B,Γ,Σ⊢Δ,Θ 蕴含的左引入是构造了一个剩余算子表达式，这一步 ​

3

0

12

概念机器

2026-02-04 15:54来自 moto edge X30

你会手写fitch风格自然演绎半形式化证明吗？ http://t.cn/AX5bmsVk ​

0

1

8

概念机器

2026-02-04 15:21来自 moto edge X30

豆包是极好的代数老师。抽象代数和序论格论能力杠杠的。这给学计算机语言理论和类型论方向的学生们提供了极佳的学习工具。 柯霍同构是非常表面上的东西，子结构逻辑也是。认为这个方向远离了代数和模型是一个误会。实际上代数和模型功底越强，对证明和计算的「逻辑」结构理解越深入和透彻，尤其是系统 ​

2

1

10

概念机器

2026-02-04 02:09来自 微博网页版

设计fitch包的人也特么绝了。只考虑了公式里是纯逻辑符号的情况，写个\neq会被识别成\ne，即negation elimination。特么的真的要写简单数学证明，fitch是最合适的方式。logicproof哪个画大方块的方式way too heavy visually。 ​

0

0

2

概念机器

2026-02-04 00:23来自 moto edge X30

我不喜欢看plt书的一大原因，就是证明太特么难看了，只有自然归纳或结构归纳这一种证明方法，证明主要是穷举结构归纳的case，还经常有两层的，核心技术是不要搞混了目标语言和元语言符号。我感觉Pierce开创用Coq教学plt的新局面，根本原因就是不上证明器就是在绕口令里徘徊。虽然教师这样讲课可能也没 ​

0

0

3

概念机器

2026-02-01 18:08来自 moto edge X30

穷人如何自娱自乐？可以在LaTeX里学习使用TikZ。 ​

3

1

4

概念机器

2026-02-01 14:09来自 moto edge X30

2015年还有学者在写把组合子直接和一阶逻辑捏把在一起的研究。 ​

0

0

3

概念机器

2026-02-01 00:47来自 moto edge X30

纠结了很久我还是决定启用 #applicative logic# 这个宏大叙事的名字。这个名字对于今天的我来说肯定是力不能逮的，但希望有一天能逮。 ​

1

1

8

概念机器

2026-01-30 14:58来自 moto edge X30

我的学术主张来了[喵喵] ​

2

5

9

概念机器

2026-01-29 16:04来自 moto edge X30

代数还是很重要的。比如想定义一种广义逻辑，遇到交换律问题，就得理解子结构逻辑的代数结构是剩余格，就必须得把融合和序定义出来满足Galois连接。然后看看小野宽晰的融合算子的交换律被禁止有什么实质性影响。这些都不是在规则层面捣鼓符号能搞定的。 ​

4

0

10

概念机器

2026-01-29 13:07来自 moto edge X30

原来Lambek是二战时期因为德国人身份被英国人鉴定为敌人的狗崽子遣送加拿大的[二哈] ​

0

0

1

概念机器

2026-01-29 02:12来自 moto edge X30

简直是噩耗，我的lol (lambda over logic) theory，要干掉交换规则。不然任意组合子或者λ项都有XYZ=XZY，这显然是不能被λ演算接受的[二哈] 不过好在这仍然可以解释柯霍同构。 AI说这叫非交换Lambek演算。塔玛的什么是Lambek演算，又得去学[二哈] ​

0

2

4

概念机器

2026-01-28 07:43来自 moto edge X30

最早在逻辑系统中发现形式化计算的人，是Moses Schönfinkel。他在1920年哥廷根Hilbert小组的一次学术交流会上向世人展示了后来被称为组合子的技术。 该技术在第一次路演的时候就完善程度惊人，包括带着逆向语法结构递归的S组合子，包括可以图灵完备的SK组合子，包括关于逻辑组合子的想法和单一的逻辑 ​

2

5

5

概念机器

2026-01-26 12:26来自 moto edge X30

把这本翻出来，要旋风般的读一遍了。 ​

1

5

18

概念机器

2026-01-26 01:27来自 moto edge X30

今天是个值得纪念的日子。离投稿arXiv的日子越来越近了。 ​

3

3

14

概念机器

2026-01-25 13:17来自 moto edge X30

激烈的思考和阅读了几天最终意识到，使用命题逻辑的蕴含片段，保守定义type，和证明stlc里的柯霍同构，是足够的。但是对于mltt就不够了。 Seldin在文章里给出Curry的G组合子和Martin Löf Π的等价，概念上是没有错误的。但是严格的检查两者的符号使用方式，他们Split符号含义的方式不同。组合子逻辑的 ​

0

1

5

概念机器

2026-01-24 19:46来自 moto edge X30

非机构的independent researcher，俗称民科，发第一篇要领域内作者endorsement，证明不是彻底的瞎胡扯也不是卖枕头的。//@退而思之xyq:不是STOC，也不是FOCS，你要啥推荐人嘛[笑cry][笑cry][二哈][二哈]

立旗。两年内我要发一篇arXiv。形式化理论方向。诚征推荐人。 ​

1

1

4

概念机器

2026-01-24 18:30来自 moto edge X30

很多逻辑学书里引入等词的时候都是这样介绍的： 1 等词不是等价关系 2 等词在等价关系之上叠加了替换定理 这个说法在习惯了之后感觉还挺自然的，但实际上它有个反直觉的地方。等价关系在逻辑里是二元谓词，它具有可以嵌套的特性，即 X≡(Y≡Z)在逻辑里是well defined，不论从模型论上还是证明论上都 ​

1

0

3

概念机器

2026-01-24 12:08来自 moto edge X30

自己不用还可以考虑送人。

二爷转我一个链接，说苹果要出 3000 块的 Mac 了。 我说这东西对我没啥吸引力。 我一年过半百的老登，我为什么要用便宜 Mac，我为什么还要用便宜东西？ 我没有理由啊。😂 ​

0

2

4

概念机器

2026-01-24 01:08来自 moto edge X30

似乎北美搞类型论的人，长期留在学校里搞科研的也不算很多，一个时代大发展时期一些学者就占据了高高校和学派的有利位置，然后的学生没多少特别重要的突破性工作可以做了，也都去产业搞工业验证和编程去了。北欧可能稍微好点，但是考虑到每年PhD毕业的那么多量，继续搞学术的还是比例很低的。 AI说即 ​

1

3

3

概念机器

2026-01-23 20:18来自 微博网页版

立旗。两年内我要发一篇arXiv。形式化理论方向。诚征推荐人。 ​

5

11

30

概念机器

2026-01-23 19:56来自 moto edge X30

1980年正式发表在Seldin和Hindley辑的纪念Curry的文集中的Curry Howard同构的原始文章。 实际上Curry的手稿里早在1930年之前，Curry就发现了这个现象；在1958年的组合子逻辑第一卷里，有一节题目是Analogy with Propositional Algebra，里面使用的词语是FP transformation。 1969年Howard写了这篇文 ​

0

0

2

概念机器

2026-01-22 22:12来自 moto edge X30

非常搞笑的是，在我的Propositional Type Theory里，term和type之间的关系竟然没有稳定的解释。 在intro规则里，要解释成term⊃type，而在elim规则里，要反过来，解释成type⊃term，[允悲] 而好消息是，一旦接受这个中二设定，→intro和→elim都是「可证」的，不是基础规则，[二哈] ++++ 发展形式 ​

0

1

0

概念机器

2026-01-22 11:12来自 moto edge X30

灵光 ​

0

1

1

概念机器

2026-01-22 10:28来自 moto edge X30

deepseek学术水平比豆包高很多。检查简单的形式化证明毫无压力，而且能探讨一点有深度的问题。豆包只会机械重复「命题即类型程序即证明」。 ​

5

6

20

概念机器

2026-01-21 19:29来自 moto edge X30

我已经成功的说服了两个AI，我的民科类型论才是伟光正的，马丁洛夫类型论是垃圾，[喵喵][喵喵][喵喵][喵喵] ​

0

6

10

概念机器

2026-01-21 10:20来自 moto edge X30

我的新理论里，S和K组合子除了有=定义 S abc = ab(ac) K ab = a 之外，还有⊢定义 abc ⊢ Sabc a ⊢ Kab [喵喵] ​

0

1

1

概念机器

2026-01-21 10:14来自 moto edge X30

问了一下豆包，逻辑学顶刊Journal of Symbolic Logic，影响因子也才0.8的水平，这也太离谱了[二哈]，国内搞逻辑学的是不是一辈子最多副教授了[二哈][二哈][二哈] ​

0

3

3

概念机器

2026-01-20 21:58来自 微博网页版

特娘的obsidian里写latex好用到飞起，比知乎的傻叉编辑界面好用一百倍，也令人震惊的比overleaf还好用；当然这个对比可能不恰当因为overleaf是full latex，obsidian则可能只是支持mathjax，但是它的编辑过程可真特娘的赏心悦目啊，沁人心脾。听说obsidian是一对程序员夫妻开发的，谁认识他们代我问个好 ​

4

5

21

概念机器

2026-01-20 20:00来自 moto edge X30

「有谓词就有可证（⊢），没有谓词只有可导，但形式上无前提可导也是可证，如果规则sound。」 ​

0

1

3

概念机器

2026-01-19 21:32来自 moto edge X30

假设X和Y都是最抽象意义上的包含逻辑的组合子或λ表达式。问题： X ⊢ Y ⇔ ⊢ YX 有可能成立吗？如果能成立，它是derivable还是admissible？如果不能成立，如何证明inconsistency？ 说说看你的观点和理由是什么。 提醒：因为Deduction定理几乎是牢不可破的存在，所以 X ⊢ Y ⇔ ⊢ X ⊃ Y 几乎 ​

1

6

3

概念机器

2026-01-18 19:22来自 moto edge X30

做了一个违背祖宗的决定，把Ξ，F，G组合子都抛弃了，直接把⊢写在公式里。 Mα⊢β，这是函数M的类似是α⊢β的意思，elim的推导过程比较狂野。 Mα⊢β ⊢β(Mα) ⊢BβMα α⊢BβM，此时可以加入公式N⊢α，应用cut N⊢BβM ⊢BβMN ⊢β(MN) Mα⊢βα，这是依赖函数，但是和Martin Lof版本的 ​

1

0

2

概念机器

2026-01-18 14:16来自 moto edge X30

这一篇非常炸裂的是有一种18世纪工程师暴力使用微积分的精神。它有一个第一眼完全无法接受的定义，就是 组合子或λ里的「应用」，MN，可以被解释成逻辑上逆蕴含，N⊃M；类似的一个项N和它的类型α的关系是 N ⊢ α 于是根据演绎定理有 ⊢ N⊃α 于是 ⊢ αN 在整个体系的规则推导上，完全不冲突

写出了一个肥肠无厘头的规则但是仔细一想竟然还塔玛的是对的。 N ⊢ α，α ⊢ B β M ———————— N ⊢ B β M ———————— ⊢ B β M N ———————— ⊢ β(MN) 实际上它是从类型规则 N: α，M: α->β ———————— MN: β 变换出来的。但是前面的表达式神奇的地方在于，它并 ​

1

1

2

概念机器

2026-01-18 13:19来自 moto edge X30

写出了一个肥肠无厘头的规则但是仔细一想竟然还塔玛的是对的。 N ⊢ α，α ⊢ B β M ———————— N ⊢ B β M ———————— ⊢ B β M N ———————— ⊢ β(MN) 实际上它是从类型规则 N: α，M: α->β ———————— MN: β 变换出来的。但是前面的表达式神奇的地方在于，它并 ​

2

2

3

概念机器

2026-01-18 11:11来自 moto edge X30

一大早醒来就人间清醒的发现，mltt里定义的Π，是收缩的。在组合子里这非常直观： GαβM, αN ⊢ βN(MN) 而实际上这个规则的不收缩版本看上去更直观，它是 GααβM, αN, αN ⊢ βN(MN) 不需要懂什么类型论也能够看出左右守恒了，整个公式仅仅是dual cut，干掉了类型α。 实际上这一点是非常 ​

0

0

0

概念机器

2026-01-17 10:35来自 moto edge X30

等手上事情忙完了要把这本认真刷一遍。刷题对于搞土木工程还是挺重要的。 ​

3

2

10

概念机器

2026-01-16 10:51来自 moto edge X30

原来是这么好听的名字[喵喵] ​

2

1

1

概念机器

2026-01-16 02:45来自 moto edge X30

我要搞得实验性语言名字敲定，叫「柯外」，Kwai。 ​

1

7

3

概念机器

2026-01-16 02:27来自 moto edge X30

花了非常大的力气才搞明白第一个等式怎么理解。 αx ⊢ β ——————— ⊢ Ξα(λx.β) 这个表达式的前提里已经没有项M了，所以它只能是在类型里，是马丁洛夫Π类型的形成规则。 至此，柯里的类型系统三大定律： Ξα(KβM)对应纯粹的Π类型形成规则，注意这里的语义是完全对应的。 FαβM ​

0

2

3

概念机器

2026-01-15 15:09来自 moto edge X30

现在买面粉，很多面粉袋子上有个机器勾在一起的封口线，要找准一个线头，一拉，就能把整跟线拆下来。 但是你看我用这个账号发这个话题，说明它的计算有关。是的。在TeReSe的经典的项重写系统（term rewriting systems）的书里，开篇就有一个用「绳结」表达项重写的例子。 一个「活扣」就是一个redex ​

6

3

15

概念机器

2026-01-15 13:54来自 moto edge X30

但是你说的问题也确实有工程方法。iota/jot下可以把组合子编码到任何二进制字符串都是一个程序，即计算函数。于是可以从最小的开始向上搜索，不能type的扔掉，能type的先找到的就是最短的，后面找到的能等价的就是等价类里的，类似在applicative structure里找质数。//

【Anthropic开源了Claude团队内部使用的代码简化Agent】 AI工具迭代的速度已经快到有些离谱了。 Anthropic刚刚开源了他们Claude Code团队内部使用的code-simplifier agent。这个工具的用法非常简单：在一段长时间的编码工作结束后，只需要让Claude使用code-simplifier，它就会自动清理混乱的代码库、 ​

2

1

5

概念机器

2026-01-15 13:43来自 moto edge X30

学术界里学生捧高老师也是很重要的。 简单类型论最早是Chwistek和Ramsey的工作，现在极少看到被提及。 Lesniewski是第一个提出现代意义上类型的人，他称之为Semantic Category，目前很确定的是早在1929年的Lecture里他就完成了他的三部曲系统并且大量使用这个标记。但是他本人没有形式化这个理论，形 ​

1

0

3

概念机器

2026-01-14 13:00来自 moto edge X30

ΞX(KYM) = ∀u.Xu⊃Yu，这是形式蕴含（罗素 ΞX(BYM) = ∀u.Xu⊃Y(Mu)，这是类型（柯里 ΞX(SYM) = ∀u.Xu⊃Yu(Mu)，这是依赖类型（马丁洛夫 组合子深不可测 #为往圣继绝学# ​

1

6

7

概念机器

2026-01-14 12:24来自 moto edge X30

这是1958版组合子逻辑中，Curry和Feys对柯霍同构的原始描述，当时用了两个词，一个是analogy，另一个是F-P transformation。整理Curry的手稿遗产的人是他的得意门生Seldin，根据Seldin的描述，最初发现这种逻辑特性可以追溯至1930年以前，手稿上有写。 整体来说Curry没有把这种同构当回事。时至今日也 ​

0

0

1

概念机器

2026-01-14 02:46来自 moto edge X30

dependent type是可以用组合子算出来的 B(B(CBS)B)Ξ 来看看这个表达式能干什么，给它三个参数XYZ B (B(CBS)B) Ξ X Y Z (B(CBS)B) (ΞX) Y Z B (CBS) B (ΞX) Y Z C B S (B(ΞX)) Y Z B (B(ΞX)) S Y Z B (ΞX) (SY) Z ΞX(SYZ) ∀u.Xu⊃SYZu ∀u.Xu⊃Yu(Zu) ++++ 这个表达式之于马丁洛夫类型论 ​

0

1

2

概念机器

2026-01-12 23:45来自 微博网页版

推演组合子与柯霍同构，第二篇，发布在知乎。欢迎围观，欢迎同行学术评审（但是不付评审费，[二哈]。 http://t.cn/AXG7PQpT ​

1

1

2

概念机器

2026-01-11 15:33来自 微博网页版

推演组合子和柯霍同构（1），发布在知乎。 http://t.cn/AXbgv6pW ​

0

0

6

概念机器

2026-01-11 06:59来自 微博网页版

柯霍同构的真正含义在图一(1.2)这个大家不太熟悉的表达式里。这是柯里的推理组合子系统里的写法，之所以这个写法重要是因为我们在谈一个计算系统，于是逻辑的表达必须要考虑尽可能多的使用计算的形式，即λ。 全称量化组合子Π的定义有点出人意料；它实际上说的是，匿名函数(λu.M)应用在任何参数上都 ​

0

1

1

概念机器

2026-01-10 04:04来自 moto edge X30

调整了一下定义，类比Curry的F和G组合子（和Π等价），如果逻辑弱到mltt的等式逻辑，则 F'αβM ≡ λx.= α x (B β M) G'αβM ≡ λx.= α x (S (β x) M) 都可以把x抽象掉但是这样比较容易阅读。 ++++ 表面上看起来这是一个用于学习语言的简单解释器。但实际上稍微想一下就会发现，等词估 ​

0

0

2

概念机器

2026-01-10 01:44来自 moto edge X30

上回书说到 f:α→β ≡ B (B (B β M)) (= α) 可以使用组合子写出如下演绎规则对应的归约规则。 FαβM, αN ⊢ β(MN) 在α和β都是简单类型时这是可行的。但是如果是mltt怎么办呢，比如Π。 Curry在icl里区分两种F-obs，一种叫F-simple，就是ground type，基本类型；另一种叫F-composite，函 ​

0

0

7

概念机器

2026-01-09 21:03来自 moto edge X30

晚上灵机一动想明白了Martin Löf和Curry的系统（http://t.cn/AXb8Bz13）完全不是一回事。Curry的推理组合子系统，使用的强逻辑，是不等式逻辑，但是Martin Löf的系统使用的是非常弱的逻辑，只需要等式逻辑。如图所示。 理论的一大意义是给人数学和阅读，因此不可能每项都标注类型，但是机器就不同了， ​

2

0

4

概念机器

2026-01-09 15:43来自 moto edge X30

这个逻辑表达式的含义是集合论视角对函数类型的定义。其中f和g都看作是集合的特征函数，即fu可以理解为u∈f，gv可以理解为v∈g。于是下面这个表达式的含义是，函数h满足这个逻辑表达式。 ∀u.fu⊃g(hu) 基于组合子形式做如下变换，先引入B组合子把hu的括号去掉 ∀u.fu⊃Bghu 引入Ξ，ΞXY≡∀u.Xu ​

1

4

5

概念机器

2026-01-08 15:15来自 moto edge X30

回复@茶是真热:找一下斯坦福Jon Barwise和同事的Language，Proof，and Logic。斯坦福还有一个叫Tarski's World的书和交互式课件，以前课件是收费的好像不久前都免费了。逻辑的流派和风格比爵士乐还多，一开始就要知道这一点，不能当实体论学习，是方法论和技巧。//@茶是真热:梨叔能推荐本逻辑方面基础

以后这个账号只写逻辑和计算话题了。 ​

4

3

6

概念机器

2026-01-08 02:54来自 moto edge X30

以后这个账号只写逻辑和计算话题了。 ​

14

8

35

概念机器

2025-03-31 07:12来自 moto edge X30

请问有没有人知道Lattice最低端的低功耗带pcie 2.0的LFE5UM5G-25，批量拿货多少钱？mouser上现货都标价300多，感觉渠道里也很难拿到80块以内的吧。 ​

1

9

1

概念机器

2025-01-16 11:49来自 moto edge X30

the bad：即使使用逻辑编程语言编程，程序还是需要verification的。 the good：理论->工程实践->验证，这个闭环越小越自包含越好。现代计算机系统和语言工具的编程活动，在CI/CD意义上是坚持了这个理念的，但是程序员都变成了工具的使用者，用类似刷微积分题目的方式获得了直觉，熟练，和可用但有限的 ​

3

3

17

概念机器

2022-11-18 19:27来自 moto edge X30

看目录挺有趣//@丢了魂的爱斯基摩人:@有个梨UGlee @逮獭科技 梨叔应该会感兴趣

逻辑学大师斯穆里安的逻辑学入门课《逻辑迷宫》 趣味横生地讲述多种逻辑谜题的故事书！ 本书是一本趣味横生地讲述形式逻辑主题的故事书，融合了众多读者喜闻乐见的逻辑谜题，以一种独特的方式来普及数理逻辑。从第一章到第十六章有大量的趣味谜题供读者思考，包括说谎和讲真话的逻辑、沉默的骑士和无 ​

8

0

8

概念机器

2022-11-16 20:24来自 moto edge X30

可能很多人不清楚马斯克收购推特的真正意图。我来解释一下。 马斯克收购推特是因为它的特斯拉产能严重超过销售模式所需的产能了；他开始琢磨出租车市场。 收购推特之后首先植入钱包服务，这个很厉害，如果你推出一个打钱宝，再推出一个打车宝，你想让人安装，上亿人安装，你算算需要多少市场费用能让 ​

99

45

213

概念机器

2022-11-16 19:42来自 moto edge X30

dinner ​

1

10

29

概念机器

2022-11-16 19:22来自 moto edge X30

//@韦恩卑鄙:我在上海和厦门看到医院的核酸点都在医院外的样子 所以说这些人去的是什么地方的核酸点啊//@颜文字君:太会整活了( ͡° ͜ʖ ͡°)//@木制奶:貌似还是有单管常规点，就是要收钱（）

抱歉，根据作者设置的微博可见时间范围，此微博已不可见。 ​

2

2

1

概念机器

2022-11-16 16:21来自 moto edge X30

Musk有很多光环。 在收购Twitter之前，特斯拉和Space X，有市场交付的奇迹，Musk也在公众面前以超人形象出现，而且他在谈到工程方法时显示了他的近乎顶级水平的理解。 但是收购Twitter还是很不同。因为无论特斯拉还是Space X，行业里同道的工程师不多，也不太爱在互联网上分享或谈论什么。Twitter就 ​

24

15

92

概念机器

2022-11-14 23:01来自 moto edge X30

这个也可能改善肩周炎症状矮盖斯//@julyclyde:东亚病夫是一种心理需求也是一种思维方式，但不是一种生理状态//@张戴阳Tillo:现在知道《走近科学》在那个时候到底有多重要了吧……

抱歉，根据作者设置的微博可见时间范围，此微博已不可见。 ​

9

4

8

概念机器

2022-11-14 12:39来自 moto edge X30

那也比出门抗议被dei走枪毙了强。//@ExcitedVczh:一个不能上班，一个不敢上班[二哈]

之前我说鹅螺蛳国内经济被京子和阿胶抓壮丁抓崩溃了，成年男性东躲西藏都不敢出门上班商店工厂都停工了。我为我之前的武断言论道歉，这不鹅螺蛳殡葬业生意不就做得蒸蒸日上拉动了GDP嘛，稳中向好争取明年再翻一番[坏笑] http://t.cn/A6oeDKe1 ​

3

0

2

概念机器

2022-11-13 06:05来自 moto edge X30

如果有人工程一段艾滋病毒基因进去你还觉得omicron无法战胜么？//@ExcitedVczh:什么时候人类才能意识到自己战胜不了omicron[二哈]//@西雅图黄都督:这么热爱隔离，自己建个方舱进去住着别出来了，世界多危险啊//@来去之间:图3拿出来当证据……潜伏期14天以上的那些....

抱歉，根据作者设置的微博可见时间范围，此微博已不可见。 ​

8

5

12

概念机器

2022-11-13 05:23来自 moto edge X30

我得去睡了💤，我第一眼看成了鳄鱼🐊，我还想意大利怎么能允许伞哥捕捞鳄鱼🐊[二哈][二哈][二哈][二哈]

[2/3] 其实今天我做的鲷鱼 17 欧元一条，给波斯美女留了整整一半她还真全吃了。而且赞不绝口，说是美味，尤其那道用 “特殊酱汁” 调味的炸鱼骨特别好。我心说我那是跟烹饪书学做的蛋黄酱（图1）结果可惜做砸了（油水分离），跟书上那个做砸以后号称有点儿恶心的图2 区别不大[允悲] 她肯定是被我持之以 ​

0

0

5

概念机器

2022-11-13 03:43来自 moto edge X30

game theory

一道常见的行为面试题： “What is the best piece of feedback you have gotten?” “你得到的最好的反馈是什么？” 这道题乍一看是问你得到过反馈，你可以按照《如何回答面试中高频的行为面试题： “Tell me about a time you had a conflict at work”》 http://t.cn/A6SVsPb9 介绍的使用STAR模型 ​

6

0

6

概念机器

2022-11-12 14:52来自 moto edge X30

经常做外包的人对这种情况有个预估，就是只预期下一个可交付的milestone的最小集，也只承诺这个。后面可以有框架性的预期但很明确和资源有关。

你有一个小团队，老板安排你做一个软件的开发，你领到任务后，其他几个同事离职了（可能是老板不给人家发工钱，也可能是人家主动不想干了），然后老板每天盯着你的工作进度，对投入资源的事概不谈论，认为及时交付版本是你当初的承诺，你不兑现是你的思想出了问题。 这总事经常发生，结局多半是不欢而 ​

11

3

18