利用相关逻辑与并行构造过程的模态逻辑方法

需积分: 3 60 浏览量更新于2024-08-02 收藏 1.26MB PDF 举报

本文主要探讨了相关逻辑（Relevance Logic）在并发（Concurrent）程序逻辑中的应用与重要性。首先，文章强调了组合性（Compositionality）在程序逻辑中的核心地位，即复合系统的性质可以通过其组成部分的性质推导得出，这对于逻辑的可处理性和实用性至关重要。对于并行系统，一个普遍的策略是通过将属性相对化，即根据平行环境的特性来调整属性，这样就产生了对属性的一个新的推理概念，通常表现为一种相关推理（Relevance Implication），它强调了推理过程中的非平凡关联。为了实现这种相关推理的可计算性和表达能力，作者建议采用模态逻辑（Modal Logic）或时间逻辑（Temporal Logic）扩展相关逻辑。这些扩展允许构建针对进程的组合逻辑，使得我们能够更好地理解和形式化并发系统的动态行为和交互。接下来，作者深入研究了命题相关逻辑的一般模型理论，引入了一种基于半 lattice（具有保下确界的二元操作的结构）的模型。在这个框架下，论文提供了多种对应关系和完备性结果，展示了与Sylvan和Meyer提出的三元关系模型之间的联系。同时，作者还构建了具体模型，这些模型是基于Milner的同步 Communicating Sequential Processes (SCCS) 的，这为实际的并发系统提供了坚实的基础。对于动态行为的处理，论文引入了线性模态逻辑的扩展，这可能涉及到可能性、必然性和时间顺序的概念，使得逻辑能够捕捉到并发系统中事件的发生顺序以及条件依赖。这样的扩展不仅有助于理解系统的动态变化，还有助于证明和验证诸如死锁、活锁等并发问题。本文的核心贡献在于将相关逻辑理论与并发系统的特性相结合，提出了用以设计和分析复杂并行系统的新方法，这对计算机科学，尤其是分布式系统和并发编程领域有着重要的实践意义。

CHAPTER 1. INTRODUCTION 16

We then in chapter 5 adapt the basic ideas of the introduction to the set-

ting of chapter 4 and consider modal relevance logics interpreted over classes

of models closed under a parallel composition. This results in interpretations

quite similar to the “initial a lg ebra” interpretations of chapter 3. The key to

axiomatising the full log ics lies, as in chapter 3, in providing the necessary ax-

iomatic tools for decompo sing implications into simpler formulas. A numb er of

such decomposition properties can be proved in quite general terms; for some

requiring an appeal to additional closure properties of model classes such as clo-

sure under disjoint union (corresponding to internal choice) and the existence

of least models satisfying certain formulas, corresponding—intuitively—to clo-

sure under guarded choice. On the basis of these decomposition properties we

obtain complete axiomatisations for the full logics using the f r om chapter 3 fa-

miliar rewriting technique—relativised w.r.t. complete axiomatisations of the

ground fragments for the given model class. We conclude the chapter by giving

a detailed example based on “testing models”, i.e. frames extended by certain

atomic propositions needed for the general preorders induced by our logics to

coincide with the corresponding testing preorders. The main part of the work

consist in showing that testing models provide an admissible model class, i.e.

that atomic propositions can be suitably decomposed, that least testing models

satisfying certain formulas exist, etc. It is then a relatively straightf orward mat-

ter to obtain (unrelativised) complete axiomatisations—this amounts basically to

specialising t he ground fragment axiomatisations to the class of testing models.

As in chapter 3 the completeness proof yield procedures for checking the validity

and satisﬁability of formulas as a spin-oﬀ.

Finally, in chapter 6, we evaluate the results obtained and discuss possible

directions for future work. We suggest that no deﬁnite answer to the viability

of the basic idea introduced has been given. Such an answer will depend on

a further development, probably focusing on the work described in chapter 3,

to the stage where full process systems such as CCS can be captured—at least

on a semantical level. Also it is important to relax the emphasis on testing-

related equivalences made here, and consider in part icular relevant extensions of

Hennessy-Milner Logic [51].

CHAPTER 2. ON RELEVANCE LOGICS AND THEIR MODELS 19

Note that a formula may occur more than once in an assumption sequence, and

that assumptions may not necessarily b e used. If it is unclear which of i) to

iii) applies to ψ

we assume this to be resolved by an appropriate annotation of

. In particular if ψ

is an assumption φ

and φ

occurs more than once among

, . . . , φ

we assume ψ

to be annotated such as to identify a unique φ

of which

is an occurrence. The existence of a deduction of φ fro m assumptions Φ in C

is denoted by Φ ⊢

φ, or by ⊢

