Normal form.md (1120B)
1 +++ 2 title = "Normal form" 3 +++ 4 5 # Normal form 6 ## Normal form 7 λ-term is in beta-normal (B-normal) form if it does not contain a beta-redex (you can't reduce it any more). 8 9 If it is in normal form, it automatically also has a normal form. 10 11 If it has a normal form, it is not necessarily in normal form. 12 13 A λ-term M is in normal form if: 14 - M = λx.M with M a normal form 15 - M = x M1 ... Mn with n ≥ 0 and M1...Mn normal forms 16 17 **Strongly normalising (terminating):** if all B-reduction sequences starting in M are finite (therefore also weakly normalising) 18 - terminating: x, λx.x, ... 19 - non-terminating: Ω, (λx.xxx) (λx.xxx), ... 20 21 **Weakly normalising:** if there exists a B-reduction sequence starting in M that ends in a normal form. 22 - so it can reach a result, but also has a reduction loop. 23 - e.g. K, Ω 24 25 26 ## Confluence 27 Confluence is when terms can be rewritten in more than one way, still giving the same final result. That is, reducing to the same normal form. 28 29 In logic: 30 31 ``` 32 ∀M1, M2: M ⇒ M1 33 M ⇒ M2 34 35 M1 ⇒β B 36 M2 ⇒β B 37 ``` 38 39 With M being some term and B being a normal form.