这是哪本书？看截图感觉不错
MIT Press 的 Semantics of Programming Language
2 个赞
谢谢。
大致看了一下，这本书是专门讲语义的，就是内容有点杂，各章节之间有一定依赖关系。
我其实想找一本专门讲domian theory的书，感觉这类书很少。。。
PS：这本书里其实也有讲domain theory，但是感觉分散在好几章里。
Abramsky & Jung 不知道你看没过
如果觉得不对口可以对照这个导读。
也可能其实你要的不是 domain theory 而是 denotation semantics
3 个赞
这本书写的很好，多谢了！
不愧是@LdBeth，这都能找得到。。。
我要的就是domain theory，原因有以下几点：
-
现在大部分介绍
denotation semantics的文章，背后都用到了domain theory。不会
domain theory看denotation semantics就和不会实分析学微积分一样。。。正如作者自己所说：
-
我想研究一下
Haskell的denotation semantics。我现在发现这个语言并没有想象中那么简单。
比如：你可以在Haskell里定义Coalgebra，但是这个Coalgebra和数学上定义的Coalgebra有一些差异（尽管Haskell里定义的Final coalgebra’s carrier 也能代表无限类型），但是仍然有一些细微的不同，因为Haskell不是totally language 且 Haskell lazy，使得问题复杂化。
有人和我说：如果你真想了解像Haskell那样的non-totally language的
denotation/categorical semantics，可能需要学一点domain theory。 -
我记得TAPL有一章专门讲递归类型的元理论。
我承认，当时看那一章的时候，我没有完全看懂（感觉需要一些
domain theory基础）。
打个比方 Rust 內存管理用了 linear logic，然而慕名去看 Girard 看半天一头雾水，最后花了很久发现內存管理只用上了 linear logic 的皮毛，包括 Girard 这书在內的 linear logic 几乎都是给逻辑学看的，用的都是 sequent calculus 因此还和 type system 不沾边，想学 PL 的去看只会增加奇怪的知识。
Abramsky & Jung 这书是给分析数学看的，里面几乎完全看不出在 PL 上应用。所以我才问是不要 denotation semantics，因为相比 Abramsky & Jung 的內容 denotation semantics 只要用到很少的 domain theory。
这不是很明顯么，编程语言的 computable function ，哪怕是 partial 的也并不能直接等价于 category theory 里的 morphism 或者 set theory 中定义 function 的 binary relation，定义出来自然也会和数学上的 counterpart 有区別。
比如你在 Haskell 里怎么求 function 的 image？
真的，这么“一点”还用不上专门找 domain theory 的书。
你缺的是任意一本讲 function category 的，和 domain theory 没关 (只会讲 recursive function，而非 recursive type )。专门找 category theory 的也没必要。而且就算你不论如何都想上 domain theory，也建议还是先看下 seven sketches 强化一下前置知识 lattice 什么的。
其实我只是想补一下domain theory基础。我发现很多讲denotation semantics的书里大多会提到：monotone function、complete lattice、order theory、convergence 等等。这些概念单独拿出来是可以理解的，但是一旦结合起来看，就觉得不太舒服（特别是那些符号，导致我很难建立直观）。
举个例子：在TAPL这本书里，他定义函子的最大最小定点使用的不是initial/final-algebra，而是使用的monotone function。。。
是的，正因为编程语言和数学之间有鸿沟，所以才需要研究它。
而且Haskell也是有它自己的denotation semantics，我们需要比较他们两者之间差异。
举个例子：
给定一个函子 F X = X + 1，这个函子的final co-algebra 是可以通过数学方法求出来的（方法是求一个ω^op chain 的 limit），以下是已经求好的final co-algebra：
τ : N^T -> N^T + 1
τ : N + T -> N + T + 1
τ = * -----> *
0 -------------> *
1 -----> 0
2 -----> 1
3 -----> 2
...
where N=Nat, T is singleton
注意：这里的N^T是final co-algebra的carrier object。从经典数学的角度看，N^T其实就是N+T，也就是Maybe N。但它实际上指称的是一个CoNat ，而不是Maybe N，你无法构造isomorphism between CoNat 和 Maybe N。因此CoNat 理论上不能在你的计算机里构造（至少你无法证明它）。
然而，由于Haskell non-total and lazy，导致了我们可以定义CoNat
data CoNat = Z | S CoNat
top :: CoNat
top = S top
注意：现在这个top是CoNat的一个term！利用这个top我们可以实现很多有趣的东西，这使得Haskell获得了连Coq都不具备能力！（我不会Coq，或许Coq也有它自己的办法，望指正）
那么接下来的问题就是：
Haskell 作为一款 non-total and lazy language，它的denotation semantics是什么？
它和经典数学和构造数学之间的关系又是什么？
再比如：怎么从N^T机械的构造CoNat？
理解这些，有助于我们理清脉络。
为了学习non-totally language的denotation semantics，可能需要学一点domain theory。
注意：你不能简单的说这里的 top = ∞，用这一句话来解释一切（这个我也知道），我要的是一套完整的理论，并使用规范的语言描述出来。
不会强上domain theory，只是想适当补一下domain theory基础。。。
请问function category是啥？
还有这张截图出自哪本书？感觉和我上面说的东西有点像。。。
抱歉，感觉好像讨论的有点离题。。。 
不知道discourse有没有迁移帖子的功能，把帖子的回复迁到另一个主题里。
这些都昰 category theory 和 topology 的基础⋯⋯ Category theory 有本叫 seven sketches in compositionally 的书。Topology 倒是不知道有哪本合适的，不过都是可以把 seven sketches 里的对应到 topology 上。
https://ecommons.cornell.edu/handle/1813/6778
请。Well, 需要一點 NuPRL 的前置知识。简要的可以看 Type theory and functional programming 的 7.12 Partial Objects and Types
http://www4.di.uminho.pt/~jno/ps/pdbc.pdf
well，我是想说 cartesian closed category。pdbc 就是这样一本书。
2 个赞
就这个 computable function 导致的区別来说和 donation semantics 没什么关系，哪怕是在 dependent type theory 里都有不能用 computable function 而是得用 relation type 表达的地方。
范畴论里似乎没有这样的概念，拓扑里有涉及一些，但是讲的东西和语言没关系（我不太了解拓扑）。。。
这些好像是Scott发明的一套语言，把可计算性规约到拓扑空间函数的连续性上去了。
注：我没看过Scott，不确定他讲的是不是domain theory（但隐隐约约觉得就是，我主要是想学习它这套方法论，很多讲semantic的书里都是用的他这套）。
seven sketches in compositionally里讲的主要是一下范畴论的高级应用，但和我说的那些距离比较远（不过也是好书，就是没时间看。。。 ）
以前看过这个的前三讲，还蛮清晰易懂又不失严谨的，便于建立直观（多画图）。我也没看过Scott domain，因为很多时候CPO就够了，比如TAPL里面讲递归类型好像只用了单调函数和不动点吧，主要就是为了讲Knaster-Tarski Theorem来证明不动点。另外Girard说Scott domain和拓扑空间只是巧合，所以我想也没必要为了这个去学拓扑。我也同意domain theory和范畴论没多大关系，非要说Scott domain是只有一个object的cartesian closed category感觉没什么意义。
1 个赞
category theory不如看awodey的，简明清晰，还讲了lambda calculus跟CCC的关系。在进阶去看topos theory之类的？
monotone function、complete lattice、order theory、convergence
这几个词让我想起这本书 Introduction to Lattices and Order 。我也不知道相不相关