Reduction strategies

• [3.1] A binary relation on \(\Lambda\) with unique choice of redex.
• Head reduction \(\overset{\!\!h}{\to}\) reduces the head redex (underlined) \[ \lambda x_1\ldots x_m.\underline{(\lambda y.t)u}s_1\ldots s_n \overset{\!\!h}{\to} \lambda x_1\ldots x_m.\underline{t[u/y]}s_1\ldots s_n \]
• Leftmost reduction \(\overset{\!l}{\to}\) reduces the leftmost redex (note that \(\overset{\!\!h}{\to} \;\subset\; \overset{\!l}{\to}\)).
• Internal reduction \(\overset{\!i}{\to}\) is NOT a reduction strategy, defined as any \(\to_\beta\) that is not a head reduction.
• Advancement of head reduction (3.1.1). If \(s \twoheadrightarrow_\beta t\) then there is some \(u\) such that \(s \overset{\!\!h}{\twoheadrightarrow} u \overset{\!i}{\twoheadrightarrow} t\).

Reduction sequences

• [3.1] A reduction sequence for term \(s\) with binary relation \(\to\) is a (possibly infinite) sequence \(s \to s_1 \to s_2 \to \ldots\).
• If \(\to\) is a reduction strategy, then it has a unique maximal reduction sequence that ends in a \(\to\)-nf if finite, and infinite otherwise.
• [3.2] A standard reduction sequence reduces redexes from left to right.
  • Lemma 3.2.1.
    • Any subsequence of a standard reduction sequence is standard.
    • Every \(\overset{\!l}{\to}\)-reduction sequence is standard (and hence likewise for \(\overset{\!\!h}{\to}\)).
    • Every standard reduction ending in a \(\beta\)-nf is a \(\overset{\!l}{\to}\) reduction sequence.
  • Standardization theorem (3.2.2). If \(s \twoheadrightarrow_\beta t\) then \(s \twoheadrightarrow_s t\) (not necessarily the same sequence).