# DOT calculus evaluation rules

The DOT calculus is an extension of lambda calculus which nicely supports polymorphic types as any other values. It seems it lays a foundation for sound evaluation rules of dependent object types.

However, I do not understand the evaluation works. Page 4 of the DOT paper mentions the following five evaluation rules ($\lambda$ represented using \)

         let x = v in e[x y]   ->   let x = v in e[[z := y]t] if v = \(z :T)t
let x = y in t   ->   [x := y]t
let x = let y = s in t in u    ->   let y = s in let x = t in u
e[t]   ->   e[u]             if t -> u
where e ::= [ ] | let x = [ ] in t | let x = v in e


For I have three questions.

1. If we follow the rules in this order of priority, if the value y assigned to x is not a value (a lambda), it seems that x is immediately replaced by y in t. But this seems to contradict the fact that they suppose it's call-by-need, that is, we evaluate lets only once.
2. If we says that the rules can be applied in any order, the complexity of evaluation can dramatically increase (e.g. if t = $\lambda f. f x x x$), so is it really out-of-order evaluation?
3. Are the rules of lambda-calculus implicitly added, or can they be recovered from this calculus ?

The rules can be applied in any order. The first three rules are mutually exclusive, while the last rule corresponds corresponds to evaluating the lets from outside in. Obviously, the last rule trivially overlaps with all the others via the first context, [ ], but this is unimportant. Using the second context let x = [ ] in t does overlap non-trivially with the third rule and corresponds to the decision between un-nesting a let and then evaluating outside in, or evaluating a nested let outside in and un-nesting it later. It's relatively easy to see that this ambiguity makes no difference. The last context let x = v in e looks like it might overlap with the first rule, but there are no reduction rules for x y, so whenever the first rule applies the fourth rule does not (except via the trivial context).
$(\lambda f.f x x x)$ is not a term in this calculus. The term that would correspond to this is $(\lambda f.\mathsf{let}\ f_1 = f x\ \mathsf{in\ let}\ f_2 = f_1 x\ \mathsf{in}\ f_2 x)$. (Or you could consider various ways of nesting the lets; it will just be undone by the second evaluation rule.) This is what it means to be in ANF (administrative normal form or A-normal form) which is mentioned by only very briefly explained: "That is, every intermediate value is abstracted out in a let binding." However, it doesn't need to be explained because the syntax for terms enforces this.
When the syntax description states "$x$, $y$, $z$ Variable" it means the meta-variables $x$, $y$, and $z$ (and variations like $x'$ or $y_1$) represent variables in the syntax. Similarly, $v$ and variations always represent a value, and $s$, $t$, and $u$ always represent a term. This means that the rule let x = y in t -> [x:=y]t only applies if $y$ is a variable. That rule does not allow, say, let x = y z in t -> [x:=(y z)]t. This is the formalization of the comment by the authors that "[r]eduction uses only variable/variable renamings instead of full substitution." Similarly, ANF is enforced because in the syntax of terms the only applications allowed are variables applied to variables (i.e. $x\, y$). $(x\, y)\, z$ is not a term. If such expression were intended to be allowed, the syntax would have had something like $s\, t$.
So, it should be mostly clear by now, but the answer to your last question is that there are no "implicit" rules. Arbitrary lambda terms are not terms in this syntax, but they can be encoded into terms via translation to ANF which simply involves let binding all subterms so that all applications are variables applied to variables. This translation can easily be formalized: \begin{align} \mathcal{A}(x) & = x \\ \mathcal{A}(\lambda x.M) & = \lambda x.\mathcal{A}(M) \\ \mathcal{A}(M N) & = \mathsf{let}\ x_1 = \mathcal{A}(M)\ \mathsf{in\ let}\ x_2 = \mathcal{A}(N)\ \mathsf{in}\ x_1\, x_2 \\ & \text{(where }x_1\text{ and }x_2\text{ are fresh)} \end{align}