IRP programming : as lambda term

From wikiosp
Jump to: navigation, search

IRP without argument[edit]

Usual programming method (in Caml) :[edit]

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 \lambda-calculus, this yields :

((\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 :

((\lambda x . \lambda y . a_build) ((\lambda z . \lambda t . x_build ) z ) t) (((\lambda u . \lambda v . y_build ) u ) v)

each term X, Y etc... is of the form :
((\lambda z . \lambda t . x_build ) z ) t
((\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 :[edit]

let a_provide = 
  let x = x_provide in
  let y = y_provide in
  a_build x y

Gives :

((\lambda x . \lambda y . a_build) X) Y [compare to upper]


((\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.