ch:lexical-effect-handlers: ch:lexical-effect-handlers

Put $\mathsf{hdl}(L_3,\mathsf{ask},11)$ between $\mathsf{call}(f)$ and the outer frame. The complete prefix is then $$\mathsf{hdl}(L_{\mathrm{i}\mathrm{n}},\mathsf{ask},9)::\mathsf{call}(f)::\mathsf{hdl}(L_3,\mathsf{ask},11)::\mathsf{hdl}(L_{\mathrm{o}\mathrm{u}\mathrm{t}},\mathsf{ask},7).$$ Name search still stops at the inner frame and returns $9$. Identity search skips both intervening $\mathsf{ask}$ frames, selects $L_{\mathrm{o}\mathrm{u}\mathrm{t}}$, and returns $7$. The compiler must preserve at least a datum that distinguishes the requested handler instance from every other live instance; in the displayed machine that datum is $L_{\mathrm{o}\mathrm{u}\mathrm{t}}$.

The first root changes the heap to $H_1=H[L_k\mapsto \mathsf{ns}]$ while reinstalling $K^{\prime }$ and binding the resumption result. A second attempt requires a premise of the form $H_1(L_k)=\mathsf{cont}(K^{″})$. Instead $H_1(L_k)=\mathsf{ns}$, so L-Resume is inapplicable and the untyped configuration is stuck.

Initially $$\mathsf{sp}=L_h^n,H({\ell }_{\mathrm{e}\mathrm{x}\mathrm{c}\mathrm{h}})=L_p^m.$$ Raise loads $L_p^m$, writes $L_h^n$ into the exchanger, and sets $\mathsf{sp}=L_p^m$. The fresh one-cell resumption contains ${\ell }_{\mathrm{e}\mathrm{x}\mathrm{c}\mathrm{h}}$, not a copy of either stack. Resume replaces that cell by $\mathsf{ns}$, loads $L_h^n$ through the exchanger, writes the current handler-stack top $L_p^m$ back, and sets $\mathsf{sp}=L_h^n$. A second resume reads $\mathsf{ns}$ where an exchanger location is required.

Terminating integer preservation and divergence preservation are conclusions: both are non-stuck behaviors, and positive simulation preserves them. Reflection of target stuckness is absent because the theorem is forward and excludes source stuckness. Source type safety is absent because Lexa is untyped. LLVM correctness is absent because Salt, not LLVM IR or native code, is the theorem’s target.

The two label-parameter cases calculate to $${\mathsf{hopper}}_{\mathcal{H}}(⟨\hat{0},F⟩)=⟨\hat{3},F⟩,{\mathsf{hopper}}_{\mathcal{H}}(⟨\hat{1},G⟩)=⟨\hat{0},G⟩.$$ If the relevant capture set contains two labels named $F$, provenance by effect name has two candidates. The nonambiguity premise on a well-formed capture set rejects the metadata before the operational hopper is used.

No dynamic handler identity or search on mainline paths is the syntactic and layout property of proposition 34.12. Terminating SL-to-TL preservation is the semantic corollary of theorem 34.11. Reported speedups are empirical engineering evidence. A constant-factor theorem would additionally require a costed source and target semantics and a bound relating their costs; none of the three claims supplies that relation.

A deep resumption prepends the captured pure suffix $\theta$ to the pure component of the current generalised-continuation frame while retaining $H$ as its return and operation handler. A later occurrence of the same operation therefore reaches $H$ again. A shallow resumption restores the captured pure frames and the handler frames outside $H$, then continues with the caller’s continuation. It does not reinstall $H$, so a later occurrence is forwarded outward unless the program explicitly installs another handler.

The source operation roots have different reducts: the deep reduct wraps the resumption body with $H$, while the shallow reduct does not. The handling lemma and Theorem 7 consequently use separate $\mathsf{res}$ and ${\mathsf{res}}^{†}$ target cases. Simulation preserves both behaviors; it does not equate them.

For the higher-order row, for example, one must fix the source syntax and semantics, target syntax and semantics, the term/type translation, and the observation plus simulation relation. Deep and shallow resumptions reduce to different terms after an operation: one reinstalls the handler and the other does not. A simulation case proved for one reduct therefore cannot be reused for the other by changing only a label in the theorem statement.

Proceed by induction on the list. If the head has the requested identity, uniqueness of identities rules out the identity in the tail, so the prefix, selected frame, and suffix are forced. Otherwise the head belongs to the prefix and the induction hypothesis gives the unique tail factorization. With names, the list $$\mathsf{hdl}(L_1,F,c_1)::\mathsf{call}(g)::\mathsf{hdl}(L_2,F,c_2)::ϵ$$ has a factorization at either $F$-frame. Thus unrestricted factorization is nonunique, not nonexistent. A separately defined nearest-name lookup restores functional choice by selecting the first frame, but selects the wrong lexical instance when $L_2$ was requested.

Induct on a terminating source derivation. The initial states are related; each source step contributes a nonempty target segment; concatenation reaches a target state related to the source final state; final-state agreement gives the integer. For divergence, let $C_0⟶C_1⟶\cdots$. Starting at the related $D_0$, simulation successively supplies $D_i{⟶}^{+}{D}_{i+1}$ with $C_{i+1}\mathcal{R}{D}_{i+1}$. Concatenating infinitely many nonempty segments yields an infinite target run. If zero target steps were permitted, every $D_i$ could be the same state and no target divergence would follow. A stuck source supplies no source step, so the simulation premise supplies no target conclusion.

Take a capability instantiation containing $\hat{1}:F,\hat{4}:F$. From $⟨\mathring{0},F⟩$, an unconstrained lookup may return either $⟨\hat{1},F⟩$ or $⟨\hat{4},F⟩$. Require that labels in every relevant capture or instantiation set have pairwise distinct effect names. Then two matching labels imply equal positions, and the label-successor case is unique. If no matching label exists, the card’s at-most-one capability-variable condition makes the continuing capability clue unique. Hence the hopper is a partial function on well-formed metadata; it remains undefined when neither case applies.

For raises crossing $h_1,\dots ,h_m$ frames, zero Lexa wins in the chosen model exactly when If all raises cross $h$ frames this becomes . The inequality only analyzes the stipulated charges. Benchmark timings do not define $d,z,r_d,r_z$, quantify over all programs, or prove correspondence with reduction steps, so the calculation is not an imported cost theorem.