English
The continuation support contSupp for halt and fix cases is empty and equals codeSupp of the corresponding code, i.e., the finite set of states reachable in evaluation includes only the states necessary to complete the continuation evaluation.
Русский
Поддержка продолжения contSupp для halt и fix равна пустому множеству и совпадает с codeSupp соответствующего кода, т.е. конечное множество состояний достигается в ходе завершения вычисления продолжения.
LaTeX
$$$\forall k\; contSupp(Cont'.halt) = \emptyset$ и аналогично contSupp(Cont'.fix f k) = codeSupp f k$$$
Lean4
/-- The (finite!) set of machine states visited during the course of evaluation of a continuation
`k`, not including the initial state `ret k`. -/
def contSupp : Cont' → Finset Λ'
| Cont'.cons₁ fs k =>
trStmts₁
(move₂ (fun _ => false) main aux <|
move₂ (fun s => s = Γ'.consₗ) stack main <| move₂ (fun _ => false) aux stack <| trNormal fs (Cont'.cons₂ k)) ∪
(codeSupp' fs (Cont'.cons₂ k) ∪ (trStmts₁ (head stack <| Λ'.ret k) ∪ contSupp k))
| Cont'.cons₂ k => trStmts₁ (head stack <| Λ'.ret k) ∪ contSupp k
| Cont'.comp f k => codeSupp' f k ∪ contSupp k
| Cont'.fix f k => codeSupp' (Code.fix f) k ∪ contSupp k
| Cont'.halt => ∅
