Лямбда-исчислСниС

Π’ этой Π³Π»Π°Π²Π΅ ΠΌΡ‹ ΡƒΠ·Π½Π°Π΅ΠΌ ΠΎ лямбда-исчислСнии. Лямбда-исчислСниС описываСт понятиС Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌΠ°. Π•Ρ‰Ρ‘ Π΄ΠΎ появлСния ΠΊΠΎΠΌΠΏΡŒΡŽΡ‚Π΅Ρ€ΠΎΠ² Π² 30-Π΅ Π³ΠΎΠ΄Ρ‹ Π΄Π²Π°Π΄Ρ†Π°Ρ‚ΠΎΠ³ΠΎ Π²Π΅ΠΊΠ° ΠΌΠ°Ρ‚Π΅ΠΌΠ°Ρ‚ΠΈΠΊΠΎΠ² интСрСсовал вопрос ΠΎ возмоТности создания Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌΠ°, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹ΠΉ ΠΌΠΎΠ³ Π±Ρ‹ Π½Π° основС Π·Π°Π΄Π°Π½Π½Ρ‹Ρ… аксиом Π΄Π°Ρ‚ΡŒ ΠΎΡ‚Π²Π΅Ρ‚ ΠΎ Ρ‚ΠΎΠΌ Π²Π΅Ρ€Π½ΠΎ ΠΈΠ»ΠΈ Π½Π΅Ρ‚ Π½Π΅ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠ΅ логичСскоС высказываниС. НапримСр Ρƒ нас Π΅ΡΡ‚ΡŒ Π±Π°Π·ΠΎΠ²Ρ‹Π΅ утвСрТдСния ΠΈ логичСскиС связки Ρ‚Π°ΠΊΠΈΠ΅ ΠΊΠ°ΠΊ β€œΠΈβ€, β€œΠΈΠ»ΠΈβ€, β€œΠ΄Π»Ρ любого из”, β€œΡΡƒΡ‰Π΅ΡΡ‚Π²ΡƒΠ΅Ρ‚ ΠΎΠ΄ΠΈΠ½ из”, с ΠΏΠΎΠΌΠΎΡ‰ΡŒΡŽ ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Ρ… ΠΌΡ‹ ΠΌΠΎΠΆΠ΅ΠΌ ΡΡ‚Ρ€ΠΎΠΈΡ‚ΡŒ ΠΈΠ· Π±Π°Π·ΠΎΠ²Ρ‹Ρ… высказываний составныС. НСкоторыС ΠΈΠ· Π½ΠΈΡ… окаТутся Π»ΠΎΠΆΠ½Ρ‹ΠΌΠΈ, Π° Π΄Ρ€ΡƒΠ³ΠΈΠ΅ истинными. Нам интСрСсно ΡƒΠ·Π½Π°Ρ‚ΡŒ ΠΊΠ°ΠΊΠΈΠ΅. Но для Ρ€Π΅ΡˆΠ΅Π½ΠΈΡ этой Π·Π°Π΄Π°Ρ‡ΠΈ ΠΏΡ€Π΅ΠΆΠ΄Π΅ всСго Π½Π΅ΠΎΠ±Ρ…ΠΎΠ΄ΠΈΠΌΠΎ Π±Ρ‹Π»ΠΎ ΠΏΠΎΠ½ΡΡ‚ΡŒ Π° Ρ‡Ρ‚ΠΎ ΠΆΠ΅ Ρ‚Π°ΠΊΠΎΠ΅ Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌ?

ΠžΡ‚Π²Π΅Ρ‚ Π½Π° этот вопрос Π΄Π°Π»ΠΈ Алонсо Π§Ρ‘Ρ€Ρ‡ (Alonso Church) ΠΈ Алан Π’ΡŒΡŽΡ€ΠΈΠ½Π³ (Alan Turing). Π§Ρ‘Ρ€Ρ‡ Ρ€Π°Π·Ρ€Π°Π±ΠΎΡ‚Π°Π» лямбда-исчислСниС, Π° Π’ΡŒΡŽΡ€ΠΈΠ½Π³ Ρ‚Π΅ΠΎΡ€ΠΈΡŽ машин Π’ΡŒΡŽΡ€ΠΈΠ½Π³Π°. Оказалось, Ρ‡Ρ‚ΠΎ Π·Π°Π΄Π°Ρ‡Π° автоматичСского опрСдСлСния истинности Ρ„ΠΎΡ€ΠΌΡƒΠ» Π² ΠΎΠ±Ρ‰Π΅ΠΌ случаС Π½Π΅ ΠΈΠΌΠ΅Π΅Ρ‚ Ρ€Π΅ΡˆΠ΅Π½ΠΈΡ.

Π’ основС лямбда-исчислСниС Π»Π΅ΠΆΠΈΡ‚ понятиС Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ. ΠœΡ‹ ΠΌΠΎΠΆΠ΅ΠΌ ΡΠΎΡΡ‚Π°Π²Π»ΡΡ‚ΡŒ слоТныС Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ ΠΈΠ· ΠΏΡ€ΠΎΡΡ‚Π΅ΠΉΡˆΠΈΡ…, Π° Ρ‚Π°ΠΊΠΆΠ΅ ΠΏΠΎΠ΄ΡΡ‚Π°Π²Π»ΡΡ‚ΡŒ Π² Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚Ρ‹, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Π΅ ΠΌΠΎΠ³ΡƒΡ‚ Π±Ρ‹Ρ‚ΡŒ ΠΊΠ°ΠΊ константами Ρ‚Π°ΠΊ ΠΈ Π΄Ρ€ΡƒΠ³ΠΈΠΌΠΈ функциями. Как Ρ‚ΠΎΠ»ΡŒΠΊΠΎ ΠΌΡ‹ составили Π²Ρ‹Ρ€Π°ΠΆΠ΅Π½ΠΈΠ΅ ΠΌΡ‹ ΠΌΠΎΠΆΠ΅ΠΌ ΠΏΠ΅Ρ€Π΅Π΄Π°Ρ‚ΡŒ Π΅Π³ΠΎ Π²Ρ‹Ρ‡ΠΈΡΠ»ΠΈΡ‚Π΅Π»ΡŽ. Он подставляСт Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚Ρ‹ Π² Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ ΠΈ Π²ΠΎΠ·Π²Ρ€Π°Ρ‰Π°Π΅Ρ‚ Ρ‚Π°ΠΊΠΎΠ΅ Π²Ρ‹Ρ€Π°ΠΆΠ΅Π½ΠΈΠ΅, Π² ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠΌ Π½Π΅Π²ΠΎΠ·ΠΌΠΎΠΆΠ½ΠΎ Π΄Π°Π»Π΅Π΅ ΠΏΡ€ΠΎΠ²ΠΎΠ΄ΠΈΡ‚ΡŒ подстановки Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚ΠΎΠ². Π­Ρ‚ΠΎΡ‚ процСсс провСдСния подстановок считаСтся вычислСниСм Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌΠ°.

Π’ Ρ€Π°ΠΌΠΊΠ°Ρ… Ρ‚Π΅ΠΎΡ€ΠΈΠΈ машин Π’ΡŒΡŽΡ€ΠΈΠ½Π³Π° Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌ описываСтся ΠΏΠΎ-Π΄Ρ€ΡƒΠ³ΠΎΠΌΡƒ. Машина Π’ΡŒΡŽΡ€ΠΈΠ½Π³Π° ΠΈΠΌΠ΅Π΅Ρ‚ Π²Π½ΡƒΡ‚Ρ€Π΅Π½Π½Π΅Π΅ состояниС, БостояниС содСрТит Π½Π΅ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠ΅ Π·Π½Π°Ρ‡Π΅Π½ΠΈΠ΅, ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠ΅ измСняСтся ΠΏΠΎ Ρ…ΠΎΠ΄Ρƒ Ρ€Π°Π±ΠΎΡ‚Ρ‹ ΠΌΠ°ΡˆΠΈΠ½Ρ‹. Машина ΠΆΠΈΠ²Ρ‘Ρ‚ Π½Π΅ сама ΠΏΠΎ сСбС, ΠΎΠ½Π° Ρ‡ΠΈΡ‚Π°Π΅Ρ‚ Π»Π΅Π½Ρ‚Ρƒ символов. Π›Π΅Π½Ρ‚Π° символов – это большая Ρ†Π΅ΠΏΠΎΡ‡ΠΊΠ° Π±ΡƒΠΊΠ². На ΠΊΠ°ΠΆΠ΄ΡƒΡŽ Π±ΡƒΠΊΠ²Ρƒ машина Ρ€Π΅Π°Π³ΠΈΡ€ΡƒΠ΅Ρ‚ сСриСй дСйствий. Она ΠΌΠΎΠΆΠ΅Ρ‚ ΠΈΠ·ΠΌΠ΅Π½ΠΈΡ‚ΡŒ Π·Π½Π°Ρ‡Π΅Π½ΠΈΠ΅ состояния, ΠΎΠ±Π½ΠΎΠ²ΠΈΡ‚ΡŒ Π±ΡƒΠΊΠ²Ρƒ Π² Π»Π΅Π½Ρ‚Π΅ ΠΈΠ»ΠΈ ΠΏΠ΅Ρ€Π΅ΠΉΡ‚ΠΈ ΠΊ ΡΠ»Π΅Π΄ΡƒΡŽΡ‰Π΅ΠΌΡƒ ΠΈΠ»ΠΈ ΠΏΡ€Π΅Π΄Ρ‹Π΄ΡƒΡ‰Π΅ΠΌΡƒ символу. Π•ΡΡ‚ΡŒ состояния, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Π΅ ΠΎΠ±ΠΎΠ·Π½Π°Ρ‡Π°ΡŽΡ‚ ΠΊΠΎΠ½Π΅Ρ† Ρ€Π°Π±ΠΎΡ‚Ρ‹, ΠΎΠ½ΠΈ Π½Π°Π·Ρ‹Π²Π°ΡŽΡ‚ΡΡ Ρ‚Π΅Ρ€ΠΌΠΈΠ½Π°Π»ΡŒΠ½Ρ‹ΠΌΠΈ. Как Ρ‚ΠΎΠ»ΡŒΠΊΠΎ машина Π΄ΠΎΠΉΠ΄Ρ‘Ρ‚ Π΄ΠΎ Ρ‚Π΅Ρ€ΠΌΠΈΠ½Π°Π»ΡŒΠ½ΠΎΠ³ΠΎ состояния ΠΌΡ‹ считаСм, Ρ‡Ρ‚ΠΎ вычислСниС Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌΠ° Π·Π°ΠΊΠΎΠ½Ρ‡ΠΈΠ»ΠΎΡΡŒ. ПослС этого ΠΌΡ‹ ΠΌΠΎΠΆΠ΅ΠΌ ΡΡ‡ΠΈΡ‚Π°Ρ‚ΡŒ Ρ€Π΅Π·ΡƒΠ»ΡŒΡ‚Π°Ρ‚ ΠΈΠ· состояний ΠΌΠ°ΡˆΠΈΠ½Ρ‹.

Π€ΡƒΠ½ΠΊΡ†ΠΈΠΎΠ½Π°Π»ΡŒΠ½Ρ‹Π΅ языки программирования основаны Π½Π° лямбда-исчислСнии. ΠŸΠΎΡΡ‚ΠΎΠΌΡƒ ΠΌΡ‹ Π±ΡƒΠ΄Π΅ΠΌ Π³ΠΎΠ²ΠΎΡ€ΠΈΡ‚ΡŒ ΠΈΠΌΠ΅Π½Π½ΠΎ ΠΎΠ± этом описании Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌΠ°.

Лямбда исчислСниС Π±Π΅Π· Ρ‚ΠΈΠΏΠΎΠ²

БоставлСниС Ρ‚Π΅Ρ€ΠΌΠΎΠ²

МоТно ΡΡ‡ΠΈΡ‚Π°Ρ‚ΡŒ, Ρ‡Ρ‚ΠΎ лямбда исчислСниС это Ρ‚Π°ΠΊΠΎΠΉ малСнький язык программирования. Π’ Π½Ρ‘ΠΌ Π΅ΡΡ‚ΡŒ мноТСство символов, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Π΅ ΡΡ‡ΠΈΡ‚Π°ΡŽΡ‚ΡΡ ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Ρ‹ΠΌΠΈ, ΠΎΠ½ΠΈ Ρ‡Ρ‚ΠΎ-Ρ‚ΠΎ ΠΎΠ±ΠΎΠ·Π½Π°Ρ‡Π°ΡŽΡ‚ ΠΈ Π½Π΅Π΄Π΅Π»ΠΈΠΌΡ‹. Π’ лямбда-исчислСнии ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠ½Ρ‹ΠΉ ΠΊΠΎΠ΄ называСтся Ρ‚Π΅Ρ€ΠΌΠΎΠΌ. Для написания ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠ½ΠΎΠ³ΠΎ ΠΊΠΎΠ΄Π° Ρƒ нас Π΅ΡΡ‚ΡŒ всСго Ρ‚Ρ€ΠΈ ΠΏΡ€Π°Π²ΠΈΠ»Π°:

Π’ Ρ„ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½ΠΎΠΌ описании Π΄ΠΎΠ±Π°Π²Π»ΡΡŽΡ‚ Π΅Ρ‰Ρ‘ ΠΎΠ΄Π½ΠΎ ΠΏΡ€Π°Π²ΠΈΠ»ΠΎ, ΠΎΠ½ΠΎ Π³ΠΎΠ²ΠΎΡ€ΠΈΡ‚ ΠΎ Ρ‚ΠΎΠΌ, Ρ‡Ρ‚ΠΎ Π΄Ρ€ΡƒΠ³ΠΈΡ… Ρ‚Π΅Ρ€ΠΌΠΎΠ² Π½Π΅Ρ‚. ΠŸΠ΅Ρ€Π²ΠΎΠ΅ ΠΏΡ€Π°Π²ΠΈΠ»ΠΎ, Π³ΠΎΠ²ΠΎΡ€ΠΈΡ‚ ΠΎ Ρ‚ΠΎΠΌ, Ρ‡Ρ‚ΠΎ Ρƒ нас Π΅ΡΡ‚ΡŒ Π°Π»Ρ„Π°Π²ΠΈΡ‚ символов, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹ΠΉ Ρ‡Ρ‚ΠΎ-Ρ‚ΠΎ ΠΎΠ±ΠΎΠ·Π½Π°Ρ‡Π°Π΅Ρ‚, эти символы ΡΠ²Π»ΡΡŽΡ‚ΡΡ Π±Π°Π·ΠΎΠ²Ρ‹ΠΌΠΈ ΡΡ‚Ρ€ΠΎΠΈΡ‚Π΅Π»ΡŒΠ½Ρ‹ΠΌΠΈ Π±Π»ΠΎΠΊΠ°ΠΌΠΈ ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡ‹. Π’Ρ‚ΠΎΡ€ΠΎΠ΅ ΠΈ Ρ‚Ρ€Π΅Ρ‚ΡŒΠ΅ ΠΏΡ€Π°Π²ΠΈΠ»Π° говорят ΠΎ Ρ‚ΠΎΠΌ ΠΊΠ°ΠΊ ΠΈΠ· Π±Π°Π·ΠΎΠ²Ρ‹Ρ… элСмСнтов ΠΏΠΎΠ»ΡƒΡ‡Π°ΡŽΡ‚ΡΡ составныС. Π’Ρ‚ΠΎΡ€ΠΎΠ΅ ΠΏΡ€Π°Π²ΠΈΠ»ΠΎ – это ΠΏΡ€Π°Π²ΠΈΠ»ΠΎ примСнСния Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ ΠΊ Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚Ρƒ. Π’ Π½Ρ‘ΠΌ $M$ ΠΎΠ±ΠΎΠ·Π½Π°Ρ‡Π°Π΅Ρ‚ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΡŽ, Π° $N$ ΠΎΠ±ΠΎΠ·Π½Π°Ρ‡Π°Π΅Ρ‚ Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚. ВсС Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ ΡΠ²Π»ΡΡŽΡ‚ΡΡ функциями ΠΎΠ΄Π½ΠΎΠ³ΠΎ Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚Π°, Π½ΠΎ ΠΎΠ½ΠΈ ΠΌΠΎΠ³ΡƒΡ‚ ΠΏΡ€ΠΈΠ½ΠΈΠΌΠ°Ρ‚ΡŒ ΠΈ Π²ΠΎΠ·Π²Ρ€Π°Ρ‰Π°Ρ‚ΡŒ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ. ΠŸΠΎΡΡ‚ΠΎΠΌΡƒ ΠΏΡ€ΠΈΠΌΠ΅Π½Π΅Π½ΠΈΠ΅ Ρ‚Ρ€Ρ‘Ρ… Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚ΠΎΠ² ΠΊ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ $Fun$ Π±ΡƒΠ΄Π΅Ρ‚ Π²Ρ‹Π³Π»ΡΠ΄Π΅Ρ‚ΡŒ Ρ‚Π°ΠΊ:

