Function lambda_calculus::combinators::y

pub fn y() -> Term

Y - the fixed-point combinator.

Y := λg.(λx.g (x x)) (λx.g (x x)) = λ (λ 2 (1 1)) (λ 2 (1 1))

Example

use lambda_calculus::combinators::y;
use lambda_calculus::arithmetic::zero;
use lambda_calculus::reduction::normalize;

assert_eq!(normalize(y().app(zero())), normalize(zero().app(y().app(zero()))));