Skip to content

常见定义 ​

布尔和条件 ​

True=λx.λy.x\text{True} = \lambda x.\lambda y.x

False=λx.λy.y\text{False} = \lambda x.\lambda y.y

If=λb.λx.λy.b x y\text{If} = \lambda b.\lambda x.\lambda y. b\ x\ y

例如,将 True M N\text{True}\ M\ N 归约:

If True M N↓β(λb.λx.λy.b x y) True M N↓β(λx.λy.True x y) M N↓β(λy.True M y) N↓βTrue M N↓β(λx.λy.x) M N↓β(λy.M) N↓βM\text{If}\ \text{True}\ M\ N \\ \downarrow_{\beta} \\ (\lambda b.\lambda x.\lambda y. b\ x\ y)\ \text{True}\ M\ N \\ \downarrow_{\beta} \\ (\lambda x.\lambda y. \text{True}\ x\ y)\ M\ N \\ \downarrow_{\beta} \\ (\lambda y. \text{True}\ M\ y)\ N \\ \downarrow_{\beta} \\ \text{True}\ M\ N \\ \downarrow_{\beta} \\ (\lambda x.\lambda y.x)\ M\ N \\ \downarrow_{\beta} \\ (\lambda y.M)\ N \\ \downarrow_{\beta} \\ M