檢視 Beta範式的原始碼

佇咧 lambda 演算中，一個項是'''beta 範式'''（規範型）， 你若是無「beta 歸約」是可能的。一個項是'''beta-eta 範式'''，若既然無 beta 歸約曷無「eta 歸約」是可能的。一個項是'''頭部範式'''，你若是無「佇頭殼位置的 beta-會當規約式」。

==Beta 歸約==

佇咧 lambda 演算中，'''beta 可歸約式'''( redex ) 是這種形式的項


: $ ( ( \ mathbf { \ lambda } x . A ( x ) ) t ) $

遮的 $ A ( x ) $ 是（可能）牽連變量 $ x $ 的項。

「 佇頭殼位置的 beta 歸約」是共如下重寫規則應用佇一个 beta 可歸約式


: $ ( ( \ mathbf { \ lambda } x . A ( x ) ) t ) \ rightarrow A ( t ) $

遮的 $ A ( t ) $ 嘿共項 $ A ( x ) $ 中變量 $ x $ 替換做項 $ t $ 的結果。

一个 beta 歸約佇頭殼位，若是伊有落形式：

* $ \ lambda x _ { 零 } \ ldots \ lambda x _ { i 影一 } . ( \ lambda x _ { i } . A ( x _ { i } ) ) M _ { 一 } M _ { 二 } \ ldots M _ { n } \ rightarrow \ lambda x _ { 零 } \ ldots \ lambda x _ { i 影一 } . A ( M _ { 一 } ) M _ { 二 } \ ldots M _ { n } $ , where $ i \ geq 零 , n \ geq 一 $ .

毋是這種形式的任何歸約攏是內部 beta 歸約。

===歸約的策略===

一般的講，對定項有偌無仝款的可能的 beta 歸約。'''正規序歸約'''是一種求值策略，伊一直終應用「頭殼位置的 beta 歸約」的規則，到閣較濟的這種歸約是可能的。佇這點頂懸，結果的項是「頭部範式」。

顛倒反的，佇咧'''應用序歸約'''中，代先應用內部歸約，只干焦佇咧無更加濟的內部歸約是可能的時陣應用頭部歸約。

正規序歸約是完備的，佇咧若是一个項有頭殼範式正正辦規序還約總是會用得最終達到伊的意義上。顛倒反的，應用序大約可能無終止，就算講佇這个項有規範的形式的時陣。比如講，使用應用序大約，下列歸約是列做是可能的：


: $ ( \ mathbf { \ lambda } x . z ) ( ( \ lambda w . www ) ( \ lambda w . www ) ) $


: $ \ rightarrow ( \ lambda x . z ) ( ( \ lambda w . www ) ( \ lambda w . www ) ( \ lambda w . www ) ) $


: $ \ rightarrow ( \ lambda x . z ) ( ( \ lambda w . www ) ( \ lambda w . www ) ( \ lambda w . www ) ( \ lambda w . www ) ) $


: $ \ rightarrow ( \ lambda x . z ) ( ( \ lambda w . www ) ( \ lambda w . www ) ( \ lambda w . www ) ( \ lambda w . www ) ( \ lambda w . www ) ) $


: $ \ ldots $

而使用正規序歸約，仝款起點猛醒的歸約到範式：


: $ ( \ mathbf { \ lambda } x . z ) ( ( \ lambda w . www ) ( \ lambda w . www ) ) $


: $ \ rightarrow z $

==參見==

* lambda 演算
* 規範化性質

[[分類: 待校正]]