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 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 :[edit]

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.