# Normalization-by-evaluation for untyped lambda calculus which results in 𝛽𝜂-normal form

Usual NbE algorithms for untyped lambda calculus, which use (P)HOAS to embed terms to a host language constructs, results in a beta-normal form of a terms.

Is there algorithms to (efficiently) exploit host language constructs to normalize untyped terms to beta-eta normal form?

• Usually, NbE results in $\beta$-normal $\eta$-long normal forms! Can you cite your source for the first claim?
– cody
Oct 2 '20 at 19:46
• @cody I don't know. Does it holds for untyped lambda calculus too? Oct 2 '20 at 20:07
• @cody I edited the question to mention untyped LC Oct 2 '20 at 20:17
• All normalization algorithms exploit host language constructs. More specifically, do you mean algorithms which use eta conversion in the host language? Oct 12 '20 at 7:58