読者です 読者をやめる 読者になる 読者になる

北海道苫小牧市出身の初老PGが書くブログ

永遠のプログラマを夢見る、苫小牧市出身のおじさんのちらしの裏

((weak )?head )?normal formの違いってなんなの

以下、拾い読みした感じこうなのかなあってのを書いただけだからあってるのかよく知らない。

例えば簡約前がこうだとすると、

(λ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