# IRP programming : as lambda term

### IRP without argument

#### Usual programming method (in Caml) :

Assume that

• 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 x = x_build z t ;;
let y = y_build u v ;;
let a = a_build x y ;;


Expand in Failed to parse (PNG conversion failed; check for correct installation of latex and dvipng (or dvips + gs + convert)): \lambda -calculus, this yields :

((Failed to parse (PNG conversion failed; check for correct installation of latex and dvipng (or dvips + gs + convert)): \lambda x . \lambda y . a_build) X) Y

which is the $\beta$-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 :

((Failed to parse (PNG conversion failed; check for correct installation of latex and dvipng (or dvips + gs + convert)): \lambda x . \lambda y . a_build) ((Failed to parse (PNG conversion failed; check for correct installation of latex and dvipng (or dvips + gs + convert)): \lambda z . \lambda t .

x_build ) z ) t) (((Failed to parse (PNG conversion failed; check for correct installation of latex and dvipng (or dvips + gs + convert)): \lambda u . \lambda v .


y_build ) u ) v)

each term X, Y etc... is of the form :
((Failed to parse (PNG conversion failed; check for correct installation of latex and dvipng (or dvips + gs + convert)): \lambda z . \lambda t .

x_build ) z ) t


((Failed to parse (PNG conversion failed; check for correct installation of latex and dvipng (or dvips + gs + convert)): \lambda u . \lambda v .

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
;;


Gives :

((Failed to parse (PNG conversion failed; check for correct installation of latex and dvipng (or dvips + gs + convert)): \lambda x . \lambda y .

 a_build) X) Y  [compare to upper]


or

((Failed to parse (PNG conversion failed; check for correct installation of latex and dvipng (or dvips + gs + convert)): \lambda x . \lambda y .

 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.