Manuscript I@2 · I.tex · section · 85631fa7

Liberal scheduling and observational confluence

Metatheory of the specified calculus › Liberal scheduling and observational confluence · lines 723–740

Liberal contexts permit independent argument evaluation:

L ::= [] ∣ L t ∣ t L ∣ ⟨ L, t ⟩ ∣ ⟨ t, L ⟩ ∣ let ⟨ x, y ⟩ = L in u ∣ let * = L in u ∣ if L then u else u^{'} ∣ V (L) ∣ Enter (L) .

They still do not enter bodies or alternatives. A scheduler chooses an enabled redex at every nonterminal configuration. Configurations are identified up to consistent live-name renaming, tensor permutation, and global phase.

Displayed formulas in this passage

unlabeled · line 726
$L ::= [] ∣ L t ∣ t L ∣ ⟨ L, t ⟩ ∣ ⟨ t, L ⟩ ∣ let ⟨ x, y ⟩ = L in u ∣ let * = L in u ∣ if L then u else u^{'} ∣ V (L) ∣ Enter (L) .$

Nearby in this section

lemma: Lemma: Concrete diamond
theorem: Theorem: Observational confluence
lemma: Lemma: Concrete composability
section: Liberal scheduling and observational confluence