ch:mixml: ch:mixml

Extensionality reduces the claim to one path. The four clauses of definition 15.2 select one result at that path, so the two result maps agree. Each clause is invariant under exchanging the two inputs: the opposite-polarity clause returns the export in either order, and the one-sided and two-import clauses return the same component. Thus merge is commutative whenever it is defined. In this signature two equal-typed exports are both represented by the same entry $p^{+}:A$; there is no stored value by which left bias between them could be observed. If left bias instead replaces the rejection of unequal overlapping components, take ${\mathrm{\Sigma }}_1=\{p^{+}:A\}$ and ${\mathrm{\Sigma }}_2=\{p^{+}:B\}$ with $A\ne B$. The two orders return $p^{+}:A$ and $p^{+}:B$, respectively, so that altered operation is not commutative.

Let $M_i=\mathsf{def}(p=e_i:A)$, with empty read sets and singleton write sets $\{p\}$, and consider $${\mathsf{seal}}_{\varnothing }(M_1)\mathsf{with}{M}_2.$$ Starting from $D=\varnothing$, the weakened first definition reaches $\{p\}$. Sealing with $Q=\varnothing$ retains that state but exposes the empty signature. The weakened second definition therefore writes $p$ again, while signature merge combines $\varnothing$ with $\{p^{+}:A\}$ and is defined. The final state is still $\{p\}$, but $p\in D^{\prime }\setminus D$ was written twice. This contradicts the unique-write clause of lemma 15.4.

1. Yes, by evidence-translation soundness under the analysis, synthesis, and core hypotheses.

2. No. Standard ML is not the source signature.

3. Yes, for a non-error terminal configuration, by LTG progress’s terminal-form clause and canonical stores. An early dereference instead steps to $\bullet$.

4. No. The import assumes sound and complete algorithms for the selected core extension.

The two opposite-polarity pairs merge to the complete signature displayed in the chapter. If keywords is first, its read set contains the absent token slot; if token is first, its read set contains the absent keywords slot. Hence the core-read premise of Mix-Def fails in both orders. Static completeness therefore does not determine a safe initialization order.

Use the cyclic family from the preceding solution. Signature completeness means that the merged signature contains no negative component. Ordered trace definedness means that every allocated cell reaches mode $U$ without an early get. The first is a signature property and holds; the second is a trace property and fails. In full LTG, either order can instead encounter the explicit $\bullet$ transition. Conversely, a module can initialize every locally allocated cell while deliberately leaving an external import in its result signature. Only elaboration soundness links the two notions for a checked complete full MixML module.

For modules with read/write pairs $(R_i,W_i)$, require $W_1\cap W_2=\varnothing$, $R_1\cap W_2=\varnothing$, and $R_2\cap W_1=\varnothing$. Each module then reads only the initial set or its own earlier writes, irrespective of the other order, and disjointness preserves single assignment. Disjoint writes alone fail for $R_1=\{q\},W_1=\{p\},R_2=\varnothing ,W_2=\{q\}$: module 1 must follow module 2.