指称语义学习笔记1

2010-04-26 黄毅

资料:

什么是程序的语义?程序语义就是说一个程序的含义,拿到一个程序,如何说出它究竟是什么含义。通常作为程序员,我们习惯在大脑中模拟程序的运行,通过运行过程中内存结构的变化来理解一个程序的语义,比如 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的语义就完全是采用指称语义的方式来描述的。

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

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 0undefined 了。

未完待续...


blog comments powered by Disqus

转载请注明出处,收藏或分享这篇文章到: