|
Scott 域的创建在 1969 年左右,对l-演算及程序语言的语义研究有着巨大的影响。语法使得人们或机器可以机械的完成计算、推理、知识获取等工作。人们研究形式逻辑的模型,又是为了了解和掌握形式系统中的人们原来不知道的东西。如果从哲学上看,形式系统就是理论,而模型就是人类的实践的世界,二者是人类认识进程中永远相辅相成的两方面。Scott
域原来是作为经典的不带类型的l-演算系统及程序语言的模型提出的,由于它深刻、丰富的内涵,完全可以作为更高级的形式系统(例如,带类型的l-演算等。)和更先进的计算机语言的模型。另外,β-归约在
Scott 域中可化的十分清楚,这是其他的模型所没有的。
一、序关系
定义8.2.1
定义8.2.2
定义8.2.3
定义8.2.4
引理8.2.1 [D1→D2]
在定义8.2.4中(2)所定义的序关系下是一个 c.p.o. 。而且,对[D1→D2] 的每一个有向子集合X
, d∈D1
, (∪X)(d) =∪( (d)
: ∈X
)
证明略。
引理8.2.2 任两个连续函数 、ψ的复合 ·ψ
,仍然是一个连续函数。这里 ∈[D1→D2],ψ∈[D2→D3],那么 ·ψ∈
[D1→D3]。
证明按常规验证即可。
|
|