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?

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.