Return to Question

added 36 characters in body; edited title

Source Link

edited Oct 2, 2020 at 20:17

Normalization-by-evaluation algorithmfor untyped lambda calculus which results in beta𝛽𝜂-eta normalnormal 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?

Source Link

asked Oct 2, 2020 at 16:21

JetNoBrains

Normalization-by-evaluation algorithm which results in beta-eta normal form

Usual NbE algorithms, 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 terms to beta-eta normal form?

Stack Exchange Network

Return to Question

Normalization-by-evaluation algorithmfor untyped lambda calculus which results in beta𝛽𝜂-eta normalnormal form

Normalization-by-evaluation algorithm which results in beta-eta normal form

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

Normalization-by-evaluation algorithm which results in beta-eta normal form