Menu
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.
916
An expression that contains no free variables is said to be closed. Closed lambda expressions are also known as combinators and are equivalent to terms in combinatory logic.
A lambda expression is an anonymous function and can be defined as a parameter. The Closures are like code fragments or code blocks that can be used without being a method or a class. It means that Closures can access variables not defined in its parameter list and also assign it to a variable.
The majority of functional programming languages at all do not require you to 'learn' lambda calculus, whatever that would mean, lambda calculus is insanely minimal, you can 'learn' its axioms in an under an hour.
In mathematics and computer programming, the Lambda symbol is used to introduce "anonymous functions." Lambda notation distinguishes between variables used as mathematical arguments and variables that stand for predefined values.
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).
61
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
