Definition. A-normal form (ANF) [1RPZ]

ANF常被叫做administrative normal form，好像是個模糊的「把administrative redex消掉」的說法。但最好想成以下的定義：對給定的A-reductions集合，化約會得到的normal form

Lambda calculus的A-normalization可以寫成以下定義

v::=ι∣x∣(λ (x) e)e::=v∣(op e⃗)∣(e e)∣(let (x e) e)∣(if0 e e e)E::=⋅∣(let (x E) e)∣(if0 E e e)∣(E e)∣(v E)∣(op v⃗ E e⃗)O::=v∣op\begin{aligned} v &::= \iota \mid x \mid (\lambda\ (x)\ e) \\ e &::= v \mid (op\ \vec{e}) \mid (e\ e) \mid (\text{let}\ (x\ e)\ e) \mid (\text{if0}\ e\ e\ e) \\ E &::= \cdot \mid (\text{let}\ (x\ E)\ e) \mid (\text{if0}\ E\ e\ e) \mid (E\ e) \mid (v\ E) \mid (op\ \vec{v}\ E\ \vec{e}) \\ O &::= v \mid op \end{aligned}

A-reductions

E[(let (x e1) e2)]→A(let (x e1) E[e2])A1where E≠⋅E[(if0 v e1 e2)]→A(if0 v E[e1] E[e2])A2where E≠⋅E[(O v⃗)]→A(let (x′ (O v⃗)) E[x′])A3where E≠⋅,E≠E′[(let (x ⋅) e)],fresh x′\begin{aligned} E[(\text{let}\ (x\ e_1)\ e_2)]\quad\rightarrow_A\quad &(\text{let}\ (x\ e_1)\ E[e_2]) \quad &A_1 \\ &\text{where}\ E \ne \cdot \\ E[(\text{if0}\ v\ e_1\ e_2)]\quad\rightarrow_A\quad &(\text{if0}\ v\ E[e_1]\ E[e_2]) \quad &A_2 \\ &\text{where}\ E \ne \cdot \\ E[(O\ \vec{v})]\quad\rightarrow_A\quad &(\text{let}\ (x'\ (O\ \vec{v}))\ E[x']) \quad &A_3 \\ &\text{where}\ E \ne \cdot, E \ne E'[(\text{let}\ (x\ \cdot)\ e)], \text{fresh}\ x' \end{aligned}

化約成的A-normal form（也就是說，不斷套用A-reductions應該讓程式變成以下形式，這些形式套用A-reductions不會再化簡）

(Values)V::=ι∣x∣(λ (x) M)(Computations)N::=V∣(V V)∣(op V⃗)(Configuration)M::=N∣(let (x N) M)∣(if0 V M M)\begin{aligned} (Values)&\quad &V &::= \iota \mid x \mid (\lambda\ (x)\ M) \\ (Computations)&\quad &N &::= V \mid (V\ V) \mid (op\ \vec{V}) \\ (Configuration)&\quad &M &::= N \mid (\text{let}\ (x\ N)\ M) \mid (\text{if0}\ V\ M\ M) \end{aligned}

我們通常會假設綁定中涉及的變數唯一且考慮 α\alpha-equivalence