1

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

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 类型的任何函数。

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

4

1 回答 1

0

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

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的 s，坦率地说，越少越好。）

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应该把它变成完全相同的东西。

于 2015-03-08T21:02:13.320 回答