$$(((Fun\ Arg1)\ Arg2)\ Arg3)$$

Π’Ρ€Π΅Ρ‚ΡŒΠ΅ ΠΏΡ€Π°Π²ΠΈΠ»ΠΎ Π³ΠΎΠ²ΠΎΡ€ΠΈΡ‚ ΠΎ Ρ‚ΠΎΠΌ ΠΊΠ°ΠΊ ΡΠΎΠ·Π΄Π°Π²Π°Ρ‚ΡŒ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ. Π‘ΠΏΠ΅Ρ†ΠΈΠ°Π»ΡŒΠ½Ρ‹ΠΉ символ лямбда ($\lambda$) Π² Π²Ρ‹Ρ€Π°ΠΆΠ΅Π½ΠΈΠΈ $(\lambda x .M)$ Π³ΠΎΠ²ΠΎΡ€ΠΈΡ‚ ΠΎ Ρ‚ΠΎΠΌ, Ρ‡Ρ‚ΠΎ ΠΌΡ‹ собираСмся ΠΎΠΏΡ€Π΅Π΄Π΅Π»ΠΈΡ‚ΡŒ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΡŽ с Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚ΠΎΠΌ $x$ ΠΈ Ρ‚Π΅Π»ΠΎΠΌ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ $M$. Π‘ Ρ‚Π°ΠΊΠΈΠΌΠΈ функциями ΠΌΡ‹ ΡƒΠΆΠ΅ ΡΡ‚Π°Π»ΠΊΠΈΠ²Π°Π»ΠΈΡΡŒ. Π­Ρ‚ΠΎ бСзымянныС Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ. ΠŸΡ€ΠΈΠ²Π΅Π΄Ρ‘ΠΌ нСсколько ΠΏΡ€ΠΈΠΌΠ΅Ρ€ΠΎΠ² Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΉ. Начнём с самого простого, ΠΎΠΏΡ€Π΅Π΄Π΅Π»ΠΈΠΌ Ρ‚ΠΎΠΆΠ΄Π΅ΡΡ‚Π²Π΅Π½Π½ΡƒΡŽ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΡŽ:

$$(\lambda x .x)$$

Ѐункция ΠΏΡ€ΠΈΠ½ΠΈΠΌΠ°Π΅Ρ‚ Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚ $x$ ΠΈ Ρ‚ΡƒΡ‚ ΠΆΠ΅ Π²ΠΎΠ·Π²Ρ€Π°Ρ‰Π°Π΅Ρ‚ Π΅Π³ΠΎ Π² Ρ‚Π΅Π»Π΅. Π’Π΅ΠΏΠ΅Ρ€ΡŒ посмотрим Π½Π° ΠΊΠΎΠ½ΡΡ‚Π°Π½Ρ‚Π½ΡƒΡŽ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΡŽ:

$$(\lambda x .(\lambda y .x))$$

ΠšΠΎΠ½ΡΡ‚Π°Π½Ρ‚Π½Π°Ρ функция являСтся Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠ΅ΠΉ Π΄Π²ΡƒΡ… Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚ΠΎΠ², поэтому наш Ρ‚Π΅Ρ€ΠΌ ΠΏΡ€ΠΈΠ½ΠΈΠΌΠ°Π΅Ρ‚ ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½ΡƒΡŽ $x$ ΠΈ Π²ΠΎΠ·Π²Ρ€Π°Ρ‰Π°Π΅Ρ‚ Π΄Ρ€ΡƒΠ³ΠΎΠΉ Ρ‚Π΅Ρ€ΠΌ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΡŽ $(\lambda y .x)$. Π­Ρ‚Π° функция ΠΏΡ€ΠΈΠ½ΠΈΠΌΠ°Π΅Ρ‚ $y$, Π° Π²ΠΎΠ·Π²Ρ€Π°Ρ‰Π°Π΅Ρ‚ x. Π’ Haskell ΠΌΡ‹ Π±Ρ‹ написали это Ρ‚Π°ΠΊ:

\x -> (\y -> x)

Π’ΠΎΡ‡ΠΊΠ° смСнилась Π½Π° стрСлку, Π° лямбда потСряла ΠΎΠ΄Π½Ρƒ Π½ΠΎΠΆΠΊΡƒ. Π’Π΅ΠΏΠ΅Ρ€ΡŒ ΠΎΠΏΡ€Π΅Π΄Π΅Π»ΠΈΠΌ ΠΊΠΎΠΌΠΏΠΎΠ·ΠΈΡ†ΠΈΡŽ. ΠšΠΎΠΌΠΏΠΎΠ·ΠΈΡ†ΠΈΡ ΠΏΡ€ΠΈΠ½ΠΈΠΌΠ°Π΅Ρ‚ Π΄Π²Π΅ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ ΠΎΠ΄Π½ΠΎΠ³ΠΎ Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚Π° ΠΈ направляСт Π²Ρ‹Ρ…ΠΎΠ΄ Π²Ρ‚ΠΎΡ€ΠΎΠΉ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ Π½Π° Π²Ρ…ΠΎΠ΄ ΠΏΠ΅Ρ€Π²ΠΎΠΉ:

$$(\lambda f .(\lambda g .(\lambda x .(f(gx)))))$$

ΠŸΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Ρ‹Π΅ $f$ ΠΈ $g$ – это Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Π΅ ΡƒΡ‡Π°ΡΡ‚Π²ΡƒΡŽΡ‚ Π² ΠΊΠΎΠΌΠΏΠΎΠ·ΠΈΡ†ΠΈΠΈ, Π° $x$ это Π²Ρ…ΠΎΠ΄ Ρ€Π΅Π·ΡƒΠ»ΡŒΡ‚ΠΈΡ€ΡƒΡŽΡ‰Π΅ΠΉ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ. Π£ΠΆΠ΅ Π² Ρ‚Π°ΠΊΠΎΠΌ простом Π²Ρ‹Ρ€Π°ΠΆΠ΅Π½ΠΈΠΈ Ρƒ нас ΠΏΡΡ‚ΡŒ скобок Π½Π° ΠΊΠΎΠ½Ρ†Π΅. Π”Π°Π²Π°ΠΉΡ‚Π΅ Π²Π²Π΅Π΄Ρ‘ΠΌ нСсколько соглашСний, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Π΅ ΠΎΠ±Π»Π΅Π³Ρ‡Π°Ρ‚ написаниС Ρ‚Π΅Ρ€ΠΌΠΎΠ²:

ПишСм ΠŸΠΎΠ΄Ρ€Π°Π·ΡƒΠΌΠ΅Π²Π°Π΅ΠΌ

ΠžΠΏΡƒΡΡ‚ΠΈΠΌ внСшниС скобки:

$\lambda x .x$

$(\lambda x .x)$

Π’ ΠΏΡ€ΠΈΠΌΠ΅Π½Π΅Π½ΠΈΠΈ Π³Ρ€ΡƒΠΏΠΏΠΈΡ€ΡƒΠ΅ΠΌ скобки Π²Π»Π΅Π²ΠΎ:

$fghx$

$((fg)h)x$

Π’ функциях Π³Ρ€ΡƒΠΏΠΏΠΈΡ€ΡƒΠ΅ΠΌ скобки Π²ΠΏΡ€Π°Π²ΠΎ:

$\lambda x.\lambda y.x$

$(\lambda x .(\lambda y .x))$

ПишСм Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ Π½Π΅ΡΠΊΠΎΠ»ΡŒΠΊΠΈΡ… Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚ΠΎΠ² с ΠΎΠ΄Π½ΠΎΠΉ лямбдой:

$\lambda xy .x$

$(\lambda x .(\lambda y .x))$

Π‘ этими соглашСниями ΠΌΡ‹ ΠΌΠΎΠΆΠ΅ΠΌ ΠΏΠ΅Ρ€Π΅ΠΏΠΈΡΠ°Ρ‚ΡŒ Ρ‚Π΅Ρ€ΠΌ для ΠΊΠΎΠΌΠΏΠΎΠ·ΠΈΡ†ΠΈΠΈ Ρ‚Π°ΠΊ:

$$\lambda f g x .f(gx)$$

Π‘Ρ€Π°Π²Π½ΠΈΡ‚Π΅ с Π²Ρ‹Ρ€Π°ΠΆΠ΅Π½ΠΈΠ΅ΠΌ Π½Π° языкС Haskell:

\f g x -> f (g x)

ВыраТСния ΠΎΡ‡Π΅Π½ΡŒ ΠΏΠΎΡ…ΠΎΠΆΠΈ. Haskell ΠΈΠ½ΠΎΠ³Π΄Π° Π½Π°Π·Ρ‹Π²Π°ΡŽΡ‚ засахарСнной вСрсиСй лямбда исчислСния. Π’ лямбда-исчислСнии ΠΌΡ‹ Π½Π΅ Π±ΡƒΠ΄Π΅ΠΌ ΡΡ‚Π°Π²ΠΈΡ‚ΡŒ ΠΏΡ€ΠΎΠ±Π΅Π»Ρ‹ для примСнСния Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚ΠΎΠ² ΠΊ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ. ΠœΡ‹ Π±ΡƒΠ΄Π΅ΠΌ ΡΡ‡ΠΈΡ‚Π°Ρ‚ΡŒ, Ρ‡Ρ‚ΠΎ всС ΠΈΠΌΠ΅Π½Π° ΠΎΠ΄Π½ΠΎΠ±ΡƒΠΊΠ²Π΅Π½Π½Ρ‹Π΅. ΠŸΡ€ΠΈ этом ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Ρ‹Π΅ ΠΌΡ‹ Π±ΡƒΠ΄Π΅ΠΌ ΠΏΠΈΡΠ°Ρ‚ΡŒ с малСнькой Π±ΡƒΠΊΠ²Ρ‹, Π° составныС Ρ‚Π΅Ρ€ΠΌΡ‹ с большой.

ΠžΠΏΡ€Π΅Π΄Π΅Π»ΠΈΠΌ Π΅Ρ‰Ρ‘ нСсколько Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΉ. НапримСр Ρ‚Π°ΠΊ выглядит функция flip:

$$\lambda fxy .fyx$$

Или ΠΌΠΎΠΆΠ½ΠΎ Π·Π°ΠΏΠΈΡΠ°Ρ‚ΡŒ Π² Π±ΠΎΠ»Π΅Π΅ явном Π²ΠΈΠ΄Π΅, Π²Ρ‹Π΄Π΅Π»ΠΈΠΌ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΡŽ Π΄Π²ΡƒΡ… Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚ΠΎΠ²:

$$\lambda f .\lambda xy .fyx$$

ΠžΠΏΡ€Π΅Π΄Π΅Π»ΠΈΠΌ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΡŽ on, ΠΎΠ½Π° ΠΏΡ€ΠΈΠ½ΠΈΠΌΠ°Π΅Ρ‚ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΡŽ Π΄Π²ΡƒΡ… Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚ΠΎΠ² $*$ ΠΈ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΡŽ ΠΎΠ΄Π½ΠΎΠ³ΠΎ Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚Π° $f$, Π° Π²ΠΎΠ·Π²Ρ€Π°Ρ‰Π°Π΅Ρ‚ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΡŽ Π΄Π²ΡƒΡ… Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚ΠΎΠ², Π² ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠΉ ΠΊ Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚Π°ΠΌ сначала примСняСтся функция $f$, Π° Π·Π°Ρ‚Π΅ΠΌ ΠΎΠ½ΠΈ ΠΏΠ΅Ρ€Π΅Π΄Π°ΡŽΡ‚ΡΡ Π² Ρ„ΡƒΠ½ΠΊΡ†ΠΈΡŽ $*$:

$$\lambda * f .\lambda x .*(fx)(fx)$$

Π’ лямбда-исчислСнии Π΅ΡΡ‚ΡŒ Ρ‚ΠΎΠ»ΡŒΠΊΠΎ прСфиксноС ΠΏΡ€ΠΈΠΌΠ΅Π½Π΅Π½ΠΈΠ΅ поэтому ΠΌΡ‹ написали $*(fx)(fx)$ вмСсто ΠΏΡ€ΠΈΠ²Ρ‹Ρ‡Π½ΠΎΠ³ΠΎ $(fx)*(fx)$. Π—Π΄Π΅ΡΡŒ опСрация $*$ это Π½Π΅ Ρ‚ΠΎΠ»ΡŒΠΊΠΎ ΡƒΠΌΠ½ΠΎΠΆΠ΅Π½ΠΈΠ΅, Π° любая бинарная функция.

Абстракция

Π€ΡƒΠ½ΠΊΡ†ΠΈΠΈ Π² лямбда-исчислСнии Π½Π°Π·Ρ‹Π²Π°ΡŽΡ‚ абстракциями. ΠœΡ‹ Π±Π΅Ρ€Ρ‘ΠΌ Ρ‚Π΅Ρ€ΠΌ $M$ ΠΈ ΠΏΠ°Ρ€Π°ΠΌΠ΅Ρ‚Ρ€ΠΈΠ·ΡƒΠ΅ΠΌ Π΅Π³ΠΎ ΠΏΠΎ ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½ΠΎΠΉ $x$ Π² Π²Ρ‹Ρ€Π°ΠΆΠ΅Π½ΠΈΠΈ $\lambda x. M$. ΠŸΡ€ΠΈ этом Ссли Π² Ρ‚Π΅Ρ€ΠΌΠ΅ $M$ встрСчаСтся пСрСмСнная $x$, Ρ‚ΠΎ ΠΎΠ½Π° становится связанной. НапримСр Π² Ρ‚Π΅Ρ€ΠΌΠ΅ $\lambda x . \lambda y . x$$ ΠŸΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Π°Ρ $x$ являСтся связанной, Π½ΠΎ Π² Ρ‚Π΅Ρ€ΠΌΠ΅ $\lambda y . x$, ΠΎΠ½Π° ΡƒΠΆΠ΅ Π½Π΅ связана. Π’Π°ΠΊΠΈΠ΅ ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Ρ‹Π΅ Π½Π°Π·Ρ‹Π²Π°ΡŽΡ‚ свободными. ΠœΠ½ΠΎΠΆΠ΅ΡΡ‚Π²ΠΎ связанных ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Ρ‹Ρ… Ρ‚Π΅Ρ€ΠΌΠ° $M$ ΠΌΡ‹ Π±ΡƒΠ΄Π΅ΠΌ ΠΎΠ±ΠΎΠ·Π½Π°Ρ‡Π°Ρ‚ΡŒ $BV(M)$$ ΠΎΡ‚ Π°Π½Π³Π». bound variables, Π° мноТСство свободных ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Ρ‹Ρ… ΠΌΡ‹ Π±ΡƒΠ΄Π΅ΠΌ ΠΎΠ±ΠΎΠ·Π½Π°Ρ‡Π°Ρ‚ΡŒ $FV(M)$ ΠΎΡ‚ Π°Π½Π³Π». free variables.

На ΠΈΠ½Ρ‚ΡƒΠΈΡ‚ΠΈΠ²Π½ΠΎΠΌ ΡƒΡ€ΠΎΠ²Π½Π΅ процСсс абстракции Π·Π°ΠΊΠ»ΡŽΡ‡Π°Π΅Ρ‚ΡΡ Π² Ρ‚ΠΎΠΌ, Ρ‡Ρ‚ΠΎ ΠΌΡ‹ смотрим Π½Π° нСсколько частных случаСв ΠΈ Π²ΠΈΠ΄ΠΈΠΌ Π² Π½ΠΈΡ… Ρ‡Ρ‚ΠΎ-Ρ‚ΠΎ ΠΎΠ±Ρ‰Π΅Π΅. Π­Ρ‚ΠΎ ΠΎΠ±Ρ‰Π΅Π΅ ΠΌΡ‹ выдСляСм Π² Ρ„ΡƒΠ½ΠΊΡ†ΠΈΡŽ, которая ΠΏΠ°Ρ€Π°ΠΌΠ΅Ρ‚Ρ€ΠΈΠ·ΠΎΠ²Π°Π½Π° частностями. НапримСр ΠΌΡ‹ Π²ΠΈΠ΄ΠΈΠΌ выраТСния:

$$\lambda x .+xx, \quad \lambda x .*xx$$

