algorithm - 证明两个算法相同

Question

我应该证明两种算法以相同的顺序执行相同的语句。一个是另一个的尾递归版本。它们是用 Eiffel 编写的。

tail_rec(x:instance_type):result_type is
    local
        y:instance_type;
    do
        if b(x) then
            Result :=c(x)
        else
            y:=d(x);
            Result:=tail_rec(y)
    end
  end

然后是非尾递归版本。

non_rec(x:instance_type):result_type is
    do
        from until b(x) loop
            x:= d(x)
        end;
        Result:= c(x)
    end  

其中 b(x)、c(x) 和 d(x) 分别是 BOOLEAN、result_type 和 instance_type 类型的任意函数。

这两种算法有何相似之处？它们如何以相同的顺序执行相同的语句？

Answer 1

通过用 goto 替换所有控制流结构，(本质上是将代码从 Eiffel 转换为伪代码，)并允许 if 语句只执行 goto，可以证明这两个函数最终由完全相同的指令集组成。

为了方便起见，让我先在这里复制原始的 tail_rec:

tail_rec(x:instance_type):result_type is
    local
        y:instance_type;
    do
        if b(x) then
            Result := c(x)
        else
            y := d(x);
            Result := tail_rec(y)
        end
    end

首先，摆脱 Eiffel 愚蠢的 Result := 结构，为方便起见将其替换为 return。 (否则，我们将不得不添加更多的 goto，坦率地说，越少越好。)

tail_rec(x:instance_type):result_type is
    local
        y:instance_type;
    do
        if b(x) then
            return c(x)
        end
        y := d(x);
        return tail_rec(y)
    end

将 if-then-end 替换为 if-then goto :

tail_rec(x:instance_type):result_type is
    local
        y:instance_type;
    do
        if not b(x) then goto label1
        return c(x)
    label1:
        y := d(x);
        return tail_rec(y)
    end

用另一个 goto 替换尾递归:

tail_rec(x:instance_type):result_type is
    do
    label0:
        if not b(x) then goto label1
        return c(x)
    label1:
        x := d(x);
        goto label0
    end

将if not b(x)替换为if b(x):

tail_rec(x:instance_type):result_type is
    do
    label0:
        if b(x) then goto label1
        x := d(x);
        goto label0
    label1:
        return c(x)
    end

对 tail_rec 的类似转换应该将其变成完全相同的东西。