[plt-scheme] Semantics of let

When you make a function call, do you push a new frame for the
arguments on the front of the list of frames the caller was using?  Do
you always resolve variable references, local or global, by working
your way down the frame list looking for a binding?  If so, then
you've implemented dynamic scope, not static scope.  R5RS does cover
this: Scheme is a statically scoped language.  So is Common Lisp. 
Emacs Lisp and many older lisp implementations are dynamic, like
yours.

You asked where R5RS covers this.  In section 1.1, it says:

Following Algol, Scheme is a statically scoped programming language.
Each use of a variable is associated with a lexically apparent binding
of that variable.

Then, in section 4.1.4,  "Procedures", it says:

Semantics: A lambda expression evaluates to a procedure. The
environment in effect when the lambda expression was evaluated is
remembered as part of the procedure. When the procedure is later
called with some actual arguments, the environment in which the lambda
expression was evaluated will be extended by binding the variables in
the formal argument list to fresh locations, the corresponding actual
argument values will be stored in those locations, and the expressions
in the body of the lambda expression will be evaluated sequentially in
the extended environment.


So that's kind of a recipe for how to implement it as well.

In your example:

(let ((f (lambda (x) (if (= x 0) 1 (* x (f (- x 1))))))) (f 3))

you could argue that the binding of 'f' is 'lexically apparent' at the
point of its use.  But the bindings introduced by 'let' shouldn't be
visible outside the body of the let.  To see why your semantics aren't
lexical scoping, consider what your interpreter would do with this:

(define x 1)
(define f (lambda (x) (lambda (y) (+ x y)))
(define g (f 10))

Now, (g 100) should evaluate to 110.  g is a procedure yielded by
evaluating (lambda (y) ...).  The use of x within that lambda should
refer to the innermost lexically apparent binding, that of (lambda (x)
...), not (define x ...).  But I bet your interpreter will evaluate (g
100) to 101, because the use of x will see the binding in scope at the
call site --- the (define x ...).  If that's right, then your
procedures don't use the innermost lexically apparent binding, as
required by R5RS.