ANF or DOT?

ANF and DOT are convenience representations used in the compilation process of lambda terms.

ANF is a representation which explicitly linearizes local computations by binding them to let expressions. Every let expression let x = E₀ in E₁ is equivalent to a normal lambda expression (x . E₁) E₀.

DOT is a representation which also lifts subcomputations out of lambda terms. I.e., a term E₀ E₁, where E₀ and E₁ are not in normal form, is translated to (. .) E₀ E₁, any normal form is not lifted out of a term.

When translating lambda terms to C, the question for my runtime is where a thunk should be pushed in the GRS, or whether a term in normal form should be placed into a thunk awaiting a result.

The advantage of DOT over ANF is that it makes explicit the thunks and where results should be stored and it linearizes the term. I.e., since dots denote where arguments should be placed in order, local computations in subterms can be lifted such that we only arrive at a series of thunks which should be pushed.

The advantage of ANF over DOT it that it is easier to translate to C since the let bindings are closer to assignment to local variables.

DOT should be more suitable for me.