proofs

[Janis Voigtlaender]

Rijk-Jan van Haaften writes:

> I used 3 main properties for the process:
> ...
> 2. Lifting local let definitions to a higher level
> let
>          f =
>                  let
>                          g = gExpr
>                  in
>                          fExpr
> in
>          expr
> 
> can be translated into
> let
>          g = gExpr
>          f = fExpr
> in
>          expr
> 
> The definition of g which is local for f in the first
> expression is made more global in the second
> one.

Care has to be taken if g (which might be bound outside this let-block) occurs 
in expr, because with the translated version it is now bound to gExpr. Renaming 
helps (for some unused g'):
> let
>          g' = gExpr
>          f  = fExpr[g <- g']
> in
>          expr

--
Janis Voigtlaender
http://wwwtcs.inf.tu-dresden.de/~voigt/
mailto:voigt@tcs.inf.tu-dresden.de