第5章

抽象解释的两个理论模型





第4章比较详细地介绍了模型检验方法。我们知道，抽象解释首先由Cousot等于1977年提出，它作为程序设计和程序静态分析的统一框架，现在已经成为描述具体系统近似语义的一个基本方法理论，应用到许多计算机科学领域，其中包括程序检验。
经典抽象解释理论是在Galois连接或与之等价的闭包算子的关于抽象论域的框架下进行的，许多学者在这方面做了大量工作。本章将给出抽象解释的两个新的理论模型。因为这两个新模型是基于经典的全总域模型［69］和部分等价模型［70］的理论构造的，所以我们也把它们分别称为抽象解释全总域模型和抽象解释部分等价逻辑关系模型。但为了简便，常把“抽象解释”几个字省略，从上下文看，并不会引起混淆。
全总域模型也是在经典抽象解释理论方向上的工作，但是作为一个综合统一模型，它是对经典抽象解释的总结。就我们所知，它与目前现存的一切有关抽象解释文献所采取的框架是相容和等价的。全总域模型的主要作用如下。
（1） 作为经典抽象解释理论的统一模型，使我们可以进一步讨论一些有关抽象解释理论需要解决的几个基本问题，如完备性问题。
（2） 模型深化了经典抽象理论的一些概念。例如，我们提出了本质函数和亚本质函数概念，对泛型概念进行广义表述，它们在模型检验理论中都是有用的理念。
（3） 模型可以启发我们把抽象解释理论应用到软件工程领域（从设计到实现的过程），即从抽象设计到具体论域的实践。
如果说，我们提出的抽象解释全总域模型仍然符合传统抽象解释模型范式，是“抽象即简化”思维的发展，那么我们提出的抽象解释部分等价逻辑关系模型却和传统抽象解释模型根本不同，是“抽象即本质”思维的发展。
部分等价逻辑关系模型不像全总域模型那样是对原系统在“近似”意义上的抽象，而是对原系统上的一切关系（包括逻辑关系）在“本质”意义上的抽象。因此，它不是原系统的“简化”，而是原系统的一个“深化”。部分等价逻辑关系模型的主要作用如下。
（1） 模型认为，抽象论域是“部分等价关系”的集聚，而语义操作算子是“逻辑部分等价关系”的集聚。因此，除了要求具体或抽象语义算子具有一定的逻辑关系以外，该模型并不要求它们具有什么特殊性质，如单调性。
（2） 模型没有从“近似”意义上对具体域进行抽象，而是从“本质”上深化原系统。它分离出原系统的“性质”单元，比原系统可能更复杂。因此，该模型从另外角度深化了我们对抽象解释理论的理解。
（3） 它可以启发我们讨论与传统模型不同的问题，如复杂性和多态性问题。
5.1抽象解释全总域模型
5.1.1构造全总域模型

