K框架：基于归约的计算系统详解

119 浏览量更新于2024-07-14 收藏 2.4MB PDF 举报

《K：基于归约的计算框架》(K: A Rewriting-Based Framework for Computations)是Grigore Rosu在2007年发布的一篇初步研究论文，发表于伊利诺伊大学厄巴纳-香槟分校计算机科学系。这篇论文探讨了K这一理论框架，它将归约（rewriting）的概念和逻辑用于抽象地描述和分析多种高级编程语言和计算模型。K框架的核心在于使用嵌套多集（nested multisets）和分离的y-列表（y-separated nested lists of tasks）来组织和执行计算过程。第3节详细阐述了K框架的结构。首先，K配置通过嵌套多集来表示，它们包含了程序的不同状态和数据结构，允许层次化的组织。接着，K计算模型利用y-分离，确保了任务之间的独立性和并发性。加热/冷却机制与严格性属性（heating/cooling and strictness attributes）则是控制计算过程中数据变化和类型约束的关键概念。接下来的章节着重于如何在K中定义理想化的编程语言。作者展示了如何通过K来形式化常见的计算范式，如图灵机、λ演算、简单命令语言、米尔纳的CCS、π-calculus、Hoare的CSP、卡德elli的Ambient Calculus、Agha的Actor模型、米尔纳的EXPL语言、罗宾逊的统一和米尔纳的W-polymorphic type inferencer，以及Plotkin的PCF语言。这些定义展示了K的强大之处，它可以作为一种通用的语言理论工具，支持对多种计算理论的统一处理。在第5章，作者比较了K框架与其他形式主义的异同，这有助于读者理解K在表达和分析复杂计算问题时的优势和局限性，以及它与其他理论在结构上的相互关系。《K：基于归约的计算框架》是一篇深入探讨理论计算语言设计和形式验证的重要文献，通过K这个框架，作者展示了如何用归约和逻辑工具来构建一个强大而灵活的工具，适用于不同计算模型的分析和设计。

a ﬁrst-order continuation-like structure), a method stack, an exception stack, and a loop stack (loops can

break and co ntinue). Therefore, there are no less than 17 leaf conﬁguration items, each containing important

information about the state of the program. Moreover, 10 of them, those within threads, can have multiple

instances, depending upon the number of threads that are alive at a given moment. Thus, the total number

of leaf conﬁguration items at any given moment is 7+n∗10, where n is the number of threads t that moment.

The a dvantage of representing conﬁgurations as nested “soups”, is that, like in MSOS [29], subsequent

semantic equations a nd rules will only need to mention those conﬁguration items that are needed for those

particular e quations and rules, as oppo sed to having to mention the entire conﬁguratio n, whether needed

or not, like in conventional SOS. We can add or remove elements from the conﬁguration multiset as we

like, only impacting rules that use those particular c onﬁguration items. Rules that do not need the changed

conﬁgurations items do not need to be touched. This is one impo rtant aspect of K’s modularity.

There are two optional conventions/guidelines regarding the use of conﬁg urations that help increase the

modularity of K language deﬁnitions. By convention, conﬁguration labels must b e distinct in the initial

conﬁguration, so that the conﬁgurations they wrap can be uniquely identiﬁed even when the exact paths

to them are not completely speciﬁed. Also, equations and rules are allowed to add new conﬁguration

item instances (a necessary process when, for example, creating threads) only at the same nesting level as

originally declared in the nested conﬁg uration. These conventions are crucial for K’s context transformation

process; essentially, equations and rules in a K deﬁnition are unambiguously and automatically modiﬁed by

completing partial conﬁguration contexts to “ﬁt” the current conﬁguration. This optional process, explained

in detail in [33], gives an additional degree of modularity to K deﬁnitions. For example, suppose that initially

KOOL was not c oncurrent and had no statements that can a bruptly change the control, such as return of

methods, exceptio ns, break/continue of loops, so there was no need for a multi-layered conﬁguration; in other

words, suppose that a ll co nﬁguration items were initially part of the top level conﬁguration. Then the rule

for variable lookup (deﬁned also in Appendix D) would match the environment and the store at the same

conﬁguration level. Adding threads and control-changing statements to the language would, unfortunately,

break the e xisting deﬁnition of variable lookup, because now each of the involved conﬁguration items a re

located at diﬀerent levels in the conﬁgura tion, so the previous rule would not match a nymore. With context

