Intensional Constructed Numbers: Towards Formalizing the Notion of Algorithm

TL;DR

This paper proposes a formal framework for defining algorithms as equivalence classes of programs by analyzing the computation history of constructed numbers with trace conditions.

Contribution

It introduces the concept of constructed numbers with history conditions to formalize the notion of algorithm as an equivalence class of programs.

Findings

Defines constructed numbers with trace conditions

Establishes equivalence relations on constructed numbers

Proposes a new formal approach to algorithm definition

Abstract

This work is meant to be a step towards the formal definition of the notion of algorithm, in the sense of an equivalence class of programs working "in a similar way". But instead of defining equivalence transformations directly on programs, we look at the computation for each particular argument and give it a structure. This leads to the notion of constructed number: the result of the computation is a constructed number whose constructors (0, successor) carry a history condition (or trace) of their computation. There are equivalence relations on these conditions and on constructed numbers. Two programs are equivalent if they produce equivalent constructed numbers for each argument.