15.5 LET Rules as Procedures

The LET statement offers an alternative syntax and semantics for procedure definition.

In place of

        procedure abc(x,y,z); <procedure body>;

one can write

        for all x,y,z let abc(x,y,z) = <procedure body>;

There are several differences to note.

If the procedure body contains an assignment to one of the formal parameters, e.g.

        x := 123;

in the PROCEDURE case it is a variable holding a copy of the first actual argument that is changed. The actual argument is not changed.

In the LET case, the actual argument is changed. Thus, if ABC is defined using LET, and abc(u,v,w) is evaluated, the value of U changes to 123. That is, the LET form of definition allows the user to bypass the protections that are enforced by the call by value conventions of standard PROCEDURE definitions.

Example: We take our earlier FACTORIAL procedure and write it as a LET statement.

        for all n let factorial n =  
                    begin scalar m,s;  
                    m:=1; s:=n;  
                l1: if s=0 then return m;  
                    go to l1  

The reader will notice that we introduced a new local variable, S, and set it equal to N. The original form of the procedure contained the statement n:=n-1;. If the user asked for the value of factorial(5) then N would correspond to, not just have the value of, 5, and REDUCE would object to trying to execute the statement 5 := 5 - 1.

If PQR is a procedure with no parameters,

        procedure pqr;  
           <procedure body>;

it can be written as a LET statement quite simply:

        let pqr = <procedure body>;

To call procedure PQR, if defined in the latter form, the empty parentheses would not be used: use PQR not PQR() where a call on the procedure is needed.

The two notations for a procedure with no arguments can be combined. PQR can be defined in the standard PROCEDURE form. Then a LET statement

        let pqr = pqr();

would allow a user to use PQR instead of PQR() in calling the procedure.

A feature available with LET-defined procedures and not with procedures defined in the standard way is the possibility of defining partial functions.

    for all x such that numberp x let uvw(x)=<procedure body>;

Now UVW of an integer would be calculated as prescribed by the procedure body, while UVW of a general argument, such as Z or p+q (assuming these evaluate to themselves) would simply stay uvw(z) or uvw(p+q) as the case may be.