transformers, no change needs to be done in the existing rule for variable lookup when the structure of

the conﬁguration changes. The correct environment will b e matched (and not the environment of another

thread), because the context transformers are resolved following a “greedy” depth-ﬁrst strategy.

3.2 K Computations: y-Separated Nested Lists of Tasks

An important conﬁguration item, present in many K deﬁnitions and “wr apped” in conﬁgurations with the

ConﬁgLabel k, is the computation, denoted by the syntactic category K. Computations generalize abstract

syntax trees (ASTs) by adding a special list construct y :

K ::= KLabel(List

[K]) | List

[K]

KLabel ::= (one per language construct, plus auxiliary ones as needed)

The ﬁrst construct scheme for K abstractly captures any prog ramming language syntax, under the form of

abstract syntax trees, provided that one adds one KLabel for each language construct. In addition to the

language syntax, one may include in KLabel additional labels for semantic rea sons and for “heating/cooling”

reasons (explained below). If one wants more K syntactic categories, then one can do that, too, but, for

simplicity, we prefer to keep only one in this paper. It is often mor e intuitive to call the language constructs

taking no arguments constants and write them as “leaves” in K structures; e.g., ski p instead of skip(); we

therefore may tacitly assume an additional syntactic subcategory of K called KConstant, for constructs

such as skip, 0, 1, true, etc. Also, for executability reasons, it may be useful to deﬁne another s yntactic

subc ategory of K, called KResult, for “ﬁnished computations” ; this may contain certain constants, such as

0, 1, true, etc., but also computations which are proper terms, such as λ . (x, e) (written in AST form).

We take the liberty to write syntax either in AST form, like in “λ . (x, e)” and “if then else (b, s

, s

)”,

or in more re adable mixﬁx form, “λx.e” and “if b then s

else s

”. In our Ma ude implementation of K

University of Illinois at Urbana-Champaign

Department of Computer Science UIUCDCS-R-2007-2926 and College of Engineering UILU-ENG-2007-1827

(see Appendix E), thanks to Ma ude’s builtin mixﬁx notation and corresponding parsing for s yntax, we

actually write programs using the mixﬁx notation. Even though theore tically unnecessary, this is a c tually

very convenient in practice, because it makes language deﬁnitions more readable and, consequently, less

error-prone. Additionally, programs in the deﬁned languages can be regarded as terms as are , without any

intermediate AST representation for them. In other implementations of K, one may need to use a n explicit

parser or to ge t used to reading syntax in AST representation. Either way, from here on we assume that

programs, or fragment of programs, parse as computations in K; the following fra gments of program in a

hypothetical language are therefore terms of sort K,

1 + 2

if true then (s; while b do s) else s

provided that all the corresponding constructs are deﬁned as constructs for KLabel and KConstant:

KLabel ::= ... | + | ; | if then else | while do

KConstant ::= ... | Bool | Nat

The second construct scheme for K allows one to sequentialize computational tasks. Intuitively, k

y k

says “process k

then k

”. How this is used and what is the ex act meaning of “ process” is left open and

depends upon the particular deﬁnition. For example, in a concrete semantic language deﬁnition it c an mean

“evalua te k

then k

”, while in a type inferencer deﬁnition it can mean “type and accumulate type constraints

in k

then do the same for k

”, etc. The following are e xamples of computations using the y cons truct:

(if true then · else ·) y while false do ·

y  + a

y a

+ 

y (a

+ a

) + 

y (a

y  + a

) + 

b y if  then s

else s

b y if  then (s y while b do s) else ·

The “·” in the ﬁrst and last computations above is the unit of K. Note that y-separated lists of computations

can be nested. Most importantly note that, unlike in evaluation contexts,  is not a “hole” in K, but r ather

part of a KLabel; The KLabels involving  above are

KLabel ::= ... | +  |  + | if  then else

The  carries the obvious “plug here” intuition; e.g., one may think of “a

y  + a

” as “process a

, then

plug its result in the hole in  + a

”. Needless to say tha t the user of K is not expected to decla re these

sp e c ial labels. We assume them whenever needed. In our implementation of K in Maude (Appendix E), all

these are generated automatically as cons tants of sort KLabel after a simple analysis of the language syntax.

Freezers. To distinguish the labels containing  in their name from the labels that encode the syntax

of the lang uage under consideration, we call the former freezers. The role of the freezers is therefore to

