2,617
次編輯
「型別理論與形式證明筆記」修訂間的差異
→第1章：無型別lambda運算(untyped lambda calculus)
Tankianting（討論 | 貢獻） |
Tankianting（討論 | 貢獻） |
||
| 行 12： | 行 12： | ||
=第1章：無型別lambda運算(untyped lambda calculus)= | =第1章：無型別lambda運算(untyped lambda calculus)= | ||
==1.6 Substitution(Beta reduction)== | |||
1a) x[x:=N]≡N // x:=N 即N代入x | |||
1b) y[x:=N]≡y (if x≢y) | |||
2) (P Q)[x:=N]≡(P[x:=N])(Q[x:=N]) | |||
3) (λy.P)[x:=N]≡(λz.P<sup>y→z</sup>[x:=N]) // P進行α重名自y到x | |||
若 λz.P<sup>y→z</sup>是λy.P的variation，且z∉FV(N) | |||
= 第2章：簡單型別lambda運算(simple typed lambda calculus) = | = 第2章：簡單型別lambda運算(simple typed lambda calculus) = | ||