lambda-calculus Definition Redex A redex (reducible expression) is a lambda expression that is reducible.