И Π² Ρ‚ΠΎΠΌ ΠΈ Π² Π΄Ρ€ΡƒΠ³ΠΎΠΌ Ρƒ нас Π΅ΡΡ‚ΡŒ функция Π΄Π²ΡƒΡ… Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚ΠΎΠ² $+$ ΠΈΠ»ΠΈ $*$ ΠΈ ΠΌΡ‹ Π΄Π΅Π»Π°Π΅ΠΌ ΠΈΠ· Π½Π΅Ρ‘ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΡŽ ΠΎΠ΄Π½ΠΎΠ³ΠΎ Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚Π°. ΠœΡ‹ ΠΌΠΎΠΆΠ΅ΠΌ Π°Π±ΡΡ‚Ρ€Π°Π³ΠΈΡ€ΠΎΠ²Π°Ρ‚ΡŒ (ΠΏΠ°Ρ€Π°ΠΌΠ΅Ρ‚Ρ€ΠΈΠ·ΠΎΠ²Π°Ρ‚ΡŒ) это ΠΏΠΎΠ²Π΅Π΄Π΅Π½ΠΈΠ΅ Π² Ρ‚Π°ΠΊΡƒΡŽ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΡŽ:

$$\lambda b.\lambda x.b xx$$

На Haskell ΠΌΡ‹ Π±Ρ‹ записали это Ρ‚Π°ΠΊ:

\b -> \x -> b x x

РСдукция. ВычислСниС Ρ‚Π΅Ρ€ΠΌΠΎΠ²

ΠŸΡ€ΠΎΡ†Π΅ΡΡ вычислСния Ρ‚Π΅Ρ€ΠΌΠΎΠ² Π·Π°ΠΊΠ»ΡŽΡ‡Π°Π΅Ρ‚ΡΡ Π² подстановкС Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚ΠΎΠ² Π²ΠΎ всС Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ. ВыраТСния Π²ΠΈΠ΄Π°:

$$(\lambda x .M)\ N$$

Π—Π°ΠΌΠ΅Π½ΡΡŽΡ‚ΡΡ Π½Π°

$$M[x = N]$$

Π­Ρ‚Π° запись ΠΎΠ·Π½Π°Ρ‡Π°Π΅Ρ‚, Ρ‡Ρ‚ΠΎ Π² Ρ‚Π΅Ρ€ΠΌΠ΅ $M$ всС вхоТдСния $x$ Π·Π°ΠΌΠ΅Π½ΡΡŽΡ‚ΡΡ Π½Π° Ρ‚Π΅Ρ€ΠΌ $N$. Π­Ρ‚ΠΎΡ‚ процСсс называСтся Ρ€Π΅Π΄ΡƒΠΊΡ†ΠΈΠ΅ΠΉ Ρ‚Π΅Ρ€ΠΌΠ°. А выраТСния Π²ΠΈΠ΄Π° $(\lambda x .M)\ N$ Π½Π°Π·Ρ‹Π²Π°ΡŽΡ‚ΡΡ рСдСксами. ΠŸΡ€ΠΎΠ²Π΅Π΄Ρ‘ΠΌ ΠΊ ΠΏΡ€ΠΈΠΌΠ΅Ρ€Ρƒ Ρ€Π΅Π΄ΡƒΠΊΡ†ΠΈΡŽ Ρ‚Π΅Ρ€ΠΌΠ°:

$$(\lambda b.\lambda x.b xx) *$$

Для этого Π½Π°ΠΌ Π½ΡƒΠΆΠ½ΠΎ Π² Ρ‚Π΅Ρ€ΠΌΠ΅ $(\lambda x.b xx)$ Π·Π°ΠΌΠ΅Π½ΠΈΡ‚ΡŒ всС вхоТдСния ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½ΠΎΠΉ $b$ Π½Π° ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½ΡƒΡŽ $*$. ПослС этого ΠΌΡ‹ ΠΏΠΎΠ»ΡƒΡ‡ΠΈΠΌ Ρ‚Π΅Ρ€ΠΌ:

$$\lambda x .* xx$$

Π’ этом Ρ‚Π΅Ρ€ΠΌΠ΅ Π½Π΅Ρ‚ рСдСксов. Π­Ρ‚ΠΎ ΠΎΠ·Π½Π°Ρ‡Π°Π΅Ρ‚, Ρ‡Ρ‚ΠΎ ΠΎΠ½ вычислСн ΠΈΠ»ΠΈ находится Π² Π½ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½ΠΎΠΉ Ρ„ΠΎΡ€ΠΌΠ΅.

$\alpha$-ΠΏΡ€Π΅ΠΎΠ±Ρ€Π°Π·ΠΎΠ²Π°Π½ΠΈΠ΅

ΠŸΡ€ΠΈ подстановкС Π½Π΅ΠΎΠ±Ρ…ΠΎΠ΄ΠΈΠΌΠΎ ΡΠ»Π΅Π΄ΠΈΡ‚ΡŒ Π·Π° Ρ‚Π΅ΠΌ, Ρ‡Ρ‚ΠΎΠ±Ρ‹ Ρƒ нас Π½Π΅ появлялись лишниС связывания ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Ρ‹Ρ…. НапримСр рассмотрим Ρ‚Π°ΠΊΠΎΠΉ рСдСкс:

$$(\lambda x y .x)\ y$$

ПослС подстановки Π·Π° счёт совпадСния ΠΈΠΌΡ‘Π½ ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Ρ‹Ρ… ΠΌΡ‹ ΠΏΠΎΠ»ΡƒΡ‡ΠΈΠΌ Ρ‚ΠΎΠΆΠ΄Π΅ΡΡ‚Π²Π΅Π½Π½ΡƒΡŽ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΡŽ:

$$\lambda y .y$$

ΠŸΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Π°Ρ $y$ Π±Ρ‹Π»Π° свободной, Π½ΠΎ послС подстановки стала связанной. НСобходимо ΠΈΡΠΊΠ»ΡŽΡ‡ΠΈΡ‚ΡŒ Ρ‚Π°ΠΊΠΈΠ΅ случаи. ΠŸΠΎΡΠΊΠΎΠ»ΡŒΠΊΡƒ с Π½ΠΈΠΌΠΈ получаСтся, Ρ‡Ρ‚ΠΎ ΠΈΠΌΠ΅Π½Π° связанных ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Ρ‹Ρ… Π² ΠΎΠΏΡ€Π΅Π΄Π΅Π»Π΅Π½ΠΈΠΈ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ Π²Π»ΠΈΡΡŽΡ‚ Π½Π° Π΅Ρ‘ смысл. НапримСр смысл Ρ‚Π°ΠΊΠΎΠ³ΠΎ выраТСния

$$(\lambda x z .x)\ y$$

ПослС подстановки Π±ΡƒΠ΄Π΅Ρ‚ совсСм Π΄Ρ€ΡƒΠ³ΠΈΠΌ. Но ΠΌΡ‹ всСго лишь ΠΈΠ·ΠΌΠ΅Π½ΠΈΠ»ΠΈ ΠΎΠ±ΠΎΠ·Π½Π°Ρ‡Π΅Π½ΠΈΠ΅ локальной ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½ΠΎΠΉ $y$ Π½Π° $z$. И смысл измСнился, для Ρ‚ΠΎΠ³ΠΎ Ρ‡Ρ‚ΠΎΠ±Ρ‹ ΠΈΡΠΊΠ»ΡŽΡ‡ΠΈΡ‚ΡŒ Ρ‚Π°ΠΊΠΈΠ΅ случаи ΠΏΠΎΠ»ΡŒΠ·ΡƒΡŽΡ‚ΡΡ ΠΏΠ΅Ρ€Π΅ΠΈΠΌΠ΅Π½ΠΎΠ²Π°Π½ΠΈΠ΅ΠΌ ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Ρ‹Ρ… ΠΈΠ»ΠΈ $\alpha$-ΠΏΡ€Π΅ΠΎΠ±Ρ€Π°Π·ΠΎΠ²Π°Π½ΠΈΠ΅ΠΌ. Для ΠΊΠΎΡ€Ρ€Π΅ΠΊΡ‚Π½ΠΎΠΉ Ρ€Π°Π±ΠΎΡ‚Ρ‹ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΉ Π½Π΅ΠΎΠ±Ρ…ΠΎΠ΄ΠΈΠΌΠΎ ΡΠ»Π΅Π΄ΠΈΡ‚ΡŒ Π·Π° Ρ‚Π΅ΠΌ, Ρ‡Ρ‚ΠΎΠ±Ρ‹ всС ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Ρ‹Π΅, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Π΅ Π±Ρ‹Π»ΠΈ свободными Π² Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚Π΅, ΠΎΡΡ‚Π°Π»ΠΈΡΡŒ свободными ΠΈ послС подстановки.

$\beta$-рСдукция

ΠŸΡ€ΠΎΡ†Π΅ΡΡ подстановки Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚ΠΎΠ² Π² Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ называСтся $\beta$-Ρ€Π΅Π΄ΡƒΠΊΡ†ΠΈΠ΅ΠΉ. Π’ рСдСксС $(\lambda x .M) N$ вмСсто свободных Π²Ρ…ΠΎΠΆΠ΄Π΅Π½ΠΈΠΉ $x$ Π² $M$ ΠΌΡ‹ подставляСм $N$. ΠŸΠΎΡΠΌΠΎΡ‚Ρ€ΠΈΠΌ Π½Π° ΠΏΡ€Π°Π²ΠΈΠ»Π° подстановки:

$x[x=N]$ $\Rightarrow$ $N$
$y[x=N]$ $\Rightarrow$ $y$
$(PQ)[x=N]$ $\Rightarrow$ $(P[x=N]\ Q[x=N])$
$(\lambda y.P)[x = N]$ $\Rightarrow$ $(\lambda y .P[x=N]), \quad y \notin FV(N)$
$(\lambda x .P)[x = N]$ $\Rightarrow$ $(\lambda x .P)$

ΠŸΠ΅Ρ€Π²Ρ‹Π΅ Π΄Π²Π° ΠΏΡ€Π°Π²ΠΈΠ»Π° ΠΎΠΏΡ€Π΅Π΄Π΅Π»ΡΡŽΡ‚ подстановку вмСсто ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Ρ‹Ρ…. Если пСрСмСнная совпадаСт с Ρ‚ΠΎΠΉ, Π½Π° мСсто ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠΉ ΠΌΡ‹ подставляСм Ρ‚Π΅Ρ€ΠΌ $N$, Ρ‚ΠΎ ΠΌΡ‹ Π²ΠΎΠ·Π²Ρ€Π°Ρ‰Π°Π΅ΠΌ Ρ‚Π΅Ρ€ΠΌ $N$, ΠΈΠ½Π°Ρ‡Π΅ ΠΌΡ‹ Π²ΠΎΠ·Π²Ρ€Π°Ρ‰Π°Π΅ΠΌ ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½ΡƒΡŽ:

$x[x=N]$ $\Rightarrow$ $N$
$y[x=N]$ $\Rightarrow$ $y$

ΠŸΠΎΠ΄ΡΡ‚Π°Π½ΠΎΠ²ΠΊΠ° примСнСния Ρ‚Π΅Ρ€ΠΌΠΎΠ² Ρ€Π°Π²Π½Π° ΠΏΡ€ΠΈΠΌΠ΅Π½Π΅Π½ΠΈΡŽ Ρ‚Π΅Ρ€ΠΌΠΎΠ², Π² ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Ρ… ΠΏΡ€ΠΎΠΈΠ·Π²Π΅Π΄Π΅Π½Π° подстановка:

$$(PQ)[x=N] \Rightarrow (P[x=N]\ Q[x=N])$$

ΠŸΡ€ΠΈ подстановкС Π² лямбда-Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ Π½Π΅ΠΎΠ±Ρ…ΠΎΠ΄ΠΈΠΌΠΎ ΡƒΡ‡ΠΈΡ‚Ρ‹Π²Π°Ρ‚ΡŒ ΡΠ²ΡΠ·Π½ΠΎΡΡ‚ΡŒ ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Ρ‹Ρ…. Если пСрСмСнная Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚Π° отличаСтся ΠΎΡ‚ Ρ‚ΠΎΠΉ ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½ΠΎΠΉ Π½Π° мСсто ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠΉ происходит подстановка, Ρ‚ΠΎ ΠΌΡ‹ замСняСм Π² Ρ‚Π΅Π»Π΅ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ всС вхоТдСния этой ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½ΠΎΠΉ Π½Π° $N$:

$$(\lambda y .P)[x = N] \Rightarrow (\lambda y .P[x=N]), \quad y \notin FV(N)$$

УсловиС $y \notin FV(N)$ ΠΎΠ·Π½Π°Ρ‡Π°Π΅Ρ‚, Ρ‡Ρ‚ΠΎ Π½Π΅ΠΎΠ±Ρ…ΠΎΠ΄ΠΈΠΌΠΎ ΡΠ»Π΅Π΄ΠΈΡ‚ΡŒ Π·Π° Ρ‚Π΅ΠΌ, Ρ‡Ρ‚ΠΎΠ±Ρ‹ Π² $N$ Π½Π΅ оказалось свободной ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½ΠΎΠΉ с ΠΈΠΌΠ΅Π½Π΅ΠΌ $y$, ΠΈΠ½Π°Ρ‡Π΅ послС подстановки ΠΎΠ½Π° окаТСтся связанной. Если такая пСрСмСнная Π² $N$ всё-Ρ‚Π°ΠΊΠΈ окаТСтся ΠΌΡ‹ ΠΏΡ€ΠΎΠ²Π΅Π΄Ρ‘ΠΌ $\alpha$-ΠΏΡ€Π΅ΠΎΠ±Ρ€Π°Π·ΠΎΠ²Π°Π½ΠΈΠ΅ Π² Ρ‚Π΅Ρ€ΠΌΠ΅ $\lambda y .M$ ΠΈ Π·Π°ΠΌΠ΅Π½ΠΈΠΌ $y$ Π½Π° ΠΊΠ°ΠΊΡƒΡŽ-Π½ΠΈΠ±ΡƒΠ΄ΡŒ Π΄Ρ€ΡƒΠ³ΡƒΡŽ ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½ΡƒΡŽ.

Π’ послСднСм ΠΏΡ€Π°Π²ΠΈΠ»Π΅ ΠΌΡ‹ Π½ΠΈΡ‡Π΅Π³ΠΎ Π½Π΅ мСняСм, ΠΏΠΎΡΠΊΠΎΠ»ΡŒΠΊΡƒ пСрСмСнная $x$ оказываСтся связанной. А ΠΌΡ‹ ΠΏΡ€ΠΎΠ²ΠΎΠ΄ΠΈΠΌ подстановку Ρ‚ΠΎΠ»ΡŒΠΊΠΎ вмСсто свободных ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Ρ‹Ρ…:

$$(\lambda x .P)[x = N] \Rightarrow(\lambda x .P)$$

ΠžΡ‚ΠΌΠ΅Ρ‚ΠΈΠΌ, Ρ‡Ρ‚ΠΎ Π½Π΅ любой Ρ‚Π΅Ρ€ΠΌ ΠΌΠΎΠΆΠ½ΠΎ Π²Ρ‹Ρ‡ΠΈΡΠ»ΠΈΡ‚ΡŒ, Π½Π°ΠΏΡ€ΠΈΠΌΠ΅Ρ€ Ρƒ Ρ‚Π°ΠΊΠΎΠ³ΠΎ Ρ‚Π΅Ρ€ΠΌΠ° Π½Π΅Ρ‚ Π½ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½ΠΎΠΉ Ρ„ΠΎΡ€ΠΌΡ‹:

$$(\lambda x .x x)(\lambda x .x x)$$

На ΠΊΠ°ΠΆΠ΄ΠΎΠΌ шагС Ρ€Π΅Π΄ΡƒΠΊΡ†ΠΈΠΈ ΠΌΡ‹ Π±ΡƒΠ΄Π΅ΠΌ вновь ΠΈ вновь Π²ΠΎΠ·Π²Ρ€Π°Ρ‰Π°Ρ‚ΡŒΡΡ ΠΊ исходному Ρ‚Π΅Ρ€ΠΌΡƒ.

Π‘Ρ‚Ρ€Π°Ρ‚Π΅Π³ΠΈΠΈ Ρ€Π΅Π΄ΡƒΠΊΡ†ΠΈΠΈ

