==================
指称语义学习笔记1
==================

资料： 

* 很haskell http://en.wikibooks.org/wiki/Haskell/Denotational_semantics
* 很数学 http://zh.wikipedia.org/zh-cn/指称语义

什么是程序的语义？程序语义就是说一个程序的含义，拿到一个程序，如何说出它究竟是什么含义。通常作为程序员，我们习惯在大脑中模拟程序的运行，通过运行过程中内存结构的变化来理解一个程序的语义，比如 `c=a+b` 这个表达式的含义就是从 `a` `b` 两个单元取数据相加并存放到 `c` 这个单元。只是这种对语义的描述方法不严谨，比如我们继续追问单元是什么，寄存器呢还是内存单元，等。如果这样一直追问下去，要成功解释一个程序的语义，得把编译器的实现都拿出来才有把握准确描述。

而语义学就是研究描述程序含义的形式化的方法。正如我们使用BNF这种语言来描述程序设计语言的语法，语义学也希望用一套形式化的语言来描述程序设计语言的语义。

指称语义是描述语义的一种方式，它把程序看作是从一个数学对象（即所谓的指称）到另一个数学对象的映射（因为我个人只对集合的概念有感觉，所以我通常就把这个数学对象当作集合了）。比如 `c:int = a:int + b:int` 就是集合 `(int,int)→int` 的映射，如果要继续追问， `int` 是什么， `int` 就是整数集合， `+` 就是整数的加法，这下就比较放心了，因为我们这就靠上了数学这座山。

实际上，这时候我们就能看出纯函数式语言和命令式语言的差异来了，比如 Integer->Integer 这样一个函数，利用指称语义，我们可以说它就是从整数集合到整数集合的一个函数，但且慢，如果这是个命令式的语言呢，它的实现里面可能会去修改一些全局变量，也可能执行IO操作，简单说它是整数到整数的函数并不能完全描述它的含义。所以要描述一个命令式语言的语义，最终你发现不得不从它具体一步一步的执行过程去理解。而纯函数式语言，通常是可以抛开其执行过程去谈它的语义的。事实上，函数式语言也确实存在多种求值策略（call-by-value，call-by-name，call-by-need），对应不同的执行方式。对于命令式语言有另一种形式语义与其对应，叫操作语义，不过这个就不是本文的谈论对象了。

实际上，haskell98的语义就完全是采用指称语义的方式来描述的。

到这里，对于指称语义是什么就有了大概的了解了，不过深入一点看，我们会发现一点问题。上面我们把程序的函数直接当作是集合之间的函数来理解，但是我们看下面这个函数的定义：

.. code-block:: haskell

    shaves :: Integer -> Integer -> Bool
    1 `shaves` 1 = True
    2 `shaves` 2 = False
    0 `shaves` x = not (x `shaves` x)
    _ `shaves` _ = False

这就是传说中的理发师悖论在haskell代码中的呈现，如果说 `shaves` 是函数映射的话， `shaves 0 0` 要映射到哪里去。这说明我们前面介绍的对函数的解释方式还是存在漏洞。

要解决这个问题，需要给所有类型引入一个 `undefined` 的值，这样我们就可以说 `shaves 0 0` 是 `undefined` 了。

未完待续...