λEnter Calculus CompanionRegistered manuscripts, kept distinct

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

A syntactic linear step bound

Configurations and specified Born semantics › A syntactic linear step bound · lines 633–657

Back to manuscript

Define

m (x) = m (q) = m (*) = m (0) = m (1) = 0, m (λ x . t) = m (t),

m (⟨ t, u ⟩) = m (t) + m (u), m (new) = 1,

m (V (t)) = m (Enter (t)) = 1 + m (t),

and

m (t u) m (let ⟨ x, y ⟩ = t in u) m (let * = t in u) m (if b then u else u^{'}) = 1 + m (t) + m (u), = 1 + m (t) + m (u), = 1 + m (t) + m (u), = 1 + m (b) + max {m (u), m (u^{'})} .

Displayed formulas in this passage

unlabeled · line 636
$m (x) = m (q) = m (*) = m (0) = m (1) = 0, m (λ x . t) = m (t),$
unlabeled · line 640
$m (⟨ t, u ⟩) = m (t) + m (u), m (new) = 1,$
unlabeled · line 644
$m (V (t)) = m (Enter (t)) = 1 + m (t),$
unlabeled · line 648
$m (t u) m (let ⟨ x, y ⟩ = t in u) m (let * = t in u) m (if b then u else u^{'}) = 1 + m (t) + m (u), = 1 + m (t) + m (u), = 1 + m (t) + m (u), = 1 + m (b) + max {m (u), m (u^{'})} .$

Nearby in this section