IRP programming : as lambda term
- see also Lambda calculus
IRP without argument
Usual programming method (in Caml) :
- to calculate a we need to apply a function a_build to two arguments x and y
- to calculate x we need to apply a function x_build to two arguments z and t
- to calculate y we need to apply a function y_build to two arguments u and v
- etc... until some data d1 ... dn are read from the disk
The Caml program will look like :
let d1 = read;; let d2 = read;; ... let dn = read;; ... let x = x_build z t ;; let y = y_build u v ;; let a = a_build x y ;;
Expand in -calculus, this yields :
((a_build) X) Y
which is the -redex of a_build with X and Y. Its reduced form is obtained by substitution of x by X and then y by Y. In fact X and Y are not in normal form (calculated values), therefore the program calculating a in the usual way is expressed as :
((a_build) (( x_build ) z ) t) (((y_build ) u ) v)
each term X, Y etc... is of the form :
(( x_build ) z ) t
(( y_build ) u ) v
which amounts to the application of a function x_build to the arguments z and t and to the application of a function y_build to the arguments u and v
IRP method :
let a_provide = let x = x_provide in let y = y_provide in a_build x y ;;
(( a_build) X) Y [compare to upper]
(( a_build) (x_provide)) (y_provide)
- X is x_provide : is a function that returns a normal form (the result of a calculus, a constant), while in the usual method X and Y were redex
- Therefore the IRP method consists in using replacing redex by normal form in the sequence of any calculation.
- With the IRP method the calculation of a is reduced to the application of a_build to the two constants x and y.
- The sequence of Beta-reduction are automatically done recursively due to the (quasi-)recursive design of the provide function.
- By construction both methods give the same result.