store the enclosing computations for future processing. One ca n freeze computations at will in K, using

freezers like the ones above, o r even by deﬁning new freezers. In complex K deﬁnitions, one may need many

computation freezer s, making deﬁnitions look heavy and hard to read if one makes poor choices for freezer

names. Therefore, we adopt the following freezer naming convention, respected by all the freeze rs above:

If a computation can be seen as c[k, k

, ..., k

] for some multi-context c and a freezer is introduced

to freeze everything except k, then the name of the freezer is c[, , ..., ].

Additionally, to increase readability, we take the freedom to generalize the adopted mixﬁx notation in K and

“plug” the remaining computations in the freezer, that is, we write c[, k

, ..., k

] instead of c[, , ..., ](k

, ..., k

For insta nce , if @ is some binary o peration and if, for some reason, in contexts of the form (e

)@(e

)

University of Illinois at Urbana-Champaign

Department of Computer Science UIUCDCS-R-2007-2926 and College of Engineering UILU-ENG-2007-1827

one wishes to freeze e

, e

and e

(in order to, e.g., process e

), then, when there is no confusion, one can

take the freedom to write (e

@ )@(e

) instead of (( @ )@ ( @ ))(e

, e

). This convention is partic-

ularly useful when one wants to follow a reduction semantics with evaluation contexts style in K , because

one can mechanically associate such a freezer to each context-deﬁning production. For example, the freez e r

( @ )@( @ ) above would be associated to a production of the form “Cxt ::= (Exp@Cxt)@(Exp@Exp)”; see

Section 5.4.6 for more details on how reduction semantics with evaluation contexts is captured by K.

3.3 K Heating/Cooling and Strictness Attributes

After deﬁning the desired language syntax so that programs or fragments of programs become terms of sort

K, the very ﬁrst step towards giving a K semantics to a language is to deﬁne the computation (structural)

equations. These allow to regard computations many diﬀerent, but completely equivalent ways. For example,

+ a

may be regarded also as a

y  + a

, with the intuition “schedule a

for proce ssing and freeze a

in freezer  + ”, but also as a

y a

+  (if, of course, addition is intended to be non-deterministic). As

discussed in Section 3.2, the freezers’ role is to store the remaining computations fo r future processing.

Heating/Cooling equations, informally. Computation structural equations know how to “pass in front”

of the computation fragments of program that need to be processed, and also how to “plug their results

back” once processed. In most langua ge deﬁnitions, all computation structural equations can be generated

automatically from K strictness operator attributes as explained below; Figure 1 s hows several examples of

strictness attributes. For example, the s trict attribute of + is equivalent to the following two computation

structural equations in K (a

and a

range over computations in K):

+ a

 a

y  + a

+ a

 a

y a

+ 

To distinguish them fr om the other equations, we use the symbol “” instead of “=” in computational

structural e quations. The symbol “” is also us e d in Cham [5], as a s horthand for combinations of a

heating rule (“*”) and a cooling rule (“)”). Even though in K we use it for equations, which have a

model-theoretical semantics that is diﬀerent from that of pairs of rewrite rules, operationally one can rega rd

an equation as a pair of rewrite rules. Moreover, “” in K carries in fact a heating/cooling intuition similar

to that of Cham. Indeed, one can think of the ﬁrst rule above as follows: to process a

+ a

, let us ﬁrst

“heat” a

, applying the equation from left to right; once a

is processed (using other equations/rules in

the semantics) producing some result, place that result back into context via a “cooling” step, applying

the equation from right to left. We actually ﬁnd the conceptual analo gy between computation s tructural

equations in K a nd heating/cooling rules in Cham so insightful, that we take the libe rty to borrow both

the notation “” and the terminology “heating/cooling” from Cham. However, it is important to realize

that these heating/cooling equations can be applied at any moment and in a ny direction, because they

are regar ded not as computational steps but as structural identities. For example, o ne c an use the two

heating/cooling equations for “ + ” above to pick and pa ss in front either a

or a

, then rewrite it one

step only using s e mantic rules (deﬁned later in this section), then plug it back into the sum, then pick

and pass in front either a

or a

again and rewrite it one step only, and so on, thus obtaining the desired

non-deterministic oper ational semantics of + .

One should always be aware in K deﬁnitions that “” is nothing but a co nvenient notation used as part

of la bel names freezing some computations for future use, and not get carried away and think of “” as a

