В настоящее время мы изучаем лямбда-исчисление и начали сокращение бета-версии. Наш лектор использует некоторые обозначения, которые не были должным образом объяснены нам. Ниже приведено то, что нам было дано.
reduction-сокращение:
(λ v . e₁) e₂
⤳?
[e₂/v]e₁ where [e₂/v] is an operator that replaces each v with an e₂
Определение оператора [e / v]
[e/v]v = e
[e/v₂]v₁ = v₁ (when v₁≠v₂, i.e., different identifiers)
[e/v](e₁ e₂) = [e/v]e₁ [e/v]e₂
[e₂/v](λ v . e₁) = (λ v . e₁)
[e₂/v₂](λ v₁ . e₁) = (λ v₁ . [e₂/v₂]e₁) (when v₁∉FV(e₂))
[x/v] (λ x . f v)
⤳ λ x . f x (WRONG, x∈FV(x)={x})
Я пытался найти ресурсыв сети, но ни один из них не использует ту же запись, что и он, со знаком «/». Любое объяснение приведенного выше кода будет очень цениться.