💾 Archived View for dcreager.net › lambda-calculus captured on 2024-05-10 at 10:57:12. Gemini links have been rewritten to link to archived content

View Raw

More Information

-=-=-=-=-=-=-

λ calculus

Standardization theorem

If a term has a normal form, normal-order reduction will find it.

[Kashima2000] A Proof of the Standardization Theorem in λ-Calculus

Weak vs strong reduction systems

A strong reduction system allows redexs inside of abstractions. A weak one does not. Weak reduction is not confluent in the λ calculus.

_Extended_ weak reduction lets you reduce inside of an abstraction if the reduction does not refer to the bound variable. That is confluent.

[Sestini2018] Normalization by Evaluation for Typed Weak λ-Reduction