Dafny 无法证明函数方法等价,高阶多态递归 vs 线性迭代 [英] Dafny cannot prove function-method equivalence, with High-Order-Polymorphic Recursive vs Linear Iterative
问题描述
这个消息会有点长,但那是因为我想尽可能地解释它.
This message is going to be a bit long, but that is because I want to explain it as best as possible.
在 Dafny 中,我遇到了下一个问题:给定一个数组,计算发生这种情况的长度为 k 的段的数量;片段左半部分的阳性数大于或等于右半部分.
In Dafny, I had the next problem: Given an array, count the number of segments of length k in which this happens; the number of positives in the left-half of the segment is bigger or equal to the right-half.
举个例子(想象段只能是偶数,所以没有关于一半是什么的讨论):
As an example (imagine segments can only be even, so that there is no discussion about what a half is):
k=2 ---> count(array[-4,-2,2,1],k) ---> 2, as [-4,-2] fulfills and also [2,1]
k=4 ---> count(array[-4,-2,2,1],k) ---> 0, as [-4,-2,2,1] does not fulfil.
k=6 ---> count(array[-4,-2,2,1],k) ---> 0, as there are not length 6 segments.
我已经通过两种方式实现了这一点:一种是使用函数,使用高阶和多态性(但不是线性的),另一种是使用线性迭代实现.
I have implemented this in two ways: one with a function, using high-order and polymorphism (but it is not linear) and the second one with an iterative implementation which does it linearly.
函数是这样工作的:
- 我们定义了一个 Count 函数,它计算数组上的一个属性.
- 我们定义了一种方法,在给定数组的情况下,生成给定长度的所有段.
- 我们定义了一个谓词,它使用 Count 告诉我们该属性是否满足.
function method CountAux<T>(P: T -> bool, sequ: seq<T>, i: int): int
//the warning just warns about how it is implemented, as when it warns about the triggers' choice
requires 0 <= i <= |sequ|
decreases |sequ| - i //necessary to prove termination
ensures CountAux(P,sequ,i)>=0; //trivial
{
if i == |sequ| then 0
else (if P(sequ[i]) then 1 else 0) + CountAux(P, sequ, i+1)
}
function method Count<T>(P: T -> bool, sequ: seq<T>): int
ensures CountAux(P, sequ, 0)>=0; //trivial
{
CountAux(P, sequ, 0)
}
function method produce_segments (sequ:seq<int>, seg_length:int) : seq<seq<int>>
requires |sequ| >= seg_length >= 0
decreases sequ
{
if |sequ| == 0 then [] //if the list is empty
else if |sequ|-1 < seg_length then [sequ[0..seg_length]] //if the list cannot have any more segments
else [sequ[0..seg_length]]+produce_segments(sequ[1..],seg_length)
}
function method segment_LeftMoreSegmentRight (sequ:seq<int>) : bool
{
if (Count(x => x >= 0, sequ[0..|sequ|/2])) >= (Count(x => x >= 0, sequ[|sequ|/2..|sequ|])) then true
else false
}
现在,这个方法是这样工作的:
Now, the method works this way:
- 我们初始化一个长度为 k 的数组,其中我们已经计算了左侧和右侧的所有正数.
- 现在,从 k 开始,在每次迭代中,我们将在每一侧增加、减少或保留相同数量的正数:例如,如果
v[i]>=0
那么我们将右边的正数加 1(显然,如果它是正数,我们会在v[ik/2]
中递减这个数字). - 为了计算这一点,我们定义了一个谓词,该谓词告诉我们右侧的正数数量是否高于或等于左侧的数量.
- We initialize an array of length k where we have counted all the positives at the left and in the right.
- Now, from k on, on each iteration, we will increment, decrement or leave the same number of positives on each side: for instance, if
v[i]>=0
then we add 1 to the number of positives on the right (and, obviously, we decrement this number inv[i-k/2]
if it was positive). - To count that, we define a predicate that tells us if the number of positives on the right is higher or equal than on the left.
//returns if the number of positives left is higher than the right or not
function method segmentL_isMore_right (pos_left:int,pos_right:int) : bool
{
if pos_left>=pos_right then true
else false
}
method initialize(sequ:seq<int>, seg_length:int) returns (sequ_new:seq<int>,pos_left: int,pos_right:int)
requires |sequ| >= seg_length >= 0
{
var length := |sequ|;
var pos_left_local := 0;
var pos_right_local :=0;
var i:=0;
while i<(length/2)
{
if sequ[i]>=1 {pos_left_local:=pos_left_local+1;}
i:=i+1;
}
while i<(length)
{
if sequ[i]>=1 {pos_right_local:=pos_right_local+1;}
i:=i+1;
}
return sequ[0..],pos_left_local,pos_right_local;
}
//Linear implementation
method Count_linear(sequ:seq<int>, seg_length:int) returns (num_segmts: int)
requires |sequ| >= seg_length >= 0
ensures num_segmts == Count(segment_LeftMoreSegmentRight, produce_segments(sequ,seg_length));
{
var num_segmts_local := 0;
var new_seq, pos_left_local, pos_right_local := initialize(sequ,seg_length);
var i:=seg_length+1;
while i<|sequ|
decreases |sequ|-i
{
if (sequ[i] >=0) {pos_right_local:=pos_right_local+1;}
if (sequ[i-seg_length]>=0) {pos_left_local:=pos_left_local+1;}
if (sequ[i-seg_length]/2>=0)
{
pos_right_local:=pos_right_local-1;
pos_left_local:=pos_left_local+1;
}
i:=i+1;
if segmentL_isMore_right (pos_left_local,pos_right_local)
{
num_segmts_local:=num_segmts_local+1;
}
}
return num_segmts_local;
}
\\if want to prove it:
method Main()
{
var aseq := [1,2,3,4,5,6,7,8,9,10];
var seg2_leftRight := Count(segment_LeftMoreSegmentRight, produce_segments(aseq,4)); //high order and polymorphic
}
现在,关键是 确保 num_segmts == Count(segment_LeftMoreSegmentRight,produce_segments(sequ,seg_length));
不会验证.显然,我将不得不用关于 Count
或 Count_linear
的引理证明一些性质,但不知道从哪里开始这个问题.
Now, the key is that ensures num_segmts == Count(segment_LeftMoreSegmentRight, produce_segments(sequ,seg_length));
does not verify. Obviously, I will have to prove some properties with lemmas about Count
or Count_linear
, but do not know where to start with this problem.
有什么帮助吗?我希望我已经尽可能最好地解释了这个问题.
Any help? I hope I have explained the problem as best as possible.
推荐答案
我正在回答这个问题,只是为了获得漂亮的代码格式.
I am making this an answer just so I can get nice code formatting.
您的 Count_linear
有一个错误.
var aseq := [1,2,3,4,5,6,7,8,9,10];
var slow := Count(segment_LeftMoreSegmentRight, produce_segments(aseq,4)); //high order and polymorphic
var fast := Count_linear(aseq, 4);
print slow, "\n";
print fast, "\n";
印刷品
7
5
这篇关于Dafny 无法证明函数方法等价,高阶多态递归 vs 线性迭代的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!