5
$\begingroup$

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?

Improve this question
$\endgroup$
4
  • 1
    $\begingroup$ Usually, NbE results in $\beta$-normal $\eta$-long normal forms! Can you cite your source for the first claim? $\endgroup$
    – cody
    Commented Oct 2, 2020 at 19:46
  • $\begingroup$ @cody I don't know. Does it holds for untyped lambda calculus too? $\endgroup$
    – JetNoBrains
    Commented Oct 2, 2020 at 20:07
  • $\begingroup$ @cody I edited the question to mention untyped LC $\endgroup$
    – JetNoBrains
    Commented Oct 2, 2020 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$
    – András Kovács
    Commented Oct 12, 2020 at 7:58

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.