以下、拾い読みした感じこうなのかなあってのを書いただけだからあってるのかよく知らない。
例えば簡約前がこうだとすると、
(λxy.(λz.y((λu.u)z))x)v
weak head normal form はλ抽象された中身のλ式は簡約しなくてよい。
λy.(λz.y((λu.u)z))v
head normal form は関数適用の頭の部分しか簡約しなくてよい。
λy.y((λu.u)v)
normal formは当然全てのβ-redexを簡約する必要がある。
λy.yv
以下、拾い読みした感じこうなのかなあってのを書いただけだからあってるのかよく知らない。
例えば簡約前がこうだとすると、
(λxy.(λz.y((λu.u)z))x)v
weak head normal form はλ抽象された中身のλ式は簡約しなくてよい。
λy.(λz.y((λu.u)z))v
head normal form は関数適用の頭の部分しか簡約しなくてよい。
λy.y((λu.u)v)
normal formは当然全てのβ-redexを簡約する必要がある。
λy.yv