PDF 是自学者的噩梦，读 Anders 的 Static Program Analysis 窒息
andyJado · AndyJado · 2023-03-19 16:11:58 +08:00 · 4438 次点击这是一个创建于 625 天前的主题，其中的信息可能已经有所发展或是发生改变。
卡在第 29 页的 exercise 3.3 两天了，没有任何办法，就硬搁这悟呐？
 |
1
westtide 2023-03-19 16:21:17 +08:00
练习 3.3：解释如何用有限自动机表示正则类型，使得如果它们的自动机接受相同的语言，则两个类型相等。展示一个代表类型μt.( int,t)→int 的自动机。
《计算理论导引》里面说，finite automata 能接收的字符串组成的语言就是 regular language ，我推测 regular type 就是 regular language ，大概同理？ |
 |
2
enchilada2020 2023-03-19 16:22:14 +08:00 via Android
？没看懂跟 PDF 有啥关系 难道不是我理解的那个 PDF （（
|
 |
3
andyJado OP @enchilada2020 我没法自在地跳转，我没法复制出去搜索，我没法找到社区。卡在一个地方，我掌握的解决问题的方法都不适用了，我还找不到人问。
|
 |
4
tuwulin365 2023-03-19 21:05:47 +08:00
配电房
|
|
5
enchilada2020 2023-03-19 21:07:26 +08:00 via Android
@andyJado 你需要正版 PDF 。。。扫描的怕是不行😅OCR 一下试试
|
|
6
andyJado OP @westtide 上箭头加 int 是什么意思，指针吗？
μt.( int,t)→int 我就看不懂了，它里面做了一些数学的东西，我数学学得不错，但它做的事情我不理解： A type of the form μα.τ is considered identical to the type τ[μα.τ/α].1 还有昨天看到“zipper struct 是数据结构的一次导数，我何止参不透，完全是摸不到了。” 问题在于我不觉得这东西困难，只是它选择了一个“严谨但难以理解的表达”，如果有老师在，只需要告诉我，“你想知道这个之前你得知道一个那个”，就完了，这样也太苦了。 |
 |
7
jfdnet 2023-03-19 21:21:31 +08:00
电子文档上面做个标记多么简单的事情哦
|
 |
8
lrigi 2023-03-19 21:23:35 +08:00 via iPhone  2
我想每个人在读大学的时候都会有这样的感悟，就是这个东西我不懂，但没有一个人可以帮我解释，也许世界上有这样的人，但我不太可能认识。要么自己钻研出来或者搜索出来，要么就放弃。
|
 |
9
metalvest 2023-03-19 21:37:32 +08:00 via Android
chatpdf 没试试？
|
 |
10
t41372 2023-03-19 21:37:43 +08:00 via Android
@andyJado 一般非扫描版(如来自官方的 pdf)是可以复制的
扫描版的 pdf 不能复制文字，是因为扫描出来的只有图象，这不是 pdf 格式的问题，而且也有解决方案 可以使用一些工具，比如 adobe acrobat, 把整个文件进行 ocr 操作，处理完，文字就可以自由复制了 自由跳转确实是硬伤，电子书肯定不能像纸质书一样凭感觉快速翻阅，不过也有工具专门优化 pdf 的体验 比如 mac, ios, windows 上都有的 liquid text, 其实有时候能给你一种超越纸质书的体验，具体功能我说不清楚，你可以自己去看看 |
 |
11
stevefan1999 2023-03-19 21:42:28 +08:00
> Explain how regular types can be represented by finite automata
so that two types are equal if their automata accept the same language. Show an automaton that represents the type µt.(promotable(int),t)→int. 大佬為什麼你要讀這個 |
|
12
stevefan1999 2023-03-19 21:44:06 +08:00 1
|
|
13
stevefan1999 2023-03-19 21:47:05 +08:00
另外我記得龍書也有説過這個
|
|
14
metalvest 2023-03-19 21:47:59 +08:00 via Android
正则类型是一种用正则表达式描述的数据类型，它可以表示一组满足某种模式的字符串。有限自动机是一种抽象的计算模型，它可以识别和接受正则类型。如果两个正则类型的有限自动机接受相同的语言，那么这两个类型相等。一个代表类型μt.( int,t)→int 的有限自动机可能如下图所示：
 这个自动机从初始状态 q0 开始，读入一个整数后转移到状态 q1 ，然后读入一个 t 类型的值后转移到状态 q2 ，最后输出一个整数并停止在终止状态 q3 。你对这个答案满意吗？ |
 |
15
ansonsiva 2023-03-19 22:06:37 +08:00
@lrigi #8 这也正是我觉得 chatgpt 给我带来巨大帮助的地方，我终于找到一个可以问各种问题而且还可以连续深入的问的“人”了。
|
 |
16
mizuhashi 2023-03-19 22:08:46 +08:00 via iPhone 1
@andyJado https://ruby-china.org/topics/7894 zipper 為什麼是導數可以看看這個 個人認為比較好懂
|
 |
17
hez2010 2023-03-19 22:26:48 +08:00 via Android 2
你说的这个的理论基础是证明正规表达式和有限自动机的等价性，用泵定理可以很容易地构造出证明。
感觉问题不在于 pdf ，而在于你的前置知识缺少太多了，建议你先放下这本书，去学一下形式语言与自动机之后再去看静态程序分析。 |
 |
18
ufo5260987423 2023-03-19 22:31:00 +08:00
笑，你的困难我都遇到过，还是前置知识缺课的缘故。
以及，如果你以后想要进一步研究 static analysis 的工程实现，可以 github 看我的 scheme-langserver ，master 分支前天刚推了 deductive inference system 上去。笑 |
 |
