# IRP programming : as lambda term

- see also Lambda calculus

### 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 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 **Failed to parse (unknown error): \lambda**
-calculus, this yields :

((**Failed to parse (unknown error): \lambda x . \lambda y . **
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 :

((**Failed to parse (unknown error): \lambda x . \lambda y . **
a_build) ((**Failed to parse (unknown error): \lambda z . \lambda t . **

x_build ) z ) t) (((Failed to parse (unknown error): \lambda u . \lambda v .

y_build ) u ) v)

each term X, Y etc... is of the form :

((**Failed to parse (unknown error): \lambda z . \lambda t . **

x_build ) z ) t

((**Failed to parse (unknown error): \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 (unknown error): \lambda x . \lambda y . **

a_build) X) Y [compare to upper]

or

((**Failed to parse (unknown error): \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.