《编程语言概论》笔记

Programming Language一直是一门神课，不同人开设的课程可以从头到尾完全不一样。

第一遍学PL的时候是08年，接触Scheme和Prolog，对于常年c、java、c++的我来说，
感觉就是“别有天地非人间”一样，崭新的天空、崭新的大地。
到最后自以为融会贯通了很多，也总结了不少Meta的东西，
但现在我深知当时很多我都理解不到位，而且后来那么多年也忘得差不多了。

这次是第二遍学习，已经过了5年，这次从Standord ML开始，再到学完了Racket
利用ML写了些static-type的语法分析相关的函数，
又站在的dynamic-type的角度用Racket写了一个简单的解释器。
function + environment = closure 这个思想已经深入我心。
所谓environment，也就是一个variable->value的map而已。

可惜编译学得太早，命令式语言又牵扯一坨的堆栈，
去你妹的堆栈，误人子弟——
现在看看无非就是把environment拆成两个map
一个是variable->location，另一个是location->value。
唉……过几年再修一遍编译原理好了。

以下是我第一次接触的概念，Soundness and Completeness
假设 some thing X we wish to prevent.

For both, the definition is with respect to some thing X we wish to prevent. For example, X could be “a program looks up a variable that is not in the environment.”

A type system is sound if it never accepts a program that, when run with some input, does X.
A type system is complete if it never rejects a program that, no matter what input it is run with, will not do X.

这两句绕了我好半天，所以整理解释如下：

解释器/编译器的目的：证明X不会发生
sound
不可漏过一个“X”
→证明的全是真的。（接受的程序绝不会发生X）
compelte
不可错杀一个“非X”
→真的全可以证明。（所有X不发生的程序都可以接受）
unsound
漏过一个”X”
→证明的可能有假的。（接受的程序可能发生X）
uncomplete
错杀一个”非X”
→真的也可能证明不了。（某种X不发生的程序可能不接受）

根据《计算理论》
一个编译器的以下三条性质不可同时满足
(a) always terminates,
(b) is sound,
(c) is complete.
由于(a)太重要必须有，所以大部分PL编译器择(b)而舍(c)。
所以就有这种情况：
→你程序运行时是正常的，可是无法通过编译。

对于某些既不sound也不complete的编译器(c、c++)
属于week type，所以bug多！！