Lambda Calculus (λa.b)((λx.xx)(λx.xx))
functional-programming, haskell, lambda, lambda-calculus
Solution
If you evaluate the right term first and continually then it will never reach a normal form, thus it is not strongly normalizable. If you evaluate the left term first it will immediately reach a normal form, thus it is normalizable and demonstrates that this term is weakly normalizable. It's also an example of the non-confluence of the untyped lambda calculus.
Note that you're more likely to want to talk about how a rewriting system is normalizing than a particular term. This term is thus a counterexample to the strong normalization property of untyped lambda calculus, but does not provide positive evidence that ULC is weakly normalizing (and it isn't).
Problem
Im looking for an example of a weakly normalising lambda term. Am I right in saying that the following: ``` (λa.b)((λx.xx)(λx.xx)) ``` Reduces to: ``` b ``` or: doesnt terminate (if you try to reduce `(λx.xx)(λx.xx)`) I wasnt sure if the first reduction is correct so just need some clarification, thanks.