19
masellum 2023-03-19 23:15:57 +08:00 1
楼上说的对，你看不懂的主要问题是前置知识太少了，可能需要了解一些简单的形式语言与自动机还有类型系统理论之类的
比如这个 regular type ，这里指的应该就不是正则表达式而是某种类型（没有上下文我也不能确定但应该是），那个 μt.( int,t)→int 是用来表达类型的记号，这里 μ 是递归类型的记号，你没有前置知识的话直接看是看不懂的 关于类型系统这一块可以看看 types and programming languages 这本书 |
 |
20
secondwtq 2023-03-20 00:28:35 +08:00 1
你说的是这本书 https://cs.au.dk/~amoeller/spa ？
这 PDF 做得不是挺好的么，跳转，复制，搜索都可以 因为以前用过这书，我 iPad 里面有一份 2018 年 10 月版的，我看了一下里面的指针不是上箭头，而是"&"符号 这个 notation 的问题，可以看一下 Guy Steele 的这个 talk： It's Time for a New Old Language (The most popular programming language in computer science) |
 |
21
cc666 2023-03-20 00:28:52 +08:00
不知道这和 PDF 有什么关系？
如果是不能复制的话，不是 PDF 的问题，而是制作 PDF 的作者用的不是文字而是图片的原因，自己用 Adobe 之类的工具进行扫描优化就行了，也可以用到的时候再 OCR ，没法跳转可能是你没有加标记。 PS：这些都是很容易就能搜到的解决方法。 |
|
22
andyJado OP @ufo5260987423 我的对象语言，一个文件会有几万行。我觉得我需要先趴到 CST 然后再趴 AST ，我抄的是 rust-analyzer 。你的索引是按函数建立的吗， 一个文件 10 个函数，编辑一个函数的时候只更新那个函数？
|
|
23
ufo5260987423 2023-03-20 08:59:47 +08:00
@andyJado #22 一个文件有几万行……用 vscode 打开都没法语法渲染了吧……
1 、我现在是按照文件更新的； 2 、如果一个文件几万行，且 10 个函数，那一个函数平均几千行代码，笑。 3 、我不能确定你的修改是否只对函数内部的语义有影响，如果你确定的话，把更新索引的粒度下降到函数也是可以的。 |
 |
26
DianQK 2023-03-21 09:55:52 +08:00 1
这刚好是我今年计划看的一本书，我试着把这块的看了，上箭头 int 就是指 int 的指针类型。
但 Exercise 3.3 我也看不明白要说啥。 似乎是说 TypeVar 这种 regular type （大概是说符合书中描述的规则的类型？）里面的 t 是不确定的，然后设计一个状态机可以用来判断两个类型是否相同？（不懂） 不过我重新翻了一下之前的版本，Types 这个章节就是一页带过，至少对我来说，这一章不是静态分析的关键内容。跳过这一章看后面的应该没啥问题。如果是我，我选择跳过不懂的这部分。 pdf 倒是我最喜欢的一种格式了，高保真&可离线。也可以跳转的，取决于作者写不写吧。我看 spa 这本又不少可以跳转的地方。或者是 OP 下载地址不对？ https://cs.au.dk/~amoeller/spa/ 除了跳过，还可以直接问作者呀。我发了邮件，不过还没回复我。 |
|
27
DianQK 2023-03-23 21:16:26 +08:00 1
我可以肯定的说，OP 你可以忽略这个习题，因为作者回复我了，说这是个不重要的习题。我跟随作者给出的一些提示 /答案，总结大概如下（我的理解不一定对）：
首先我可以肯定，这是将自动机（ FA ）相关的问题，前置知识在龙书的第 3.6 小节（不推荐看网上的一些介绍，感觉没有龙书写的详细易懂）。Type Analysis 虽然也是静态分析？但通常提到的静态分析对应的应当是本书后面章节的内容。Type Analysis 应该划分为另一个范畴了吧，我觉得忽略这章看本书更合适一些。 这里一直提到的 language 翻译过来虽然是语言，但我觉得解释为句子 /一段话更贴切一些。比如“很高兴见到你”，这是一段话，也是中文（对应的 language ）。 所以这里说的就是正则语言（表达式），只不过不是平常理解的正则表达式，而是更通用的概念。即符合某种正确规则的具体描述语言（一段话）。 抱歉，我没有继续把龙书的 3.7-3.9 看了，这几节应该是讲 FA 的应用部分。Ex 3.3 也**只是说怎么把定义的各种类型画成对应的 FA**，至于啥用，我不知道。作者回我的图片很模糊，感觉不是标准的 FA 。（抱歉，我不能直接贴这张图，因为我忘记了要一份授权，但我基于自己的理解重新画一遍应该没问题吧。） OP 你把 3.6 小节看了之后，应该就可以了解底下的内容（如果没有，那一定是我转述 /理解的不对）。 画出来的 FA 如图：  有些字符我还不知道怎么打出来，就平替一下。这里 FA 用来判断能否接受一个描述对应类型的语言。 一些设定： - 虚线圈似乎表示这里可以自由发挥 /匹配，什么类型都可以接受 - 1 、2 、3 数字用来表示状态转换的顺序 /参数？，当遇到一个 TypeVar （ t ）时候，回到初始状态按照数字顺序匹配 - ut.(&int, t)->int 中的 t 是受限（递归的）的，t 必须满足自身的 (&int, t)->int 类型，这种时候可以回到初始状态接着匹配 所以图中的 FA 可以接受 ut.(&int, t)->int ，首先匹配参数 1 ，&int 成功，然后参数 2 是 t 回到开始状态，参数 3 直接一个 int 结束。 |
Select Language