1. 具体语义论域
用S表示一个具体系统,其中元素可以是无限的。例如，在经典模型检验中，S是一个（具体的）Kripke结构，S中的元素表示系统的状态。下面我们用状态指称S中的元素，假设S是可数无限的，并称它为状态空间。我们用 (S)表示S的幂集，用它表示系统S的语义论域。 (S)中的元素是S的子集，它是S中状态组成的集合。对于任意a∈ (S)，它可以是S中有限子集合或是S中无限子集合。即
a={s1,s2,…,sn}或a={s1,s2,…,sn,…}
其中，si∈S是S中的状态，i=1,2,…,n,…。关于a的意义叙述如下。
(1) a可以表示一个（成员关系）谓词P,即每个si使该谓词P为真。如果适当扩展 (S)和/或S（扩展后仍记为 (S)）,则a还可以表示一个（任意元）的谓词。
(2) a可以表示某一属性（性质）φ，即每个si具有该属性（或该性质）φ。为了简单叙述下面引进的语义操作算子的单调性，在考虑属性φ时，我们限制“否定性质”到基本原子层次上，这和（模型检验）讨论LTL逻辑公式时所作的限制一样。
(3) a可以表示状态空间S的某些轨道可达到的状态集合。例如，在考虑程序“不变式”属性时，我们常常是这样做的［64］。当然，a也可以表示状态空间S中的一条（具有某性质）轨道，即s1,s2,… 是从s1出发的一条轨道的顺序出现的状态集合。不过为了表示循环轨道，必须扩展语义域 (S)和/或S，仍记为 (S)，则a也可以表示状态空间中的循环轨道。
(4) a可以表示一个类型T，准确地说，它是类型T的值域，即a中所有元素si都属于类型T。
总之，我们在非常广泛的意义上，理解 (S)中的元素的语义特征，如果需要，还可以扩展S和/或 (S)使它们可以表达更多的内容，如文献［64］ 的时序模型（Temporal Models）。为了确定起见，我们称 (S)中的元素为属性，这样也较直观些。同样，我们也可以在 (S)上建立（一般）格结构。例如，在集合包含的自然序下， (S)的任意子集都有最小上界和最大下界，所以 (S)是一个完备格。为了确定起见，不妨认为 (S)是一个完备格，且沿用集合论包含符号，作为格中序关系，并在直观上也把它作为集合包含关系理解。也就是说， (S)是权当作在集合论包含自然序下组成的格。但这时，若a,b∈ (S),ab，则认为a较b更精确，即b是a的近似。
2. 抽象语义总域
在经典抽象解释框架中，依据具体状态幂集的抽象解释，Golois连接和闭包操作是等价的。闭包操作具有独立于抽象元素表示法的优点，如果推理不涉及抽象表示内涵，用闭包操作作为抽象语义领域是比较方便的。因此，我们用uco( (S))表示系统S的抽象语义全总域，其中任意元素μ∈uco( (S))是一个闭包，即μ是具体语义域 (S)的一个抽象语义域，而全总域uco( (S))是所有抽象语义域的集合。对于闭包μ∈uco( (S))，它可以从以下两个等价角度定义。
（1） μ是 (S)上单调、幂等、扩展的操作，因此可以把μ看作函数。即设a和b是 (S)中任意两个元素，若ab，则μ(a) μ(b)（单调性）； μμ(a)Δμ(μ(a))=μ(a)（幂等性）； μ(a) a（扩展性）。
（2） μ是由它的不动点唯一确定的，且μ在 (S)上操作的所有不动点组成的集合与μ的像集μ( (S))一致。因此,可以把μ看作 (S)中的子集合，即
μ( (S))={a∈ (S)|μ(a)=a}
今后称任意闭包μ∈uco( (S))，我们互用它的函数和集合两种表示。值得注意的是，a∈ (S)表示系统S某个属性φ，于是由μ∈uco( (S))的扩展性μ(a) a，就可以认为一个闭包是将一个任意的a∈ (S)到a的满足某个性质的最小超集的映射，而那个最小超集可以看作属性φ的从上面的一个最“精确”近似。实质上，关于μ的两种等价定义，我们有： a∈ (S)，μ∈uco( (S))，μ(a)=∩{b|ab且b∈μ}。
所以，若μ(a)=b′，b′就是最接近a的一个近似表示。
在经典抽象解释框架下，这种近似就称为抽象。这也是我们称任意闭包μ∈uco( (S))为具体语义域 (S)的一个抽象语义域的原因，而uco( (S))就是所有抽象语义域的全总域。
对于任意闭包μ∈uco( (S))，μ由S的子集合组成，按照集合的包含自然序，μ可以构成一个完备格，虽然它未必是 (S)上的完备子格。若a,b∈μ，ab，则称a较b精确，即b是a的一个近似。对于全总域uco( (S))，我们在抽象域之间规定一个序 ，它就是通用的函数之间的逐点序。这样任意两个闭包ρ,η∈uco( (S))，ρ η，即a∈ (S)，都有ρ(a) η(a)（等价地，η( (S))ρ( (S))），它表示在uco( (S))全总域，ρ较η精确，η较ρ抽象。于是，uco( (S))在逐点序 下也构成一个完备格。
3. 具体语义操作和抽象语义操作
我们用f表示 (S)具体语义域上的一个语义操作，为了简单起见，只考虑f:  (S)→ (S)是 (S)上的一元单调函数情形。因为对一般情况的单调函数可以类似处理，例如，当我们考虑完备性问题时，文献［46］指出，可以把n元函数的完备性问题划归为一组一元函数的完备性问题。更复杂一些，回忆前面说过的扩充 (S)和/或S，可以使 (S)具有需要的语义属性，同样能使用递归配对函数或参数分离处理多元函数，甚至利用并行系统还可以处理不确定的语义操作，因此只考虑一元单调函数并不丧失一般性。下面互用语义操作和语义函数两个术语。
对于任意语义函数f，若ρ,η∈uco( (S))是两个任意闭包，令
fρ,ηΔηfρ(5.1)
为f的关于〈ρ,η〉的抽象语义操作。在经典抽象解释框架中，fρ,η为f在抽象域ρ,η上的最正确近似抽象语义操作。注意ρ和η也可以是同一个闭包。
合理性和完备性是经典抽象解释理论里最基本的两个概念［4547］。
f是任意具体的语义函数，ρ和η是任意两个闭包，f#:ρ→η是对应的在〈ρ,η〉上的抽象语义函数，若
ηf f#ρ(5.2)
则称f#为合理抽象语义函数。注意，合理性与近似性等价。由此观之，最正确近似fρ,η自动满足式(5.2)，这是由于ρ,η都是单调函数且满足幂等性的缘故。若f#是〈ρ,η〉上的任意一个合理抽象函数，因为ηf f#ρ，于是ηfρ f#ρρ，根据ρ的幂等性，可得ηfρ f#ρ，再根据fρ,η的定义和f#的定义域，所以fρ,η f#关系成立，这也是我们称fρ,η是最正确近似的原因。
沿用上面的术语，如果式(5.2)成立，即
ηf=f#ρ(5.3)
则称抽象解释f#关于f在〈ρ,η〉上是完备的。下面我们将证明这时fρ,η关于f在〈ρ,η〉上也是完备的。所以,为了方便，这时也称〈ρ,η〉关于f是完备的。上下文不会混淆，我们互用f#（fρ,η）完备或〈ρ,η〉完备两个术语。
更进一步，如果给定〈ρ,η〉，f#关于f是完备的，则fρ,η也是完备的，并且fρ,η与f#一致。实际上
f#=(因为ρ,η的幂等性)
f# ρ=(由f#完备性定义： 式(5.3))
ηf (由fρ,η的合理性： 式(5.2))
ηfρ (由近似性： fρ,η f#)
f#
鉴于此，式(5.3)也可以改写为ηf=ηfρ（今后将此式也记为式（5.3））。
所以这里只讨论最正确近似抽象fρ,η，除非特殊声明，我们把fρ,η简记为f#，即在定义抽象语义操作时，只用式(5.1)。因为f# =fρ,η=ηfρ，它是ρ→η上相应于f的抽象语义函数，所以直观上它是这样的抽象语义函数： 首先强制实参x∈ (S)为闭包ρ中的元素，接着应用f，然后强制结果为闭包η中的元素。可以看出，若x∈ρ，则fρ,η(x)=ηfρ(x)∈η，因此，fρ,η实质上是一个特殊的“具体”语义函数，限制它的定义域和值域分别到ρ闭包集合和η闭包集合上，即fρ,η是ρ→η函数，是在〈ρ,η〉上关于f的抽象语义操作。
令F={f|f:  (S)→ (S),(单调)具体语义函数}是所有具体语义函数的集合，用FF表示F的子集合，它是若干个语义操作的集聚。并用F#={f#|f∈F,ρ,η∈uco( (S)),使f# =ηfρ}表示所有抽象语义函数的集合，同样记F# F#为相应于具体语义函数集聚F的抽象语义函数集聚。
4. 全总域模型 
按照前面的叙述，实际上我们已经为抽象解释框架构造了一个模型，称为全总域模型，它是一个5元组
A={S, (S),uco( (S)),F,F#}(5.4)
其中，每个符号的解释如上所述。
例5.1闭包示例［45,46,71］
Z表示整数集合， (Z)是Z中所有子集合组成的集合。用集合包含关系，(Z, (Z))构成具体语义论域体系，它是一个完备格。现在考查经典符号关系，令0+={x|x∈Z,x≥0}，-0={x|x∈Z,x≤0}，0={0}； 表示空集，Z表示全集。使用上述符号可以定义 (Z)上的一个闭包ρs={Z,-0,0+,0,}。
考虑具体逐点乘法运算*：  (Z)2→ (Z)，其定义为： X∈ (Z),Y∈ (Z)，X*Y= {x·y|x∈X,y∈Y}，以及抽象乘法运算#： ρs2→ρs。按通常乘法符号法则定义，有-0#0+=-0； 0#0+=0； -0#-0=0+，等等。
下面证明，#关于*在〈ρ2s,ρs〉上是完备的。因为，对于Z1,Z2∈ (Z)，有
ρs(Z1Z2)=ρs(Z1)#ρs(Z2)
若记f=*，则f#=*#，且把Z1 *Z2写成*(Z1,Z2)形式，类似地，ρs(Z1)#ρs(Z2)写成#(ρs(Z1),ρs(Z2))形式，则上式即为ρsf=f#ρ2s。它符合完备性定义（式(5.3)），只要在式(5.3)中令η=ρs，ρ=ρs×ρs=ρ2s即可得到。例如，ρs({-1} * {-2})=ρs({2})=0+=-0 *# -0=ρs({-1}) *#ρs({-2})。于是，用闭包ρ2s和ρs描述具体乘法符号规则是适宜的。严格地说，这里所说的f和f#的定义域分别是前面定义中情况的扩充。前面只是为了叙述简便，才做了一些简化，并不失一般性。
例5.2全总域示例［45,46,71］
沿用例5.1中的符号，定义sign={Z,-0,0+,0,}，现在把sign当作具体域，我们可以考虑sign所有可能的抽象闭包如下。
ρ1={Z},ρ2={Z,0+},ρ3={Z,0},ρ4={Z,},ρ5={Z,-0},ρ6={Z,0+,}
ρ7={Z,0+,0},ρ8={Z,0,},ρ9={Z,-0,0},ρ10={Z,-0,}
ρ11={Z,0+,0,},ρ12={Z,-0,+0,0},ρ13={Z,-0,0,},ρs=sign
于是，uco(sign)在逐点序 下也构成一个完备格。所有可能抽象闭包构成的完备格如图5.1所示。

从上述模型的构造流程中可以看出现今文献关于经典抽象解释所采用的框架，在隐蔽形式或等价形式下，都与式(5.4)的框架相容。利用式(5.4)模型，至少可以讨论有关抽象解释的大部分重要问题。


图5.1uco(sign)完备格

（转摘于文献［46］图2）



5.1.2理论性问题
1. 最优完备存在性
在式(5.4)框架中，对任意具体语义函数f，无论η如何确定，只要令ρ= (S)，则式(5.3)成立，即
ηf=ηfρ
也就是说，只要选择ρ= (S)，对任意的f和η，抽象语义函数fρ,η关于f是平凡完备的。
同样，若选择η={S}，即η映射 (S)任意子集为基本集合S，对于任意f∈F，任意ρ∈uco( (S))，式(5.3)也成立，即
ηf=ηfρ={S}
也就是说，只要选择η={S}，f∈F，ρ∈uco( (S))，抽象语义函数fρ,η关于f是平凡完备的。
根据文献［46］,若〈ρ,η〉关于f完备，ρ δ∈uco( (S))和η β∈uco( (S))，则〈δ,β〉也关于f完备。也就是说，若〈ρ,η〉关于f完备，将ρ“精确化”到δ(δ( (S))ρ( (S)))，将η“抽象化”到β(β( (S)) η( (S)))，则〈δ,β〉也关于f完备。注意δ和β是从两个不同方向分别对ρ和η的“改良”，ρ→δ是延展，η→β是简化。
鉴于上述考虑，我们提出最优完备的定义。
定义5.1（最优完备）设〈ρ,η〉关于f完备，如果对任意关于f的完备抽象〈ρ′,η′〉，都有
ρ ρ′，η η′(5.5)
则称ηfρ是f的最优完备抽象语义函数，也称〈ρ,η〉是f的最优完备抽象语义域。
根据文献［46］，对于最优完备〈ρ,η〉，无须进一步对ρ在精确化方向和对η在抽象化方向分别加以改进。同样，也无法进一步对ρ在抽象化方向和对η在精确化方向分别加以改进，若存在这样的改进〈δ,β〉，由于δ是ρ的抽象化，即ρ δ，由最优完备定义，ρ δ，所以ρ=δ； 由于β是η的精确化，即β η，由最优完备定义，η β，所以β=η。
因此，提出以下问题。
问题1对于具体语义函数f，是否存在它的最优完备抽象语义函数f#，或者它的最优完备抽象语义域？
对于函数族F，若〈ρ,η〉对于F中的每个函数都完备，则称〈ρ,η〉关于F完备。同样，也可以对于函数族F定义最优完备问题，即若存在〈ρ,η〉关于F完备，且对任意关于F的完备〈ρ′,η′〉，式(5.5)条件成立，则称〈ρ,η〉是F的最优完备抽象语义域。
问题2对于语义函数族F={f1,f2,…,fn}，是否存在它的最优完备抽象语义域？如果i=1,2,…,n,〈ρi,ηi〉关于fi最优完备，那么F的最优完备抽象语义域（如果存在）与〈ρi,ηi〉之间有什么样关系？即能否从〈ρi,ηi〉（i=1,2,…,n）构造F的最优完备？
根据文献［46］，设F为具体语义函数族，ρ,η∈uco( (S))，定义算子CρF和SnF如下。
CρF： uco( (S))→uco( (S))
其中,CρF(η)Δ {β∈uco( (S))|μ β,〈ρ,β〉关于F完备}。
SnF： uco( (S))→uco( (S))
其中，SηF(ρ)Δ {δ∈uco( (S))|δ ρ,〈δ,η〉关于F完备}。
再根据文献［46］，设F为具体语义函数族，ρ,η∈uco( (S)),若〈ρ,CρF(η)〉关于F完备，则称CρF(η)是关于F相对于ρ的η完备核； 若〈SηF(ρ),η〉关于F完备，则称SηF(ρ)是关于F相对于η的ρ的完备壳。
根据SηF(ρ)的定义，可知SηF(ρ)是一切满足定义的δ（δ ρ）的上确界，于是SηF(ρ) ρ，若它是（相对于η关于F）ρ的完备壳，则〈SηF(ρ),η〉是〈ρ,η〉在ρ上向精确化方向的一次改良。
同样，CρF(η) η，若它是（相对于ρ关于F）η的完备核，则〈ρ,CρF(η)〉是〈ρ,η〉在η上向抽象化方向的一次改良。
问题3给定具体语义函数族F，其最优完备（如果存在的话）〈ρ,η〉能否通过初始化ρ={S}，η= (S)递归运用SηF(ρ)、CρF(η)算子分别对ρ在精确化方向、对η在抽象化方向进行改良而得？
2． 最优函数存在性
回忆前面关于抽象语义函数f#=ηfρ的解释，对于给定的闭包ρ,η∈uco( (S))，仿照λ演算，定义
ρ→ηΔλf: F.ηfρ(5.6)
其中，f: F，表示f∈F，其直观意义是所有的关于闭包〈ρ,η〉上的抽象语义函数的集合。现在我们证明ρ→η中的元素是外延的。
ρ→η的任务是取任意具体语义函数f，并产生这样的函数ηfρ，即它把每个函数f强制为从ρ的值域到η的值域的抽象函数。因此，若对所有x∈ρ，有
(ηf1ρ)x=(ηf2ρ)x
又注意到限制x∈ρ是无关紧要的，所以x∈ (S)，都有(ηf1ρ)x=(ηf2ρ)x，于是
λx.(ηf1ρ)x=λx. (ηf2ρ)x（5.7）
根据复合的意义，在式（5.7）成立的意义上，应该有ηf1ρ=ηf2ρ，这意味着ρ→η的值域对于每个在 (S)上入射ρ到η的单调函数恰好包含一个代表，这说明ρ→η模型是外延的。下面的讨论就是基于上面叙述的直观意义，把ρ→η看作关于闭包〈ρ,η〉上的抽象语义函数的集合。
可以看出，若f已经是一个从ρ到η的（具体）语义函数，也就是说，一旦x∈ρ，就有f(x)∈η，那么对所有的x∈ρ，有f# (x)=ηfρ(x)=f(x)，基于这样的观察，我们引入下面的定义。
定义5.2（本质函数和亚本质函数）
（1） 若对任意x∈ρ，f(x)=f# (x)∈η，则称f是ρ→η中的本质（具体）函数。换言之，把f的定义域限制到ρ闭包上，记为f↓ρ，则f↓ρ≡f#。
（2） 若对任意x∈ (S)，ηf=f#=ηfρ，则称f是ρ→η中的亚本质（具体）函数。对于亚本质函数f，〈ρ,η〉是完备的抽象语义域。
因此，（亚）本质函数是ρ→η类中的特殊函数族。直观意义是，设计一个系统（检验一个系统也一样）时，我们对系统的特性、功能和行为都应有一个预先的设想，这些设想就是抽象语义域及其在抽象域上的操作。当我们实现系统时，具体的语义域及其上的操作受到技术及其环境的限制，自然要复杂迂回得多。所以，本质函数和亚本质函数反映了理想操作的忠实可靠的实现。在这个意义上，它们都是最优函数族。
问题4如果ρ和η抽象语义域构想完美，能否解决技术上的问题，使实现ρ和η的具体语义域上的操作都是本质函数或亚本质函数？或者说，能否改进具体语义操作到至多是只用亚本质函数就能解决的实际问题（如完备性）？
在一般意义上，〈ρ,η〉抽象域比具体语义域 (S)简单，而ρ→η上的抽象语义函数也比 (S)→ (S)上的具体语义函数少。所以在模型检验应用中，我们从两方面（域和操作）做了简化，只要解决了完备性问题，那么模型检验中的高期望强保留特性就能满足。
可惜的是，从问题1到问题4，至今仍然没有“彻底”解决。文献［46］指出： 以可能最好的方式，即最小化延展或简化正在考虑的抽象域和操作算子，使抽象解释完备，仍然是一个开放问题。甚至，寻找某些合理的很强的条件施加于具体语义域和/或具体操作算子，使抽象域的不动点完备壳存在，一般来说都是不能保证的。因此，对于上述问题，是否能够定义某种“近似”标准和“近似”计算，寻找相关问题的某种意义上的“最优”解决，这些都是值得探讨的。
3. 与不可预知多态模型类比
简写V=uco( (S))，并用记号ρ: V表示ρ∈uco( (S))，定义
→#Δλρ:V.λη:V.(λf:F.ηfρ)(5.8)
表示所有的抽象函数的集合。式(5.8)表明它可以看作式(5.4)全总域模型A中的元素F#，即→#=F#。
改写→#为，即
=λf:F.(λρ:V.λη:V.ηfρ)=λf:F.(λ〈ρ,η〉:V×V.ηfρ)(5.9)
于是，f的定义域为V×V=uco( (S))×uco( (S))，值域为{ηfρ}，即
f=λ〈ρ,η〉:V×V.ηfρ:V×V→ηfρ(5.10)
直观上，f是抽象函数族，它是具体操作f的泛化，在不同的〈ρ,η〉上呈现出不同的特性，具有多态特征。在某种意义上，它体现了多态性或泛型性。
现在扩展式(5.4)的全总域模型A如下，扩展后记为A′。
A′={S, (S),uco( (S)) ,F,F#,{ρ→η},{f}}(5.11)
A′是7元组，其中符号是自明的。例如,{ρ→η}是一切形如式(5.6)定义的函数族的集聚,其中ρ→η是在固定的闭包对〈ρ,η〉上讨论每个具体操作相应的抽象操作，重点是具体操作和抽象操作之间的对应关系； {f}是一切形如式(5.10)定义的函数族的集合，其中f是讨论具体操作f的在每对〈ρ,η〉闭包上的多态表现，即f是f的泛型。
式(5.11)模型总的想法是： 一个多态函数是一种可以作用在多种“类型”实参上的函数。在某种意义上，该多态函数在各个类型上使用了“本质同样的算法”。例如，对于具体语义函数f，式(5.10)定义的f，它可以作用在所有“类型”的〈ρ,η〉上，因为在每个〈ρ,η〉上，它都是相应于f的抽象语义函数ηfρ，所以它们的算法在本质上具有“共性”。关于它的具体实例可以参考文献［39］中的Pw模型。
随着网络技术的发展，现代社会已经处于一个信息爆炸的时代。为了能够从大量数据中寻找有意义的新的关系和模式，数据挖掘技术从而诞生。事实上，人类研究自然现象、社会现象，大都采用一般途径。根据大量经验数据，通过各种定性分析或定量分析，对数据加以整理，归纳产生抽象解释，进一步将这种抽象解释总结成理论，甚至上升到“定律”高度。如果从这个角度考虑问题，式(5.4)和式(5.11)所示的模型还具有方法论意义。

数据挖掘是指从大型数据库中提取潜在有用的知识，将这些知识表达为概念、规则、规律和模式等形式。抽象解释也和人类认知思维类似，从大量的数据中提取感兴趣的知识，加以抽象，上升为模型。
前面提出的问题1到问题3，都是立足在{ρ→η}上讨论，怎样改良〈ρ,η〉使具体语义函数和抽象语义函数之间满足（例如）完备性关系； 而问题4立足于{f}，讨论怎样设计良好操作，使它具有“安全”的泛型，即它一切泛化都具有完备特性。再把A′与文献［39］相比较，A′与其使用Pω的闭包构造出来的模型在许多方面都是类似的。实际上，A和A′模型都是受到文献［39］的启发构造出来的。文献［39］构造的模型是λ→,（不可预知多态）模型，因此有以下问题。
问题5基于A′，能否构造一个有关抽象解释的计算理论？
综上所述，针对现有的抽象解释理论构造了一个统一模型，并把它称为抽象解释全总域模型。在该模型上，可以很方便地讨论经典抽象理论的一些问题，如完备性问题等。并且在该模型的基础上，提出了本质函数和亚本质函数的概念，以及对泛型概念给出了其广义表达方式。这个模型一方面可以深化我们对经典抽象理论概念的理解，另一方面可以作为抽象解释理论的基础。如果以上提出的开放性问题能够得到解决，那么通用性模型将有助于人们处理各个应用领域中存在的复杂结构及特性等问题。
5.2抽象解释部分等价逻辑关系模型
现在采取另外的观点，认为抽象论域是“部分等价关系”的集聚，而语义操作算子是“逻辑部分等价关系”的集聚，提出一个新模型部分等价逻辑关系模型。这个模型除了要求具体或抽象语义算子具有一定的逻辑关系以外，并不要求它们具有什么特殊性质，如单调性，因此它与传统模型不同，同样也与全总域模型不同。尤为重要的是，该模型并没有从“近似”意义上对具体域进行简化，反而是从“性质”上深化原系统，在某种意义上，它分离出原系统的“性质”单元，比原系统可能要复杂些。因此，基于这样的模型，可以讨论与传统模型不同的问题，如复杂性和多态性问题，从而深化我们对抽象解释理论的理解。
5.2.1具体语义域和语义函数
用S表示一个（可能是无限）的具体系统，例如在模型检验中，经典的方式通常将系统S表达为一个Kripke结构，S中的元素表示具体系统的状态。以下称S中的元素为状态，并认为S是可数无限的，称S为（具体）状态空间。
通常，系统S由许多组件组成，各个组件内部和各个组件之间都存在着一定的关系，下面用部分等价关系和逻辑部分等价关系分别概括组件内部的元素性质和组件内部元素之间以及组件和组件之间的相互作用。首先引入几个概念。
（1） 部分等价关系per的含义就是一个成员关系谓词和一个等价关系［39］。具体地说，系统S上的一个部分等价关系是S的某个子集上的等价关系。例如，序偶〈S′,R〉，其中S′ S，且RS′×S′是一个等价关系。然而，由于只通过S′={a|aRa}就可以决定S′，所以子集S′在技术上是多余的。注意到，R是子集S′上的等价关系，当且仅当R在（全域）S上是对称和传递的。因此，一个部分等价关系是一个S上的对称和传递关系。部分等价关系的一个直接有用的事实是： 对于任意per R，若aRb，则aRa［39］。今后当我们说R是一个部分等价关系时，用|R|Δ {a|aRa}指代R在其上是一个等价关系的子集S′。
（2） 若S上的一个部分等价关系是逻辑关系时，则称此部分等价关系为逻辑部分等价关系。逻辑关系和逻辑部分等价关系的定义可以参阅文献［39］。粗略地说，文献［39］认为，逻辑关系R在本质上是类型化关系的集聚{Rσ|σ是一个类型}，使类型σ→τ的关系Rσ→τ以保证在作用和λ抽象下闭合的方法意义上由关系Rσ和Rτ确定。类似部分等价关系per的定义，逻辑部分等价关系（逻辑per）R是指它使每个Rσ是对称和传递的。我们的模型主要是在思想原理上借用上述概念阐述的理念。
下面举例阐述本章用到的有关函数之间的逻辑关系的含义。设f,g： A→B是映射A到B上的两个函数，如A内和B内元素之间分别存在关系R,T，若x,y∈A，xRy，都有f(x),g(y)∈B且f(x)Tg(y)，则称f,g满足A→B上关于函数的逻辑关系。注意，在函数的逻辑关系定义中，并没有考虑R和T的per性。但在下面我们将看到，当考虑系统所有部分等价关系“对”上的函数逻辑关系时，如果上述函数逻辑关系是所讨论的系统中的一个对称和传递关系，则称它为（函数）逻辑部分等价关系，这里只用到此类型的逻辑per。
下面构造具体语义域及其上的语义操作算子。
用{R}表示S上所有部分等价关系集聚，更直观些，{R}={〈S′,R〉}，其中序偶〈S′,R〉，表示R是S的子集S′上的等价关系，即|R|=S′。下面互用{R}、{〈S′,R〉}和{〈|R|,R〉}等记号。{R}就是我们在S上构造出来的具体语义域，简记为U，即U={R}={〈S′,R〉}={〈|R|,R〉}。需要强调的是，也有可能在一个子集S′上存在不同的等价关系。例如，有两个等价关系R1和R2，则〈S′,R1〉和〈S′,R2〉应视为是U中的不同元素。当把部分等价关系看作全域上的一个对称和传递关系时，更容易理解上述规定。
设〈S1,R1〉和〈S2,R2〉∈U，只讨论从S1到S2满足以下性质的函数，f:S1→S2，即对任意x,y∈S1，且xR1y，有f(x),f(y)∈S2且f(x)R2f(y)。直观上看，f和它自身满足S1→S2上的函数逻辑关系。为了强调此种类型逻辑关系，特别用符号
f: 〈S1,R1〉→〈S2,R2〉表示满足上述性质的函数，并称f为从〈S1,R1〉到〈S2,R2〉上的语义函数（或语义算子），有时简称它为从S1到S2的语义函数（操作），如果不会产生歧义，简称f为函数。注意在上述定义中，也有可能〈S1,R1〉=〈S2,R2〉，即它们是同一个部分等价关系，这时f就是一个部分等价关系内部的语义操作。也就是说，部分等价关系内部以及部分等价关系之间的操作，我们都视为满足函数逻辑关系的操作。
用符号［〈S1,R1〉→〈S2,R2〉］（或简记为［R1→R2］）表示从〈S1,R1〉到〈S2,R2〉所有语义操作的集合，在［〈S1,R1〉→〈S2,R2〉］集合上定义一个等价关系如下： 即若f,g∈［〈S1,R1〉→〈S2,R2〉］，对x,y∈S1,xR1y，有f(x),g(y)∈S2，且f(x)R2g(y)，也就是我们前面所说的f,g满足S1到S2上函数逻辑关系，显然如此定义的关系是等价关系。
用符号U→U={［〈S1,R1〉→〈S2,R2〉］}表示系统S所有的语义操作的集合，则上面在［〈S1,R1〉→〈S2,R2〉］上定义的等价关系（即S1→S2的函数逻辑关系）就是整个讨论的U→U上的一个逻辑部分等价关系。今后记语义操作集合U→U上的一个部分等价关系为R→T，它是［R→T］=［〈|R|,R〉→〈|T|,T〉］上的等价关系。因此，U→U上的部分等价关系详细写出来应是一个序偶〈［R→T］,R→T〉，但我们简写它为R→T，因为对这个序偶的成员关系谓词，有
［R→T］={f|f(R→T)f}
它也可以通过R→T唯一确定。
鉴于我们的目的是“关注”（部分）逻辑关系，所以常常局限语义操作算子集合U→U为其上的部分等价关系的集聚。即使这样，为了节省符号，仍然用U→U符号表示。总之，对于具体系统，在其状态空间上规定了语义域U={R}={〈|R|,R〉}以及语义操作算子集合U→U={(R→T)}={〈［R→T］,R→T〉}。直观上，U中的每个per表示系统中一些元素间的某个固有性质关系，而U→U中的每个per表示系统中一些元素之间的动态联系或相互作用的关系。注意，这里的符号虽然有点混用，即现在仍用U→U表示所有函数逻辑部分等价关系的集合，通过上下文应不至于混淆。
5.2.2抽象解释
首先引入几个概念和符号。
（1） 因为一个per RS×S是一个子集|R|={s|sRs}上的等价关系，这样的per R的“元素”就是等价类［s］R={t|sRt}，对于s∈|R|［39］。
（2） 因为一个逻辑per R→T∈U×U是一个函数子集［R→T］上的等价关系，因此R→T中的“元素”就是等价类［f］R→T={g|f(R→T)g}，对于f∈［R→T］。
下面构造抽象语义域和抽象语义操作。
对每个per RS×S，它的成员关系谓词成立的集合为|R|，令|R|*由|R|中元素的等价类组成，即|R|*={［s］R|s∈|R|}。于是，如果R*为R的抽象，它也应为|R|*上的等价关系，显然，R*应是|R|*上的恒等关系。直观上，在抽象层次上，R*与|R|*应视为等同，即原先在|R|上的等价关系R已经转变为|R|*上恒等关系R*。于是令U*={R*}={〈|R|*,R*〉}，R*就是U*上的一个部分等价关系，它相应于U={R}中具体的per R。特别地，若R1与R2都具有相同的成员关系谓词S′，则|R1|*和|R2|*应视为两个不同的集合，前者为{［s］R1|s∈S′}，后者为{［s］R2|s∈S′}。对于元素s∈S′，［s］R1和［s］R2是s在S中不同的两个副本。
类似地，若记［R→T］*为［R→T］上（函数）元素等价类的集合，［R→T］*={［f］R→T|f∈［R→T］}，则应定义R→T的抽象(R→T)*是［R→T］*上的恒等关系。在抽象层次上，(R→T)*与其成员关系谓词成立的集合［R→T］*等同。若记(U→U)*={ (R→T)*|(R→T)*是［R→T］*上的恒等关系}，则(R→T)*就是(U→U)*论域上的一个部分等价逻辑关系。今后称(R→T)*中的元素［f］R→T是抽象语义操作算子，(U→U)*是相应于所有具体语义操作算子的抽象语义操作算子集合。特别要强调的是，［f］R→T实际上是|R|*→|T|*上的函数，即把原先定义在|R|→|T|上的函数转化为该函数所属等价类［f］R→T表达的一个从|R|*到|T|*的函数，而且与等价类［f］R→T的代表无关。
总结如下： 对应于具体状态空间S={s}，具体语义域U={R}，具体语义操作算子集聚U→U={R→T}，我们定义抽象状态空间S*={［s］R|R,s∈|R|}，抽象语义域U*={R*|视R*={［s］R|s∈|R|}}，抽象语义算子集聚(U→U)*={(R→T)*|视(R→T)*={［f］R→T|f∈［R→T］}}。这样，便构造了抽象解释的一个部分等价关系模型，它是一个六元组
A={S,U,U→U,S*,U*,(U→U)*}

这个模型的优点是它并不要求具体的或抽象的语义操作算子有特殊的性质（如单调性），它只反映系统功能上的逻辑关系。所以，这里的抽象并不是经典意义上的抽象，经典处理方法大致把对具体状态的某种近似称为抽象，并要求具体语义域和抽象语义域是特殊的数学结构，如是格或cpo，这是由“近似”作为抽象的基本内涵所致。而这个模型利用部分等价关系和逻辑部分等价关系，把具体系统S从语义域和语义操作两个方面结构化，即把它们的组件一一析取出来，最后形成在{［s］R}集合上讨论语义域和语义算子，其中语义域U*由{［s］R}上的一些子集组成，即U* ({［s］R})，而语义算子便是定义在U*上的一些（部分）函数。
5.2.3理论问题
1. 复杂性问题
从前面的叙述不难看出，f∈［R→T］，［f］R→T在功能上与f完全一致，所以在我们的模型中并不存在经典抽象框架中遇到的完备性问题。然而，我们的模型却存在另一个问题。表面上抽象状态［s］R是具体状态的一个等价类，似乎把状态空间S={s}换成抽象状态空间S*={［s］R}时，已经对具体状态空间进行了压缩。但事实并非如此，当S′S上存在不同的（部分）等价关系，或者s∈S使不同的部分等价关系成员关系谓词成立时，则S*中便存在许多形如［s］R1，［s］R2，…的副本。同样，对于操作函数也有类似的情况。例如，f:S→S是这样的函数，当它局限到|R1|→|T1|时，f∈［R1→T1］，也许它能局限到|R2|→|T2|成为［R2→T2］中的一个函数，即f∈［R2→T2］，于是在抽象结构中，也有［f］R1→T1，［f］R2→T2，…等副本。特别地，在全域S上，因恒等关系I是一个等价关系，所以可以视〈S,I〉为一个特殊的部分等价关系，这样抽象结构也可能有［f］I→I这个副本。前面已经说过，部分等价关系模型是非常细致地把原系统的组件按照特征析取出来，当考虑不同特征时，“同一”实体往往分离成“不同”的实体，因此，我们提出如下问题。
能否选取适当的部分等价关系和逻辑部分等价关系，使抽象结构不至于太庞杂？更进一步，能否在此抽象结构上，再使用基于“近似”意义的抽象解释手段，进行传统上的分析？
2. 与多态的关系
固定某一操作算子f:|R|→|T|，能否将它扩展使之成为U→U中不同元素中的成员，即在抽象结构中，应该有f的不同版本： ［f］R→T，［f］R′→T′，［f］R″→T″,…。这与程序设计语言多态理论有点相似。实际上，我们的模型就是受到λ→,的部分等价关系模型［39］的启发构造的（尽管与它在许多地方不同）。另外，文献［72］也提出了基于特殊定义的per发展的抽象解释的框架，但是它与我们模型的立足点是不同的。现在把上面的叙述总结为如下问题。
对任意的f，能否将它的逻辑功能泛化，使之在系统中不同的满足一定性质（表达为部分等价关系）的组件上都发挥相应的功能？
抽象解释的部分等价逻辑关系模型是基于部分等价关系和逻辑部分等价关系的一个模型。该模型认为抽象领域是“部分等价关系”的集聚，语义操作算子是“逻辑部分等价关系”的集聚。在该模型上，可以很方便地讨论经典抽象理论的一些问题，如复杂性和多态性问题等。这个模型一方面可以深化我们对经典抽象理论概念的理解，另一方面可以作为抽象解释理论的基础。