🚀 go-pugleaf

guy@dcs.glasgow.ac.uk (Guy Argo) writes:


>	Apologies for the delay in following up this thread but
>	I've been in communicado writing up my thesis.

>	Shah Namrata Abhaykumar asks if lambda-lifting is really necessary
>	in a TIM-like architecture ?

>	The answer is no. It is a simple matter to modify the TIM to
>	have a linked environment to handle scope. There is a chapter
>	in my forthcoming thesis on this topic. Note that a linked
>	environment is preferable to a display in a higher-order
>	language; it is also simpler to implement. For a convincing
>	demontration of this see David Krantz' PhD thesis - it's
>	a Yale tech report. This is not peculiar to the TIM; any
>	SECD-style machine has this property as Tony Davie points out
>	about the CASE machine.

I have found that TIM for a scoped language looks remarkably like the
Krivine machine. Well, to be exact, adding a small compilation trick
to the KM yields a TIM-like machine.

The KM reduces pure lambda-calculus to WHNF using a CBN strategy. Its
state consists of the current expression C, the environment E and a
stack S. The stack will always contain expression/environment pairs.
The state transitions are:

 \x.e	  E		   empty   ->  stop with (\x.e,E) as the WHNF
 \x.e	  E		   p:S	   ->  e     (x,p):E	S
 (e1 e2)  E		   S	   ->  e1    E		(e2,E):S
 x	  ...(x,(e,E))...  S	   ->  e     E		S

It can be seen that the actions are in the main controlled by the
current expression. Also, the environment lookup can be translated to
an offset by using deBruijn numbers. This suggests the following
translation of expressions to an abstract machine:

C[[\x.e]] R    	= take; (C[[e]] (\y. (y=x) -> 0 || (R y)+1))
C[[(e1 e2)]] R 	= push {C[[e2]] R}; (C[[e1]] R)
C[[x]] R	= enter (R x)

Thus \x.\y.(x y) translates to

    take; take; push {enter 0}; enter 1

The instructions has the following effects:

 take; C        E		empty	-> stop with (C,E) as the WHNF
 take; C        E		p:S	-> C    p:E     S
 push {C'}; C   E       	S	-> C    E	(C',E):S
 enter n        ...(C,E)...     S       -> C    E	S

where the pair (C,E) in the last equation is at position n in the
environment. Laziness can be added using markers like in TIM:

 take; C   E		<<(C',E')>>:S	-> C    E     S
						update (C',E') := (C,E)
 enter n   ...(C,E)...     S       -> C    E	<<(C,E)>>:S

When copying environments, care must be taken that the update reaches
the copy as well as the original. The original TIM uses a complex
scheme for this, but I prefer sharing the pointers to the (C,E) pairs.
Note that this is independent of whether a linked list or a display is
used. When using a display, an extra indirection is needed though.

I have tried extending this "simplified TIM" to cover strict
applications, numbers etc. I found that the take instruction has to
test for a lot of cases, so I considered making it "tagless", by just
calling the code at the top of the stack. This approach led me to
rephrase the KM as a continuation semantics: calling the continuation
corresponds to calling the code at the top of the stack. The original
KM (without markers) looks like this in continuation style:

K[[\x.e]]    R k = k (\v.\k'.K[[e]] (\y. (y=x) -> v || (R y)) k')
K[[(e1 e2)]] R k = K[[e1]] R (\f. f (K[[e2]] R) k)
K[[x]]       R k = (R x) k

It is easy to derive KM from this: we note that the continuation is
extended in one place (at application) and called in one place (at
abstraction). Thus the caller need only distuinguish between an empty
constinuation (\x.x) and one build at application. When building the
continuation, the free variables are e2, R and k, so it can be
represented as a triple of these. Likewise, the environment is built
in the abstraction rule with free variables x, v and R. Using this
"first order" representation we get:

K[[\x.e]]    R empty     = stop with (\x.e,R)
K[[\x.e]]    R (e',R',k) = K[[e]] (x,(e',R'),R) k
K[[(e1 e2)]] R k         = K[[e1]] R (e2,R,k)
K[[x]]       R k 	 = K[[e']] R' k
				where R = (... (x,(e',R'),R'')...)

which is easy to recognize as the KM.

Similar can be done for a continuation semantics using a store and
updating to implement laziness, yielding a lazy KM with markers.
However, I do not believe that going to the first order representation
of the continuation is a good thing. By letting it remain higher order
we obtain the taglessness we wanted for the take instruction. Now
compilation essentially amounts to partially evaluating the
continuation semantics with respect to a program. This yields a large
tail-recursive lambda-expression. By recognizing that the store and
the continuation are single-treaded (this can be done in the
continuation semantics before partial evaluation), these can be
globalized, avoiding a lot of intermediate parameter passing. The
resulting compiled program now consists of a mixture of function
definitions, calls and updates to the stack and the store. Since the
redex selection has been compiled away by using cps, the resulting
code is fairly easy to translate to machine code.

I have not implemented these ideas, just worked them out on paper, but
they seem promising. I believe the partial evaluation of the semantics
will reduce a lot of the push-followed-by-pop combinations that need
separate optimization in classical TIM. Essentially TIM can be
compared to a SKI combinator implementation, where the partial
evaluation, by generating specialized code, is more like the
supercombinator approach.

	Torben Mogensen (torbenm@diku.dk)