IRP programming : a definition

From WikiOsp
Jump to: navigation, search
it is proved that in any - non iterative - computer program any function having arguments can be recast in an argumentless function giving the same result.
Assume that
  • to calculate an entity e we use a function e_build (x, y)
  • to calculate the argument x we use a function x_build (z, t)
  • to calculate the argument y we use a function y_build (u, v)
  • etc ... for z, t, u, v
  • until some constant d1 ... dn are reached, which are either read from the disk or directly provided.

(the choice of two arguments for each function is of course arbitrary, it can be any positive integer. In case of zero argument the entity is by definition a constant).

The program will look like :

 define or read d1   <- data
 define or read d2
 define or read dn
 x := x_build (z, t)
 y := y_build (u, v)
 e := e_build (x, y)   <- target

To calculate e it is clear that the programmer needs to know explicitly how to compute all the arguments (parameters) of all the functions applied in the sequence leading from the data d1 ... dn to the target e.

We show below that things can always be done in a simpler and more efficient way by making Implicit the References to the Parameters (i.e. using the IRP method)
if an entity e of a program is calculated by a unique function (e_build) applied to some arguments x, y,... then, it can also be calculated by the application of a unique and argumentless function (e_provide).
there are two kinds of entities in a program :
  • 1 data, the values of which are not calculated but only set or read from the disk.
  • 2 calculated entities, the values of which are calculated from the values of other entities of the program (their parameters : x, y, ... for e)
  • in case 1, the Proposition is true : no argument is needed to calculate a constant.
  • in case 2, suppose that the Proposition is true for the arguments of e_build x, y, ... therefore we have :
  x := x_provide
  y := y_provide
  etc ... 

and a valid expression for e_provide is :

 e_provide = {
   x := x_provide
   y := y_provide
   e_build (x, y, ...)

which is conform to the Proposition.
It follows by induction that any calculable entity e of a non-iterative program (i.e. for which each entity e is calculated by unique function e_build) can be calculated by application of a unique and argumentless function.

if e_build is unique e_provide is also unique. e_build is unique : if it were not, this would simply mean that there is more than one e entity to be calculated by the program.

while a program written with the usual method follows the sequence described upper :

i.e. : get data and calculate all intermediate values until target can be calculated

The IRP method does a supplementary sequence of calculations :

i.e : starts from the target, ask for all argument values needed to calculate the target value, for that, ask for all argument values needed to calculate them ... until data are reached
then do the same sequence of calculation as for the usual method.

ask for e                  calculate e
      \                      /
  ask for x              calculate x
        \                  /
     ask for z         calculate z
          \              /
      ask for t      calculate t
            \          /
            ...      ...
               \     /

                        /        \
                      x          y
                    /   \       / \
                   z     t     u   v
             /  /                     \
            d1 d2  ...                dn

       / \
      /   \
     u     v
    / \   / \
   d1 d2 u   w
        / \   \
      d1  d2   d3