More Semantic Computation Items

In this lesson we see more examples of semantic (i.e., non-syntactic) computational items, and how useful they can be. Specifically, we fix the environment-based definition of callcc and give an environment-based definition of the mu construct for recursion.

Let us first fix callcc. As discussed in Lesson 4, the problem that we noticed there was that we only recovered the computation, but not the environment, when a value was passed to the current continuation. This is quite easy to fix: we modify cc to take both an environment and a computation, and its rules to take a snapshot of the current environment with it, and to recover it at invocation time:

syntax Val ::= cc(Map,K)
rule <k> (callcc V:Val => V cc(Rho,K)) ~> K </k> <env> Rho </env>
rule <k> cc(Rho,K) V:Val ~> _ =>  V ~> K </k> <env> _ => Rho </env>

Let us kompile and make sure it works with the callcc-env2.lambda program, which should evaluate to 3, not to 4.

Note that the cc value, which can be used as a computation item in the <k/> cell, is now quite semantic in nature, pretty much the same as the closures.

Let us next add one more closure-like semantic computational item, for mu. But before that, let us reuse the semantics of letrec in terms of mu that was defined in Lesson 8 of Part 1 of the tutorial on LAMBDA:

syntax Exp ::= "letrec" Id Id "=" Exp "in" Exp [macro]
             | "mu" Id "." Exp                 [latex(\mu{#1}.{#2})]
rule letrec F:Id X = E in E' => let F = mu F . lambda X . E in E'

We removed the binder annotation of mu, because it is not necessary anymore (since we do not work with substitutions anymore).

To save the number of locations needed to evaluate mu X . E, let us replace it with a special closure which already binds X to a fresh location holding the closure itself:

syntax Exp ::= muclosure(Map,Exp)

rule <k> mu X . E => muclosure(Rho[X <- !N], E) ...</k>
     <env> Rho </env>
     <store>... .Map => (!N:Int |-> muclosure(Rho[X <- !N], E)) ...</store>

Since each time mu X . E is encountered during the evaluation it needs to evaluate E, we conclude that muclosure cannot be a value. We can declare it as either an expression or as a computation. Let's go with the former.

Finally, here is the rule unrolling the muclosure:

rule muclosure(Rho,E) => E ~> Rho' ... Rho' => Rho

Note that the current environment Rho' needs to be saved before and restored after E is executed, because the fixed point may be invoked from a context with a completely different environment from the one in which mu X . E was declared.

We are done. Let us now kompile and krun factorial-letrec.lambda from Lesson 7 in Part 1 of the tutorial on LAMBDA. Recall that in the previous lesson this program generated a lot of garbage into the store, due to the need to allocate space for the arguments of all those lambda abstractions needed to run the fixed-point combinator. Now we need much fewer locations, essentially only locations for the argument of the factorial function, one at each recursive call. Anyway, much better than before.

In the next lesson we wrap up the environment definition of LAMBDA++ and generate its documentation.

Go to Lesson 6, LAMBDA++: Wrapping Up and Documenting LAMBDA++.

MOVIE (out of date) [5'19"]