sp e c ial “hole expression” of sort K. For example, a hasty reader may think that K’s approach to strictness

is unsound, because one can “prove” wrong equalities as follows:

+ a

= a

y  + a

(by the ﬁrst equation above applied left-to-right)

= a

y a

y  +  (by the second equation above applied left-to-right)

= a

y a

+  (by the ﬁrst equation above applied right-to- left)

= a

+ a

(by the second equation above applied right-to-left)

University of Illinois at Urbana-Champaign

Department of Computer Science UIUCDCS-R-2007-2926 and College of Engineering UILU-ENG-2007-1827

What is wrong in the above “proof” is that one cannot apply the second equatio n in the second step above,

because  + a

is nothing but a c onve nient way to write the frozen computation  + (a

). One may say

that there is no problem with the above, because + is intended to be commutative a nyway; unfortunately,

the sa me could be proved for any non-deterministic construct, fo r example for a division operation, “/”, if

that was to be included in our language. Since the heating/cooling equations are thought of as structural

identities, so that computational steps take place modulo them, then it would certainly be wrong to have

both “a

” and “a

” in the same computational equivalence class. One of K’s most subtle technical

aspects, which fortunately is transparent to users, is to ﬁnd the right (i.e., as weak as possible) restrictions

on the applications of heating/cooling equations, so that each computational equivalence class contains no

more than one fragment of program. This is called “computation adequacy” and is discussed in detail in

Appendix ??. The idea is to only allow heating and/or cooling o f operator arguments that are proper

syntactic computations (i.e., terms over the original s yntax, i.e., diﬀerent from “·” and containing no “y”).

With that, for example, the computation equivalence class of the expression x ∗ (y + 2) in the context of a

language deﬁnition with non-deterministically strict binary + and ∗, consists of the terms:

x ∗ (y + 2)

x y ( ∗ (y + 2))

x y ( ∗ (y y ( + 2)))

x y ( ∗ (2 y (y + )))

(y + 2) y (x ∗ )

y y ( + 2) y (x ∗ )

2 y (y + ) y (x ∗ )

x ∗ (y y ( + 2))

x ∗ (2 y (y + ))

Note that there is only one syntactic computation in the computation equivalence class above, namely the

original expression itself. This is a crucial desired property of K.

Strict attribute. In K deﬁnitions, one typically deﬁnes zero, one, or more heating/cooling e quations per lan-

guage construct, depending on its intended processing strateg y. These equations tend to be straightforward

and boring to write, so in K we prefer a higher- level and more compact and intuitive approach: we annotate

the language syntax with strictness attributes. A language construct annotated as s trict, such as for example

the “ + ” in Figure 1, is automatically associated a heating/cooling equation as above for each of its subex-

pressions. If an operator is intended to be strict in only some of its arguments, then the positio ns of the strict

arguments are listed as arguments of the strict attribute. For example, note that the strictness attribute of

if then else in Fig ure 1 is strict(1); that means that a hea ting /cooling equation is added only for the ﬁrst

sube xpression of the conditional, namely the equatio n “if b then s

else s

 b y if  then s

else s

”.

Seqstrict attribute. Recall that the two heating/cooling equations corr e sponding to the strictness attribute

strict of + above did not enforce any particular order in which the two subexpressions were processed. It

is often the case that one wants a deterministic order in which the strict arguments of a language construct

are pr ocessed, typically from left to right. Such an example is the relational op e rator ≤ in Figure 1, which

was declared the strictness attribute seqstrict, saying that its subexpressions are processed deterministically,

from left to right. The attribute seqstrict can be used only in deﬁnitions with a non-empty KResult and

can be desugare d automatically as follows: generate a heating/cooling equatio n for each a rgument like in

the case of st rict, but req uiring that all its previous arguments are in KResult. For example, the seqstrict

attribute of ≤ desugars into (a

, a

range over K and r

over KResult):

≤ a

 a

y  ≤ a

≤ a

 a

y r

≤ 

Like in the case of the strict attribute, seqstrict can also take a list o f numbers as argument and then the

heating/cooling equations a re generated so that the corresponding arguments are processed in that order.

Useful K labels. One can use heating/cooling equations to also deﬁne computational structural equivalences

University of Illinois at Urbana-Champaign

Department of Computer Science UIUCDCS-R-2007-2926 and College of Engineering UILU-ENG-2007-1827

on K terms involving auxiliary K labels, not necessarily corresponding to the original language syntax. For