Π’ Π³Π»Π°Π²Π΅ ΠΎ Π»Π΅Π½ΠΈΠ²Ρ‹Ρ… вычислСниях Π½Π°ΠΌ Π²ΡΡ‚Ρ€Π΅Ρ‚ΠΈΠ»ΠΈΡΡŒ Π΄Π²Π΅ стратСгии вычислСния Π²Ρ‹Ρ€Π°ΠΆΠ΅Π½ΠΈΠΉ. Π­Ρ‚ΠΎ вычислСниС ΠΏΠΎ ΠΈΠΌΠ΅Π½ΠΈ ΠΈ вычислСниС ΠΏΠΎ Π·Π½Π°Ρ‡Π΅Π½ΠΈΡŽ. Π’Π°ΠΊΠΆΠ΅ Ρ‚Π°ΠΌ ΠΌΡ‹ ΡƒΠ·Π½Π°Π»ΠΈ ΠΎ Ρ‚ΠΎΠΌ, Ρ‡Ρ‚ΠΎ Π»Π΅Π½ΠΈΠ²Ρ‹Π΅ вычислСния это ΡƒΠ»ΡƒΡ‡ΡˆΠ΅Π½Π½Π°Ρ вСрсия вычислСния ΠΏΠΎ ΠΈΠΌΠ΅Π½ΠΈ, Π² ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠΉ Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚Ρ‹ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΉ Π²Ρ‹Ρ‡ΠΈΡΠ»ΡΡŽΡ‚ΡΡ Π½Π΅ Π±ΠΎΠ»Π΅Π΅ ΠΎΠ΄Π½ΠΎΠ³ΠΎ Ρ€Π°Π·Π°.

Π­Ρ‚ΠΈ стратСгии вычислСния ΠΏΡ€ΠΈΡˆΠ»ΠΈ ΠΈΠ· лямбда-исчислСния. Если Π½Π°ΠΌ Π½ΡƒΠΆΠ½ΠΎ ΠΈΠ·Π±Π°Π²ΠΈΡ‚ΡŒΡΡ ΠΎΡ‚ всСх рСдСксов Π² Π²Ρ‹Ρ€Π°ΠΆΠ΅Π½ΠΈΠΈ, Ρ‚ΠΎ с ΠΊΠ°ΠΊΠΎΠ³ΠΎ рСдСкса Π»ΡƒΡ‡ΡˆΠ΅ Π½Π°Ρ‡Π°Ρ‚ΡŒ? Π’ вычислСнии ΠΏΠΎ Π·Π½Π°Ρ‡Π΅Π½ΠΈΡŽ (аппликативная стратСгия) ΠΌΡ‹ Π½Π°Ρ‡ΠΈΠ½Π°Π΅ΠΌ с самого Π»Π΅Π²ΠΎΠ³ΠΎ рСдСкса, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹ΠΉ Π½Π΅ содСрТит Π΄Ρ€ΡƒΠ³ΠΈΡ… рСдСксов, Ρ‚ΠΎ Π΅ΡΡ‚ΡŒ с самого малСнького подвыраТСния. А Π² вычислСнии ΠΏΠΎ ΠΈΠΌΠ΅Π½ΠΈ (Π½ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½Π°Ρ стратСгия) ΠΌΡ‹ Π½Π°Ρ‡ΠΈΠ½Π°Π΅ΠΌ с самого Π»Π΅Π²ΠΎΠ³ΠΎ внСшнСго рСдСкса. Π›Π΅Π²Ρ‹ΠΉ рСдСкс ΠΎΠ·Π½Π°Ρ‡Π°Π΅Ρ‚, Ρ‡Ρ‚ΠΎ Π² записи выраТСния ΠΎΠ½ находится Π±Π»ΠΈΠΆΠ΅ всСх ΠΊ Π½Π°Ρ‡Π°Π»Ρƒ выраТСния.

Π’Π΅ΠΎΡ€Π΅ΠΌΠ° (ΠšΠ°Ρ€Ρ€ΠΈ)
Если Ρƒ Ρ‚Π΅Ρ€ΠΌΠ° Π΅ΡΡ‚ΡŒ Π½ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½Π°Ρ Ρ„ΠΎΡ€ΠΌΠ°, Ρ‚ΠΎ ΠΏΠΎΡΠ»Π΅Π΄ΠΎΠ²Π°Ρ‚Π΅Π»ΡŒΠ½ΠΎΠ΅ сокращСниС самого Π»Π΅Π²ΠΎΠ³ΠΎ внСшнСго рСдСкса ΠΏΡ€ΠΈΠ²ΠΎΠ΄ΠΈΡ‚ ΠΊ Π½Π΅ΠΉ.

Π­Ρ‚Π° Ρ‚Π΅ΠΎΡ€Π΅ΠΌΠ° Π³ΠΎΠ²ΠΎΡ€ΠΈΡ‚ ΠΎ Ρ‚ΠΎΠΌ, Ρ‡Ρ‚ΠΎ стратСгия вычислСния ΠΏΠΎ ΠΈΠΌΠ΅Π½ΠΈ ΠΌΠΎΠΆΠ΅Ρ‚ Π²Ρ‹Ρ‡ΠΈΡΠ»ΠΈΡ‚ΡŒ всС Ρ‚Π΅Ρ€ΠΌΡ‹, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Π΅ ΠΈΠΌΠ΅ΡŽΡ‚ Π½ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½ΡƒΡŽ Ρ„ΠΎΡ€ΠΌΡƒ. Π’ Ρ‚ΠΎΠΌ, Ρ‡Ρ‚ΠΎ вычислСниС ΠΏΠΎ Π·Π½Π°Ρ‡Π΅Π½ΠΈΡŽ ΠΌΠΎΠΆΠ΅Ρ‚ Π½Π΅ ΡΠΏΡ€Π°Π²ΠΈΡ‚ΡŒΡΡ с Π½Π΅ΠΊΠΎΡ‚ΠΎΡ€Ρ‹ΠΌΠΈ Ρ‚Π°ΠΊΠΈΠΌΠΈ Ρ‚Π΅Ρ€ΠΌΠ°ΠΌΠΈ ΠΌΡ‹ ΠΌΠΎΠΆΠ΅ΠΌ Π½Π° ΡΠ»Π΅Π΄ΡƒΡŽΡ‰Π΅ΠΌ ΠΏΡ€ΠΈΠΌΠ΅Ρ€Π΅:

$$(\lambda x y .x)\ z\ ((\lambda x .xx) (\lambda x .xx))$$

Π­Ρ‚ΠΎΡ‚ Ρ‚Π΅Ρ€ΠΌ ΠΈΠΌΠ΅Π΅Ρ‚ Π½ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½ΡƒΡŽ Ρ„ΠΎΡ€ΠΌΡƒ $z$ нСсмотря Π½Π° Ρ‚ΠΎ, Ρ‡Ρ‚ΠΎ ΠΌΡ‹ ΠΏΠ΅Ρ€Π΅Π΄Π°Ρ‘ΠΌ Π²Ρ‚ΠΎΡ€Ρ‹ΠΌ Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚ΠΎΠΌ Π² ΠΊΠΎΠ½ΡΡ‚Π°Π½Ρ‚Π½ΡƒΡŽ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΡŽ Ρ‚Π΅Ρ€ΠΌ, Ρƒ ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠ³ΠΎ Π½Π΅Ρ‚ Π½ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½ΠΎΠΉ Ρ„ΠΎΡ€ΠΌΡ‹. Алгоритм вычислСния ΠΏΠΎ Π·Π½Π°Ρ‡Π΅Π½ΠΈΡŽ зависнСт ΠΏΡ€ΠΈ вычислСнии Π²Ρ‚ΠΎΡ€ΠΎΠ³ΠΎ Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚Π°. Π’ Ρ‚ΠΎ врСмя ΠΊΠ°ΠΊ Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌ вычислСния ΠΏΠΎ ΠΈΠΌΠ΅Π½ΠΈ Π½Π°Ρ‡Π½Ρ‘Ρ‚ с самого внСшнСго Ρ‚Π΅Ρ€ΠΌΠ° ΠΈ Ρ‚Π°ΠΌ ΠΎΠΏΡ€Π΅Π΄Π΅Π»ΠΈΡ‚, Ρ‡Ρ‚ΠΎ Π²Ρ‚ΠΎΡ€ΠΎΠΉ Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚ Π½Π΅ Π½ΡƒΠΆΠ΅Π½.

Π•Ρ‰Ρ‘ ΠΎΠ΄ΠΈΠ½ Π²Π°ΠΆΠ½Ρ‹ΠΉ Ρ€Π΅Π·ΡƒΠ»ΡŒΡ‚Π°Ρ‚ Π² лямбда-исчислСнии Π±Ρ‹Π» сформулирован Π² ΡΠ»Π΅Π΄ΡƒΡŽΡ‰Π΅ΠΉ Ρ‚Π΅ΠΎΡ€Π΅ΠΌΠ΅:

Π’Π΅ΠΎΡ€Π΅ΠΌΠ° (Π§Ρ‘Ρ€Ρ‡Π°-РоссСра)
Если Ρ‚Π΅Ρ€ΠΌ $X$ рСдуцируСтся ΠΊ Ρ‚Π΅Ρ€ΠΌΠ°ΠΌ $Y_1$ ΠΈ $Y_2$, Ρ‚ΠΎ сущСствуСт Ρ‚Π΅Ρ€ΠΌ $L$, ΠΊ ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠΌΡƒ Ρ€Π΅Π΄ΡƒΡ†ΠΈΡ€ΡƒΡŽΡ‚ΡΡ ΠΈ Ρ‚Π΅Ρ€ΠΌ $Y_1$ ΠΈ Ρ‚Π΅Ρ€ΠΌ $Y_2$.

Π­Ρ‚Π° Ρ‚Π΅ΠΎΡ€Π΅ΠΌΠ° Π³ΠΎΠ²ΠΎΡ€ΠΈΡ‚ ΠΎ Ρ‚ΠΎΠΌ, Ρ‡Ρ‚ΠΎ Ρƒ Ρ‚Π΅Ρ€ΠΌΠ° ΠΌΠΎΠΆΠ΅Ρ‚ Π±Ρ‹Ρ‚ΡŒ Ρ‚ΠΎΠ»ΡŒΠΊΠΎ ΠΎΠ΄Π½Π° Π½ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½Π°Ρ Ρ„ΠΎΡ€ΠΌΠ°. ΠŸΠΎΡΠΊΠΎΠ»ΡŒΠΊΡƒ Ссли Π±Ρ‹ ΠΈΡ… Π±Ρ‹Π»ΠΎ Π΄Π²Π΅, Ρ‚ΠΎ сущСствовал Ρ‚Ρ€Π΅Ρ‚ΠΈΠΉ Ρ‚Π΅Ρ€ΠΌ, ΠΊ ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠΌΡƒ ΠΌΠΎΠΆΠ½ΠΎ Π±Ρ‹Π»ΠΎ Π±Ρ‹ Ρ€Π΅Π΄ΡƒΡ†ΠΈΡ€ΠΎΠ²Π°Ρ‚ΡŒ эти Π½ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½Ρ‹Π΅ Ρ„ΠΎΡ€ΠΌΡ‹. Но ΠΏΠΎ ΠΎΠΏΡ€Π΅Π΄Π΅Π»Π΅Π½ΠΈΡŽ Π½ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½ΠΎΠΉ Ρ„ΠΎΡ€ΠΌΡ‹, ΠΌΡ‹ Π½Π΅ ΠΌΠΎΠΆΠ΅ΠΌ Π΅Ρ‘ Ρ€Π΅Π΄ΡƒΡ†ΠΈΡ€ΠΎΠ²Π°Ρ‚ΡŒ. Из этого слСдуСт, Ρ‡Ρ‚ΠΎ Π½ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½Ρ‹Π΅ Ρ„ΠΎΡ€ΠΌΡ‹ Π΄ΠΎΠ»ΠΆΠ½Ρ‹ ΡΠΎΠ²ΠΏΠ°Π΄Π°Ρ‚ΡŒ.

Π’Π΅ΠΎΡ€Π΅ΠΌΠ° Π§Ρ‘Ρ€Ρ‡Π°-РоссСра ΡƒΠΊΠ°Π·Ρ‹Π²Π°Π΅Ρ‚ Π½Π° способ сравнСния Ρ‚Π΅Ρ€ΠΌΠΎΠ². Для Ρ‚ΠΎΠ³ΠΎ Ρ‡Ρ‚ΠΎΠ±Ρ‹ ΠΏΠΎΠ½ΡΡ‚ΡŒ Ρ€Π°Π²Π½Ρ‹ Ρ‚Π΅Ρ€ΠΌΡ‹ ΠΈΠ»ΠΈ Π½Π΅Ρ‚, Π½Π΅ΠΎΠ±Ρ…ΠΎΠ΄ΠΈΠΌΠΎ привСсти ΠΈΡ… ΠΊ Π½ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½ΠΎΠΉ Ρ„ΠΎΡ€ΠΌΠ΅ ΠΈ ΡΡ€Π°Π²Π½ΠΈΡ‚ΡŒ. Если Ρ‚Π΅Ρ€ΠΌΡ‹ ΡΠΎΠ²ΠΏΠ°Π΄Π°ΡŽΡ‚ Π² Π½ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½ΠΎΠΉ Ρ„ΠΎΡ€ΠΌΠ΅, Π·Π½Π°Ρ‡ΠΈΡ‚ ΠΎΠ½ΠΈ Ρ€Π°Π²Π½Ρ‹.

РСкурсия. ΠšΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€ Π½Π΅ΠΏΠΎΠ΄Π²ΠΈΠΆΠ½ΠΎΠΉ Ρ‚ΠΎΡ‡ΠΊΠΈ

Π’ лямбда-исчислСнии всС Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ ΡΠ²Π»ΡΡŽΡ‚ΡΡ бСзымянными. Π­Ρ‚ΠΎ ΠΎΠ·Π½Π°Ρ‡Π°Π΅Ρ‚, Ρ‡Ρ‚ΠΎ ΠΌΡ‹ Π½Π΅ ΠΌΠΎΠΆΠ΅ΠΌ Π² Ρ‚Π΅Π»Π΅ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ Π²Ρ‹Π·Π²Π°Ρ‚ΡŒ саму Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ, вСдь ΠΌΡ‹ Π½Π΅ ΠΌΠΎΠΆΠ΅ΠΌ Π½Π° Π½Π΅Ρ‘ ΡΠΎΡΠ»Π°Ρ‚ΡŒΡΡ, каТСтся, Ρ‡Ρ‚ΠΎ Ρƒ нас Π½Π΅Ρ‚ возмоТности ΡΡ‚Ρ€ΠΎΠΈΡ‚ΡŒ рСкурсивныС Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ. Однако это Π½Π΅ Ρ‚Π°ΠΊ. Нам Π½Π° ΠΏΠΎΠΌΠΎΡ‰ΡŒ ΠΏΡ€ΠΈΠ΄Ρ‘Ρ‚ ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€ Π½Π΅ΠΏΠΎΠ΄Π²ΠΈΠΆΠ½ΠΎΠΉ Ρ‚ΠΎΡ‡ΠΊΠΈ. По ΠΎΠΏΡ€Π΅Π΄Π΅Π»Π΅Π½ΠΈΡŽ ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€ Π½Π΅ΠΏΠΎΠ΄Π²ΠΈΠΆΠ½ΠΎΠΉ Ρ‚ΠΎΡ‡ΠΊΠΈ Ρ€Π΅ΡˆΠ°Π΅Ρ‚ Π·Π°Π΄Π°Ρ‡Ρƒ: для Ρ‚Π΅Ρ€ΠΌΠ° $F$ Π½Π°ΠΉΡ‚ΠΈ Ρ‚Π΅Ρ€ΠΌ $X$ Ρ‚Π°ΠΊΠΎΠΉ, Ρ‡Ρ‚ΠΎ

$$F X = X$$

БущСствуСт ΠΌΠ½ΠΎΠ³ΠΎ ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€ΠΎΠ² Π½Π΅ΠΏΠΎΠ΄Π²ΠΈΠΆΠ½ΠΎΠΉ Ρ‚ΠΎΡ‡ΠΊΠΈ. Рассмотрим $Y$-ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€:

$$Y\ =\ \lambda f .(\lambda x .f(xx)) (\lambda x .f(xx))$$

УбСдимся Π² Ρ‚ΠΎΠΌ, Ρ‡Ρ‚ΠΎ для любого Ρ‚Π΅Ρ€ΠΌΠ° $F$, Π²Ρ‹ΠΏΠΎΠ»Π½Π΅Π½ΠΎ тоТдСство: $F(YF) = YF$:

$$YF = (\lambda x .F(xx)) (\lambda x .F(xx)) = F (\lambda x .F(xx)) (\lambda x .F(xx)) = F(YF)$$

