# λ-Calculus Homework

### Расставьте скобки
* λv.vp λu.v u
* (λv.vp) λu.w λw.wupv
* λv.v u λv.uv

### Подчеркните все свободные переменные
* λv.v p λu.v u
* (λv. v p) λu. w λw. w u p v
* λv. v u λv. u v

### Примените β-редукцию (и α-конверсию там, где это необходимо) до тех пор, пока это возможно. В ответе укажите все этапы преобразования выражения
* (λv.v v) (λu.u v) p
* (λv. (λu. (v u)) u) p
* ((λv.v v) (λu.u)) (λu.u)
* (((λv. λu.(v u))(λu.u)) w)

### Покажите, что заданные выражения имеют несколько различных последовательностей редукции, найдите нормальную форму
* (λv.u) ((λu.u u u) (λv.v v v))
* (λvu.v) (λu.u) ((λv.v v) (λv.v v))

#### Пусть and ≡ λx.λy. x y 𝔽
* Докажите, что and 𝕋 𝕋 = 𝕋.
* Докажите, что and 𝕋 𝔽 = 𝔽.
* Докажите, что or 𝔽 𝔽 = 𝔽.

### Арифметические операции над нумералами Чёрча
#### Пусть cn≡ λf.λx. fn(x) — n-й нумерал Черча, и succ ≡ λx.λf.λp. f (x f p)
* Докажите, что succ 1 = 2.
* Докажите, что succ 4 = 5.

#### Пусть cn≡ λf.λx. fn(x) — n-й нумерал Черча и x + y ≡ λx.λy.λp.λq. x p (y p q)
* Докажите, что 1 + 2 = 3.
* Докажите, что 2 + 3 = 5.

#### Пусть cn≡ λf.λx. fn(x) — n-й нумерал Черча и x ⋅ y ≡ λx.λy.λz. x (y z)
* Докажите, что 1 * 2 = 2.
* Докажите, что 2 * 2 = 4.
*