example, some language constructs may have an arbitrary number of arguments, not always appear ing as a

list, such as, for example, a letrec construct with a syntax like “letrec x

= e

and x

= e

and · · · and x

in e ”. Since the expressions e

, e

, ..., e

will need to be processed at some moment, it is very useful

to extract them and schedule them for processing all at once. We assume two special K labels, strict and

seqstrict, designed for such situations and deﬁned as follows (kl, kl

∈ List[K], rl ∈ List[KResult], k ∈ K):

strict(·) = seqstrict(·) = ·

strict(kl, k, kl

)  k y strict(kl, , kl

)

seqstrict(rl, k, kl

)  k y seqstrict(rl, , kl

)

As before, “” is not a hole but part of the name of a freezer, in our case of “strict( , , )” and “seqstrict( , , )”,

respectively, written in mixﬁx notation to ease reading. Recall that in the theoretica l developments of K all

sentences ar e schematas, so the two heating/cooling equa tions above compr ise a recursively enumerable set

of ground equations, one for each instance of the variables, including o nes with kl, kl

, or rl empty lists. In

practice, though, the above equations are universally quantiﬁed (or parametric) in their variables and their

application involves a matching modulo associativity; that is precisely how we implemented them in our

Maude implementa tion of K (see Section E).

General strictness convention. More generally, we allow any K labels to be associated s trictness at-

tributes. For example, one may deﬁne s ome label myEval as follows:

KLabel ::= · · · | myEval [strict]

That means that m yEval is strict in all its arguments, no matter how many they a re, so that one can

schedule e

, e

, . . . , e

for proce ssing by wrapping them in a term myEval(e

, e

, . . . , e

). With this g e neral

convention, the str ictness of + and ≤ can also be deﬁned as follows

KLabel ::= · · · | + [strict] | ≤ [seqstrict]

while the useful K labels strict and seqstrict are nothing but two builtin labels deﬁned as follows:

KLabel ::= · · · | strict [strict] | seqst rict [seqstrict].

3.4 K Semantic Sentences: Equations and Rules

In its full g e nerality as described in [33], K allows three types of sentences: structural (or non-computational),

computational and non-deterministic. Regarded from a rewriting logic point o f view, the structural sentences

are always equatio ns, while the non-deterministic ones are always rewrite rules; the computational sentences

can be either equations or rules, depending upon how one uses the K deﬁnition: if used exclusively for

execution to get an interpreter for the deﬁned language, then it does not matter whether the computational

sentences are equations or rules; if used fo r proofs by induction on computatio ns, then one may want to

regard all computational sentences as rules, so that the equational eq uivalence classes are as s mall and precise

as possible; if used for model-checking a program, then one may regard all the computational sentences as

equations, becaus e they add no new behaviors and keeping them equatio ns signiﬁcantly reduces the state-

space to be analyzed by the model checker. However, to keep the presentation simple, in this paper we only

consider two types of sentences, like in rewriting logic: equations and rules. Equations are structural in

nature and thus carry no computational meaning ; they only say which terms should be viewed as identical

and their r ole is to transparently modify the term so that rewrite rules can apply. Rewrite rules are se e n

as irreversible computational steps and can happen concurrently. All the heating/cooling equations in the

previous section were K equations. The following are also examples of equations:

JpK = Jk(p) state(∅)K

; s

= s

y s

while b do s = if b then (s; while b do s) else ·

University of Illinois at Urbana-Champaign

Department of Computer Science UIUCDCS-R-2007-2926 and College of Engineering UILU-ENG-2007-1827

剩余123页未读，继续阅读

weixin_38688745

粉丝: 4
资源: 908

K框架：基于归约的计算系统详解

LNCS 2009-6 Rewriting Techniques and Applications

The K Semantic Framework (CS422-Spring-2010-K)-计算机科学

git-history-rewriting-talk

Rewriting-Based Instance Retrieval for Negated Concepts in Description Logic Ontologies

Rewriting History - USC FBE Finance Seminar - (F_2-15-07_MALLOY-Anonymous)-计算机科学

Rewriting x86 Binaries without Code Producer Cooperation (wartell12thesis)-计算机科学

Text-Rewriting-Simplification:Text神经文本简化以提高Chatbot性能

Python库 | gtirb_rewriting-0.0.24-py3-none-any.whl

UrlRewriting Filter-开源

ldap protocol rewriting proxy-开源

最新资源