Докажите два алгоритма идентичны

Question

Я должен показать, что два алгоритма выполняют одинаковые операторы в одинаковом порядке. Один является хвостовой рекурсивной версией другого. Они написаны на Эйфелевой.

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 операторы только для выполнения 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

Во-первых, избавьтесь от глупой Эйфелевой 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 должен превратить это в точно то же самое.