Нумералы

Введем по индукции обозначение

aⁿb nN n ab= aⁿb

a⁰b=b

aⁿ⁺¹b=a(aⁿb)

Пример. a³b=a(a(ab))

Определение:

Нумераломn будем называть λ-выражение вида λху.хⁿy, где n=0,1,2,…

n = λху.хⁿy

n =(SB) ⁿ(KI) (то же выражение, но в терминах комбинаторной логики)

Введем функцию прибавления единицы σ.

σ = λхуz.y(хyz) (σ = λхуz.xy(yz))

σn = n+1

Пример. 0 = λху.y 2 = λху.x(xy)

Покажем, что для таких нумералов (n) σ прибавляет единицу:

┌───────_↓

σ n ab = (λхуz.y(xyz))(λху.хⁿy)ab = (((λx.(λy.(λz.y(xyz))))(λx.λy.хⁿy))a)b └───_σ──┘└── _n ─┘ ^↑───────────└─────┘

┌────_↓───────_↓ ┌─────────_↓

= ((λy.(λz.(y((λx.λy.хⁿy)yz)))a)b = (λz.a((λx.λy.хⁿy))az))b = a((λx.λy.хⁿy)ab) =

^↑──────────────┘ ^↑──────────┘ └─ _n ───┘

= a(aⁿb) =aⁿ⁺¹b = /(λху.хⁿ⁺¹y)ab/ = (n+1) ab.

½ ↓

σ (SB) ⁿ(KI) = (λхуz.y(xyz))((SB) ⁿ(KI))(λхуz.y(xyz))[(SB) ⁿ(KI)]ab =

^↑──────└─────┘

= a(((SB) ⁿ(KI)a)b) =^B Ba[(SB) ⁿ(KI)a]b =^S SB[(SB) ⁿ(KI)]ab = (SB) ⁿ⁺¹(KI)ab

└_a┘└──_b───┘_{c x z}└──_y──┘ _z

σ^| = λхуz.xy(yz)- альтернативное определение σ, которое также приводится в литературе. Для него можно провести аналогичные выводы.

TRUE λху.x

FALSE λху.y

If x then y else z xyz

Как это проверить?

If TRUE then A else B A

If FALSE then A else B B

┌─_↓

(λху.x)AB = A

┌─_↓

(λху.y)AB = B

X&Y If X then Y else FALSE

XVY If X then TRUE else Y

Дата добавления: 2014-01-11