返回介绍

H.3.5 Tight satisfaction with local variables

发布于 2020-09-09 22:56:16 字数 3067 浏览 944 评论 0 收藏 0

A local variable context is a function that assigns values to local variable names. If L is a local variable context,

then dom(L) denotes the set of local variable names that are in the domain of L. If D dom(L), then L|D

means the local variable context obtained from L by restricting its domain to D.

In the presence of local variables, tight satisfaction is a four-way relation defining when a finite word w over

the alphabet Σ together with an input local variable context L0 satisfies an unclocked sequence R and yields an

output local variable context L1. This relation is denoted

w, L0, L1 R .

and is defined below. It can be proved that the definition guarantees that w, L0, L1 R implies

dom(L1) = flow (dom(L0), R) .

? w, L0, L1 ( 1, v = e ) iff |w| = 1 and w 0 1 and L1 = {(v, e[L0, w 0])} U L0|D , where e[L0, w 0] denotes the

value obtained from e by evaluating first according to L0 and second according to w 0 and D = dom(L0) –

{v}. In case w 0 {T, }, e[L0,T] and e[L0, ] can be any constant values of the type of e.

? w, L0, L1 b iff |w| = 1 and w 0 b[L0] and L1 = L0. Here b[L0] denotes the expression obtained from b by

substituting values from L0 .

? w, L0, L1 ( R ) iff w, L0, L1 R .

? w, L0, L1 ( R1 ##1 R2 ) iff there exist x, y, L’ such that w = xy and x, L0, L’ R1 and y, L’, L1 R2 .

? w, L0, L1 ( R1 ##0 R2 ) iff there exist x, y, z, L’ such that w = xyz and |y| = 1, and xy, L0, L’ R1 and

yz, L’, L1 R2 .

? w, L0, L1 ( R1 or R2 ) iff there exists L’ such that both of the following hold:

— either w, L0, L’ R1 or w, L0, L’ R2, and

— L1 = L’ |D, where D = flow (dom(L0), ( R1 or R2 )) .

? w, L0, L1 ( R1 intersect R2 ) iff there exist L’, L" such that

w, L0, L’ R1 and w, L0, L" R2 and L1 = L’ |D’ U L" |D’’ , where

D’ = flow (dom(L0), R1) – (block (( R1 intersect R2 )) U sample (R2))

D’’ = flow (dom(L0), R2) – (block (( R1 intersect R2 )) U sample (R1))

Remark: It can be proved that if w, L0, L’ R1 and w, L0, L" R2 , then L’ |D’ U L" |D’’ is a function.

? w, L0, L1 first_match ( R ) iff both

— w, L0, L1 R and

— if there exist x, y, L’ such that w = xy and x, L0, L’ R, then y is empty.

? w, L0, L1 R [*0] iff |w| = 0 and L1 = L0.

? w, L0, L1 R [*1:$] iff there exist L(0) = L0, w1, L(1), w2, L(2),..., wj, L( j) = L1 ( j > 1) such that w = w1w2...wj

and for every i such that 1 < i < j, wi, L(i –1), L(i) R .

If S is a clocked sequence, then w, L0, L1 S iff w, L0, L1 S’, where S’ is the unclocked sequence that results

from S by applying the rewrite rules.

An unclocked sequence R is non-degenerate iff there exist a non-empty finite word w over Σ and local variable

contexts L0, L1 such that w, L0, L1 R. A clocked sequence S is non-degenerate iff the unclocked sequence S’

that results from S by applying the rewrite rules is non-degenerate.

如果你对这篇内容有疑问,欢迎到本站社区发帖提问 参与讨论,获取更多帮助,或者扫码二维码加入 Web 技术交流群。

扫码二维码加入Web技术交流群

发布评论

需要 登录 才能够评论, 你可以免费 注册 一个本站的账号。
列表为空,暂无数据
    我们使用 Cookies 和其他技术来定制您的体验包括您的登录状态等。通过阅读我们的 隐私政策 了解更多相关信息。 单击 接受 或继续使用网站,即表示您同意使用 Cookies 和您的相关数据。
    原文