Π’Π°ΠΊ с ΠΏΠΎΠΌΠΎΡ‰ΡŒΡŽ $Y$-ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€Π° ΠΌΠΎΠΆΠ½ΠΎ ΡΠΎΡΡ‚Π°Π²Π»ΡΡ‚ΡŒ рСкурсивныС Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ.

ΠšΠΎΠ΄ΠΈΡ€ΠΎΠ²Π°Π½ΠΈΠ΅ структур Π΄Π°Π½Π½Ρ‹Ρ…

Π’Ρ‹ Π½Π°Π²Π΅Ρ€Π½ΠΎΠ΅ Π·Π°ΠΌΠ΅Ρ‚ΠΈΠ»ΠΈ, Ρ‡Ρ‚ΠΎ ΠΏΠΎΠΊΠ° ΠΌΡ‹ составляли лишь ΠΎΠ±ΠΎΠ±Ρ‰Ρ‘Π½Π½Ρ‹Π΅ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ. Π­Ρ‚ΠΈ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ ΠΊΠΎΠΌΠ±ΠΈΠ½ΠΈΡ€ΡƒΡŽΡ‚ Π΄Ρ€ΡƒΠ³ΠΈΠ΅ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ, ΠΎΠ½ΠΈ Π½Π΅ Π²Ρ‹ΠΏΠΎΠ»Π½ΡΡŽΡ‚ Π½ΠΈΠΊΠ°ΠΊΠΈΡ… дСйствий Π½Π°Π΄ элСмСнтами. Π§Ρ‚ΠΎ Ссли Π½Π°ΠΌ захочСтся Π²Ρ‹Ρ‡ΠΈΡΠ»ΡΡ‚ΡŒ логичСскиС значСния ΠΈΠ»ΠΈ Π²ΠΎΡΠΏΠΎΠ»ΡŒΠ·ΠΎΠ²Π°Ρ‚ΡŒΡΡ числами?

ΠžΠΊΠ°Π·Ρ‹Π²Π°Π΅Ρ‚ΡΡ, Ρ‡Ρ‚ΠΎ логичСскиС значСния, числа, ΠΏΠ°Ρ€Ρ‹, списки ΠΈ Π΄Ρ€ΡƒΠ³ΠΈΠ΅ конструкции ΠΌΠΎΠ³ΡƒΡ‚ Π±Ρ‹Ρ‚ΡŒ Π·Π°ΠΊΠΎΠ΄ΠΈΡ€ΠΎΠ²Π°Π½Ρ‹ с ΠΏΠΎΠΌΠΎΡ‰ΡŒΡŽ Ρ‚Π΅Ρ€ΠΌΠΎΠ² лямбда-исчислСния. ВСзис Π§Ρ‘Ρ€Ρ‡Π° ΡƒΡ‚Π²Π΅Ρ€ΠΆΠ΄Π°Π΅Ρ‚, Ρ‡Ρ‚ΠΎ с ΠΏΠΎΠΌΠΎΡ‰ΡŒΡŽ лямбда-Ρ‚Π΅Ρ€ΠΌΠ° ΠΌΠΎΠΆΠ½ΠΎ ΠΏΡ€Π΅Π΄ΡΡ‚Π°Π²ΠΈΡ‚ΡŒ Π»ΡŽΠ±ΡƒΡŽ Π²Ρ‹Ρ‡ΠΈΡΠ»ΠΈΠΌΡƒΡŽ Ρ‡ΠΈΡΠ»ΠΎΠ²ΡƒΡŽ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΡŽ. Π’ 1936 Π³ΠΎΠ΄Ρƒ Π§Ρ‘Ρ€Ρ‡ с ΠΏΠΎΠΌΠΎΡ‰ΡŒΡŽ лямбда-исчислСния Π΄ΠΎΠΊΠ°Π·Π°Π» сущСствованиС Π½Π΅Ρ€Π°Π·Ρ€Π΅ΡˆΠΈΠΌΡ‹Ρ… ΠΏΡ€ΠΎΠ±Π»Π΅ΠΌ Π² Ρ‚Π΅ΠΎΡ€ΠΈΠΈ чисСл. Из этого слСдовала Π½Π΅Ρ€Π°Π·Ρ€Π΅ΡˆΠΈΠΌΠΎΡΡ‚ΡŒ Π°Ρ€ΠΈΡ„ΠΌΠ΅Ρ‚ΠΈΠΊΠΈ ΠΈ Π½Π΅Ρ€Π°Π·Ρ€Π΅ΡˆΠΈΠΌΠΎΡΡ‚ΡŒ исчислСния Π»ΠΎΠ³ΠΈΠΊΠΈ ΠΏΡ€Π΅Π΄ΠΈΠΊΠ°Ρ‚ΠΎΠ² ΠΏΠ΅Ρ€Π²ΠΎΠ³ΠΎ порядка. БистСма аксиом называСтся Ρ€Π°Π·Ρ€Π΅ΡˆΠΈΠΌΠΎΠΉ Π² Ρ‚ΠΎΠΌ случаС, Ссли сущСствуСт Ρ‚Π°ΠΊΠΎΠΉ Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌ, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹ΠΉ позволяСт ΠΏΠΎ Π²ΠΈΠ΄Ρƒ Ρ„ΠΎΡ€ΠΌΡƒΠ»Ρ‹ ΠΎΠΏΡ€Π΅Π΄Π΅Π»ΠΈΡ‚ΡŒ слСдуСт Π»ΠΈ ΠΎΠ½Π° ΠΈΠ· Π·Π°Π΄Π°Π½Π½Ρ‹Ρ… аксиом ΠΈΠ»ΠΈ Π½Π΅Ρ‚.

ΠŸΠΎΡΠΌΠΎΡ‚Ρ€ΠΈΠΌ ΠΊΠ°ΠΊ с ΠΏΠΎΠΌΠΎΡ‰ΡŒΡŽ Ρ‚Π΅Ρ€ΠΌΠΎΠ² ΠΊΠΎΠ΄ΠΈΡ€ΡƒΡŽΡ‚ΡΡ структуры Π΄Π°Π½Π½Ρ‹Ρ…. Π”Π°Π»Π΅Π΅ для сокращСния записи ΠΌΡ‹ Π±ΡƒΠ΄Π΅ΠΌ ΡΡ‡ΠΈΡ‚Π°Ρ‚ΡŒ, Ρ‡Ρ‚ΠΎ Π² лямбда исчислСнии ΠΌΠΎΠΆΠ½ΠΎ ΠΎΠΏΡ€Π΅Π΄Π΅Π»ΡΡ‚ΡŒ синонимы с ΠΏΠΎΠΌΠΎΡ‰ΡŒΡŽ Π·Π½Π°ΠΊΠ° Ρ€Π°Π²Π½ΠΎ. Π—Π°ΠΏΠΈΡΡŒ $N = M$ Π³ΠΎΠ²ΠΎΡ€ΠΈΡ‚ ΠΎ Ρ‚ΠΎΠΌ, Ρ‡Ρ‚ΠΎ ΠΌΡ‹ Π΄Π°Π»ΠΈ ΠΎΠ±ΠΎΠ·Π½Π°Ρ‡Π΅Π½ΠΈΠ΅ $N$ Ρ‚Π΅Ρ€ΠΌΡƒ $M$. Π­Ρ‚ΠΎΠΉ ΠΎΠΏΠ΅Ρ€Π°Ρ†ΠΈΠΈ Π½Π΅Ρ‚ Π² лямбда-исчислСнии, Π½ΠΎ ΠΌΡ‹ Π±ΡƒΠ΄Π΅ΠΌ ΠΏΠΎΠ»ΡŒΠ·ΠΎΠ²Π°Ρ‚ΡŒΡΡ Сю для удобства.

ЛогичСскиС значСния

Π‘ΡƒΡ‚ΡŒ логичСских Π·Π½Π°Ρ‡Π΅Π½ΠΈΠΉ Π·Π°ΠΊΠ»ΡŽΡ‡Π°Π΅Ρ‚ΡΡ Π² ΠΎΠΏΠ΅Ρ€Π°Ρ‚ΠΎΡ€Π΅ $If$, с ΠΏΠΎΠΌΠΎΡ‰ΡŒΡŽ ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠ³ΠΎ ΠΌΡ‹ ΠΌΠΎΠΆΠ΅ΠΌ ΠΎΡ€Π³Π°Π½ΠΈΠ·ΠΎΠ²Ρ‹Π²Π°Ρ‚ΡŒ Π²Π΅Ρ‚Π²Π»Π΅Π½ΠΈΠ΅ Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌΠ°. Π•ΡΡ‚ΡŒ Π΄Π²Π° Ρ‚Π΅Ρ€ΠΌΠ° $True$ ΠΈ $False$, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Π΅ для Π»ΡŽΠ±Ρ‹Ρ… Ρ‚Π΅Ρ€ΠΌΠΎΠ² $a$ ΠΈ $b$, ΠΎΠ±Π»Π°Π΄Π°ΡŽΡ‚ свойствами:

$If\ True\ a\ b$ $=$ $a$
$If\ False\ a\ b$ $=$ $b$

Π’Π΅Ρ€ΠΌΡ‹ $True$, $False$ ΠΈ $If$, ΡƒΠ΄ΠΎΠ²Π»Π΅Ρ‚Π²ΠΎΡ€ΡΡŽΡ‰ΠΈΠ΅ Ρ‚Π°ΠΊΠΈΠΌ свойствам выглядят Ρ‚Π°ΠΊ:

$True$ $=$ $\lambda t\ f .t$
$False$ $=$ $\lambda t\ f .f$
$If$ $=$ $\lambda b\ x\ y .b x y$

ΠŸΡ€ΠΎΠ²Π΅Ρ€ΠΈΠΌ Π²Ρ‹ΠΏΠΎΠ»Π½Π΅Π½ΠΈΠ΅ свойств:

$$If\ True\ a\ b \Rightarrow(\lambda b \ x \ y .b x y) (\lambda t\ f .t)\ a\ b \Rightarrow(\lambda t\ f .t)\ a\ b \Rightarrowa$$

$$If\ False\ a\ b \Rightarrow(\lambda b \ x \ y .b x y) (\lambda t\ f .f)\ a\ b \Rightarrow(\lambda t\ f .f)\ a\ b \Rightarrowb$$

Бвойства Π²Ρ‹ΠΏΠΎΠ»Π½Π΅Π½Ρ‹. ЛогичСскиС константы ΠΊΠΎΠ΄ΠΈΡ€ΡƒΡŽΡ‚ΡΡ постоянными функциями Π΄Π²ΡƒΡ… Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚ΠΎΠ². Ѐункция True Π²ΠΎΠ·Π²Ρ€Π°Ρ‰Π°Π΅Ρ‚ ΠΏΠ΅Ρ€Π²Ρ‹ΠΉ Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚, игнорируя Π²Ρ‚ΠΎΡ€ΠΎΠΉ. А функция False Π΄Π΅Π»Π°Π΅Ρ‚ Ρ‚ΠΎ ΠΆΠ΅ самоС, Π½ΠΎ Π½Π°ΠΎΠ±ΠΎΡ€ΠΎΡ‚. Π’ Ρ‚Π°ΠΊΠΎΠΉ ΠΈΠ½Ρ‚Π΅Ρ€ΠΏΡ€Π΅Ρ‚Π°Ρ†ΠΈΠΈ логичСскоС ΠΎΡ‚Ρ€ΠΈΡ†Π°Π½ΠΈΠ΅ ΠΌΠΎΠΆΠ½ΠΎ Π·Π°ΠΊΠΎΠ΄ΠΈΡ€ΠΎΠ²Π°Ρ‚ΡŒ с ΠΏΠΎΠΌΠΎΡ‰ΡŒΡŽ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ flip. Π’Π°ΠΊΠΆΠ΅ ΠΌΡ‹ ΠΌΠΎΠΆΠ΅ΠΌ Π²Ρ‹Ρ€Π°Π·ΠΈΡ‚ΡŒ ΠΈ Π΄Ρ€ΡƒΠ³ΠΈΠ΅ логичСскиС ΠΎΠΏΠ΅Ρ€Π°Ρ†ΠΈΠΈ:

$And$ $=$ $\lambda a\ b .a\ b\ False$
$Or$ $=$ $\lambda a\ b .a\ True\ b$

ΠœΡ‹ ΠΎΠΏΡ€Π΅Π΄Π΅Π»ΠΈΠ»ΠΈ логичСскиС значСния Π½Π΅ ΠΊΠΎΠ½ΠΊΡ€Π΅Ρ‚Π½Ρ‹ΠΌΠΈ значСниями, Π° свойствами Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΉ. ΠœΡ‹ построили Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Π΅ Π²Π΅Π΄ΡƒΡ‚ сСбя ΠΊΠ°ΠΊ логичСскиС значСния. Π­Ρ‚ΠΎΡ‚ способ опрСдСлСния Π½Π°ΠΏΠΎΠΌΠΈΠ½Π°Π΅Ρ‚, ΠΎΠΏΡ€Π΅Π΄Π΅Π»Π΅Π½ΠΈΠ΅ класса Ρ‚ΠΈΠΏΠΎΠ². ΠœΡ‹ объявили Ρ‚Ρ€ΠΈ ΠΌΠ΅Ρ‚ΠΎΠ΄Π° $True$, $False$ ΠΈ $If$ ΠΈ сказали, Ρ‡Ρ‚ΠΎ экзСмпляр класса Π΄ΠΎΠ»ΠΆΠ΅Π½ ΡƒΠ΄ΠΎΠ²Π»Π΅Ρ‚Π²ΠΎΡ€ΡΡ‚ΡŒ ΠΎΠΏΡ€Π΅Π΄Π΅Π»Ρ‘Π½Π½Ρ‹ΠΌ свойствам, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Π΅ Π½Π°ΠΊΠ»Π°Π΄Ρ‹Π²Π°ΡŽΡ‚ Π²Π·Π°ΠΈΠΌΠ½Ρ‹Π΅ ограничСния Π½Π° ΠΌΠ΅Ρ‚ΠΎΠ΄Ρ‹ класса. Ни ΠΎΠ΄ΠΈΠ½ ΠΈΠ· ΠΌΠ΅Ρ‚ΠΎΠ΄ΠΎΠ² Π½Π΅ ΠΈΠΌΠ΅Π΅Ρ‚ смысла ΠΏΠΎ ΠΎΡ‚Π΄Π΅Π»ΡŒΠ½ΠΎΡΡ‚ΠΈ, Π²Π°ΠΆΠ½ΠΎ Ρ‚ΠΎ ΠΊΠ°ΠΊ ΠΎΠ½ΠΈ Π²Π·Π°ΠΈΠΌΠΎΠ΄Π΅ΠΉΡΡ‚Π²ΡƒΡŽΡ‚.

ΠΠ°Ρ‚ΡƒΡ€Π°Π»ΡŒΠ½Ρ‹Π΅ числа

ΠžΠΊΠ°Π·Ρ‹Π²Π°Π΅Ρ‚ΡΡ, Ρ‡Ρ‚ΠΎ с ΠΏΠΎΠΌΠΎΡ‰ΡŒΡŽ Ρ‚Π΅Ρ€ΠΌΠΎΠ² лямбда исчислСния ΠΌΠΎΠΆΠ½ΠΎ Π·Π°ΠΊΠΎΠ΄ΠΈΡ€ΠΎΠ²Π°Ρ‚ΡŒ ΠΈ Π½Π°Ρ‚ΡƒΡ€Π°Π»ΡŒΠ½Ρ‹Π΅ числа с арифмСтичСскими опСрациями. ΠœΡ‹ Π±ΡƒΠ΄Π΅ΠΌ ΠΊΠΎΠ΄ΠΈΡ€ΠΎΠ²Π°Ρ‚ΡŒ числа ПСано. Для этого Π½Π°ΠΌ понадобится Π½ΡƒΠ»Π΅Π²ΠΎΠΉ элСмСнт ΠΈ функция опрСдСлСния ΡΠ»Π΅Π΄ΡƒΡŽΡ‰Π΅Π³ΠΎ элСмСнта. Π˜Ρ… ΠΌΠΎΠΆΠ½ΠΎ Π·Π°ΠΊΠΎΠ΄ΠΈΡ€ΠΎΠ²Π°Ρ‚ΡŒ Ρ‚Π°ΠΊ:

$Zero$ $=$ $\lambda sz .z$
$Succ$ $=$ $\lambda nsz .s(nsz)$

