逻辑算法语言与CHR的对应关系及实现

### 逻辑算法语言与CHR的对应关系及实现 #### 1. 逻辑算法转CHRrp程序 逻辑算法可以翻译成等价的CHRrp程序，下面详细介绍翻译方案及相关对应关系。 - **翻译方案** - **集合与删除语义**：使用内部表示将断言作为CHR约束，包含断言本身和一个额外的参数（模式指示符），表示断言是正断言（“p”）、负断言（“n”）还是两者兼有（“b”）。对于程序P中出现的每个用户定义谓词a/n，TS/D(P)包含以下规则： ```plaintext ar( ¯X, M) \ a( ¯X) ⇐⇒ M ̸= n | true pragma priority(1) ar( ¯X, n), a( ¯X) ⇐⇒ ar( ¯X, b) pragma priority(1) a( ¯X) ⇐⇒ ar( ¯X, p) pragma priority(2) ar( ¯X, M) \ del(a( ¯X)) ⇐⇒ M ̸= p | true pragma priority(1) ar( ¯X, p), del(a( ¯X)) ⇐⇒ ar( ¯X, b) pragma priority(1) del(a( ¯X)) ⇐⇒ ar( ¯X, n) pragma priority(2) ``` 如果已有表示，优先级为1的规则会更新该表示；否则，优先级为2的规则会生成新表示。在较低优先级下，保证每个断言（无论正、负或两者兼有）在存储中由一个约束表示。 - **规则翻译**：对于LA规则r ∈ P，形式为r @ p : A1, ..., An ⇒ C，翻译步骤如下： - **拆分前件**：使用split函数将前件拆分为用户定义前件和比较前件。 ```plaintext split([A|T ]) = ⟨[A|Au], Ac⟩ if A is a user - defined atom ⟨Au, [A|Ac]⟩ if A is a comparison where split(T ) = ⟨Au, Ac⟩ split([]) = ⟨[], []⟩ ``` - **处理语义差异**：逻辑算法中一个断言可多次参与同一规则实例，而CHR中单个规则实例的约束必须不同。将单个LA规则翻译为一组CHR规则，每个CHR规则覆盖语法相等的头约束情况。 - **计算最一般合一**：对于给定分区ρ，计算最一般合一partition_to_mgu(ρ, [Au1, ..., Aum])。 - **过滤前件**：对每个⟨ρ, θ⟩∈ PU，计算filter(Au, ⟨ρ, θ⟩)，确保分区中每个集合只有一个代表。 - **添加模式指示符**：对剩余的用户定义前件添加模式指示符。 - **生成CHR规则**：对于每个⟨ρ, θ⟩∈ PU，CHR翻译TR(P)包含规则rρ @ H =⇒ g1, g2 | C′ pragma priority(p + 2)，其中⟨H, g1⟩ = modes(filter(Au, ⟨ρ, θ⟩))，g2 = θ(Ac)，C′ = θ(C)。 - **示例** - **Dijkstra最短路径算法**：LA实现如下： ```plaintext d1 @ 1 : source(V) => dist(V,0). d2 @ 1 : dist(V,D1), dist(V,D2), D2 < D1 => del(dist(V,D1)). d3 @ D+2 : dist(V,D), e(V,C,U) => dist(U,D+C). ``` 其翻译后的CHRrp程序为： ```plaintext er(V,C,U,M) \ e(V,C,U) <=> M \= n | true pragma priority(1). er(V,C,U,n) , e(V,C,U) <=> er(V,C,U,b) pragma priority(1). e(V,C,U) <=> er(V,C,U,p) pragma priority(2). er(V,C,U,M) \ del(e(V,C,U)) <=> M \= p | true pragma priority(1). er(V,C,U,p) , del(e(V,C,U)) <=> er(V,C,U,b) pragma priority(1). del(e(V,C,U)) <=> er(V,C,U,n) pragma priority(2). ... % (similar rules for source/1 and dist/2) d11 @ sourcer(V,p) ==> dist(V,0) pragma priority(3). d21/2 @ distr(V,D1,p), distr(V,D2,p) ==> D2 < D1 | del(dist(V,D1)) pragma priority(3). d31/2 @ distr(V,D,p), er(V,C,U,p) ==> dist(U,D+C) pragma priority(D+4). ``` - **并查集规则**：规则uf4 @ 1 : union(X,Y), find(X,Z), find(Y,Z) => del(union(X,Y))翻译为： ```plaintext uf41/2/3 @ unionr(X,Y,p), findr(X,Z,p), findr(Y,Z,p) ==> del(union(X,Y)) pragma priority(3). uf41/23 @ unionr(X,X,p), findr(X,Z,p) ==> del(union(X,X)) pragma priority(3). ``` - **LA与CHRrp推导的对应关系** 引入一个映射函数chr_to_la(σ)，用于将（可达的）CHR执行状态映射到LA状态： ```plaintext chr_to_la(σ) = {a( ¯X) | a( ¯X) ∈ A ∨ (ar( ¯X, M) ∈ A ∧ M ̸= n)} ∪ {del(a( ¯X)) | del(a( ¯X)) ∈ A ∨ (ar( ¯X, M) ∈ A ∧ M ̸= p)} where σ = ⟨G, S, B, T⟩n and A = G ∪ chr(S) ``` 有以下定理： - **定理2**：对于每个可达的CHRrp状态σ，如果σ ωp ↣T (P ) σ′，则要么chr_to_la(σ) = chr_to_la(σ′