PDF 是自学者的噩梦，读 Anders 的 Static Program Analysis 窒息

[andyJado]

卡在第 29 页的 exercise 3.3 两天了，没有任何办法，就硬搁这悟呐？

[westtide]

练习 3.3：解释如何用有限自动机表示正则类型，使得如果它们的自动机接受相同的语言，则两个类型相等。展示一个代表类型μt.( int,t)→int 的自动机。

《计算理论导引》里面说，finite automata 能接收的字符串组成的语言就是 regular language ，我推测 regular type 就是 regular language ，大概同理？

[enchilada2020]

？没看懂跟 PDF 有啥关系 难道不是我理解的那个 PDF （（

[andyJado]

@enchilada2020 我没法自在地跳转，我没法复制出去搜索，我没法找到社区。卡在一个地方，我掌握的解决问题的方法都不适用了，我还找不到人问。

[tuwulin365]

配电房

[enchilada2020]

@andyJado 你需要正版 PDF 。。。扫描的怕是不行😅OCR 一下试试

[andyJado]

@westtide 上箭头加 int 是什么意思，指针吗？

μt.( int,t)→int 我就看不懂了，它里面做了一些数学的东西，我数学学得不错，但它做的事情我不理解： A type of the form μα.τ is considered identical to the type τ[μα.τ/α].1

还有昨天看到“zipper struct 是数据结构的一次导数，我何止参不透，完全是摸不到了。”

问题在于我不觉得这东西困难，只是它选择了一个“严谨但难以理解的表达”，如果有老师在，只需要告诉我，“你想知道这个之前你得知道一个那个”，就完了，这样也太苦了。

[jfdnet]

电子文档上面做个标记多么简单的事情哦

[lrigi]

我想每个人在读大学的时候都会有这样的感悟，就是这个东西我不懂，但没有一个人可以帮我解释，也许世界上有这样的人，但我不太可能认识。要么自己钻研出来或者搜索出来，要么就放弃。

[metalvest]

chatpdf 没试试？

[t41372]

@andyJado 一般非扫描版(如来自官方的 pdf)是可以复制的
扫描版的 pdf 不能复制文字，是因为扫描出来的只有图象，这不是 pdf 格式的问题，而且也有解决方案
可以使用一些工具，比如 adobe acrobat, 把整个文件进行 ocr 操作，处理完，文字就可以自由复制了
自由跳转确实是硬伤，电子书肯定不能像纸质书一样凭感觉快速翻阅，不过也有工具专门优化 pdf 的体验
比如 mac, ios, windows 上都有的 liquid text, 其实有时候能给你一种超越纸质书的体验，具体功能我说不清楚，你可以自己去看看

[stevefan1999]

> 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.

大佬為什麼你要讀這個

[stevefan1999]

https://en.wikipedia.org/wiki/Graph_isomorphism

我目前不是要讀 PhD 我也不知道怎麼做 static analysis 但我不知道這能不能幫到你

[stevefan1999]

另外我記得龍書也有説過這個

[metalvest]

正则类型是一种用正则表达式描述的数据类型，它可以表示一组满足某种模式的字符串。有限自动机是一种抽象的计算模型，它可以识别和接受正则类型。如果两个正则类型的有限自动机接受相同的语言，那么这两个类型相等。一个代表类型μt.( int,t)→int 的有限自动机可能如下图所示：


这个自动机从初始状态 q0 开始，读入一个整数后转移到状态 q1 ，然后读入一个 t 类型的值后转移到状态 q2 ，最后输出一个整数并停止在终止状态 q3 。你对这个答案满意吗？

[ansonsiva]

@lrigi #8 这也正是我觉得 chatgpt 给我带来巨大帮助的地方，我终于找到一个可以问各种问题而且还可以连续深入的问的“人”了。

[mizuhashi]

@andyJado https://ruby-china.org/topics/7894 zipper 為什麼是導數可以看看這個 個人認為比較好懂

[hez2010]

你说的这个的理论基础是证明正规表达式和有限自动机的等价性，用泵定理可以很容易地构造出证明。
感觉问题不在于 pdf ，而在于你的前置知识缺少太多了，建议你先放下这本书，去学一下形式语言与自动机之后再去看静态程序分析。

[ufo5260987423]

笑，你的困难我都遇到过，还是前置知识缺课的缘故。
以及，如果你以后想要进一步研究 static analysis 的工程实现，可以 github 看我的 scheme-langserver ，master 分支前天刚推了 deductive inference system 上去。笑

[masellum]

楼上说的对，你看不懂的主要问题是前置知识太少了，可能需要了解一些简单的形式语言与自动机还有类型系统理论之类的
比如这个 regular type ，这里指的应该就不是正则表达式而是某种类型（没有上下文我也不能确定但应该是），那个 μt.( int,t)→int 是用来表达类型的记号，这里 μ 是递归类型的记号，你没有前置知识的话直接看是看不懂的
关于类型系统这一块可以看看 types and programming languages 这本书

[secondwtq]

你说的是这本书 https://cs.au.dk/~amoeller/spa ？
这 PDF 做得不是挺好的么，跳转，复制，搜索都可以

因为以前用过这书，我 iPad 里面有一份 2018 年 10 月版的，我看了一下里面的指针不是上箭头，而是"&"符号
这个 notation 的问题，可以看一下 Guy Steele 的这个 talk： <amp-youtube data-videoid="dCuZkaaou0Q" layout="responsive" width="480" height="270"></amp-youtube> It's Time for a New Old Language (The most popular programming language in computer science)