Как ΠΈ Π² случаС логичСских Π·Π½Π°Ρ‡Π΅Π½ΠΈΠΉ числа ΠΊΠΎΠ΄ΠΈΡ€ΡƒΡŽΡ‚ΡΡ функциями Π΄Π²ΡƒΡ… Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚ΠΎΠ². Число опрСдСляСтся ΠΏΠΎ Ρ‚Π΅Ρ€ΠΌΡƒ, подсчётом Ρ†Π΅ΠΏΠΎΡ‡ΠΊΠΈ ΠΏΠ΅Ρ€Π²Ρ‹Ρ… Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚ΠΎΠ² $s$. НапримСр Ρ‚Π°ΠΊ выглядит число Π΄Π²Π°:

$$Succ\ (Succ\ Zero) \Rightarrow(\lambda nsz .s(nsz)) (Succ\ Zero) \Rightarrow\lambda sz .s((Succ\ Zero) sz) \Rightarrow$$

$$\lambda sz .s(((\lambda ns'z' .s'(ns'z'))\ Zero)sz) \Rightarrow\lambda sz .s((\lambda s'z' .s'(Zero\ s'z'))\ sz) \Rightarrow$$

$$\lambda sz .s((\lambda s'z' .s'z')\ sz) \Rightarrow\lambda sz .s(sz)$$

И ΠΌΡ‹ ΠΏΠΎΠ»ΡƒΡ‡ΠΈΠ»ΠΈ Π΄Π²Π° вхоТдСния ΠΏΠ΅Ρ€Π²ΠΎΠ³ΠΎ Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚Π° Π² Ρ‚Π΅Π»Π΅ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ. ΠžΠΏΡ€Π΅Π΄Π΅Π»ΠΈΠΌ слоТСниС ΠΈ ΡƒΠΌΠ½ΠΎΠΆΠ΅Π½ΠΈΠ΅. Π‘Π»ΠΎΠΆΠ΅Π½ΠΈΠ΅ ΠΏΡ€ΠΈΠ½ΠΈΠΌΠ°Π΅Ρ‚ Π΄Π²Π΅ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ Π΄Π²ΡƒΡ… Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚ΠΎΠ² ΠΈ Π²ΠΎΠ·Π²Ρ€Π°Ρ‰Π°Π΅Ρ‚ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΡŽ Π΄Π²ΡƒΡ… Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚ΠΎΠ².

$$Add = \lambda\ m\ n\ s\ z .m\ s\ (n\ s\ z)$$

Π’ этой Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ ΠΌΡ‹ примСняСм $m$ Ρ€Π°Π· Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚ $s$ ΠΊ Π·Π½Π°Ρ‡Π΅Π½ΠΈΡŽ, Π² ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠΌ Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚ $s$ ΠΏΡ€ΠΈΠΌΠ΅Π½Ρ‘Π½ $n$ Ρ€Π°Π·, Ρ‚Π°ΠΊ ΠΌΡ‹ ΠΈ ΠΏΠΎΠ»ΡƒΡ‡Π°Π΅ΠΌ $m+n$ ΠΏΡ€ΠΈΠΌΠ΅Π½Π΅Π½ΠΈΠΉ Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚Π° $s$. Π‘Π»ΠΎΠΆΠΈΠΌ 3 ΠΈ 2:

$$Add\ 3\ 2 \Rightarrow\lambda s\ z .3\ s\ (2\ s\ z) \Rightarrow\lambda s\ z .3\ s\ (s\ (s\ z)) \Rightarrow\lambda s\ z .s\ (\ s\ (s\ (s\ (s\ z)))) \Rightarrow5$$

Π’ ΡƒΠΌΠ½ΠΎΠΆΠ΅Π½ΠΈΠΈ чисСл $m$ ΠΈ $n$ ΠΌΡ‹ Π±ΡƒΠ΄Π΅ΠΌ $m$ Ρ€Π°Π· ΡΠΊΠ»Π°Π΄Ρ‹Π²Π°Ρ‚ΡŒ число $n$:

$$Mul = \lambda m\ n\ s\ z .m\ (Add\ n)\ Zero$$

ΠšΠΎΠ½ΡΡ‚Ρ€ΡƒΠΊΡ‚ΠΈΠ²Π½Π°Ρ ΠΌΠ°Ρ‚Π΅ΠΌΠ°Ρ‚ΠΈΠΊΠ°

Π’ конструктивной ΠΌΠ°Ρ‚Π΅ΠΌΠ°Ρ‚ΠΈΠΊΠ΅ сущСствованиС ΠΎΠ±ΡŠΠ΅ΠΊΡ‚Π° ΠΌΠΎΠΆΠ΅Ρ‚ Π±Ρ‹Ρ‚ΡŒ Π΄ΠΎΠΊΠ°Π·Π°Π½ΠΎ Ρ‚ΠΎΠ»ΡŒΠΊΠΎ описаниСм Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌΠ°, с ΠΏΠΎΠΌΠΎΡ‰ΡŒΡŽ ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠ³ΠΎ ΠΌΠΎΠΆΠ½ΠΎ ΠΏΠΎΡΡ‚Ρ€ΠΎΠΈΡ‚ΡŒ ΠΎΠ±ΡŠΠ΅ΠΊΡ‚. НапримСр Π΄ΠΎΠΊΠ°Π·Π°Ρ‚Π΅Π»ΡŒΡΡ‚Π²ΠΎ ΠΌΠ΅Ρ‚ΠΎΠ΄ΠΎΠΌ β€œΠΎΡ‚ противного” отвСргаСтся.

Лямбда исчислСниС строит конструктивноС описаниС Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ. По лямбда-Ρ‚Π΅Ρ€ΠΌΡƒ ΠΌΡ‹ ΠΌΠΎΠΆΠ΅ΠΌ Π½Π΅ Ρ‚ΠΎΠ»ΡŒΠΊΠΎ Π²Ρ‹Ρ‡ΠΈΡΠ»ΡΡ‚ΡŒ значСния Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ, Π½ΠΎ ΠΈ ΠΏΠΎΠ½ΡΡ‚ΡŒ ΠΊΠ°ΠΊ ΠΎΠ½Π° Π±Ρ‹Π»Π° построСна. Π’ классичСской Ρ‚Π΅ΠΎΡ€ΠΈΠΈ, функция это мноТСство ΠΏΠ°Ρ€ $(x,\ f(x))$ Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚-Π·Π½Π°Ρ‡Π΅Π½ΠΈΠ΅, ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠ΅ ΠΎΠ±Π»Π°Π΄Π°Π΅Ρ‚ свойством:

$$x = y\ \Rightarrow\ f(x) = f(y)$$

По этому ΠΎΠΏΡ€Π΅Π΄Π΅Π»Π΅Π½ΠΈΡŽ ΠΌΡ‹ Π½ΠΈΡ‡Π΅Π³ΠΎ Π½Π΅ ΠΌΠΎΠΆΠ΅ΠΌ ΡΠΊΠ°Π·Π°Ρ‚ΡŒ ΠΎ Π²Π½ΡƒΡ‚Ρ€Π΅Π½Π½Π΅ΠΉ структурС Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ. ΠœΡ‹ ΠΌΠΎΠΆΠ΅ΠΌ ΡΠΎΠ±ΠΈΡ€Π°Ρ‚ΡŒ ΠΈΠ· ΠΎΠ΄Π½ΠΈΡ… Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΉ Π΄Ρ€ΡƒΠ³ΠΈΠ΅ с ΠΏΠΎΠΌΠΎΡ‰ΡŒΡŽ подстановки Π·Π½Π°Ρ‡Π΅Π½ΠΈΠΉ, Π½ΠΎ ΠΌΡ‹ Π½ΠΈΠΊΠ°ΠΊ Π½Π΅ смоТСм ΠΏΠΎΠ½ΡΡ‚ΡŒ, Ρ‡Ρ‚ΠΎ находится Π²Π½ΡƒΡ‚Ρ€ΠΈ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ. Лямбда исчислСниС Ρ€Π΅ΡˆΠ°Π΅Ρ‚ эту ΠΏΡ€ΠΎΠ±Π»Π΅ΠΌΡƒ.

Π Π°ΡΡˆΠΈΡ€Π΅Π½ΠΈΠ΅ лямбда исчислСния

ΠŸΡ€Π΅Π΄ΠΏΠΎΠ»ΠΎΠΆΠΈΠΌ, Ρ‡Ρ‚ΠΎ ΠΌΡ‹ Ρ€Π΅ΡˆΠΈΠ»ΠΈ Π½Π°ΠΏΠΈΡΠ°Ρ‚ΡŒ язык программирования Π½Π° основС лямбда-исчислСния. Π‘Ρ‹Π»ΠΎ Π±Ρ‹ ΠΎΡ‡Π΅Π½ΡŒ нСэффСктивно ΠΏΡ€Π΅Π΄ΡΡ‚Π°Π²Π»ΡΡ‚ΡŒ числа с ΠΏΠΎΠΌΠΎΡ‰ΡŒΡŽ чисСл ПСано. Π’Π΅Π΄ΡŒ Ρƒ нас Π΅ΡΡ‚ΡŒ процСссор ΠΈ ΠΌΡ‹ ΠΌΠΎΠΆΠ΅ΠΌ ΡΠΏΡ€ΠΎΡΠΈΡ‚ΡŒ Ρƒ Π½Π΅Π³ΠΎ Ρ‡Π΅ΠΌΡƒ Ρ€Π°Π²Π½ΠΎ Π·Π½Π°Ρ‡Π΅Π½ΠΈΠ΅ ΠΈ ΠΏΠΎΠ»ΡƒΡ‡ΠΈΡ‚ΡŒ ΠΎΡ‚Π²Π΅Ρ‚ ΠΎΡ‡Π΅Π½ΡŒ быстро.

Π’ этом случаС ΠΏΠΎΠ»ΡŒΠ·ΡƒΡŽΡ‚ΡΡ Ρ€Π°ΡΡˆΠΈΡ€Π΅Π½Π½Ρ‹ΠΌ лямбда исчислСниСм. Π’ Π½Ρ‘ΠΌ Π΄Π²Π° Ρ‚ΠΈΠΏΠ° ΠΏΡ€ΠΈΠΌΠΈΡ‚ΠΈΠ²ΠΎΠ² это ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Ρ‹Π΅ ΠΈ константы. Для констант ΠΌΡ‹ ΠΌΠΎΠΆΠ΅ΠΌ ΠΎΠΏΡ€Π΅Π΄Π΅Π»ΡΡ‚ΡŒ ΡΠΏΠ΅Ρ†ΠΈΠ°Π»ΡŒΠ½Ρ‹Π΅ ΠΏΡ€Π°Π²ΠΈΠ»Π° Ρ€Π΅Π΄ΡƒΠΊΡ†ΠΈΠΈ. НапримСр ΠΌΡ‹ ΠΌΠΎΠΆΠ΅ΠΌ Π΄ΠΎΠΏΠΎΠ»Π½ΠΈΡ‚ΡŒ исчислСниС константами:

$$+,\ *,\ 0,\ 1,\ 2,\ ...$$

И ввСсти для Π½ΠΈΡ… ΠΏΡ€Π°Π²ΠΈΠ»Π° Ρ€Π΅Π΄ΡƒΠΊΡ†ΠΈΠΈ, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Π΅ Π·Π°ΠΏΡ€Π°ΡˆΠΈΠ²Π°ΡŽΡ‚ ΠΎΡ‚Π²Π΅Ρ‚ Ρƒ процСссора:

$a+b$ $=$ $AddWithCPU(a, b)$
$a*b$ $=$ $MulWithCPU(a, b)$

Π’Π°ΠΊ ΠΆΠ΅ ΠΌΡ‹ ΠΌΠΎΠΆΠ΅ΠΌ ΠΎΠΏΡ€Π΅Π΄Π΅Π»ΠΈΡ‚ΡŒ ΠΈ константы для логичСских Π·Π½Π°Ρ‡Π΅Π½ΠΈΠΉ:

$$True,\ False,\ If,\ Not,\ And,\ Or$$

И ΠΎΠΏΡ€Π΅Π΄Π΅Π»ΠΈΡ‚ΡŒ ΠΏΡ€Π°Π²ΠΈΠ»Π° Ρ€Π΅Π΄ΡƒΠΊΡ†ΠΈΠΈ:

$If\ True\ a\ b$ Β $=$ $a$
$If\ False\ a\ b$ Β $=$ $b$
$Not\ True$ Β $=$ $False$
$Not\ False$ Β $=$ $True$
$Add\ False\ a$ Β $=$ $False$
$Add\ True\ b$ Β $=$ $b$
…

Π’Π°ΠΊΠΈΠ΅ ΠΏΡ€Π°Π²ΠΈΠ»Π° Π½Π°Π·Ρ‹Π²Π°ΡŽΡ‚ $\delta$-Ρ€Π΅Π΄ΡƒΠΊΡ†ΠΈΠ΅ΠΉ (Π΄Π΅Π»ΡŒΡ‚Π°-рСдукция).

ΠšΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€Π½Π°Ρ Π»ΠΎΠ³ΠΈΠΊΠ°

ΠžΠ΄Π½ΠΎΠ²Ρ€Π΅ΠΌΠ΅Π½Π½ΠΎ с лямбда-исчислСниСм Ρ€Π°Π·Π²ΠΈΠ²Π°Π»Π°ΡΡŒ комбинаторная Π»ΠΎΠ³ΠΈΠΊΠ°. Она отличаСтся Π±ΠΎΠ»Π΅Π΅ ΠΊΠΎΠΌΠΏΠ°ΠΊΡ‚Π½Ρ‹ΠΌ прСдставлСниСм. Π•ΡΡ‚ΡŒ всСго лишь ΠΎΠ΄Π½ΠΎ ΠΏΡ€Π°Π²ΠΈΠ»ΠΎ, это ΠΏΡ€ΠΈΠΌΠ΅Π½Π΅Π½ΠΈΠ΅ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ ΠΊ Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚Ρƒ. А Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ строятся Π½Π΅ ΠΈΠ· ΠΏΡ€ΠΎΠΈΠ·Π²ΠΎΠ»ΡŒΠ½Ρ‹Ρ… Ρ‚Π΅Ρ€ΠΌΠΎΠ², Π° ΠΈΠ· Π½Π°Π±ΠΎΡ€Π° основных Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΉ. Набор основных Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΉ Π½Π°Π·Ρ‹Π²Π°ΡŽΡ‚ базисом.

Рассмотрим лямбда-Ρ‚Π΅Ρ€ΠΌΡ‹:

$$\lambda x .x, \quad \lambda y .y, \quad \lambda z .z$$

ВсС эти Ρ‚Π΅Ρ€ΠΌΡ‹ нСсут ΠΎΠ΄ΠΈΠ½ ΠΈ Ρ‚ΠΎΡ‚ ΠΆΠ΅ смысл. Они ΠΏΡ€Π΅Π΄ΡΡ‚Π°Π²Π»ΡΡŽΡ‚ Ρ‚ΠΎΠΆΠ΄Π΅ΡΡ‚Π²Π΅Π½Π½ΡƒΡŽ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΡŽ. Они Ρ€Π°Π²Π½Ρ‹, Π½ΠΎ с Ρ‚ΠΎΡ‡Π½ΠΎΡΡ‚ΡŒΡŽ Π΄ΠΎ ΠΎΠ±ΠΎΠ·Π½Π°Ρ‡Π΅Π½ΠΈΠΉ. Π­Ρ‚Π° навязчивая ΠΏΡ€ΠΎΠ±Π»Π΅ΠΌΠ° с ΠΏΠ΅Ρ€Π΅ΠΎΠ±ΠΎΠ·Π½Π°Ρ‡Π΅Π½ΠΈΠ΅ΠΌ Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚ΠΎΠ² Π±Ρ‹Π»Π° Ρ€Π΅ΡˆΠ΅Π½Π° Π² ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€Π½ΠΎΠΉ Π»ΠΎΠ³ΠΈΠΊΠ΅. ΠŸΠΎΡΠΌΠΎΡ‚Ρ€ΠΈΠΌ ΠΊΠ°ΠΊ строятся Ρ‚Π΅Ρ€ΠΌΡ‹:

ΠžΠΏΡ€Π΅Π΄Π΅Π»Π΅Π½Ρ‹ ΠΏΡ€Π°Π²ΠΈΠ»Π° Ρ€Π΅Π΄ΡƒΠΊΡ†ΠΈΠΈ для базисных Ρ‚Π΅Ρ€ΠΌΠΎΠ²:

$Kxy$ $=$ $x$
$Sxyz$ $=$ $xz(yz)$

Π’ этих ΠΏΡ€Π°Π²ΠΈΠ»Π°Ρ… ΠΌΡ‹ ΠΏΠΎΠ»ΡŒΠ·ΡƒΠ΅ΠΌΡΡ соглашСниСм ΠΎ расстановки скобок. Π’Π°ΠΊΠΆΠ΅ ΠΊΠ°ΠΊ ΠΈ Π² лямбда исчислСнии Π² ΠΏΡ€ΠΈΠΌΠ΅Π½Π΅Π½ΠΈΠΈ скобки Π³Ρ€ΡƒΠΏΠΏΠΈΡ€ΡƒΡŽΡ‚ΡΡ Π²Π»Π΅Π²ΠΎ. Когда ΠΌΡ‹ пишСм $Kxy$, ΠΌΡ‹ ΠΏΠΎΠ΄Ρ€Π°Π·ΡƒΠΌΠ΅Π²Π°Π΅ΠΌ $((Kx)y)$. Π’Π΅Ρ€ΠΌΡ‹ Π² ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€Π½ΠΎΠΉ Π»ΠΎΠ³ΠΈΠΊΠ΅ принято Π½Π°Π·Ρ‹Π²Π°Ρ‚ΡŒ ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€Π°ΠΌΠΈ. РСдукция происходит Π΄ΠΎ Ρ‚Π΅Ρ… ΠΏΠΎΡ€ ΠΏΠΎΠΊΠ° ΠΌΡ‹ ΠΌΠΎΠΆΠ΅ΠΌ Π·Π°ΠΌΠ΅Π½ΡΡ‚ΡŒ вхоТдСния базисных ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€ΠΎΠ². Π’Π°ΠΊ Ссли ΠΌΡ‹ Π²ΠΈΠ΄ΠΈΠΌ связку $KXY$ ΠΈΠ»ΠΈ $SXYZ$, Π³Π΄Π΅ $X$, $Y$, $Z$ ΠΏΡ€ΠΎΠΈΠ·Π²ΠΎΠ»ΡŒΠ½Ρ‹Π΅ Ρ‚Π΅Ρ€ΠΌΡ‹, Ρ‚ΠΎ ΠΌΡ‹ ΠΌΠΎΠΆΠ΅ΠΌ ΠΈΡ… Π·Π°ΠΌΠ΅Π½ΠΈΡ‚ΡŒ согласно ΠΏΡ€Π°Π²ΠΈΠ»Π°ΠΌ Ρ€Π΅Π΄ΡƒΠΊΡ†ΠΈΠΈ. Π’Π°ΠΊΠΈΠ΅ связки Π½Π°Π·Ρ‹Π²Π°ΡŽΡ‚ рСдСксами. Если Π² Ρ‚Π΅Ρ€ΠΌΠ΅ Π½Π΅Ρ‚ Π½ΠΈ ΠΎΠ΄Π½ΠΎΠ³ΠΎ рСдСкса, Ρ‚ΠΎ ΠΎΠ½ находится Π² Π½ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½ΠΎΠΉ Ρ„ΠΎΡ€ΠΌΠ΅. Π—Π°ΠΌΠ΅Π½Ρƒ рСдСкса принято Π½Π°Π·Ρ‹Π²Π°Ρ‚ΡŒ свёрткой

Π˜Π½Ρ‚Π΅Ρ€Π΅ΡΠ½ΠΎ, Ρ‡Ρ‚ΠΎ ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€Ρ‹ $K$ ΠΈ $S$ ΡΠΎΠ²ΠΏΠ°Π΄Π°ΡŽΡ‚ с ΠΎΠΏΡ€Π΅Π΄Π΅Π»Π΅Π½ΠΈΠ΅ΠΌ класса Applicative для Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΉ:

instance Applicative (r->) where
    pure a r = a
    (<*>) a b r = a r (b r)

Π’ этом ΠΎΠΏΡ€Π΅Π΄Π΅Π»Π΅Π½ΠΈΠΈ Ρƒ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΉ Π΅ΡΡ‚ΡŒ ΠΎΠ±Ρ‰Π΅Π΅ ΠΎΠΊΡ€ΡƒΠΆΠ΅Π½ΠΈΠ΅ $r$, ΠΈΠ· ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠ³ΠΎ ΠΎΠ½ΠΈ ΠΌΠΎΠ³ΡƒΡ‚ Ρ‡ΠΈΡ‚Π°Ρ‚ΡŒ значСния, Ρ‚Π°ΠΊ ΠΆΠ΅ ΠΊΠ°ΠΊ ΠΈ Π² случаС Ρ‚ΠΈΠΏΠ° Reader. Π’ ΠΌΠ΅Ρ‚ΠΎΠ΄Π΅ pure (ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€ $K$) ΠΌΡ‹ ΠΈΠ³Π½ΠΎΡ€ΠΈΡ€ΡƒΠ΅ΠΌ ΠΎΠΊΡ€ΡƒΠΆΠ΅Π½ΠΈΠ΅ (это константная функция), Π° Π² ΠΌΠ΅Ρ‚ΠΎΠ΄Π΅ <*> (ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€ $S$) ΠΏΠ΅Ρ€Π΅Π΄Π°Ρ‘ΠΌ ΠΎΠΊΡ€ΡƒΠΆΠ΅Π½ΠΈΠ΅ Π² Ρ„ΡƒΠ½ΠΊΡ†ΠΈΡŽ ΠΈ Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚ ΠΈ составляСм ΠΏΡ€ΠΈΠΌΠ΅Π½Π΅Π½ΠΈΠ΅ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ Π² контСкстС окруТСния r ΠΊ Π·Π½Π°Ρ‡Π΅Π½ΠΈΡŽ, ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠ΅ Π±Ρ‹Π»ΠΎ ΠΏΠΎΠ»ΡƒΡ‡Π΅Π½ΠΎ Π² контСкстС Ρ‚ΠΎΠ³ΠΎ ΠΆΠ΅ окруТСния.

ВСрнёмся ΠΊ ΠΏΡ€ΠΎΠ±Π»Π΅ΠΌΠ΅ Ρ€Π°Π·Π»ΠΈΡ‡Π½ΠΎΠ³ΠΎ прСдставлСния тоТдСствСнной Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ Π² лямбда-исчислСнии. Π’ ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€Π½ΠΎΠΉ Π»ΠΎΠ³ΠΈΠΊΠ΅ тоТдСствСнная функция выраТаСтся Ρ‚Π°ΠΊ:

$$I = SKK$$

ΠŸΡ€ΠΎΠ²Π΅Ρ€ΠΈΠΌ, опрСдСляСт Π»ΠΈ этот ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€ Ρ‚ΠΎΠΆΠ΄Π΅ΡΡ‚Π²Π΅Π½Π½ΡƒΡŽ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΡŽ:

$$Ix = SKKx = Kx(Kx) = x$$

Π‘Π½Π°Ρ‡Π°Π»Π° ΠΌΡ‹ Π·Π°ΠΌΠ΅Π½ΠΈΠ»ΠΈ $I$ Π½Π° Π΅Π³ΠΎ ΠΎΠΏΡ€Π΅Π΄Π΅Π»Π΅Π½ΠΈΠ΅, Π·Π°Ρ‚Π΅ΠΌ свСрнули ΠΏΠΎ ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€Ρƒ $S$, Π·Π°Ρ‚Π΅ΠΌ ΠΏΠΎ Π»Π΅Π²ΠΎΠΌΡƒ ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€Ρƒ $K$. Π’ ΠΈΡ‚ΠΎΠ³Π΅ ΠΏΠΎΠ»ΡƒΡ‡ΠΈΠ»ΠΎΡΡŒ, Ρ‡Ρ‚ΠΎ

$$Ix = x$$

Бвязь с лямбда-исчислСниСм

ΠšΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€Π½Π°Ρ Π»ΠΎΠ³ΠΈΠΊΠ° ΠΈ лямбда-исчислСниС тСсно связаны ΠΌΠ΅ΠΆΠ΄Ρƒ собой. МоТно ΠΎΠΏΡ€Π΅Π΄Π΅Π»ΠΈΡ‚ΡŒ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΡŽ $\phi$, которая ΠΏΠ΅Ρ€Π΅Π²ΠΎΠ΄ΠΈΡ‚ Ρ‚Π΅Ρ€ΠΌΡ‹ ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€Π½ΠΎΠΉ Π»ΠΎΠ³ΠΈΠΊΠΈ Π² Ρ‚Π΅Ρ€ΠΌΡ‹ лямбда-исчислСния:

$\phi(x)$ $=$ $x$
$\phi(K)$ $=$ $\lambda xy .x$
$\phi(S)$ $=$ $\lambda xyz .xz(yz)$
$\phi(XY)$ $=$ $\phi(X)\ \phi(Y)$

Π’ ΠΏΠ΅Ρ€Π²ΠΎΠΌ ΡƒΡ€Π°Π²Π½Π΅Π½ΠΈΠΈ $x$ – пСрСмСнная. Π’Π°ΠΊΠΆΠ΅ ΠΌΠΎΠΆΠ½ΠΎ ΠΎΠΏΡ€Π΅Π΄Π΅Π»ΠΈΡ‚ΡŒ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΡŽ $\psi$, которая ΠΏΠ΅Ρ€Π΅Π²ΠΎΠ΄ΠΈΡ‚ Ρ‚Π΅Ρ€ΠΌΡ‹ лямбда-исчислСния Π² Ρ‚Π΅Ρ€ΠΌΡ‹ ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€Π½ΠΎΠΉ Π»ΠΎΠ³ΠΈΠΊΠΈ.

$\psi(x)$ $=$ $x$
$\psi(XY)$ $=$ $\psi(X)\ \psi(Y)$
$\psi(\lambda x .Y)$ $=$ $[x] .\psi(Y)$

Π—Π°ΠΏΠΈΡΡŒ $[x].T$, Π³Π΄Π΅ $x$ – пСрСмСнная, $T$ – Ρ‚Π΅Ρ€ΠΌ, ΠΎΠ±ΠΎΠ·Π½Π°Ρ‡Π°Π΅Ρ‚ Ρ‚Π°ΠΊΠΎΠΉ Ρ‚Π΅Ρ€ΠΌ $D$, ΠΈΠ· ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠ³ΠΎ ΠΌΠΎΠΆΠ½ΠΎ ΠΏΠΎΠ»ΡƒΡ‡ΠΈΡ‚ΡŒ Ρ‚Π΅Ρ€ΠΌ $T$ подстановкой ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½ΠΎΠΉ $x$, Π²Ρ‹ΠΏΠΎΠ»Π½Π΅Π½ΠΎ свойство:

$$([x].T)\ x = T$$

Π­Ρ‚Π° запись ΠΎΠ·Π½Π°Ρ‡Π°Π΅Ρ‚ ΠΏΠ°Ρ€Π°ΠΌΠ΅Ρ‚Ρ€ΠΈΠ·Π°Ρ†ΠΈΡŽ Ρ‚Π΅Ρ€ΠΌΠ° $T$ ΠΏΠΎ ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½ΠΎΠΉ $x$. Π’Π΅Ρ€ΠΌ $[x].T$ ΠΌΠΎΠΆΠ½ΠΎ ΠΏΠΎΠ»ΡƒΡ‡ΠΈΡ‚ΡŒ с ΠΏΠΎΠΌΠΎΡ‰ΡŒΡŽ ΡΠ»Π΅Π΄ΡƒΡŽΡ‰Π΅Π³ΠΎ Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌΠ°:

$[x] .x$ $=$ $SKK$
$\left[x\right] .X$ $=$ $KX, \quad x \notin V(X)$
$\left[x\right] .XY$ $=$ $S([x] .X)([x].Y)$

Π’ ΠΏΠ΅Ρ€Π²ΠΎΠΌ ΡƒΡ€Π°Π²Π½Π΅Π½ΠΈΠΈ ΠΌΡ‹ замСняСм ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½ΡƒΡŽ Π½Π° Ρ‚ΠΎΠΆΠ΄Π΅ΡΡ‚Π²Π΅Π½Π½ΡƒΡŽ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΡŽ, ΠΏΠΎΡΠΊΠΎΠ»ΡŒΠΊΡƒ ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Ρ‹Π΅ ΡΠΎΠ²ΠΏΠ°Π΄Π°ΡŽΡ‚. Π—Π°ΠΏΠΈΡΡŒ $V(X)$ Π²ΠΎ Π²Ρ‚ΠΎΡ€ΠΎΠΌ ΡƒΡ€Π°Π²Π½Π΅Π½ΠΈΠΈ ΠΎΠ±ΠΎΠ·Π½Π°Ρ‡Π°Π΅Ρ‚ мноТСство всСх ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Ρ‹Ρ… Π² Ρ‚Π΅Ρ€ΠΌΠ΅ $X$. ΠŸΠΎΡΠΊΠΎΠ»ΡŒΠΊΡƒ пСрСмСнная ΠΏΠΎ ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠΉ ΠΌΡ‹ Ρ…ΠΎΡ‚ΠΈΠΌ ΠΏΠ°Ρ€Π°ΠΌΠ΅Ρ‚Ρ€ΠΈΠ·ΠΎΠ²Π°Ρ‚ΡŒ Ρ‚Π΅Ρ€ΠΌ (ΠΈΠ»ΠΈ Π°Π±ΡΡ‚Ρ€Π°Π³ΠΈΡ€ΠΎΠ²Π°Ρ‚ΡŒ) Π½Π΅ участвуСт Π² самом Ρ‚Π΅Ρ€ΠΌΠ΅, ΠΌΡ‹ ΠΌΠΎΠΆΠ΅ΠΌ ΠΏΡ€ΠΎΠΈΠ³Π½ΠΎΡ€ΠΈΡ€ΠΎΠ²Π°Ρ‚ΡŒ Π΅Ρ‘ с ΠΏΠΎΠΌΠΎΡ‰ΡŒΡŽ постоянной Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ $K$. Π’ послСднСм ΡƒΡ€Π°Π²Π½Π΅Π½ΠΈΠΈ ΠΌΡ‹ ΠΏΠ°Ρ€Π°ΠΌΠ΅Ρ‚Ρ€ΠΈΠ·ΡƒΠ΅ΠΌ ΠΏΡ€ΠΈΠΌΠ΅Π½Π΅Π½ΠΈΠ΅.

Π‘ ΠΏΠΎΠΌΠΎΡ‰ΡŒΡŽ этого Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌΠ° ΠΌΠΎΠΆΠ½ΠΎ для любого Ρ‚Π΅Ρ€ΠΌΠ° $T$, всС ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Ρ‹Π΅ ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠ³ΠΎ содСрТатся Π² $\{x_1, ... x_n\}$ ΡΠΎΡΡ‚Π°Π²ΠΈΡ‚ΡŒ Ρ‚Π°ΠΊΠΎΠΉ ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€ $D$, Ρ‡Ρ‚ΠΎ $Dx_1 ... x_n = T$. Для этого ΠΌΡ‹ ΠΏΠΎΡΠ»Π΅Π΄ΠΎΠ²Π°Ρ‚Π΅Π»ΡŒΠ½ΠΎ ΠΏΠ°Ρ€ΠΌΠ΅Ρ‚Ρ€ΠΈΠ·ΡƒΠ΅ΠΌ Ρ‚Π΅Ρ€ΠΌ $T$ ΠΏΠΎ всСм ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Ρ‹ΠΌ:

$$[x1,...,\ x_n] .T = [x_1] .([x_2, ... ,\ x_n] .T)$$

Π’Π°ΠΊ постСпСнно ΠΌΡ‹ ΠΏΡ€ΠΈΠ΄Ρ‘ΠΌ ΠΊ Π²Ρ‹Ρ€Π°ΠΆΠ΅Π½ΠΈΡŽ, считаСм Ρ‡Ρ‚ΠΎ скобки Π³Ρ€ΡƒΠΏΠΏΠΈΡ€ΡƒΡŽΡ‚ΡΡ Π²ΠΏΡ€Π°Π²ΠΎ:

$$[x_1] .[x_2] .... [x_n] .T$$

НСмного истории

ΠšΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€Π½ΡƒΡŽ Π»ΠΎΠ³ΠΈΠΊΡƒ ΠΎΡ‚ΠΊΡ€Ρ‹Π» МоисСй Π¨Π΅ΠΉΠ½Ρ„ΠΈΠ½ΠΊΠ΅Π»ΡŒ. Π’ 1920 Π³ΠΎΠ΄Ρƒ Π½Π° Π΄ΠΎΠΊΠ»Π°Π΄Π΅ Π² Π“Ρ‘Ρ‚Ρ‚ΠΈΠ½Π³Π΅Π½Π΅ ΠΎΠ½ рассказал основныС полоТСния этой Ρ‚Π΅ΠΎΡ€ΠΈΠΈ. ΠšΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€Π½Π°Ρ Π»ΠΎΠ³ΠΈΠΊΠ° Π½Π°ΠΏΡ€Π°Π²Π»Π΅Π½Π° Π½Π° Π²Ρ‹Π΄Π΅Π»Π΅Π½ΠΈΠ΅ ΠΏΡ€ΠΎΡΡ‚Π΅ΠΉΡˆΠΈΡ… ΡΡ‚Ρ€ΠΎΠΈΡ‚Π΅Π»ΡŒΠ½Ρ‹Ρ… Π±Π»ΠΎΠΊΠΎΠ² матСматичСской Π»ΠΎΠ³ΠΈΠΊΠΈ. Π’ этом Π΄ΠΎΠΊΠ»Π°Π΄Π΅ появилось понятиС частичного примСнСния. Π¨Π΅ΠΉΠ½Ρ„ΠΈΠ½ΠΊΠ΅Π»ΡŒ ΠΏΠΎΠΊΠ°Π·Π°Π» ΠΊΠ°ΠΊ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ ΠΌΠ½ΠΎΠ³ΠΈΡ… ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Ρ‹Ρ… ΠΌΠΎΠ³ΡƒΡ‚ Π±Ρ‹Ρ‚ΡŒ свСдСны ΠΊ функциям ΠΎΠ΄Π½ΠΎΠ³ΠΎ ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½ΠΎΠ³ΠΎ. Π”Π°Π»Π΅Π΅ Π² Π΄ΠΎΠΊΠ»Π°Π΄Π΅ ΠΎΠΏΠΈΡΡ‹Π²Π°ΡŽΡ‚ΡΡ ΠΏΡΡ‚ΡŒ основных Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΉ, Π½Π°Π·Ρ‹Π²Π°Π΅ΠΌΡ‹Ρ… ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€Π°ΠΌΠΈ:

$Ix$ $=$ $x$ – функция тоТдСства
$Cxy$ $=$ $x$ – константная функция
$Txyz$ $=$ $xzy$ – функция пСрСстановки
$Zxyz$ $=$ $x(yz)$ – функция Π³Ρ€ΡƒΠΏΠΏΠΈΡ€ΠΎΠ²ΠΊΠΈ
$Sxyz$ $=$ $xz(yz)$ – функция слияния

Π‘ ΠΏΠΎΠΌΠΎΡ‰ΡŒΡŽ этих Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΉ ΠΌΠΎΠΆΠ½ΠΎ ΠΈΠ·Π±Π°Π²ΠΈΡ‚ΡŒΡΡ Π² Ρ„ΠΎΡ€ΠΌΡƒΠ»Π°Ρ… ΠΎΡ‚ ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Ρ‹Ρ…, Ρ‚Π°ΠΊ Π½Π°ΠΏΡ€ΠΈΠΌΠ΅Ρ€ свойство коммутативности Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ $A$ ΠΌΠΎΠΆΠ½ΠΎ ΠΏΡ€Π΅Π΄ΡΡ‚Π°Π²ΠΈΡ‚ΡŒ Ρ‚Π°ΠΊ: $TA = A$. Π­Ρ‚ΠΈ ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€Ρ‹ зависят Π΄Ρ€ΡƒΠ³ ΠΎΡ‚ Π΄Ρ€ΡƒΠ³Π°. МоТно ΡƒΠ±Π΅Π΄ΠΈΡ‚ΡŒΡΡ Π² Ρ‚ΠΎΠΌ, Ρ‡Ρ‚ΠΎ:

$I$ $=$ $SCC$
$Z$ $=$ $S(CS)S$
$T$ $=$ $S(ZZS)(CC)$

ВсС ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€Ρ‹ Π²Ρ‹Ρ€Π°ΠΆΠ°ΡŽΡ‚ΡΡ Ρ‡Π΅Ρ€Π΅Π· ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€Ρ‹ $C$ ΠΈ $S$. Π Π°Π½Π΅Π΅ ΠΌΡ‹ пользовались Π΄Ρ€ΡƒΠ³ΠΈΠΌΠΈ обозначСниями для этих ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€ΠΎΠ². ΠžΠ±ΠΎΠ·Π½Π°Ρ‡Π΅Π½ΠΈΡ $K$ ΠΈ $S$ Π²Π²Ρ‘Π» Π₯аскСль ΠšΠ°Ρ€Ρ€ΠΈ (Haskell Curry). НСзависимо ΠΎΡ‚ ШСйнфинкСля ΠΎΠ½ ΠΏΠ΅Ρ€Π΅ΠΎΡ‚ΠΊΡ€Ρ‹Π» ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€Π½ΡƒΡŽ Π»ΠΎΠ³ΠΈΠΊΡƒ ΠΈ сущСствСнно Ρ€Π°Π·Π²ΠΈΠ» Π΅Ρ‘. Π’ соврСмСнной ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€Π½ΠΎΠΉ Π»ΠΎΠ³ΠΈΠΊΠ΅ для обозначСния ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€ΠΎΠ² $I$, $C$, $T$, $Z$ ΠΈ $S$ (ΠΏΠΎ Π¨Π΅ΠΉΠ½Ρ„ΠΈΠ½ΠΊΠ΅Π»ΡŽ) принято ΠΈΡΠΏΠΎΠ»ΡŒΠ·ΠΎΠ²Π°Ρ‚ΡŒ ΠΈΠΌΠ΅Π½Π° $I$, $K$, $C$, $B$, $S$ (ΠΏΠΎ ΠšΠ°Ρ€Ρ€ΠΈ).

Лямбда-исчислСниС с Ρ‚ΠΈΠΏΠ°ΠΌΠΈ

ΠœΡ‹ ΠΌΠΎΠΆΠ΅ΠΌ Π΄ΠΎΠ±Π°Π²ΠΈΡ‚ΡŒ Π² лямбда-исчислСниС Ρ‚ΠΈΠΏΡ‹. ΠŸΡ€Π΅Π΄ΠΏΠΎΠ»ΠΎΠΆΠΈΠΌ, Ρ‡Ρ‚ΠΎ Ρƒ нас Π΅ΡΡ‚ΡŒ мноТСство $V$ Π±Π°Π·ΠΎΠ²Ρ‹Ρ… Ρ‚ΠΈΠΏΠΎΠ². Π’ΠΎΠ³Π΄Π° Ρ‚ΠΈΠΏ это:

$$T = V \ ?|\ T \rightarrowT$$

Π’ΠΈΠΏ ΠΌΠΎΠΆΠ΅Ρ‚ Π±Ρ‹Ρ‚ΡŒ Π»ΠΈΠ±ΠΎ ΠΎΠ΄Π½ΠΈΠΌ элСмСнтом ΠΈΠ· мноТСства Π±Π°Π·ΠΎΠ²Ρ‹Ρ… Ρ‚ΠΈΠΏΠΎΠ². Π›ΠΈΠ±ΠΎ стрСлочным (Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΎΠ½Π°Π»ΡŒΠ½Ρ‹ΠΌ) Ρ‚ΠΈΠΏΠΎΠΌ. Π’Ρ‹Ρ€Π°ΠΆΠ΅Π½ΠΈΠ΅ β€œΡ‚Π΅Ρ€ΠΌ $M$ ΠΈΠΌΠ΅Π΅Ρ‚ Ρ‚ΠΈΠΏ $\alpha$” принято ΠΏΠΈΡΠ°Ρ‚ΡŒ Ρ‚Π°ΠΊ: $M^{\alpha}$. Π‘Ρ‚Ρ€Π΅Π»ΠΎΡ‡Π½Ρ‹ΠΉ Ρ‚ΠΈΠΏ $\alpha \rightarrow\beta$ ΠΊΠ°ΠΊ ΠΈ Π² Haskell Π³ΠΎΠ²ΠΎΡ€ΠΈΡ‚ ΠΎ Ρ‚ΠΎΠΌ, Ρ‡Ρ‚ΠΎ Ссли Ρƒ нас Π΅ΡΡ‚ΡŒ Π·Π½Π°Ρ‡Π΅Π½ΠΈΠ΅ Ρ‚ΠΈΠΏΠ° $\alpha$, Ρ‚ΠΎ с ΠΏΠΎΠΌΠΎΡ‰ΡŒΡŽ ΠΎΠΏΠ΅Ρ€Π°Ρ†ΠΈΠΈ примСнСния ΠΌΡ‹ ΠΌΠΎΠΆΠ΅ΠΌ ΠΈΠ· Ρ‚Π΅Ρ€ΠΌΠ° с этим стрСлочным Ρ‚ΠΈΠΏΠΎΠΌ ΠΏΠΎΠ»ΡƒΡ‡ΠΈΡ‚ΡŒ Ρ‚Π΅Ρ€ΠΌ Ρ‚ΠΈΠΏΠ° $\beta$.

ОпишСм ΠΏΡ€Π°Π²ΠΈΠ»Π° построСния Ρ‚Π΅Ρ€ΠΌΠΎΠ² Π² лямбда-исчислСнии с Ρ‚ΠΈΠΏΠ°ΠΌΠΈ:

Випизация Π½Π°ΠΊΠ»Π°Π΄Ρ‹Π²Π°Π΅Ρ‚ ΠΎΠ³Ρ€Π°Π½ΠΈΡ‡Π΅Π½ΠΈΠ΅ Π½Π° Ρ‚ΠΎ, ΠΊΠ°ΠΊΠΈΠ΅ выраТСния ΠΌΡ‹ ΠΌΠΎΠΆΠ΅ΠΌ ΠΊΠΎΠΌΠ±ΠΈΠ½ΠΈΡ€ΠΎΠ²Π°Ρ‚ΡŒ. Π’ этом Π΅ΡΡ‚ΡŒ ΠΏΠ»ΡŽΡΡ‹ ΠΈ минусы. Π’Π΅ΠΏΠ΅Ρ€ΡŒ наша систСма являСтся строго Π½ΠΎΡ€ΠΌΠ°Π»ΠΈΠ·ΡƒΠ΅ΠΌΠΎΠΉ, это ΠΎΠ·Π½Π°Ρ‡Π°Π΅Ρ‚, Ρ‡Ρ‚ΠΎ любой Ρ‚Π΅Ρ€ΠΌ ΠΈΠΌΠ΅Π΅Ρ‚ Π½ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½ΡƒΡŽ Ρ„ΠΎΡ€ΠΌΡƒ. Но Ρ‚Π΅ΠΏΠ΅Ρ€ΡŒ ΠΌΡ‹ Π½Π΅ ΠΌΠΎΠΆΠ΅ΠΌ Π²Ρ‹Ρ€Π°Π·ΠΈΡ‚ΡŒ всС Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ Π½Π° числах. НапримСр ΠΌΡ‹ Π½Π΅ ΠΌΠΎΠΆΠ΅ΠΌ ΡΠΎΡΡ‚Π°Π²ΠΈΡ‚ΡŒ $Y$-ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€, ΠΏΠΎΡΠΊΠΎΠ»ΡŒΠΊΡƒ Ρ‚Π΅ΠΏΠ΅Ρ€ΡŒ самопримСнСниС $(e e)$ Π½Π΅Π²ΠΎΠ·ΠΌΠΎΠΆΠ½ΠΎ.

ΠœΡ‹ Π²Π²Π΅Π»ΠΈ Ρ‚ΠΈΠΏΡ‹, Π½ΠΎ лишились рСкурсии. Как Π½Π°ΠΌ Π±Ρ‹Ρ‚ΡŒ? Π­Ρ‚Π° ΠΏΡ€ΠΎΠ±Π»Π΅ΠΌΠ° Ρ€Π΅ΡˆΠ°Π΅Ρ‚ΡΡ с ΠΏΠΎΠΌΠΎΡ‰ΡŒΡŽ ввСдСния ΡΠΏΠ΅Ρ†ΠΈΠ°Π»ΡŒΠ½ΠΎΠΉ константы $Y_\tau^{(\tau \rightarrow\tau) \rightarrow\tau}$, которая ΠΎΠ±ΠΎΠ·Π½Π°Ρ‡Π°Π΅Ρ‚ ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€ Π½Π΅ΠΏΠΎΠ΄Π²ΠΈΠΆΠ½ΠΎΠΉ Ρ‚ΠΎΡ‡ΠΊΠΈ. ΠŸΡ€Π°Π²ΠΈΠ»ΠΎ Ρ€Π΅Π΄ΡƒΠΊΡ†ΠΈΠΈ для $Y$:

$$(Y_\tau f^{\tau \rightarrow\tau})^\tau = (f^{\tau \rightarrow\tau}(Y_\tau f^{\tau \rightarrow\tau}))^\tau$$

МоТно ΡƒΠ±Π΅Π΄ΠΈΡ‚ΡŒΡΡ Π² Ρ‚ΠΎΠΌ, Ρ‡Ρ‚ΠΎ это ΠΏΡ€Π°Π²ΠΈΠ»ΠΎ ΠΏΡ€ΠΎΡ…ΠΎΠ΄ΠΈΡ‚ ΠΏΡ€ΠΎΠ²Π΅Ρ€ΠΊΡƒ Ρ‚ΠΈΠΏΠΎΠ². Π’ΠΈΠΏΠΈΠ·ΠΈΡ€ΠΎΠ²Π°Π½Π½ΠΎΠ΅ лямбда-исчислСниС Π΄ΠΎΠΏΠΎΠ»Π½Π΅Π½Π½ΠΎΠ΅ ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€ΠΎΠΌ Π½Π΅ΠΏΠΎΠ΄Π²ΠΈΠΆΠ½ΠΎΠΉ Ρ‚ΠΎΡ‡ΠΊΠΈ способно Π²Ρ‹Ρ€Π°Π·ΠΈΡ‚ΡŒ всС числовыС Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ.

ΠšΡ€Π°Ρ‚ΠΊΠΎΠ΅ содСрТаниС

Π’ этой Π³Π»Π°Π²Π΅ ΠΌΡ‹ познакомились с лямбда-исчислСниСм ΠΈ ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ‚ΠΎΡ€Π½ΠΎΠΉ Π»ΠΎΠ³ΠΈΠΊΠΎΠΉ, двумя конструктивными тСориями Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΉ. ΠšΠΎΠ½ΡΡ‚Ρ€ΡƒΠΊΡ‚ΠΈΠ²Π½Ρ‹ΠΌΠΈ Π² Ρ‚ΠΎΠΌ смыслС, Ρ‡Ρ‚ΠΎ ΠΎΠΏΡ€Π΅Π΄Π΅Π»Π΅Π½ΠΈΠ΅ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ содСрТит Π½Π΅ Π½Π°Π±ΠΎΡ€ Π·Π½Π°Ρ‡Π΅Π½ΠΈΠΉ, Π° Ρ€Π΅Ρ†Π΅ΠΏΡ‚ получСния этих Π·Π½Π°Ρ‡Π΅Π½ΠΈΠΉ. Π’ лямбда-исчислСнии ΠΌΡ‹ Π²ΠΈΠ΄ΠΈΠΌ ΠΊΠ°ΠΊ функция Π±Ρ‹Π»Π° построСна, ΠΈΠ· ΠΊΠ°ΠΊΠΈΡ… ΠΏΡ€ΠΎΡΡ‚Π΅ΠΉΡˆΠΈΡ… частСй ΠΎΠ½Π° состоит. РСдукция Ρ‚Π΅Ρ€ΠΌΠΎΠ² позволяСт Π²Ρ‹Ρ‡ΠΈΡΠ»ΡΡ‚ΡŒ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ.

ΠœΡ‹ ΡƒΠ·Π½Π°Π»ΠΈ, Ρ‡Ρ‚ΠΎ функциями ΠΌΠΎΠΆΠ½ΠΎ ΠΊΠΎΠ΄ΠΈΡ€ΠΎΠ²Π°Ρ‚ΡŒ логичСскиС значСния ΠΈ числа. Π£Π·Π½Π°Π»ΠΈ, Ρ‡Ρ‚ΠΎ всС числСнныС Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΈ ΠΌΠΎΠ³ΡƒΡ‚ Π±Ρ‹Ρ‚ΡŒ Π·Π°ΠΊΠΎΠ΄ΠΈΡ€ΠΎΠ²Π°Π½Ρ‹ лямбда-Ρ‚Π΅Ρ€ΠΌΠ°ΠΌΠΈ.

УпраТнСния

ЗарСгистрировано ΠΏΠΎΠ΄ Π»ΠΈΡ†Π΅Π½Π·ΠΈΠ΅ΠΉ Creative commons Attribution-NonCommercial-NoDerivs 3.0 Generic (CC BY-NC-ND 3.0)