![](https://csdnimg.cn/release/download_crawler_static/88734908/bg5.jpg)
3
多余的论点
TRS中函数
f
的参数的冗余度取决于我们感兴趣观察的语义属性。本文中考
虑的语义是函数式编程中最常考虑的,是
R
能够从基础项(eval
R
(t)=)在
有限数量的重写步骤中产生的值(基础构造器项)的集合。
{
s
∈ T(C)|
t
→
s
})。我们经常忽略子索引
R
,当它是明确的,从
背景与冗余问题相关的其他语义在
[1
,
2
,
22]
中讨论。
粗略地说,函数
f
的冗余参数是一个参数
t
i
,我们不需要考虑它来计算任
何包含子项f(t
1
,
.
,
t
k
)。
定义3.1 [2]设
R
=(R
,
R)是一个TRS,
f
∈ R,i∈ {1
,
.
,
ar(f)}。
f
的第i
个参数是
冗余的
(
w.r.t.
eval
R
)如果,对于所有上下文
C[ ]
和所有
t
,
s
∈ T
(t)使得root(t)=f,eval
R
(C[t])=eval
R
(C[t[s]
i
])。
我们用rarg
eval
R
(f)表示符号
f
∈N.语义学eval
R
for R。
当分析函数
f
in的属性时,摆脱上下文并执行更容易的局部分析是有用
的,这使我们能够将注意力集中在重写规则的语法结构这激发了以下动
机。
定义3.2 [2]设
R
=(R
,
R)是一个TRS,
f
∈ R,i∈ {1
,
.
,
ar(f)}。
f
的第i
个自变量是
局部冗余
的(
w.r.t.
eval
R
)如果对所有
t
,
s
∈ T(
t
)使得
root
(t)=f,eval
R
(t)=eval
R
(t[s]
i
).
我们用
lrarg
eval
R
(
f
)表示符号
f
w.r.t.
的局部冗余参数集。伊瓦尔河
一个论点的冗余。语义eval意味着局部冗余w.r. t。评估,即,rarg
eval
(
f
)
lrarg
eval
(
f
)
.
不幸的是,相反的说法通常并不正确。
[2]
中的以下结果
确保了当TRS接地时,局部冗余意味着冗余,
非常完整。
定理
3.3
设
R
是一个基连通且次完全的
TRS
。然后,对所有
f
∈
N
,
lrarg
eval
(
f
)=
rarg
eval
(
f
)
。
现在问题是如何挑出局部冗余的论点。为了解决这个问题,我们形式化
的冗余问题的归纳理论的程序。
3.1
表示论证冗余的归纳定理
下 面 的 结 果 形 式 化 了 归 纳 定 理 和 冗 余 的 论 点 之 间 的 关 系 , 在 连 续 和
susciently
完全
TRS
。