Scott Encoding Construction Of The Y Combinator In An Untyped Lambda Calculus

(\lambda t b a r. \\ r t b a (bF(a(bX(a(tF)(a(tX)(tX))))(bX(a(tF)(a(tX)(tX))))))) \\ \ (\lambda x c_1 c_2 c_3. c_1 x) \\ \ (\lambda x y c_1 c_2 c_3. c_2 x y) \\ \ (\lambda x y c_1 c_2 c_3. c_3 x y)

Where the r argument in the first expression exposes a continuation using the construction in the function body. In this case, the continuation exposes constructors for terms, abstraction, application, and a construction of the Y combinator in the lambda calculus encoded using these constructors. The terms F and X here are free variables.