φ if Φ is the empty sequence ε.

A logic (over Fm) is a subset o f Fm. The logic axiomatised by C is the set

L(C) = {φ | ⊢

φ}. We use boldface characters such as R, E to refer to logics

with ﬁxed concrete axiomatisations, and L as a variable ranging over such logics.

These can be sub- and superscripted as for sublanguages of Fm. Thus L

refers

to the logic axiomatised by the set of axioms and rules in L that only mention

connectives in Fm

. Note that only when L is a conservative extension of L

L ∩ Fm

= L

These notions a pply equally well to languages other than Fm. In particular we

have occasion to consider sequents, or consecutions [7]. These are expressions of

the form Φ ⊢ φ, and the provability o f such a sequent in C is denoted alternatively

by Φ ⊢

φ. The notational ambiguity here is resolved by C.

2.2 Some rele vance logics

The purpose of t he present section is to obtain some initial familiarity with

relevance logics, and to establish some terminology. The section follows to a

certain extent section 1.3 of Dunn’s survey [34] to which—together with Anderson

and Belnap’s volume [7]—we refer for additional material.

2.2.1 The implicative fragment

The subject matter of relevance log ic is the notion of relevant deduction and

its companion, relevant implication. The task is to grasp the idea of relevance

between assumption, or antecedent, and conclusion. The deduction theorem is

the to ol relating deduction and implication, and so provides an excellent setting

for discussing the issues involved.

The deduction theorem for a logic L ⊆ Fm

→

states that whenever Φ, φ ⊢

then Φ ⊢

φ → ψ. The deduction theorem holds in particular for the implicative

fragment, H

→

, of intuitionistic propositional logic. H

→

may be axiomatised by

CHAPTER 2. ON RELEVANCE LOGICS AND THEIR MODELS 20

the axioms

S: (φ → (ψ → γ)) → ((φ → ψ) → (φ → γ)) (Self-distribution)

K: φ → (ψ → φ) (Positive paradox)

together with modus ponens:

m.p.: From φ → ψ and φ infer ψ.

The deduction theorem for H

→

is proved by induction on deductions and shows

that whenever H

→

⊆ L then the deduction theorem holds for L. Moreover if the

deduction theorem holds for L then it contains S and K as theorems. Thus H

→

is minimal among the logics containing m.p. as a derived rule and satisfying the

deduction theorem.

The deduction theorem, however, allows for irrelevance—the canonical exam-

ple is the standard derivation of K. For φ is a deduction of φ from assumptions φ, ψ

for arbitrary ψ, hence if the deduction theorem holds for L then ⊢

φ → (ψ → φ).

But the assumption ψ wa s never used and the deduction is thus rejected by rel-

evantists as irrelevant.

This situation may be remedied by restricting attention to deductions that

have some desired property R of relevance. Then the R deduction theorem for L

states that if there is an R deduction in L of ψ fr om a ssumptions Φ, φ then there

is an R deduction in L of φ → ψ from assumptions Φ. Further, if L is minimal

with this property then we say that the R deduction theorem characterises L.

We use this perspective to introduce a number of relevance log ics. We restrict

for the time b eing attention to logics with m.p. as their sole rule of inference.

Relevance and linearity

We ﬁrst investigate the idea of relating relevance to the usage of occurren ces

of assumptions. We can make this precise by introducing the notion of the

i’th assumption being used n times in a deduction ψ

, . . . , ψ

. This is deﬁned

inductively as the least relation s.t.

i) if ψ

is an occurrence of the i’th assumption then that assumption occurs

once in ψ

, . . . , ψ

ii) if ψ

is an application of m.p. to ψ

, ψ

and the i’th assumption occurs

times in ψ

, . . . , ψ

, j ∈ {1, 2}, then that assumption occurs n

+ n

times in ψ

, . . . , ψ

剩余221页未读，继续阅读

quwenjian

粉丝: 4

利用相关逻辑与并行构造过程的模态逻辑方法

亚马逊相关性评分插件Amazon Relevance-crx使用介绍

"基于机器学习的问答推荐算法设计-电子科技大学学士论文初稿

Elasticsearch Relevance Engine™2023上海会议：向量搜索与机器学习应用程序ESRE™介绍和未来变化。...

IBM.Press.Audience.Relevance.and.Search.Apr.2010.rar

A Relevance and Redundancy Aware Performance Feature Selection Approach for Distributed File System

Nonlinear model predictive control with relevance vector regression and particle swarm optimization (2013年)

The Probabilistic Relevance Framework - BM25 and Beyond-计算机科学

Modeling and exploiting tag relevance for Web service mining

Relevance Ranking

srvm.gz_Relevance vector_relevance

最新资源