💾 Archived View for dcreager.net › lambda-calculus captured on 2024-08-25 at 00:25:28. Gemini links have been rewritten to link to archived content

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

λ calculus

Standardization theorem

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

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.