2,732
次編輯
「型別理論與形式證明筆記」修訂間的差異
無編輯摘要
Tankianting（討論 | 貢獻） |
Tankianting（討論 | 貢獻） |
||
| 行 23： | 行 23： | ||
若 λz.P<sup>y→z</sup>是λy.P的variation，且z∉FV(N) | 若 λz.P<sup>y→z</sup>是λy.P的variation，且z∉FV(N) | ||
==1.9 Normal form and confluence(合流)== | |||
Theorem 1.9.8 Church-Rosser(CR); Confluence | |||
假設有lambda term M，若 | |||
<math display="inline">M\twoheadrightarrow N_1</math>且 | |||
<math display="inline">M\twoheadrightarrow N_2</math> | |||
則有<math display="inline">N_3</math>使得 | |||
<math display="inline">N_1\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) = | ||