2,617
次編輯
「型別理論與形式證明筆記」修訂間的差異
跳至導覽
跳至搜尋
→1.9 Normal form and confluence(合流)
Tankianting（討論 | 貢獻） |
Tankianting（討論 | 貢獻） |
||
| 行 24： | 行 24： | ||
==1.9 Normal form and confluence(合流)== | ==1.9 Normal form and confluence(合流)== | ||
Theorem 1.9.8 Church-Rosser(CR); Confluence | ===Def 1.9.6 weak normalization 和strong normalization弱正規化和強正規化=== | ||
*若有N滿足<math display="inline">M\twoheadrightarrow_{\beta} N</math>，則M是弱正規化 weak normalizing。 | |||
*若沒有從M起始的無限歸約路徑，則M是強正規化 strong normalizing。 | |||
===Theorem 1.9.8 Church-Rosser(CR); Confluence=== | |||
假設有lambda term M，若 | 假設有lambda term M，若 | ||
| 行 35： | 行 40： | ||
<math display="inline">N_1\twoheadrightarrow N_3</math>且 | <math display="inline">N_1\twoheadrightarrow N_3</math>且 | ||
<math display="inline">N_2\twoheadrightarrow N_3</math> | <math display="inline">N_2\twoheadrightarrow N_3</math> | ||
= 第2章：簡單型別lambda運算(simple typed lambda calculus) = | = 第2章：簡單型別lambda運算(simple typed lambda calculus) = | ||